Extraction: more factorization of common match branches

In addition to the "| _ -> cst" situation, now we can also
 reconstruct a "| e -> f e" final branch. For instance,
 this has a tremenduous effect on Compcert/backend/Selection.v.

 NB: The "fun" factorisation is almost more general than the "cst"
 situation, but not always. Think of A=>A|B=>A, 1st branch will be
 recognized as (fun x->x), not (fun x->A). We also add a fine
 detection of inductive types with phantom type variables, for which
 this optimisation is type-unsafe.

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

1 files changed, 19 insertions, 9 deletions

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index d42840613..97f49d833 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -182,18 +182,28 @@ 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, []
+  in
+  let par = expr_needs_par factor_br in
+  let last = Array.length pv - 1 in
   prvecti
-    (fun i x -> if List.mem i factors then mt () else
+    (fun i x -> if List.mem i factor_l then mt () else
        (pp_one_pat pv.(i) ++
-	if factors = [] && i = Array.length pv - 1 then mt ()
-	else fnl () ++ str "  ")) pv
+       if i = last && factor_l = [] then mt () else
+       fnl () ++ str "  ")) pv
   ++
-  match factors with
-    | [] -> mt ()
-    | i::_ ->
-	let (_,ids,t) = pv.(i) in
-	let t = ast_lift (-List.length ids) t in
-	hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
+  if factor_l = [] then mt () else match factors with
+    | BranchFun _ ->
+	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
+    | BranchNone -> mt ()
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)