Merge PR #978: In printing, experimenting factorizing "match" clauses with same right-hand side.

3 files changed, 107 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4f3669a2b9..1207c967b5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1566,11 +1566,9 @@ substituer après par les initiaux *)
 
 (* builds the matrix of equations testing that each eqn has n patterns
  * and linearizing the _ patterns.
- * Syntactic correctness has already been done in astterm *)
+ * Syntactic correctness has already been done in constrintern *)
 let matx_of_eqns env eqns =
-  let build_eqn (loc,(ids,lpat,rhs)) =
-    let initial_lpat,initial_rhs = lpat,rhs in
-    let initial_rhs = rhs in
+  let build_eqn (loc,(ids,initial_lpat,initial_rhs)) =
     let avoid = ids_of_named_context_val (named_context_val env) in
     let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6527ba9355..23993243f4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -252,6 +252,89 @@ let lookup_index_as_renamed env sigma t n =
   in lookup n 1 t
 
 (**********************************************************************)
+(* Factorization of match patterns *)
+
+let print_factorize_match_patterns = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "factorization of \"match\" patterns in printing";
+      optkey   = ["Printing";"Factorizable";"Match";"Patterns"];
+      optread  = (fun () -> !print_factorize_match_patterns);
+      optwrite = (fun b -> print_factorize_match_patterns := b) }
+
+let print_allow_match_default_clause = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "possible use of \"match\" default pattern in printing";
+      optkey   = ["Printing";"Allow";"Match";"Default";"Clause"];
+      optread  = (fun () -> !print_allow_match_default_clause);
+      optwrite = (fun b -> print_allow_match_default_clause := b) }
+
+let rec join_eqns (ids,rhs as x) patll = function
+  | (loc,(ids',patl',rhs') as eqn')::rest ->
+     if not !Flags.raw_print && !print_factorize_match_patterns &&
+        List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs'
+     then
+       join_eqns x (patl'::patll) rest
+     else
+       let eqn,rest = join_eqns x patll rest in
+       eqn, eqn'::rest
+  | [] ->
+     patll, []
+
+let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll
+
+let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = []
+
+let rec move_more_factorized_default_candidate_to_end eqn n = function
+  | eqn' :: eqns ->
+     let set,get = set_temporary_memory () in
+     if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then
+       let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in
+       if isbest then false, dft, eqns else false, dft, eqn' :: eqns
+     else
+       let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in
+       isbest, dft, eqn' :: eqns
+  | [] -> true, Some eqn, []
+
+let rec select_default_clause = function
+  | eqn :: eqns ->
+     let set,get = set_temporary_memory () in
+     if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then
+       let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in
+       if isbest then dft, eqns else dft, eqn :: eqns
+     else
+       let dft, eqns = select_default_clause eqns in dft, eqn :: eqns
+  | [] -> None, []
+
+let factorize_eqns eqns =
+  let rec aux found = function
+  | (loc,(ids,patl,rhs))::rest ->
+     let patll,rest = join_eqns (ids,rhs) [patl] rest in
+     aux ((loc,(ids,patll,rhs))::found) rest
+  | [] ->
+     found in
+  let eqns = aux [] (List.rev eqns) in
+  let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in
+  if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then
+    match select_default_clause eqns with
+    (* At least two clauses and the last one is disjunctive with no variables *)
+    | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)]
+    (* Only one clause which is disjunctive with no variables: we keep at least one constructor *)
+    (* so that it is not interpreted as a dummy "match" *)
+    | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)]
+    | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false
+    | None, eqns -> eqns
+  else
+    eqns
+
+(**********************************************************************)
 (* Fragile algorithm to reverse pattern-matching compilation          *)
 
 let update_name sigma na ((_,(e,_)),c) =
@@ -284,13 +367,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
 let rec build_tree na isgoal e sigma ci cl =
   let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
   let cnl = ci.ci_pp_info.cstr_tags in
-  let cna = ci.ci_cstr_nargs in
   List.flatten
     (List.init (Array.length cl)
-      (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i))))
+      (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i))))
 
 and align_tree nal isgoal (e,c as rhs) sigma = match nal with
-  | [] -> [[],rhs]
+  | [] -> [Id.Set.empty,[],rhs]
   | na::nal ->
     match EConstr.kind sigma c with
     | Case (ci,p,c,cl) when
@@ -300,19 +382,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 	computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e sigma ci cl in
 	List.flatten
-          (List.map (fun (pat,rhs) ->
+          (List.map (fun (ids,pat,rhs) ->
 	      let lines = align_tree nal isgoal rhs sigma in
-	      List.map (fun (hd,rest) -> pat::hd,rest) lines)
+              List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines)
 	    clauses)
     | _ ->
-	let pat = DAst.make @@ PatVar(update_name sigma na rhs) in
-	let mat = align_tree nal isgoal rhs sigma in
-	List.map (fun (hd,rest) -> pat::hd,rest) mat
+        let na = update_name sigma na rhs in
+        let pat = DAst.make @@ PatVar na in
+        let mat = align_tree nal isgoal rhs sigma in
+        List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat
 
-and contract_branch isgoal e sigma (cdn,can,mkpat,b) =
-  let nal,rhs = decomp_branch cdn [] isgoal e sigma b in
+and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
+  let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in
   let mat = align_tree nal isgoal rhs sigma in
-  List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
+  List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat
 
 (**********************************************************************)
 (* Transform internal representation of pattern-matching into list of *)
@@ -648,7 +731,7 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
     let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
-    List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c))
+    List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
     Array.to_list
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cb1c0d8d4b..f150cb1956 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -26,10 +26,20 @@ val print_universes : bool ref
 (** If true, prints full local context of evars *)
 val print_evar_arguments : bool ref
 
+(** If true, contract branches with same r.h.s. and same matching
+    variables in a disjunctive pattern *)
+val print_factorize_match_patterns : bool ref
+
+(** If true and the last non unique clause of a "match" is a
+    variable-free disjunctive pattern, turn it into a catch-call case *)
+val print_allow_match_default_clause : bool ref
+
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
 val subst_glob_constr : substitution -> glob_constr -> glob_constr
 
+val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g
+
 (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr 
    de Bruijn indexes are turned to bound names, avoiding names in [avoid] 
    [isgoal] tells if naming must avoid global-level synonyms as intro does