Algorithmically faster algorithm for term replacing.

Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.

In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.

Fixes #13896: cbn very slow.

1 files changed, 12 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cbf12ac22f..3c7f8c55d7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2796,7 +2796,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let open Context.Rel.Declaration in
   let decls,cl = decompose_prod_n_assum sigma i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
-  let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
+  let cache = ref Int.Map.empty in
+  let eq sigma (k, c) t =
+    let c =
+      try Int.Map.find k !cache
+      with Not_found ->
+        let c = EConstr.Vars.lift k c in
+        let () = cache := Int.Map.add k c !cache in
+        c
+    in
+    EConstr.eq_constr_nounivs sigma c t
+  in
+  let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma eq c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name env sigma c t ids cl' na in
   let r = Retyping.relevance_of_type env sigma t in