From a670c5fd339ee0acbb4fa7da5a2214b68bc3c865 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Thu, 28 Apr 2016 16:09:37 +0200
Subject: [PATCH] Add deferral tracking for Fusion
---
src/lib/CoAlgLogics.ml | 24 ++++++++++++++++++++----
1 file changed, 20 insertions(+), 4 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 7f7b48a..16eda8f 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -600,7 +600,12 @@ let mkRule_Choice sort bs defer sl : stateExpander =
let mkRule_Fusion sort bs defer sl : stateExpander =
assert (List.length sl = 2);
- let defer1 = bsetMake () in (* TODO: track deferrals *)
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let deferral_tracking defer f nextf =
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then bsetAdd defer nextf
+ in
let dep proj bsl =
assert (List.length bsl = 1);
let bs1 = List.hd bsl in
@@ -615,17 +620,28 @@ let mkRule_Fusion sort bs defer sl : stateExpander =
res
in
let bs1 = bsetMake () in
+ let defer1 = bsetMakeRealEmpty () in
let bs2 = bsetMake () in
+ let defer2 = bsetMakeRealEmpty () in
let getRule f =
if lfGetType sort f = FusF then
- if lfGetDest3 sort f = 0 then bsetAdd bs1 (lfGetDest1 sort f)
- else bsetAdd bs2 (lfGetDest1 sort f)
+ if lfGetDest3 sort f = 0 then
+ begin
+ deferral_tracking defer1 f (lfGetDest1 sort f);
+ bsetAdd bs1 (lfGetDest1 sort f)
+ end
+ else
+ begin
+ deferral_tracking defer2 f (lfGetDest1 sort f);
+ bsetAdd bs2 (lfGetDest1 sort f)
+ end
else ()
in
bsetIter getRule bs;
let s1 = List.nth sl 0 in
let s2 = List.nth sl 1 in
- lazylistFromList [(dep 0, lazylistFromList [(s1, bs1, defer1)]); (dep 1, lazylistFromList [(s2, bs2, defer1)])]
+ lazylistFromList [(dep 0, lazylistFromList [(s1, bs1, defer1)]);
+ (dep 1, lazylistFromList [(s2, bs2, defer2)])]
(* Maps a logic represented by the type "functors" to the corresponding
--
GitLab