diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml index 7f7b48a6ff9af72082e620c8c316997967322dbd..16eda8fb0fd7f3de7ba3678365b8790d1b4a0aa4 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