summaryrefslogtreecommitdiff
path: root/test-suite/output/Extraction_matchs_2413.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-12-24 11:53:29 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2010-12-24 11:53:29 +0100
commit6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch)
treeb04b45d1a6f42d19b1428c522d647afbad2f9b83 /test-suite/output/Extraction_matchs_2413.v
parent3e96002677226c0cdaa8f355938a76cfb37a722a (diff)
Imported Upstream version 8.3pl1upstream/8.3pl1
Diffstat (limited to 'test-suite/output/Extraction_matchs_2413.v')
-rw-r--r--test-suite/output/Extraction_matchs_2413.v128
1 files changed, 128 insertions, 0 deletions
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
new file mode 100644
index 00000000..f5610efc
--- /dev/null
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -0,0 +1,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) *)
+