Unverified Commit 657a553a authored by Merlin's avatar Merlin 💧
Browse files

WIP: refactoring to know implementations in lib

parent f222439b
Pipeline #13354 waiting for manual action with stages
...@@ -7,6 +7,8 @@ open CoAlgMisc ...@@ -7,6 +7,8 @@ open CoAlgMisc
open CoolUtils open CoolUtils
open CoAlgLogicUtils open CoAlgLogicUtils
module O = Option
module S = MiscSolver module S = MiscSolver
module type S = sig module type S = sig
...@@ -16,9 +18,11 @@ module type S = sig ...@@ -16,9 +18,11 @@ module type S = sig
type rule = (dependencies * (sort * bset * focus) lazylist) type rule = (dependencies * (sort * bset * focus) lazylist)
type stateExpander = rule lazylist type stateExpander = rule lazylist
type ruleEnumeration = rule lazyliststep type ruleEnumeration = rule lazyliststep
type implementation = ((sort -> bset -> focus -> sort list -> stateExpander), (bset list -> (sort * bset) -> bool)) these
val getExpandingFunctionProducer : functors -> sort -> bset -> focus -> sort list -> stateExpander val getExpandingFunctionProducer : functors -> sort -> bset -> focus -> sort list -> stateExpander
val oneStepSatisfiability : functors -> (bset list -> (sort * bset) -> bool) val oneStepSatisfiability : functors -> (bset list -> (sort * bset) -> bool)
val implementationLookup : (functors * implementation) list
end end
module Make (T: FocusTracking.FocusTracker) = struct module Make (T: FocusTracking.FocusTracker) = struct
...@@ -31,6 +35,12 @@ type ruleEnumeration = rule lazyliststep ...@@ -31,6 +35,12 @@ type ruleEnumeration = rule lazyliststep
module Focus = T module Focus = T
type implementation = ((sort -> bset -> focus -> sort list -> stateExpander), (bset list -> (sort * bset) -> bool)) these
let getTableau = These.fst
let getOneStepFun = These.snd
(** directly return a list of rules **) (** directly return a list of rules **)
let mkRuleList_MultiModalK sort bs focus sl : rule list = let mkRuleList_MultiModalK sort bs focus sl : rule list =
(* arguments: (* arguments:
...@@ -561,20 +571,6 @@ let mkRule_Fusion sort bs focus sl : stateExpander = ...@@ -561,20 +571,6 @@ let mkRule_Fusion sort bs focus sl : stateExpander =
(dep 1, lazylistFromList [(s2, bs2, Focus.finalize focus2)])] (dep 1, lazylistFromList [(s2, bs2, Focus.finalize focus2)])]
(* Maps a logic represented by the type "functors" to the corresponding
"plug-in" function.
*)
let getExpandingFunctionProducer = function
| MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
| Monotone -> mkRule_Monotone
| CoalitionLogic -> mkRule_CL
| Constant colors -> mkRule_Const colors
| Identity -> mkRule_Identity
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
| other -> raise (CoAlgFormula.CoAlgException ("one-step rule based satisfiability is not implemented for " ^ string_of_functor other))
let oneStepSat_MultiModalK (u: bset list) sv = let oneStepSat_MultiModalK (u: bset list) sv =
let (sort, v) = sv in let (sort, v) = sv in
let boxargs = bsetMap (lfGetDest1 sort) (bsetFilter v (fun lf -> (lfGetType sort lf) = AxF)) in let boxargs = bsetMap (lfGetDest1 sort) (bsetFilter v (fun lf -> (lfGetType sort lf) = AxF)) in
...@@ -665,10 +661,28 @@ let oneStepSat_GML u sv = ...@@ -665,10 +661,28 @@ let oneStepSat_GML u sv =
oneStepGMLRec counters sort v u oneStepGMLRec counters sort v u
let oneStepSatisfiability = function let implementationLookup = [ (MultiModalK, These (mkRule_MultiModalK, oneStepSat_MultiModalK))
| MultiModalK -> oneStepSat_MultiModalK ; (MultiModalKD, This mkRule_MultiModalKD)
| GML -> oneStepSat_GML ; (Monotone, This mkRule_Monotone)
| other -> raise (CoAlgFormula.CoAlgException ("one-step function based satisfiability is not implemented for " ^ string_of_functor other)) ; (CoalitionLogic, This mkRule_CL)
(* ; (Constant colors, ost mkRule_Const colors) *) (* this is an issue because we can't bind this here... *)
; (Identity, This mkRule_Identity)
; (Choice, This mkRule_Choice)
; (Fusion, This mkRule_Fusion)
; (GML, That oneStepSat_GML)
]
let oval o d = match o with
| None -> d ()
| Some v -> v
let obind o f = match o with
| None -> None
| Some v -> f v
let getExpandingFunctionProducer func = oval (obind (obind (List.assoc_opt func implementationLookup) (fun impl -> These.fst impl)) getTableau) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step tableau based satisfiability is not implemented for " ^ string_of_functor func)))
let oneStepSatisfiability func = oval (obind (obind (List.assoc_opt func implementationLookup) (fun impl -> These.snd impl)) getOneStepFun) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step function based satisfiability is not implemented for " ^ string_of_functor func)))
end end
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
open CoAlgMisc open CoAlgMisc
open CoolUtils
module type S = sig module type S = sig
type focus type focus
...@@ -12,9 +13,11 @@ module type S = sig ...@@ -12,9 +13,11 @@ module type S = sig
type rule = (dependencies * (sort * bset * focus) lazylist) type rule = (dependencies * (sort * bset * focus) lazylist)
type stateExpander = rule lazylist type stateExpander = rule lazylist
type ruleEnumeration = rule lazyliststep type ruleEnumeration = rule lazyliststep
type implementation = ((sort -> bset -> focus -> sort list -> stateExpander), (bset list -> (sort * bset) -> bool)) these
val getExpandingFunctionProducer : functors -> sort -> bset -> focus -> sort list -> stateExpander val getExpandingFunctionProducer : functors -> sort -> bset -> focus -> sort list -> stateExpander
val oneStepSatisfiability : functors -> bset list -> (sort * bset) -> bool val oneStepSatisfiability : functors -> bset list -> (sort * bset) -> bool
val implementationLookup : (functors * implementation) list
end end
module Make (T: FocusTracking.FocusTracker) : S with type focus = T.t module Make (T: FocusTracking.FocusTracker) : S with type focus = T.t
......
...@@ -147,7 +147,25 @@ let fromSome optionalvalue = ...@@ -147,7 +147,25 @@ let fromSome optionalvalue =
| Some x -> x | Some x -> x
| None -> raise No_value | None -> raise No_value
(* vim: set et sw=2 sts=2 ts=8 : *)
let curry f x y = f (x, y) let curry f x y = f (x, y)
let uncurry f (x, y) = f x y let uncurry f (x, y) = f x y
type ('a, 'b) these = This of 'a | That of 'b | These of 'a * 'b
let these fa fb fd = function
| This a -> fa a
| That b -> fb b
| These (a, b) -> fd a b
module These = struct
let fst = function
| This a -> Some a
| That _ -> None
| These (a, _) -> Some a
let snd = function
| This _ -> None
| That b -> Some b
| These (_, b) -> Some b
end
(* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -87,8 +87,15 @@ val (<<) : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) ...@@ -87,8 +87,15 @@ val (<<) : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
exception No_value exception No_value
val fromSome : 'a option -> 'a val fromSome : 'a option -> 'a
type ('a, 'b) these = This of 'a | That of 'b | These of 'a * 'b
val these : ('a -> 'c) -> ('b -> 'c) -> ('a -> 'b -> 'c) -> ('a, 'b) these -> 'c
(* vim: set et sw=2 sts=2 ts=8 : *) module These : sig
val fst : ('a, 'b) these -> 'a option
val snd : ('a, 'b) these -> 'b option
end
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
(* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -129,18 +129,18 @@ let ctl_fast_testcases = ...@@ -129,18 +129,18 @@ let ctl_fast_testcases =
use_functor "KD" nop CTL.fastTests use_functor "KD" nop CTL.fastTests
let testcases = let testcases =
[ (* "DL98" >::: dl98_testcases *) [ "DL98" >::: dl98_testcases
(*; "CTL" >::: ctl_fast_testcases *) ; "CTL" >::: ctl_fast_testcases
"K" >::: k_testcases ; "K" >::: k_testcases
(*; "KD" >::: kd_testcases *) ; "KD" >::: kd_testcases
(*; "K*K" >::: kAndK_testcases *) ; "K*K" >::: kAndK_testcases
(*; "K*KD" >::: kAndKd_testcases *) ; "K*KD" >::: kAndKd_testcases
(*; "K+KD" >::: kOrKd_testcases *) ; "K+KD" >::: kOrKd_testcases
(* ; "Nominals" >::: nominal_testcases *) ; "Nominals" >::: nominal_testcases
(*; "CL" >::: cl_testcases *) ; "CL" >::: cl_testcases
(*; "CL" >::: cl_testcases_2agents *) ; "CL" >::: cl_testcases_2agents
(* ; "PML" >::: pml_testcases (\* PML is currently disabled. See CoAlgLogics.ml *\) *) ; "PML" >::: pml_testcases (* PML is currently disabled. See CoAlgLogics.ml *)
(* ; "PML+K" >::: pmlOrK_testcases (\* PML is currently disabled. See CoAlgLogics.ml *\) *) ; "PML+K" >::: pmlOrK_testcases (* PML is currently disabled. See CoAlgLogics.ml *)
; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases ; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
] ]
;; ;;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment