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.
---
 test-suite/bugs/closed/bug_13896.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13896.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v
new file mode 100644
index 0000000000..10f24d8564
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13896.v
@@ -0,0 +1,24 @@
+Inductive type : Set :=
+    Tptr : type -> type
+  | Tref : type -> type
+  | Trv_ref : type -> type
+  | Tint : type -> type -> type
+  | Tvoid : type
+  | Tarray : type -> type -> type
+  | Tnamed : type -> type
+  | Tfunction : type -> type -> type -> type
+  | Tbool : type
+  | Tmember_pointer : type -> type -> type
+  | Tfloat : type -> type
+  | Tqualified : type -> type -> type
+  | Tnullptr : type
+  | Tarch : type -> type -> type
+.
+Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }.
+Proof. fix IHty1 1.  decide equality. Defined.
+
+Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False).
+Proof.
+timeout 1 cbn.
+constructor.
+Qed.
-- 
cgit v1.2.3