blob: f5610efc4117192a657ee2acbd32abe15f8d0b5e (
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
|
(** Extraction : tests of optimizations of pattern matching *)
(** 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) *)
|
