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, 22 insertions, 17 deletions

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 3d18431aa7..6ca4488264 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -154,10 +154,10 @@ let rec pp_expr par env args =
 	hov 2 (str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
 	       ++ pp_expr true env [] t)
-    | MLcase ((_,factors),t, pv) ->
+    | MLcase (info,t, pv) ->
       	apply (pp_par par'
 		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		       fnl () ++ str "  " ++ pp_pat env factors pv)))
+		       fnl () ++ str "  " ++ pp_pat env info pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -170,7 +170,7 @@ let rec pp_expr par env args =
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
 
-and pp_pat env factors pv =
+and pp_pat env info pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
     let par = expr_needs_par t in
@@ -182,27 +182,32 @@ and pp_pat env factors pv =
 			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
 	   str " ->" ++ spc () ++ pp_expr par env' [] t)
   in
-  let factor_br, factor_l = try match factors with
-    | BranchFun (i::_ as l) -> check_function_branch pv.(i), l
-    | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l
-    | _ -> MLdummy, []
-  with Impossible -> MLdummy, []
+  let factor_br, factor_set = try match info.m_same with
+    | BranchFun ints ->
+        let i = Intset.choose ints in
+	branch_as_fun info.m_typs pv.(i), ints
+    | BranchCst ints ->
+        let i = Intset.choose ints in
+        ast_pop (branch_as_cst pv.(i)), ints
+    | BranchNone -> MLdummy, Intset.empty
+  with _ -> MLdummy, Intset.empty
   in
-  let par = expr_needs_par factor_br in
   let last = Array.length pv - 1 in
   prvecti
-    (fun i x -> if List.mem i factor_l then mt () else
+    (fun i x -> if Intset.mem i factor_set then mt () else
        (pp_one_pat pv.(i) ++
-       if i = last && factor_l = [] then mt () else
+       if i = last && Intset.is_empty factor_set then mt () else
        fnl () ++ str "  ")) pv
   ++
-  if factor_l = [] then mt () else match factors with
+  if Intset.is_empty factor_set then mt () else
+  let par = expr_needs_par factor_br in
+  match info.m_same with
     | BranchFun _ ->
-	let ids, env' = push_vars [anonymous_name] env in
-	pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-	pp_expr par env' [] factor_br
+        let ids, env' = push_vars [anonymous_name] env in
+        pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+	  pp_expr par env' [] factor_br
     | BranchCst _ ->
-	str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
+        str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
     | BranchNone -> mt ()
 
 (*s names of the functions ([ids]) are already pushed in [env],
@@ -282,7 +287,7 @@ let rec pp_ind first kn i ind =
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dind (kn,i) when i.ind_info = Singleton ->
+  | Dind (kn,i) when i.ind_kind = Singleton ->
       pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl ()
   | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i)
   | Dtype (r, l, t) ->