(hds -> orig) + changelog

Author: Tragicus

doc/changelog/14-misc/19987-fold-evd-Changed.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  The unification algorithm (evarconv) may need to unfold its two input terms to succeed. Now, when one of the terms is an evar, it instantiates it with the folded version of the other term. In other words, tactics now unfold less than before, which may change the behavior of subsequent tactics.
+  (`#19987 <https://github.com/rocq-prover/rocq/pull/19987>`_,
+  by Quentin Vermande).

pretyping/evarconv.ml

@@ -685,6 +685,8 @@ struct
     if l2r then clear_left c else clear_left (flip c)
 end
 
+type orig = { left : state; right : state }
+
 let rec evar_conv_x flags env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
@@ -708,7 +710,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
           let hd2 = (whd_nored_state env evd (term2,Stack.empty)) in
         match
           evar_eqappr_x flags env evd pbty (Cs_keys_cache.empty ()) None
-            (hd1, hd2) hd1 hd2
+            { left = hd1; right = hd2 } hd1 hd2
         with
         | UnifFailure _ as x ->
            if Retyping.is_term_irrelevant env evd term1 ||
@@ -745,7 +747,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
 and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     keys (* canonical structure keys cache *)
     lastUnfolded (* tells which side was last unfolded, if any, where `true` means RHS. *)
-    hds (term1, sk1 as appr1) (term2, sk2 as appr2) =
+    orig (term1, sk1 as appr1) (term2, sk2 as appr2) =
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
@@ -782,8 +784,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       flags.open_ts env' evd (c'1, Stack.empty) in
     let out2 = whd_nored_state env' evd
       (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty) in
-    if onleft then evar_eqappr_x flags env' evd CONV keys None (out1, out2) out1 out2
-    else evar_eqappr_x flags env' evd CONV (Cs_keys_cache.flip keys) None (out2, out1) out2 out1
+    if onleft then evar_eqappr_x flags env' evd CONV keys None { left = out1; right = out2 } out1 out2
+    else evar_eqappr_x flags env' evd CONV (Cs_keys_cache.flip keys) None { left = out2; right = out1 } out2 out1
   in
   let rigids env evd sk term sk' term' =
     let nargs = Stack.args_size sk in
@@ -828,8 +830,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       (* We cheat here. Unfolding here means that we should not go back to the heads
         when rediscovering the problem ?e=t, so we put the unfolded term in place of the
         head. *)
-      let hds = (apprM', apprM') in
-      switch (evar_eqappr_x flags env i pbty keys None hds) apprF apprM'
+      let orig = { left = apprM'; right = apprM' } in
+      switch (evar_eqappr_x flags env i pbty keys None orig) apprF apprM'
     in
     let default i = ise_try i [miller l2r ev apprF apprM;
                                consume l2r apprF apprM;
@@ -853,9 +855,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                   (* We cheat here. Unfolding here means that we should not go back to the heads
                      when rediscovering the problem ?e=t, so we put the unfolded term in place of the
                      head. *)
-                  let hds = if l2r then (fst hds, apprM') else (apprM', snd hds) in
+                  let orig = if l2r then { left = orig.right; right = apprM' } else { left = apprM'; right = orig.left } in
                   let delta' i =
-                    switch (evar_eqappr_x flags env i pbty keys None hds) apprF apprM'
+                    switch (evar_eqappr_x flags env i pbty keys None orig) apprF apprM'
                   in
                   fun i -> ise_try i [miller l2r ev apprF apprM';
                                    consume l2r apprF apprM'; delta']
@@ -910,7 +912,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                      UnifFailure (evd,OccurCheck (fst ev,tR)))])
             ev lF tR evd
   in
-  let first_order env i t1 t2 sk1 sk2 hds =
+  let first_order env i t1 t2 sk1 sk2 orig =
     (* Try first-order unification *)
     match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
     | None, Success i' ->
@@ -922,7 +924,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                           (position_problem true pbty,destEvar i' ev1',term2)
        else
          (* HH: Why not to drop sk1 and sk2 since they unified *)
-         evar_eqappr_x flags env evd pbty keys None hds
+         evar_eqappr_x flags env evd pbty keys None orig
                        (ev1', sk1) (term2, sk2)
     | Some (r,[]), Success i' ->
        (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
@@ -932,7 +934,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
          solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r))
        else
-         evar_eqappr_x flags env evd pbty keys None hds
+         evar_eqappr_x flags env evd pbty keys None orig
                        (ev2', sk1) (term2, sk2)
     | Some ([],r), Success i' ->
        (* Symmetrically *)
@@ -944,7 +946,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                           (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r))
        else
          (* HH: Why not to drop sk1 and sk2 since they unified *)
-         evar_eqappr_x flags env evd pbty keys None hds
+         evar_eqappr_x flags env evd pbty keys None orig
                           (ev1', sk1) (term2, sk2)
     | None, (UnifFailure _ as x) ->
        (* sk1 and sk2 have no common outer part *)
@@ -1017,11 +1019,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
     | Flexible (sp1,al1), Flexible (sp2,al2) ->
-        let k1 = if lastUnfolded = Some true && not (Stack.not_purely_applicative sk1) then let (t, sk) = fst hds in flex_kind_of_term flags env evd t sk else Flexible (sp1, al1) in
-        let k2 = if lastUnfolded = Some false && not (Stack.not_purely_applicative sk2) then let (t, sk) = snd hds in flex_kind_of_term flags env evd t sk else Flexible (sp2, al2) in
+        let k1 = if lastUnfolded = Some true && not (Stack.not_purely_applicative sk1) then let (t, sk) = orig.left in flex_kind_of_term flags env evd t sk else Flexible (sp1, al1) in
+        let k2 = if lastUnfolded = Some false && not (Stack.not_purely_applicative sk2) then let (t, sk) = orig.right in flex_kind_of_term flags env evd t sk else Flexible (sp2, al2) in
         begin match (k1, k2) with
-        | Flexible ev1, MaybeFlexible v2 -> flex_maybeflex true ev1 appr1 (snd hds) (snd hds)
-        | MaybeFlexible v1, Flexible ev2 -> flex_maybeflex false ev2 appr2 (fst hds) (fst hds)
+        | Flexible ev1, MaybeFlexible v2 -> flex_maybeflex true ev1 appr1 orig.right orig.right
+        | MaybeFlexible v1, Flexible ev2 -> flex_maybeflex false ev2 appr2 orig.left orig.left
         | _, Rigid | Rigid, _ -> anomaly (Pp.str "flexible terms cannot fold to rigid ones")
         | _ ->
       (* Notations:
@@ -1035,7 +1037,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
            1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂]
              recursively solve E2[?n[inst]] = E'2[redex]
            2. fails if neither E₁ nor E₂ is a prefix of the other *)
-        let f1 i = first_order env i term1 term2 sk1 sk2 hds
+        let f1 i = first_order env i term1 term2 sk1 sk2 orig
         and f2 i =
           if Evar.equal sp1 sp2 then
             match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
@@ -1066,10 +1068,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         end
 
     | Flexible ev1, MaybeFlexible v2 ->
-      flex_maybeflex true ev1 appr1 appr2 (if Stack.not_purely_applicative sk1 then appr2 else snd hds)
+      flex_maybeflex true ev1 appr1 appr2 (if Stack.not_purely_applicative sk1 then appr2 else orig.right)
 
     | MaybeFlexible vsk1, Flexible ev2 ->
-      flex_maybeflex false ev2 appr2 appr1 (if Stack.not_purely_applicative sk2 then appr1 else fst hds)
+      flex_maybeflex false ev2 appr2 appr1 (if Stack.not_purely_applicative sk2 then appr1 else orig.left)
 
     | MaybeFlexible (v1', sk1' as vsk1'), MaybeFlexible (v2', sk2' as vsk2') -> begin
         match EConstr.kind evd term1, EConstr.kind evd term2 with
@@ -1089,7 +1091,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         and f2 i =
           let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1'
           and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2'
-          in evar_eqappr_x flags env i pbty keys None hds out1 out2
+          in evar_eqappr_x flags env i pbty keys None orig out1 out2
         in
         ise_try evd [f1; f2]
 
@@ -1101,7 +1103,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           and f2 i =
             let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1'
             and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2'
-            in evar_eqappr_x flags env i pbty keys None hds out1 out2
+            in evar_eqappr_x flags env i pbty keys None orig out1 out2
           in
             ise_try evd [f1; f2]
 
@@ -1113,7 +1115,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           in
             (match res with
             | Some (f1,args1) ->
-              evar_eqappr_x flags env evd pbty keys None hds (f1,Stack.append_app args1 sk1)
+              evar_eqappr_x flags env evd pbty keys None orig (f1,Stack.append_app args1 sk1)
                 appr2
             | None -> UnifFailure (evd,NotSameHead))
 
@@ -1124,7 +1126,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           in
             (match res with
             | Some (f2,args2) ->
-              evar_eqappr_x flags env evd pbty keys None hds appr1 (f2,Stack.append_app args2 sk2)
+              evar_eqappr_x flags env evd pbty keys None orig appr1 (f2,Stack.append_app args2 sk2)
             | None -> UnifFailure (evd,NotSameHead))
 
         | _, _ ->
@@ -1187,14 +1189,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           ise_try i [
             (fun i ->
               if b || !no_cs1 then
-                evar_eqappr_x flags env i pbty keys (Some false) hds
+                evar_eqappr_x flags env i pbty keys (Some false) orig
                   (whd_betaiota_deltazeta_for_iota_state
                      flags.open_ts env i vsk1')
                   appr2
               else quick_fail i);
             fun i ->
               if b then quick_fail i else
-              evar_eqappr_x flags env i pbty keys (Some true) hds appr1
+              evar_eqappr_x flags env i pbty keys (Some true) orig appr1
                 (whd_betaiota_deltazeta_for_iota_state
                    flags.open_ts env i vsk2')]
         in
@@ -1215,15 +1217,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
 
     | Flexible ev1, Rigid ->
         if Stack.not_purely_applicative sk1 then flex_rigid true ev1 appr1 appr2 else
-        let (t2, sk2) as appr2 = snd hds in
+        let (t2, sk2) as appr2 = orig.right in
         begin match flex_kind_of_term flags env evd t2 sk2 with
         | Flexible ev2 -> anomaly (Pp.str "rigid terms can not fold to flexible ones")
         | MaybeFlexible v2 -> flex_maybeflex true ev1 appr1 appr2 appr2
         | Rigid -> flex_rigid true ev1 appr1 appr2
         end
     | Rigid, Flexible ev2 ->
         if Stack.not_purely_applicative sk2 then flex_rigid false ev2 appr2 appr1 else
-        let (t1, sk1) as appr1 = fst hds in
+        let (t1, sk1) as appr1 = orig.left in
         begin match flex_kind_of_term flags env evd t1 sk1 with
         | Flexible ev1 -> anomaly (Pp.str "rigid terms can not fold to flexible ones")
         | MaybeFlexible v1 -> flex_maybeflex false ev2 appr2 appr1 appr1
@@ -1238,7 +1240,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              | Inl x -> x
              | Inr _ -> UnifFailure (i,NoCanonicalStructure)
         and f4 i =
-          evar_eqappr_x flags env i pbty keys (Some false) hds
+          evar_eqappr_x flags env i pbty keys (Some false) orig
             (whd_betaiota_deltazeta_for_iota_state
                flags.open_ts env i vsk1')
             appr2
@@ -1253,7 +1255,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              | Inl x -> x
              | Inr _ -> UnifFailure (i,NoCanonicalStructure)
         and f4 i =
-          evar_eqappr_x flags env i pbty keys (Some true) hds appr1
+          evar_eqappr_x flags env i pbty keys (Some true) orig appr1
             (whd_betaiota_deltazeta_for_iota_state
                flags.open_ts env i vsk2')
         in

pretyping/evarconv.mli

@@ -156,10 +156,12 @@ val evar_unify : Evarsolve.unifier
 (* For debugging *)
 module Cs_keys_cache : sig type t end
 
+type orig = { left: state; right: state }
+
 val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
   env -> evar_map -> conv_pb ->
   Cs_keys_cache.t ->
-  bool option -> (state * state) -> state -> state ->
+  bool option -> orig -> state -> state ->
       Evarsolve.unification_result
 
 val occur_rigidly : Evarsolve.unify_flags ->