fixed matching - broken reduction

Author: oskgo

src/ecHiGoal.ml

@@ -453,8 +453,8 @@ let process_done tc =
 
 (* -------------------------------------------------------------------- *)
 let process_apply_bwd ~implicits mode (ff : ppterm) (tc : tcenv1) =
-  let pt = PT.tc1_process_full_pterm ~implicits tc ff in
 
+  let pt = PT.tc1_process_full_pterm ~implicits tc ff in
   try
     match mode with
     | `Alpha ->

src/ecLowGoal.ml

@@ -2290,6 +2290,9 @@ type cstate = {
   cs_sbeq : Sid.t;
 }
 
+let pp_tc1 tc =
+  pp_tc (FApi.tcenv_of_tcenv1 tc)
+
 let t_debug ?(tag="") t tc =
   Format.eprintf "Before (tag: %s):" tag;
   pp_tc (FApi.tcenv_of_tcenv1 tc);

src/ecLowGoal.mli

@@ -358,3 +358,9 @@ val t_debug :
   -> FApi.backward
   -> FApi.backward
 [@@ocaml.alert debug "Debug function, remove uses before merging"]
+
+val pp_tc :tcenv -> unit
+[@@ocaml.alert debug "Debug function, remove uses before merging"]
+
+val pp_tc1 :tcenv1 -> unit
+[@@ocaml.alert debug "Debug function, remove uses before merging"]

src/ecMatching.ml

@@ -677,6 +677,11 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
       | FhoareF hf1, FhoareF hf2 -> begin
           if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then
             failure ();
+          let subst =
+            if   id_equal hf1.hf_m hf2.hf_m
+            then subst
+            else Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in
+          assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs));
           let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in
           List.iter2 (doit env (subst, mxs))
             [hf1.hf_pr; hf1.hf_po] [hf2.hf_pr; hf2.hf_po]

src/ecReduction.ml

@@ -1453,7 +1453,10 @@ let rec conv ri env f1 f2 stk =
       conv_next ri env f1 stk
 
   | FhoareF hf1, FhoareF hf2 when EqTest_i.for_xp env hf1.hf_f hf2.hf_f ->
-    conv ri env hf1.hf_pr hf2.hf_pr (zhl f1 [hf1.hf_po] [hf2.hf_po] stk)
+    let subst = if id_equal hf1.hf_m hf2.hf_m then Fsubst.f_subst_id 
+      else Fsubst.f_bind_mem Fsubst.f_subst_id hf1.hf_m hf2.hf_m in
+    let subst = Fsubst.f_subst subst in
+      conv ri env hf1.hf_pr (subst hf2.hf_pr) (zhl f1 [hf1.hf_po] [subst hf2.hf_po] stk)
 
   | FhoareS hs1, FhoareS hs2
       when EqTest_i.for_stmt env hs1.hs_s hs2.hs_s ->