Allow functors to get parameters in the syntax

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";

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

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