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, 15 insertions, 7 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 1e2793aa5d..5131704a7c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -27,7 +27,7 @@ open Table
 open Mlutil
 (*i*)
 
-exception I of inductive_info
+exception I of inductive_kind
 
 (* A set of all fixpoint functions currently being extracted *)
 let current_fixpoints = ref ([] : constant list)
@@ -356,7 +356,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     in
 
     add_ind kn mib
-      {ind_info = Standard;
+      {ind_kind = Standard;
        ind_nparams = npar;
        ind_packets = packets;
        ind_equiv = equiv
@@ -441,7 +441,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	Record field_glob
       with (I info) -> info
     in
-    let i = {ind_info = ind_info;
+    let i = {ind_kind = ind_info;
 	     ind_nparams = npar;
 	     ind_packets = packets;
 	     ind_equiv = equiv }
@@ -699,9 +699,15 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
   let magic2 = needs_magic (a, mlt) in
   let head mla =
-    if mi.ind_info = Singleton then
+    if mi.ind_kind = Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
-    else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
+    else
+      let typeargs = match snd (type_decomp type_cons) with
+	| Tglob (_,l) -> List.map type_simpl l
+	| _ -> assert false
+      in
+      let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
+      put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
   in
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then
@@ -767,7 +773,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
 	(r, List.rev ids, e')
       in
-      if mi.ind_info = Singleton then
+      if mi.ind_kind = Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
@@ -778,7 +784,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	end
       else
 	(* Standard case: we apply [extract_branch]. *)
-	MLcase ((mi.ind_info,BranchNone), a, Array.init br_size extract_branch)
+	let typs = List.map type_simpl (Array.to_list metas) in
+	let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
+	in MLcase (info, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)