From 68ba7342ae683c37ad44ae09eb641d17ac2982d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Wed, 16 Jul 2014 14:23:19 +0200
Subject: [PATCH] Implement sortTable generation
---
src/lib/FunctorParsing.ml | 38 +++++++++++++++++++++++++++++++++
src/lib/FunctorParsing.mli | 5 +++++
src/testsuite/cool-testsuite.ml | 5 +----
3 files changed, 44 insertions(+), 4 deletions(-)
diff --git a/src/lib/FunctorParsing.ml b/src/lib/FunctorParsing.ml
index 6962013..be27697 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 4e2f8c1..0358ba1 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 498592b..fd36446 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
--
GitLab