From 4706decbaeb97aaed07de78684c8d6417c190acf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Wed, 29 Jan 2014 19:53:34 +0100
Subject: [PATCH] Make CoAlgLogics with GML rules compile
---
CoAlgLogics.ml | 39 ++++++++++++++++++++++++++++++++-------
1 file changed, 32 insertions(+), 7 deletions(-)
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index c826d15..06cfc69 100644
--- a/CoAlgLogics.ml
+++ b/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 () ->
--
GitLab