Make CoAlgLogics with GML rules compile

CoAlgLogics.ml

@@ -278,13 +278,38 @@ let mkRule_GML sort bs sl =
   in
   bsetIter addRole boxes;
   bsetIter addRole diamonds;
-  (*
-    mkRule_GML sort bs [s1]
-    = { (λ[bs1]. bs, [(s1, { ?a_i | i∈I, ?=neg iff a_i should be false })])
-        | I some rule conclusion
-        }
-  *)
-  let rules = [] in
+  let addRule role acc =
+      let premise: (bool*int*int) list =
+        let modality isDiamond m acc =
+            if lfGetDest3 sort m = role
+            then (isDiamond,lfGetDestNum sort m,lfToInt (lfGetDest1 sort m))::acc
+            else acc
+        in
+        List.append
+            (bsetFold (modality true) diamonds [])
+            (bsetFold (modality false) boxes [])
+      in
+      let conclusion = gml_rules premise in
+      (* conclusion is a set of rules, each of the forman \/ /\ lit *)
+      let handleRuleConcl rc acc =
+        let handleConjunction conj =
+            let res = bsetMake () in
+            List.iter (fun (f,positive) ->
+                        let f = lfFromInt f in
+                        let f = if positive then f else
+                                    match lfGetNeg sort f with
+                                    | Some nf -> nf
+                                    | None -> raise (CoAlgFormula.CoAlgException ("Negation of formula missing"))
+                                    in
+                        bsetAdd res f)
+                      conj;
+            (s1,res)
+        in
+        let rc = List.map handleConjunction rc in
+        ((fun bs1 -> bs),rc)::acc
+      in List.fold_right handleRuleConcl conclusion acc
+  in
+  let rules = S.foldBS addRule roles [] in
   (* standard return procedure *)
   let res = ref (Some rules) in
   fun () ->