From 559819d79f895fa2f17fd4b56baff1f9443a9fdb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Thu, 12 Dec 2013 16:00:27 +0100
Subject: [PATCH] Add some explaining comments

---
 CoAlgLogics.ml | 33 +++++++++++++++++++++++----------
 CoAlgMisc.ml   |  8 ++++----
 2 files changed, 27 insertions(+), 14 deletions(-)

diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 80d9213..27b8436 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -8,37 +8,50 @@ open CoAlgMisc
 
 let mkRule_MultiModalK sort bs sl =
   assert (List.length sl = 1);
-  let dep f bsl =
-    assert (List.length bsl = 1);
-    let bs1 = List.hd bsl in
+  let dep f bsl =                 (* dependencies for formula f *)
+    assert (List.length bsl = 1); (* -+                 *)
+    let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
     let res = bsetMake () in
     bsetAdd res f;
-    let (role : int) = lfGetDest3 sort f in
+    let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
     let filterFkt f1 =
       if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
         && bsetMem bs1 (lfGetDest1 sort f1)
-      then bsetAdd res f1
+      then
+        (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
+        bsetAdd res f1
       else ()
     in
     bsetIter filterFkt bs;
     res
   in
   let getRules f acc =
-    if lfGetType sort f = ExF then
+    if lfGetType sort f = ExF then (* f = ∃R.C *)
       let bs1 = bsetMake () in
-      bsetAdd bs1 (lfGetDest1 sort f);
-      let (role : int) = lfGetDest3 sort f in
+      bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C }          *)
+      let (role : int) = lfGetDest3 sort f in (* role := R *)
       let filterFkt f1 =
         if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
+          (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
           bsetAdd bs1 (lfGetDest1 sort f1)
         else ()
       in
-      bsetIter filterFkt bs;
-      let s1 = List.hd sl in
+      bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
+      let s1 = List.hd sl in (* [s1] := sl *)
       let rle = (dep f, [(s1, bs1)]) in
       rle::acc
     else acc
   in
+  (* effectively:
+        mkRule_MultiModalK sort bs [s1]
+            = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
+                                     | ∀R.D ∈ bs, D ∈ bs1
+                                     }
+                , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
+                )
+              | "∃R.C" ∈ bs
+              }
+  *)
   let rules = bsetFold getRules bs [] in
   let res = ref (Some rules) in
   fun () ->
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index 6eb456a..8b5e301 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -77,10 +77,10 @@ type formulaType =
   | OrF
   | AtF
   | NomF
-  | ExF
-  | AxF
-  | ChcF
-  | FusF
+  | ExF  (* Existential / diamond *)
+  | AxF  (* Universal / box *)
+  | ChcF (* Choice *)
+  | FusF (* Fusion *)
 
 type localFormula = int
 type bset = S.bitset
-- 
GitLab