fix alpha-conversion problems in ehoare

Author: bgregoir

src/phl/ecPhlApp.ml

@@ -26,12 +26,13 @@ let t_hoare_app_r i phi tc =
 let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r
 
 (* -------------------------------------------------------------------- *)
-let t_ehoare_app_r i f tc =
+let t_ehoare_app_r i phi tc =
   let env = FApi.tc1_env tc in
   let hs = tc1_as_ehoareS tc in
   let s1, s2 = s_split env i hs.ehs_s in
-  let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) f in
-  let b = f_eHoareS (snd hs.ehs_m) f (stmt s2) (ehs_po hs) in
+  let phi = ss_inv_rebind phi (fst hs.ehs_m) in
+  let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in
+  let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in
   FApi.xmutate1 tc `HlApp [a; b]
 
 let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r

src/phl/ecPhlConseq.ml

@@ -453,6 +453,9 @@ let t_bdHoareS_conseq_nm = gen_conseq_nm t_bdHoareS_notmod t_bdHoareS_conseq
 let t_ehoareF_concave (fc: ss_inv) pre post tc =
   let env = FApi.tc1_env tc in
   let hf = tc1_as_ehoareF tc in
+  let pre = ss_inv_rebind pre hf.ehf_m in
+  let post = ss_inv_rebind post hf.ehf_m in
+  let fc = ss_inv_rebind fc hf.ehf_m in
   let f = hf.ehf_f in
   let mpr,mpo = Fun.hoareF_memenv hf.ehf_m f env in
   let fsig = (Fun.by_xpath f env).f_sig in
@@ -491,6 +494,9 @@ let t_ehoareS_concave (fc: ss_inv) (* xreal -> xreal *) pre post tc =
   let hs = tc1_as_ehoareS tc in
   let s = hs.ehs_s in
   let m = fst hs.ehs_m in
+  let pre = ss_inv_rebind pre m in
+  let post = ss_inv_rebind post m in
+  let fc = ss_inv_rebind fc m in
   (* ensure that f only depend of notmod *)
   let modi = s_write env s in
   let fv = PV.fv env m fc.inv in

src/phl/ecPhlDeno.ml

@@ -86,8 +86,8 @@ let t_phoare_deno_r pre post tc =
 
 (* -------------------------------------------------------------------- *)
 let t_ehoare_deno_r pre post tc =
-  assert (pre.m = post.m);
   let m = pre.m in
+  assert (m = post.m);
   let env, _, concl = FApi.tc1_eflat tc in
 
   let f, bd =
@@ -111,6 +111,7 @@ let t_ehoare_deno_r pre post tc =
 
   (* forall m, ev%r%xr <= post *)
   let ev = pr.pr_event in
+  let ev = ss_inv_rebind ev m in
   let concl_po = map_ss_inv2 f_xreal_le (map_ss_inv1 f_b2xr ev) post in
   let concl_po = f_forall_mems_ss_inv mpo concl_po in