fix res in proc

Author: oskgo

src/ecEnv.ml

@@ -1757,12 +1757,12 @@ module Fun = struct
     Memory.push_active_ts prel prer env,
     Memory.push_active_ts postl postr env
 
-  let equivS path1 path2 env =
+  let equivS ml mr path1 path2 env =
     let fun1 = by_xpath path1 env in
     let fun2 = by_xpath path2 env in
-    let fd1, mem1 = actmem_body EcCoreFol.mleft fun1 in
-    let fd2, mem2 = actmem_body EcCoreFol.mright fun2 in
-    mem1, fd1, mem2, fd2, Memory.push_all [mem1; mem2] env
+    let fd1, mem1 = actmem_body ml fun1 in
+    let fd2, mem2 = actmem_body mr fun2 in
+    mem1, fd1, mem2, fd2, Memory.push_active_ts mem1 mem2 env
 end
 
 (* -------------------------------------------------------------------- *)

src/ecEnv.mli

@@ -119,7 +119,7 @@ module Fun : sig
 
   val equivF : memory -> memory -> xpath -> xpath -> env -> env * env
 
-  val equivS : xpath -> xpath -> env ->
+  val equivS : memory -> memory -> xpath -> xpath -> env ->
     memenv * (funsig * function_def) * memenv * (funsig * function_def) * env
 end
 

src/phl/ecPhlEager.ml

@@ -215,6 +215,7 @@ let t_eager_while_r h tc =
 let t_eager_fun_def_r tc =
   let env = FApi.tc1_env tc in
   let eg  = tc1_as_eagerF tc in
+  let ml, mr = eg.eg_ml, eg.eg_mr in
 
   let fl, fr =
     (NormMp.norm_xfun env eg.eg_fl,
@@ -225,7 +226,7 @@ let t_eager_fun_def_r tc =
   EcPhlFun.check_concrete !!tc env fr;
 
   let (memenvl, (fsigl,fdefl),
-       memenvr, (fsigr,fdefr), env) = Fun.equivS fl fr env in
+       memenvr, (fsigr,fdefr), env) = Fun.equivS ml mr fl fr env in
 
   let extend mem fdef =
     match fdef.f_ret with

src/phl/ecPhlFun.ml

@@ -118,23 +118,25 @@ let t_bdhoareF_fun_def_r tc =
 let t_equivF_fun_def_r tc =
   let env = FApi.tc1_env tc in
   let ef = tc1_as_equivF tc in
+  let ml, mr = ef.ef_ml, ef.ef_mr in
   let fl = NormMp.norm_xfun env ef.ef_fl in
   let fr = NormMp.norm_xfun env ef.ef_fr in
   check_concrete !!tc env fl; check_concrete !!tc env fr;
-  let (menvl, eqsl, menvr, eqsr, env) = Fun.equivS fl fr env in
+  let (menvl, eqsl, menvr, eqsr, env) = Fun.equivS ml mr fl fr env in
   let (fsigl, fdefl) = eqsl in
   let (fsigr, fdefr) = eqsr in
-  let ml = EcMemory.memory menvl in
-  let mr = EcMemory.memory menvr in
   let fresl = odfl {m=ml;inv=f_tt} (omap (ss_inv_of_expr ml) fdefl.f_ret) in
-  let fresr = odfl {m=ml;inv=f_tt} (omap (ss_inv_of_expr mr) fdefr.f_ret) in
+  let fresr = odfl {m=mr;inv=f_tt} (omap (ss_inv_of_expr mr) fdefr.f_ret) in
   let s = PVM.add env pv_res ml fresl.inv PVM.empty in
   let s = PVM.add env pv_res mr fresr.inv s in
   let post = map_ts_inv1 (PVM.subst env s) (ef_po ef) in
   let s = subst_pre env fsigl ml PVM.empty in
   let s = subst_pre env fsigr mr s in
   let pre = map_ts_inv1 (PVM.subst env s) (ef_pr ef) in
   let concl' = f_equivS (snd menvl) (snd menvr) pre fdefl.f_body fdefr.f_body post in
+  !pp_debug_form env fresl.inv;
+  !pp_debug_form env post.inv;
+  !pp_debug_form env (ef_po ef).inv;
   FApi.xmutate1 tc `FunDef [concl']
 
 (* -------------------------------------------------------------------- *)