From 5e0983fe843e57e64be9cd072b3f89f9f8d76ca1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Fri, 23 Jan 2015 06:23:22 +1100
Subject: [PATCH] Implement functor parameters for Const
---
src/coalg/coalg.ml | 2 +
src/lib/CoAlgLogics.ml | 1 +
src/lib/CoAlgMisc.ml | 82 ++++++++++++++++++++++++++-------------
src/lib/CoAlgMisc.mli | 10 +++--
src/lib/FunctorParsing.ml | 6 +--
5 files changed, 69 insertions(+), 32 deletions(-)
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index 68484d4..a100d2d 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 20c78b4..6d21a11 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 bd7093d..d52be14 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 9eab31c..b088cb5 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 519e3a0..23c4ce1 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
--
GitLab