diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml index 33322cee4b6be7177fb054728a399402b6dda35d..68484d45b9703c007e7e6292d73005f23cfaf8dd 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 79ff7d5e6e37bb6e85b7d8aa09e3fb748f7f4f4e..519e3a04eb282e973b8ad90d6f2fa786e358f0d7 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 aa1838c64bc1c118a89267152d260884daafcee2..61f6f7961fa3bb90ecdfb051841c04bf91d88060 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