blob: 1ecd9771eb547285ec2f5474276a88d42bcb3c3c (
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
(** Extraction : tests of optimizations of pattern matching *)
Require Coq.extraction.Extraction.
(** First, a few basic tests *)
Definition test1 b :=
match b with
| true => true
| false => false
end.
Extraction test1. (** should be seen as the identity *)
Definition test2 b :=
match b with
| true => false
| false => false
end.
Extraction test2. (** should be seen a the always-false constant function *)
Inductive hole (A:Set) : Set := Hole | Hole2.
Definition wrong_id (A B : Set) (x:hole A) : hole B :=
match x with
| Hole _ => @Hole _
| Hole2 _ => @Hole2 _
end.
Extraction wrong_id. (** should _not_ be optimized as an identity *)
Definition test3 (A:Type)(o : option A) :=
match o with
| Some x => Some x
| None => None
end.
Extraction test3. (** Even with type parameters, should be seen as identity *)
Inductive indu : Type := A : nat -> indu | B | C.
Definition test4 n :=
match n with
| A m => A (S m)
| B => B
| C => C
end.
Extraction test4. (** should merge branchs B C into a x->x *)
Definition test5 n :=
match n with
| A m => A (S m)
| B => B
| C => B
end.
Extraction test5. (** should merge branches B C into _->B *)
Inductive indu' : Type := A' : nat -> indu' | B' | C' | D' | E' | F'.
Definition test6 n :=
match n with
| A' m => A' (S m)
| B' => C'
| C' => C'
| D' => C'
| E' => B'
| F' => B'
end.
Extraction test6. (** should merge some branches into a _->C' *)
(** NB : In Coq, "| a => a" corresponds to n, hence some "| _ -> n" are
extracted *)
Definition test7 n :=
match n with
| A m => Some m
| B => None
| C => None
end.
Extraction test7. (** should merge branches B,C into a _->None *)
(** Script from bug #2413 *)
Set Implicit Arguments.
Section S.
Definition message := nat.
Definition word := nat.
Definition mode := nat.
Definition opcode := nat.
Variable condition : word -> option opcode.
Section decoder_result.
Variable inst : Type.
Inductive decoder_result : Type :=
| DecUndefined : decoder_result
| DecUnpredictable : decoder_result
| DecInst : inst -> decoder_result
| DecError : message -> decoder_result.
End decoder_result.
Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode)
(w : word) (inst : Type) (g : mode -> opcode -> inst) :
decoder_result inst :=
match condition w with
| Some oc =>
match f w with
| DecInst i => DecInst (g i oc)
| DecError _ m => @DecError inst m
| DecUndefined _ => @DecUndefined inst
| DecUnpredictable _ => @DecUnpredictable inst
end
| None => @DecUndefined inst
end.
End S.
Extraction decode_cond_mode.
(** inner match should not be factorized with a partial x->x (different type) *)
|
