From e08cd8a9c9971dd0897200e1137596aecd83c4cb Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Thu, 12 May 2016 17:33:39 +0200
Subject: [PATCH] Fix deferral tracking when "empty" least fixpoints appear
---
src/lib/CoAlgMisc.ml | 13 +++++++++----
1 file changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 8fd1f68..85d08bc 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -1017,10 +1017,15 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
*)
| C.HCMU (name, f1) ->
- let () = C.HcFHt.replace vset.(s) f name in
- let unfold = C.hc_replace hcF name f f1 in
- let appendvars = List.append newvars [name] in
- detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
+ begin
+ if C.hc_freeIn name f1
+ then
+ C.HcFHt.replace vset.(s) f name
+ else ();
+ let unfold = C.hc_replace hcF name f f1 in
+ let appendvars = List.append newvars [name] in
+ detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
+ end
| C.HCNU (name, f1) ->
let unfold = C.hc_replace hcF name f f1 in
detClosure_ nomTbl hcF fset vset atset nomset s unfold
--
GitLab