summaryrefslogtreecommitdiff
path: root/test-suite/output/Extraction_matchs_2413.v
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) *)