From b09d87a1cdaa21037b0b1a1b81750c473c22c42d Mon Sep 17 00:00:00 2001 From: barras Date: Mon, 9 Feb 2009 16:34:56 +0000 Subject: 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 --- test-suite/complexity/unification.v | 51 +++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 test-suite/complexity/unification.v (limited to 'test-suite/complexity') 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 _). -- cgit v1.2.3