aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-09 16:34:56 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-09 16:34:56 +0000
commitb09d87a1cdaa21037b0b1a1b81750c473c22c42d (patch)
tree46b216488c970e111dc6b713979dc14aff3d4b2c /test-suite
parentc580f69cc36cc4cc908febb900a55ae751039a0c (diff)
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
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/complexity/unification.v51
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 _).