blob: a92490862fec6500774aeae3f29edc3fdce6b665 (
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
(*********************************************)
(* This has been a bug reported by Y. Bertot *)
Inductive expr : Set :=
| b : expr -> expr -> expr
| u : expr -> expr
| a : expr
| var : nat -> expr.
Fixpoint f (t : expr) : expr :=
match t with
| b t1 t2 => b (f t1) (f t2)
| a => a
| x => b t a
end.
Fixpoint f2 (t : expr) : expr :=
match t with
| b t1 t2 => b (f2 t1) (f2 t2)
| a => a
| x => b x a
end.
(*********************************************)
(* Test expansion of aliases *)
(* Originally taken from NMake_gen.v *)
Local Notation SizePlus n := (S (S (S (S (S (S n)))))).
Local Notation Size := (SizePlus O).
Parameter zn2z : Type -> Type.
Parameter w0 : Type.
Fixpoint word (w : Type) (n : nat) {struct n} : Type :=
match n with
| 0 => w
| S n0 => zn2z (word w n0)
end.
Definition w1 := zn2z w0.
Definition w2 := zn2z w1.
Definition w3 := zn2z w2.
Definition w4 := zn2z w3.
Definition w5 := zn2z w4.
Definition w6 := zn2z w5.
Definition dom_t n := match n with
| 0 => w0
| 1 => w1
| 2 => w2
| 3 => w3
| 4 => w4
| 5 => w5
| 6 => w6
| SizePlus n => word w6 n
end.
Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n).
(* This used to fail because of a bug in expansion of SizePlus wrongly
reusing n as an alias for the subpattern *)
Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
| SizePlus (S n') as n => plus_t n
| _ as n =>
fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
| SizePlus (S (S m')) as m => plus_t n m
| _ => fun x => x
end
end.
(* Test (useless) intermediate alias *)
Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
| S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n''
| _ as n =>
fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
| SizePlus (S (S m')) as m => plus_t n m
| _ => fun x => x
end
end.
(*****************************************************************************)
(* Check that alias expansion behaves consistently from versions to versions *)
Definition g m :=
match pred m with
| 0 => 0
| n => n (* For compatibility, right-hand side should be (S n), not (pred m) *)
end.
Goal forall m, g m = match pred m with 0 => 0 | S n => S n end.
intro; reflexivity.
Abort.
|
