Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)

 We now keep some type information in the "info" field of constructors
 and cases, and compact a match with some default branches (or remove
 this match completely) only if this transformation is type-preserving.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 52 insertions, 0 deletions

diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out
new file mode 100644
index 000000000..7bce6671a
--- /dev/null
+++ b/test-suite/output/Extraction_matchs_2413.out
@@ -0,0 +1,52 @@
+(** val test1 : bool -> bool **)
+
+let test1 b =
+  b
+(** val test2 : bool -> bool **)
+
+let test2 b =
+  False
+(** val wrong_id : 'a1 hole -> 'a2 hole **)
+
+let wrong_id = function
+  | Hole -> Hole
+  | Hole2 -> Hole2
+(** val test3 : 'a1 option -> 'a1 option **)
+
+let test3 o =
+  o
+(** val test4 : indu -> indu **)
+
+let test4 = function
+  | A m -> A (S m)
+  | x -> x
+(** val test5 : indu -> indu **)
+
+let test5 = function
+  | A m -> A (S m)
+  | _ -> B
+(** val test6 : indu' -> indu' **)
+
+let test6 = function
+  | A' m -> A' (S m)
+  | E' -> B'
+  | F' -> B'
+  | _ -> C'
+(** val test7 : indu -> nat option **)
+
+let test7 = function
+  | A m -> Some m
+  | _ -> None
+(** val decode_cond_mode :
+    (word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1
+    -> opcode -> 'a2) -> 'a2 decoder_result **)
+
+let decode_cond_mode condition f w g =
+  match condition w with
+    | Some oc ->
+        (match f w with
+           | DecUndefined -> DecUndefined
+           | DecUnpredictable -> DecUnpredictable
+           | DecInst i -> DecInst (g i oc)
+           | DecError m -> DecError m)
+    | None -> DecUndefined