commited complexity test for exponential behavior of unification

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11894 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 51 insertions, 0 deletions

diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v
new file mode 100644
index 000000000..0e1ec00d6
--- /dev/null
+++ b/test-suite/complexity/unification.v
@@ -0,0 +1,51 @@
+(* Test parsing/interpretation/pretyping on a large example *)
+(* Expected time < 0.10s *)
+
+(* Complexity of unification used to be exponential in the number of nested
+   constants, as pointed out by Georges Gonthier and Nicolas Tabareau (a.o.)
+
+   The problem is that unification of id^n+1(0) and id^n+1(1) proceeds as:
+   - try not unfold the outermost id by trying to unify its arguments:
+     1st rec. call on id^n(0) id^n(1), which fails
+   - Coq then tries to unfold id^n+1(k) which produces id^n(k)
+   - 2nd rec. call on id^n(0) id^n(1), which also fails
+   Complexity is thus at least exponential.
+
+   This is fixed (in the ground case), by the fact that when we try to
+   unify two ground terms (ie. without unsolved evars), we call kernel
+   conversion and if this fails, then the terms are not unifiable.
+   Hopefully, kernel conversion is not exponential on cases like the one
+   below thanks to sharing (as long as unfolding the fonction does not
+   use its argument under a binder).
+
+   There are probably still many cases where unification goes astray.
+ *)
+
+
+Definition id (n:nat) := n.
+Goal
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+   0
+   ))))
+   ))))
+   ))))
+   ))))
+   ))))
+   =
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+   1
+   ))))
+   ))))
+   ))))
+   ))))
+   ))))
+.
+Time try refine (refl_equal _).