From 77644d144ccbff41372df930b828d3679f6f69fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Fri, 23 Jan 2015 05:30:37 +1100
Subject: [PATCH] Allow functors to get parameters in the syntax
---
src/coalg/coalg.ml | 3 +++
src/lib/FunctorParsing.ml | 28 ++++++++++++++++++++++------
src/lib/FunctorParsing.mli | 2 +-
3 files changed, 26 insertions(+), 7 deletions(-)
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index 33322ce..68484d4 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -38,6 +38,9 @@ let nomTable name =
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
+let _ =
+ let str = "A . B C" in
+ print_endline (FE.stringFromFunctorExp (FE.functorExpFromString str))
let printUsage () =
print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
diff --git a/src/lib/FunctorParsing.ml b/src/lib/FunctorParsing.ml
index 79ff7d5..519e3a0 100644
--- a/src/lib/FunctorParsing.ml
+++ b/src/lib/FunctorParsing.ml
@@ -5,16 +5,16 @@ type functorExp =
| Choice of functorExp * functorExp
| Fusion of functorExp * functorExp
| Composition of functorExp * functorExp
- | Unary of string
+ | Unary of string list (* a non-empty list of identifiers *)
let rec stringFromFunctorExp = function
- | Unary str -> str
+ | Unary str -> String.concat " " str
| Composition (a,b) -> "("^(stringFromFunctorExp a)^" . "^(stringFromFunctorExp b)^")"
| Choice (a,b) -> "("^(stringFromFunctorExp a)^" + "^(stringFromFunctorExp b)^")"
| Fusion (a,b) -> "("^(stringFromFunctorExp a)^" * "^(stringFromFunctorExp b)^")"
(* example
- Choice (Unary "K", Fusion (Unary "KD", Unary "GML"))
+ Choice (Unary ["K"], Fusion (Unary ["KD"], Unary ["GML"]))
*)
@@ -49,6 +49,7 @@ let functorExpFromString str : functorExp =
| Some ' ' -> (Stream.junk stream ; dropWhitespace ())
| _ -> ()
in
+ (* try to parse an identifier as long as possible *)
let identifier () =
let rec ident () =
match (Stream.peek stream) with
@@ -60,6 +61,20 @@ let functorExpFromString str : functorExp =
in
implode (ident ())
in
+ (* try to parse as many identifiers, separated by whitespace, as possible *)
+ let rec identifier_list () =
+ dropWhitespace ();
+ let i = identifier () in (* get the next identifier *)
+ if (String.length i <> 0)
+ then i::(identifier_list ())
+ else []
+ in
+ let nonempty_identifier_list () =
+ let idlist = identifier_list () in
+ if List.length idlist <> 0
+ then idlist
+ else error "Expected list of at least one identifiers but got none"
+ in
let rec parse (state:state) : functorExp =
let _ = dropWhitespace () in
let binary (operator:char) (nextStep: state)
@@ -88,7 +103,7 @@ let functorExpFromString str : functorExp =
| _ -> error "Missing closing )"
end
| None -> error "Expected identifier but got end of string"
- | Some ch -> Unary (identifier ())
+ | Some ch -> Unary (nonempty_identifier_list ())
end
in
let result = parse ParseSum in
@@ -118,9 +133,10 @@ let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable =
afterwards.
*)
match fe with
- | Unary str ->
+ | Unary str_list ->
let nr = getLineNr () in
- (fun parameter -> [ (logicName2Functor str, [parameter])]), nr
+ let functorname = List.hd str_list in
+ (fun parameter -> [ (logicName2Functor functorname, [parameter])]), nr
| Choice (a,b) ->
let nr = getLineNr () in
let (a_table, a_nr) = generateSorts a in
diff --git a/src/lib/FunctorParsing.mli b/src/lib/FunctorParsing.mli
index aa1838c..61f6f79 100644
--- a/src/lib/FunctorParsing.mli
+++ b/src/lib/FunctorParsing.mli
@@ -4,7 +4,7 @@ type functorExp =
| Choice of functorExp * functorExp
| Fusion of functorExp * functorExp
| Composition of functorExp * functorExp
- | Unary of string
+ | Unary of string list (* a nonempty list of identifiers *)
exception FunctorParsingFailed of string
--
GitLab