diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index 68484d45b9703c007e7e6292d73005f23cfaf8dd..a100d2d5e193581b881a2ad7538773d12db24ae6 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -38,9 +38,11 @@ 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/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 20c78b402de05344f7be662672d651f16943232b..6d21a116349fe84bfe2b421169a399b5fbb1ac47 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -409,5 +409,6 @@ let getExpandingFunctionProducer = function
| CoalitionLogic -> mkRule_CL
| GML -> mkRule_GML
| PML -> mkRule_PML
+ (* | Constant colors -> mkRule_Constant parameters *) (* TODO: implement this *)
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index bd7093d1b7d8a53e0a6ec86fb503990ad68ece2b..d52be14681f90617323bb9f2d34d4861fa8b48b4 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -71,45 +71,71 @@ type functors =
| CoalitionLogic
| GML
| PML
- | Constant
+ | Constant of string list
| Choice
| Fusion
-let unaryfunctor2name : (functors*string) list =
- [ (MultiModalK , "MultiModalK")
- ; (MultiModalKD , "MultiModalKD")
- ; (GML , "GML")
- ; (PML , "PML")
- ; (CoalitionLogic , "CoalitionLogic")
- ; (MultiModalK , "K")
- ; (MultiModalKD , "KD")
- ; (CoalitionLogic , "CL")
- ; (Constant , "Const")
- ; (Constant , "Constant")
+(* functors whose constructor takes additional parameters *)
+type parametricFunctorName =
+ | NameConstant
+
+(* this type should only be used in the following few helper functions *)
+type functorName =
+ | NPa of functors (* No Parameters = functor without parameters *)
+ | Pa of parametricFunctorName (* Parameters = functor with parameters *)
+
+let unaryfunctor2name : (functorName*string) list =
+ [ (NPa MultiModalK , "MultiModalK")
+ ; (NPa MultiModalKD , "MultiModalKD")
+ ; (NPa GML , "GML")
+ ; (NPa PML , "PML")
+ ; (NPa CoalitionLogic , "CoalitionLogic")
+ ; (NPa MultiModalK , "K")
+ ; (NPa MultiModalKD , "KD")
+ ; (NPa CoalitionLogic , "CL")
+ ; (Pa NameConstant , "Const")
+ ; (Pa NameConstant , "Constant")
]
-let functor2name : (functors*string) list =
+let functor2name : (functorName*string) list =
L.append unaryfunctor2name
- [ (Choice , "Choice")
- ; (Fusion , "Fusion")
+ [ (NPa Choice , "Choice")
+ ; (NPa Fusion , "Fusion")
]
-let functor_of_string str : functors option =
+let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
+ (* apply parameter list to the constructor, denoted by the functor name func *)
+ (* return None, if the parameters somehow don't match the required parameters *)
+ match func with
+ | NameConstant -> Some (Constant params)
+
+
+let functor_of_string str params : functors option =
let fst (a,b) = a in
try
- Some (fst (List.find (fun (f,name) -> name = str) functor2name))
+ let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
+ match functorName with
+ | NPa x -> Some x
+ | Pa f -> functor_apply_parameters f params
with Not_found -> None
-let unaryfunctor_of_string str =
- match (functor_of_string str) with
+let unaryfunctor_of_string str params =
+ match (functor_of_string str params) with
| Some Choice -> None
| Some Fusion -> None
| x -> x
let string_of_functor (f: functors) : string =
+ (* replace f orrectly with possibly some Pa wrapper *)
+ (* also put the parameters into some suffix which will be appended later *)
+ let f,suffix = match f with
+ | Constant params -> Pa NameConstant, " "^(String.concat " " params)
+ | _ -> NPa f, ""
+ in
let snd (a,b) = b in
try
- (snd (List.find (fun (f2,name) -> f = f2) functor2name))
+ let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
+ name ^ suffix
with Not_found -> assert false
(* This type may be extended for additional logics. *)
@@ -688,12 +714,16 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
TODO: add ¬ f1 to the closure!
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
*)
- | C.HCCONST _ ->
- if func <> Constant || List.length sortlst <> 1
- then raise (C.CoAlgException "=-formula is used in wrong sort.")
- else ();
- | C.HCCONSTN _ ->
- if func <> Constant || List.length sortlst <> 1
+ | C.HCCONST color
+ | C.HCCONSTN color ->
+ begin match func with
+ | Constant params ->
+ if not (List.exists ((=) color) params)
+ then raise (C.CoAlgException ("=-formula mentions \""^color^"\" but the only"
+ ^" choices are: "^(String.concat ", " params)))
+ | _ -> raise (C.CoAlgException "=-formula is used in wrong sort.")
+ end;
+ if List.length sortlst <> 1
then raise (C.CoAlgException "=-formula is used in wrong sort.")
else ();
(* NB: =-formulae have no subformlae hence no closure *)
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 9eab31cf0c2855ebc12decd55e0d1ea55741c0e1..b088cb503df9fb5e81a2e3cdb588cd031ca7fd17 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -15,12 +15,16 @@ type functors =
| CoalitionLogic
| GML
| PML
- | Constant
+ | Constant of string list
| Choice
| Fusion
-val functor_of_string : string -> functors option
-val unaryfunctor_of_string : string -> functors option
+(* functors whose constructor takes additional parameters *)
+type parametricFunctorName =
+ | NameConstant
+
+val functor_of_string : string -> string list -> functors option
+val unaryfunctor_of_string : string -> string list -> functors option
val string_of_functor : functors -> string
(* This type may be extended for additional logics. *)
diff --git a/src/lib/FunctorParsing.ml b/src/lib/FunctorParsing.ml
index 519e3a04eb282e973b8ad90d6f2fa786e358f0d7..23c4ce1c741d5f27e6e8ffc372e3b5d8143d91d3 100644
--- a/src/lib/FunctorParsing.ml
+++ b/src/lib/FunctorParsing.ml
@@ -115,9 +115,9 @@ let functorExpFromString str : functorExp =
let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable =
- let logicName2Functor str = match (CM.unaryfunctor_of_string str) with
+ let logicName2Functor str params = match (CM.unaryfunctor_of_string str params) with
| Some x -> x
- | None -> raise (FunctorParsingFailed ("Unknown Functor name "^str))
+ | None -> raise (FunctorParsingFailed ("Unknown Functor name or invalid number of parameters passed"^str))
in
let line = ref(0) in
let getLineNr () =
@@ -136,7 +136,7 @@ let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable =
| Unary str_list ->
let nr = getLineNr () in
let functorname = List.hd str_list in
- (fun parameter -> [ (logicName2Functor functorname, [parameter])]), nr
+ (fun parameter -> [ (logicName2Functor functorname (List.tl str_list), [parameter])]), nr
| Choice (a,b) ->
let nr = getLineNr () in
let (a_table, a_nr) = generateSorts a in