← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/complexity/unification.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/complexity/unification.v
 
1
(* Test parsing/interpretation/pretyping on a large example *)
 
2
(* Expected time < 0.10s *)
 
3
 
 
4
(* Complexity of unification used to be exponential in the number of nested
 
5
   constants, as pointed out by Georges Gonthier and Nicolas Tabareau (a.o.)
 
6
 
 
7
   The problem is that unification of id^n+1(0) and id^n+1(1) proceeds as:
 
8
   - try not unfold the outermost id by trying to unify its arguments:
 
9
     1st rec. call on id^n(0) id^n(1), which fails
 
10
   - Coq then tries to unfold id^n+1(k) which produces id^n(k)
 
11
   - 2nd rec. call on id^n(0) id^n(1), which also fails
 
12
   Complexity is thus at least exponential.
 
13
 
 
14
   This is fixed (in the ground case), by the fact that when we try to
 
15
   unify two ground terms (ie. without unsolved evars), we call kernel
 
16
   conversion and if this fails, then the terms are not unifiable.
 
17
   Hopefully, kernel conversion is not exponential on cases like the one
 
18
   below thanks to sharing (as long as unfolding the fonction does not
 
19
   use its argument under a binder).
 
20
 
 
21
   There are probably still many cases where unification goes astray.
 
22
 *)
 
23
 
 
24
 
 
25
Definition id (n:nat) := n.
 
26
Goal
 
27
  (id (id (id (id
 
28
  (id (id (id (id
 
29
  (id (id (id (id
 
30
  (id (id (id (id
 
31
  (id (id (id (id
 
32
   0
 
33
   ))))
 
34
   ))))
 
35
   ))))
 
36
   ))))
 
37
   ))))
 
38
   =
 
39
  (id (id (id (id
 
40
  (id (id (id (id
 
41
  (id (id (id (id
 
42
  (id (id (id (id
 
43
  (id (id (id (id
 
44
   1
 
45
   ))))
 
46
   ))))
 
47
   ))))
 
48
   ))))
 
49
   ))))
 
50
.
 
51
Time try refine (refl_equal _).