fix proc*

Author: oskgo

src/ecPV.ml

@@ -823,7 +823,8 @@ module Mpv2 = struct
       List.fold_left2 do1 local ids1 ids2
     with _ -> raise EqObsInError
 
-  let needed_eq env ml mr f =
+  let needed_eq env f =
+    let ml, mr = f.ml, f.mr in
 
     let rec add_eq local eqs f1 f2 =
       match f1.f_node, f2.f_node with
@@ -897,8 +898,7 @@ module Mpv2 = struct
         end
       | _ -> raise Not_found in
 
-    try aux Mid.empty empty f
-    with _ -> raise Not_found
+    aux Mid.empty empty f.inv
 
   let check_glob eqs =
     Mnpv.iter (fun pv (s,_)->

src/ecPV.mli

@@ -158,7 +158,7 @@ module Mpv2 : sig
   val to_form_ts_inv : t -> ts_inv -> ts_inv
   val to_form : t -> memory -> memory -> form -> form
   val of_form : env -> ts_inv -> t
-  val needed_eq : env -> EcIdent.t -> EcIdent.t -> form -> t
+  val needed_eq : env -> ts_inv -> t
   val union   : t -> t -> t
   val subset   : t -> t -> bool
   val equal    : t -> t -> bool

src/phl/ecPhlCall.ml

@@ -239,6 +239,10 @@ let t_bdhoare_call fpre fpost opt_bd tc =
 let t_equiv_call fpre fpost tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
   let es = tc1_as_equivS tc in
+  let ml, mr = fst es.es_ml, fst es.es_mr in
+  let fpre = ts_inv_rebind fpre ml mr in
+  let fpost = ts_inv_rebind fpost ml mr in
+
   let (lpl,fl,argsl),sl = tc1_last_call tc es.es_sl in
   let (lpr,fr,argsr),sr = tc1_last_call tc es.es_sr in
   (* The functions satisfy their specification *)

src/phl/ecPhlDeno.ml

@@ -438,7 +438,7 @@ let post_iff ml mr eq env evl evr =
   try
     if not eq then raise Not_found;
     Mpv2.to_form
-      (Mpv2.needed_eq env ml mr post)  ml mr f_true
+      (Mpv2.needed_eq env {ml; mr; inv=post})  ml mr f_true
   with Not_found -> post
 
 (* -------------------------------------------------------------------- *)

src/phl/ecPhlEqobs.ml

@@ -457,8 +457,8 @@ let process_eqobs_inS info tc =
     | Some pf ->
       process_eqs env tc (TTC.tc1_process_prhl_formula tc pf)
     | None ->
-      try Mpv2.needed_eq env mleft mright es.es_po
-      with _ -> tc_error !!tc "cannot infer the set of equalities" in
+      try Mpv2.needed_eq env (es_po es)
+      with Not_found -> tc_error !!tc "cannot infer the set of equalities" in
   let post = Mpv2.to_form_ts_inv eqo inv in
   let sim = init_sim env spec inv in
   let t_main tc =
@@ -501,7 +501,7 @@ let process_eqobs_inF info tc =
     | Some pf ->
       process_eqs env tc (TTC.tc1_process_prhl_form tc tbool pf)
     | None ->
-      try Mpv2.needed_eq env mleft mright ef.ef_po
+      try Mpv2.needed_eq env (ef_po ef)
       with _ -> tc_error !!tc "cannot infer the set of equalities" in
   let eqo = Mpv2.remove env pv_res pv_res eqo in
   let sim = init_sim env spec inv in
@@ -519,7 +519,6 @@ let process_eqobs_in cm info tc =
   let prett cm tc =
     let dt, ts = EcHiGoal.process_crushmode cm in
       EcPhlConseq.t_conseqauto ~delta:dt ?tsolve:ts tc in
-
   let tt tc =
     let concl = FApi.tc1_goal tc in
     match concl.f_node with

src/phl/ecPhlFun.ml

@@ -425,8 +425,8 @@ let t_fun_to_code_hoare_r tc =
   let spo = ToCodeLow.add_var env pv_res m r me PVM.empty in
   let pre  = PVM.subst env spr (hf_pr hf).inv in
   let post = PVM.subst env spo (hf_po hf).inv in
-  let concl = f_hoareS (snd me) {m;inv=pre} st {m;inv=post} in
-
+  let m, mt = me in
+  let concl = f_hoareS mt {m;inv=pre} st {m;inv=post} in
   FApi.xmutate1 tc `FunToCode [concl]
 
 (* -------------------------------------------------------------------- *)
@@ -435,14 +435,14 @@ let t_fun_to_code_ehoare_r tc =
   let hf = tc1_as_ehoareF tc in
   let f = hf.ehf_f in
   let m = hf.ehf_m in
-  let (_,mt) as me, st, r, a = ToCodeLow.to_code env f m in
+  let me, st, r, a = ToCodeLow.to_code env f m in
   let spr = ToCodeLow.add_var_tuple env pv_arg m a me PVM.empty in
   let spo = ToCodeLow.add_var env pv_res mhr r me PVM.empty in
 
   let pre = PVM.subst env spr hf.ehf_pr in
 
   let post = PVM.subst env spo hf.ehf_po in
-
+  let m, mt = me in
   let concl = f_eHoareS mt {m;inv=pre} st {m;inv=post} in
 
   FApi.xmutate1 tc `FunToCode [concl]
@@ -451,59 +451,65 @@ let t_fun_to_code_ehoare_r tc =
 let t_fun_to_code_bdhoare_r tc =
   let env = FApi.tc1_env tc in
   let hf = tc1_as_bdhoareF tc in
+  let m0 = hf.bhf_m in
   let f = hf.bhf_f in
-  let m, st, r, a = ToCodeLow.to_code env f mhr in
-  let spr = ToCodeLow.add_var_tuple env pv_arg mhr a m PVM.empty in
-  let spo = ToCodeLow.add_var env pv_res mhr r m PVM.empty in
+  let m, st, r, a = ToCodeLow.to_code env f m0 in
+  let spr = ToCodeLow.add_var_tuple env pv_arg m0 a m PVM.empty in
+  let spo = ToCodeLow.add_var env pv_res m0 r m PVM.empty in
   let pre  = PVM.subst env spr hf.bhf_pr in
   let post = PVM.subst env spo hf.bhf_po in
   let bd   = PVM.subst env spr hf.bhf_bd in
-  let concl = f_bdHoareS_old m pre st post hf.bhf_cmp bd in
+  let m, mt = m in
+  let concl = f_bdHoareS mt {m;inv=pre} st {m;inv=post} hf.bhf_cmp {m;inv=bd} in
   FApi.xmutate1 tc `FunToCode [concl]
 
 (* -------------------------------------------------------------------- *)
 let t_fun_to_code_equiv_r tc =
   let env = FApi.tc1_env tc in
   let ef = tc1_as_equivF tc in
+  let ml0, mr0 = ef.ef_ml, ef.ef_mr in
   let (fl,fr) = ef.ef_fl, ef.ef_fr in
-  let ml, sl, rl, al = ToCodeLow.to_code env fl mleft in
-  let mr, sr, rr, ar = ToCodeLow.to_code env fr mright in
+  let ml, sl, rl, al = ToCodeLow.to_code env fl ml0 in
+  let mr, sr, rr, ar = ToCodeLow.to_code env fr mr0 in
   let spr =
     let s = PVM.empty in
-    let s = ToCodeLow.add_var_tuple env pv_arg mleft  al ml s in
-    let s = ToCodeLow.add_var_tuple env pv_arg mright ar mr s in
+    let s = ToCodeLow.add_var_tuple env pv_arg ml0  al ml s in
+    let s = ToCodeLow.add_var_tuple env pv_arg mr0 ar mr s in
     s in
   let spo =
     let s = PVM.empty in
-    let s = ToCodeLow.add_var env pv_res mleft  rl ml s in
-    let s = ToCodeLow.add_var env pv_res mright rr mr s in
+    let s = ToCodeLow.add_var env pv_res ml0  rl ml s in
+    let s = ToCodeLow.add_var env pv_res mr0 rr mr s in
     s in
   let pre   = PVM.subst env spr ef.ef_pr in
   let post  = PVM.subst env spo ef.ef_po in
-  let concl = f_equivS_old ml mr pre sl sr post in
+  let (ml, mlt), (mr, mrt) = ml, mr in
+  let concl = f_equivS mlt mrt {ml;mr;inv=pre} sl sr {ml;mr;inv=post} in
 
   FApi.xmutate1 tc `FunToCode [concl]
 
 let t_fun_to_code_eager_r tc =
   let env = FApi.tc1_env tc in
   let eg = tc1_as_eagerF tc in
+  let ml0, mr0 = eg.eg_ml, eg.eg_mr in
   let (fl,fr) = eg.eg_fl, eg.eg_fr in
-  let ml, sl, rl, al = ToCodeLow.to_code env fl mleft in
-  let mr, sr, rr, ar = ToCodeLow.to_code env fr mright in
+  let ml, sl, rl, al = ToCodeLow.to_code env fl ml0 in
+  let mr, sr, rr, ar = ToCodeLow.to_code env fr mr0 in
   let spr =
     let s = PVM.empty in
-    let s = ToCodeLow.add_var_tuple env pv_arg mleft  al ml s in
-    let s = ToCodeLow.add_var_tuple env pv_arg mright ar mr s in
+    let s = ToCodeLow.add_var_tuple env pv_arg ml0  al ml s in
+    let s = ToCodeLow.add_var_tuple env pv_arg mr0 ar mr s in
     s in
   let spo =
     let s = PVM.empty in
-    let s = ToCodeLow.add_var env pv_res mleft  rl ml s in
-    let s = ToCodeLow.add_var env pv_res mright rr mr s in
+    let s = ToCodeLow.add_var env pv_res ml0  rl ml s in
+    let s = ToCodeLow.add_var env pv_res mr0 rr mr s in
     s in
   let pre   = PVM.subst env spr eg.eg_pr in
   let post  = PVM.subst env spo eg.eg_po in
+  let (ml, mlt), (mr, mrt) = ml, mr in
   let concl =
-    f_equivS_old ml mr pre (s_seq eg.eg_sl sl) (s_seq sr eg.eg_sr) post in
+    f_equivS mlt mrt {ml;mr;inv=pre} (s_seq eg.eg_sl sl) (s_seq sr eg.eg_sr) {ml;mr;inv=post} in
   FApi.xmutate1 tc `FunToCode [concl]
 
 (* -------------------------------------------------------------------- *)

src/phl/ecPhlTrans.ml

@@ -47,7 +47,6 @@ module Low = struct
     let cond1, cond2 =
       transitivity_side_cond hyps
         m1 m3 m1 m3 (es_pr es) (es_po es) p1 q1 mt p2 q2 in
-    !pp_debug_form (FApi.tc1_env tc) cond1;
     let cond3 =
       f_equivS (snd es.es_ml) mt p1 es.es_sl c2 q1 in
     let cond4 =