Extraction: factorisation of identical branches in a match

If a match has two or more identical branches (that moreover do not 
depend on their pattern variables), we merge them in a last branch 
whose pattern is _

If _all_ branches are identical, we just remove the match



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

7 files changed, 68 insertions, 36 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 09f03f328..5a192b62e 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -753,7 +753,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	end 
       else 
 	(* Standard case: we apply [extract_branch]. *)
-	MLcase (mi.ind_info, a, Array.init br_size extract_branch)
+	MLcase ((mi.ind_info,[]), a, Array.init br_size extract_branch)
   
 (*s Extraction of a (co)-fixpoint. *)
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 5b2ff8636..1e26f6c75 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -161,10 +161,10 @@ let rec pp_expr par env args =
 	assert (args=[]);
 	pp_par par (pp_global r ++ spc () ++ 
 		    prlist_with_sep spc (pp_expr true env []) args')
-    | MLcase (_,t, pv) ->
+    | MLcase ((_,factors),t, pv) ->
       	apply (pp_par par' 
 		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		       fnl () ++ str "  " ++ pp_pat env pv)))
+		       fnl () ++ str "  " ++ pp_pat env factors 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
@@ -177,7 +177,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 pv = 
+and pp_pat env factors pv = 
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev ids) env in
     let par = expr_needs_par t in
@@ -189,7 +189,18 @@ and pp_pat env pv =
 			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
 	   str " ->" ++ spc () ++ pp_expr par env' [] t)
   in 
-  (prvect_with_sep (fun () -> (fnl () ++ str "  ")) pp_one_pat pv)
+  prvecti 
+    (fun i x -> if List.mem i factors then mt () else 
+       (pp_one_pat pv.(i) ++
+	if factors = [] && i = Array.length pv - 1 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)
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 2a609f139..d728a8a14 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -58,6 +58,8 @@ type inductive_info =
   | Standard 
   | Record of global_reference list 
 
+type case_info = int list (* list of branches to merge in a _ pattern *)
+
 (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. 
    If the inductive is logical ([ip_logical = false]), then all other fields
    are unused. Otherwise, 
@@ -92,7 +94,7 @@ type ml_ast =
   | MLletin  of identifier * ml_ast * ml_ast
   | MLglob   of global_reference
   | MLcons   of inductive_info * global_reference * ml_ast list
-  | MLcase   of inductive_info * ml_ast * 
+  | MLcase   of (inductive_info*case_info) * ml_ast * 
       (global_reference * identifier list * ml_ast) array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index aa74b6cea..2d8a1beac 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -658,20 +658,27 @@ let check_generalizable_case unsafe br =
     if check_and_generalize br.(i) <> f then raise Impossible 
   done; f
 
-(*s Do all branches correspond to the same thing? *)
-
-let check_constant_case br = 
-  if Array.length br = 0 then raise Impossible; 
-  let (r,l,t) = br.(0) in
-  let n = List.length l in 
-  if ast_occurs_itvl 1 n t then raise Impossible; 
-  let cst = ast_lift (-n) t in 
-  for i = 1 to Array.length br - 1 do 
-    let (r,l,t) = br.(i) in
-    let n = List.length l in
-    if (ast_occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) 
-    then raise Impossible
-  done; cst
+(*s Detecting similar branches of a match *)
+
+(* If several branches of a match are equal (and independent from their 
+   patterns) we will print them using a _ pattern. If _all_ branches 
+   are equal, we remove the match.
+*)
+
+let common_branches br = 
+  let tab = Hashtbl.create 13 in 
+  for i = 0 to Array.length br - 1 do 
+    let (r,ids,t) = br.(i) in 
+    let n = List.length ids in 
+    if not (ast_occurs_itvl 1 n t) then 
+       let t = ast_lift (-n) t in 
+       let l = try Hashtbl.find tab t with Not_found -> [] in 
+       Hashtbl.replace tab t (i::l)
+  done; 
+  let best = ref [] in 
+  Hashtbl.iter 
+    (fun _ l -> if List.length l > List.length !best then best := l) tab; 
+  if List.length !best < 2 then [] else !best
 
 (*s If all branches are functions, try to permut the case and the functions. *)
 
@@ -805,18 +812,20 @@ and simpl_case o i br e =
       let f = check_generalizable_case o.opt_case_idg br in 
       simpl o (MLapp (MLlam (anonymous,f),[e]))
     with Impossible -> 
-      try (* Is each branch independant of [e] ? *) 
-	if not o.opt_case_cst then raise Impossible;
-	check_constant_case br 
-      with Impossible ->
+      (* Detect common branches *)
+      let common_br = if not o.opt_case_cst then [] else common_branches br in
+      if List.length common_br = Array.length br && br <> [||] then 
+	let (_,ids,t) = br.(0) in ast_lift (-List.length ids) t
+      else 
+	let new_i = (fst i, common_br) in 
 	(* Swap the case and the lam if possible *)
 	if o.opt_case_fun 
 	then 
 	  let ids,br = permut_case_fun br [] in 
 	  let n = List.length ids in 
-	  if n <> 0 then named_lams ids (MLcase (i,ast_lift n e, br))
-	  else MLcase (i,e,br) 
-	else MLcase (i,e,br)
+	  if n <> 0 then named_lams ids (MLcase (new_i,ast_lift n e, br))
+	  else MLcase (new_i,e,br) 
+	else MLcase (new_i,e,br)
 
 let rec post_simpl = function 
   | MLletin(_,c,e) when (is_atomic (eta_red c)) -> 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 519565888..87713e4d5 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -189,7 +189,7 @@ let ast_iter_references do_term do_cons do_type a =
 	  if lang () = Ocaml then record_iter_references do_term i; 
 	  do_cons r 
       | MLcase (i,_,v) -> 
-	  if lang () = Ocaml then record_iter_references do_term i; 
+	  if lang () = Ocaml then record_iter_references do_term (fst i); 
 	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 547ad73e8..6a0f38af5 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -263,7 +263,7 @@ let rec pp_expr par env args =
 	assert (args=[]);
 	let tuple = pp_tuple (pp_expr true env []) args' in 
 	pp_par par (pp_global r ++ spc () ++ tuple)
-    | MLcase (i, t, pv) ->
+    | MLcase ((i,factors), t, pv) ->
 	let expr = if i = Coinductive then 
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
 	else 
@@ -301,7 +301,7 @@ let rec pp_expr par env args =
 	     apply
       	       (pp_par par' 
       		  (v 0 (str "match " ++ expr ++ str " with" ++
-			fnl () ++ str "  | " ++ pp_pat env i pv))))
+			fnl () ++ str "  | " ++ pp_pat env (i,factors) 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
@@ -335,16 +335,26 @@ and pp_one_pat env i (r,ids,t) =
       else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in 
     pp_global r ++ args, expr
   
-and pp_pat env i pv = 
-  prvect_with_sep (fun () -> (fnl () ++ str "  | ")) 
-    (fun x -> let s1,s2 = pp_one_pat env i x in 
-     hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv
+and pp_pat env (info,factors) pv = 
+  prvecti 
+    (fun i x -> if List.mem i factors then mt () else 
+       let s1,s2 = pp_one_pat env info x in 
+       hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
+       (if factors = [] && i = Array.length pv-1 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)
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
   match t' with 
-    | MLcase(i,MLrel 1,pv) when i=Standard -> 
+    | MLcase(i,MLrel 1,pv) when fst i=Standard -> 
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then 
 	  (f ++ pr_binding (List.rev (List.tl bl)) ++
        	     str " = function" ++ fnl () ++
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 1c51035ea..0b358f77d 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -105,7 +105,7 @@ let rec pp_expr env args =
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in 
 	if i = Coinductive then paren (str "delay " ++ st) else st 
-    | MLcase (i,t, pv) ->
+    | MLcase ((i,_),t, pv) ->
 	let e = 
 	  if i <> Coinductive then pp_expr env [] t 	
 	  else paren (str "force" ++ spc () ++ pp_expr env [] t)