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.
---
 engine/termops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 12df61e4c8..bfdb3fbc40 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -125,12 +125,12 @@ val pop : constr -> constr
 (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
    as equality *)
 val subst_term_gen : Evd.evar_map ->
-  (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr
+  (Evd.evar_map -> int * constr -> constr -> bool) -> constr -> constr -> constr
 
 (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
    as equality *)
 val replace_term_gen :
-  Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) ->
+  Evd.evar_map -> (Evd.evar_map -> int * constr -> constr -> bool) ->
     constr -> constr -> constr -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-- 
cgit v1.2.3