diff --git a/src/lib/FunctorParsing.ml b/src/lib/FunctorParsing.ml index 69620132c1c1a69fdecf47d805b4743b38db63b1..be27697ac190dd49973f5308c3f8f7c4f9a8f3e3 100644 --- a/src/lib/FunctorParsing.ml +++ b/src/lib/FunctorParsing.ml @@ -1,4 +1,5 @@ (* Parsing strings to sort tables *) +module CM = CoAlgMisc type functorExp = | Choice of functorExp * functorExp @@ -97,3 +98,40 @@ let functorExpFromString str : functorExp = result +let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable = + let logicName2Functor str = match str with + | "K" -> CM.MultiModalK + | "KD" -> CM.MultiModalKD + | "CL" -> CM.CoalitionLogic + | "GML" -> CM.GML + | "MultiModalK" -> CM.MultiModalK + | "MultiModalKD" -> CM.MultiModalKD + | "CoalitionLogic" -> CM.CoalitionLogic + | _ -> raise (FunctorParsingFailed ("Unknown Functor name "^str)) + in + let line = ref(0) in + let getLineNr () = + let nr = !line in + line := nr + 1; + nr + in + let rec generateSorts (fe:functorExp) : ((CM.functors * int list) list * int) = + (* generate sortTable lines for that functor and tell its line number *) + let nr = getLineNr () in + match fe with + | Unary str -> [ (logicName2Functor str, [0])], nr + | Choice (a,b) -> + let (a_table, a_nr) = generateSorts a in + let (b_table, b_nr) = generateSorts b in + ((CM.Choice, [a_nr; b_nr])::(List.append a_table b_table)), nr + | Fusion (a,b) -> + let (a_table, a_nr) = generateSorts a in + let (b_table, b_nr) = generateSorts b in + ((CM.Fusion, [a_nr; b_nr])::(List.append a_table b_table)), nr + in + let fst (x,_ ) = x in + Array.of_list (fst (generateSorts fe)) + +let sortTableFromString str : CoAlgReasoner.sortTable = + sortTableFromFunctorExp (functorExpFromString str) + diff --git a/src/lib/FunctorParsing.mli b/src/lib/FunctorParsing.mli index 4e2f8c10fa4ae8391957552d4189bd4279fc9a30..0358ba1c40f4d06e3adbc14fedaad761ba2e102c 100644 --- a/src/lib/FunctorParsing.mli +++ b/src/lib/FunctorParsing.mli @@ -10,4 +10,9 @@ exception FunctorParsingFailed of string val stringFromFunctorExp : functorExp -> string val functorExpFromString : string -> functorExp +val sortTableFromFunctorExp : functorExp -> CoAlgReasoner.sortTable + +val sortTableFromString : string -> CoAlgReasoner.sortTable + +val stringFromSortTable : CoAlgReasoner.sortTable -> string diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml index 498592ba895cb0ff31f228c9bdd7131f47775a28..fd364468511ac45a03a3ec0891a305bd64170ce5 100644 --- a/src/testsuite/cool-testsuite.ml +++ b/src/testsuite/cool-testsuite.ml @@ -64,10 +64,7 @@ let cl_testcases : satCheck list = ; c Sat "([{1 3}] C) & ([{ 2 3 }] ~C )" ] -let kAndKd = [| (CoAlgMisc.Fusion, [1; 2]); - (CoAlgMisc.MultiModalK, [0]); - (CoAlgMisc.MultiModalKD, [0]) - |] +let kAndKd = FunctorParsing.sortTableFromString "K * KD" let kAndKd_testcases : satCheck list = let c a b = (a,kAndKd,b) in