blob: 0e1ec00d6b5d660b8aecd3ac411c36371f3b14cf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
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 _).
|
