From 93ea9206cbf29617feb23646f95e794b11e87793 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 6 Mar 2021 22:54:16 +0100 Subject: 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. --- tactics/tactics.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'tactics') 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 -- cgit v1.2.3