Implement rule for CL

CoAlgLogicUtils.ml

@@ -14,6 +14,7 @@ module TArray = struct
     let all f = any (fun x -> not (f x))
     let elem (x: 'a) (arr: 'a array) =
         any (fun y -> x == y) arr
+    let included sub sup = all (fun x -> elem x sup) sub
 end
 
 let disjointAgents sort a b =

CoAlgLogicUtils.mli

@@ -10,6 +10,7 @@ module TArray : sig
     val all : ('a -> bool) -> 'a array -> bool
     val any : ('a -> bool) -> 'a array -> bool
     val elem : 'a -> 'a array -> bool
+    val included : 'a array -> 'a array -> bool
 end
 
 val disjointAgents : sort -> localFormula -> localFormula -> bool

CoAlgLogics.ml

@@ -210,6 +210,45 @@ let mkRule_CL sort bs sl =
   in
   (* Candidates for D in Rule 2 *)
   let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
+  let c_j : localFormula list =
+    bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
+  in
+  let getRule2 diamDb acc = (* diamDb = <D> b *)
+    let d = lfGetDestAg sort diamDb in (* the agent list *)
+    let b = lfGetDest1 sort diamDb in
+    let hasAppropriateAglist f =
+        let aglist = lfGetDestAg sort f in
+        TArray.included aglist d
+    in
+    let maxdisj = maxDisjoints sort (bsetFilter boxes hasAppropriateAglist) in
+    let createSingleRule acc coalitions =
+        let a_i : localFormula list =
+            bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
+        in
+        (* now do rule 2:
+            coalitions  /\ <d> b /\ nCands
+           ————————————————————————————————
+              a_i       /\     b /\ c_j
+        *)
+        let children = bsetMake () in
+        List.iter (bsetAdd children) (b::c_j) ;
+        List.iter (bsetAdd children) (a_i) ;
+        ((fun bs1 -> bs), [(s1, children)])::acc
+    in
+    List.fold_left createSingleRule acc maxdisj
+  in
+  let rules = bsetFold getRule2 dCands [] in
+  let getRule1 acc coalitions =
+    (* do rule 1:
+        coalitions
+       ————————————
+           a_i
+    *)
+    let a_i : bset = bsetMake () in
+    bsetIter (fun f -> bsetAdd a_i (lfGetDest1 sort f)) coalitions ;
+    ((fun bs1 -> bs), [(s1, a_i)])::acc
+  in
+  let rules = List.fold_left getRule1 rules disjoints in
   (*
     mkRule_CL sort bs [s1]
     = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
@@ -217,8 +256,14 @@ let mkRule_CL sort bs sl =
           C_i pairwise disjoint and I maximal
         }
   *)
-  (* just do this to let it compile... *)
-  mkRule_MultiModalK sort bs sl
+  (* standard return procedure *)
+  let res = ref (Some rules) in
+  fun () ->
+    match !res with
+    | None -> NoMoreRules
+    | Some rules ->
+        res := None;
+        AllInOne rules
 
 let mkRule_Choice sort bs sl =
   assert (List.length sl = 2);