In printing, factorizing "match" clauses with same right-hand side.

Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.

Adding options

  Unset Printing Allow Default Clause.

to deactivate the second behavior, and

  Unset Printing Factorizable Match Patterns.

to deactivate the first behavior (deactivating the first one
deactivates also the second one).

E.g. printing

  match x with Eq => 1 | _ => 0 end

gives

  match x with
  | Eq => 1
  | _ => 0
  end

or (with default clause deactivates):

  match x with
  | Eq => 1
  | Lt | Gt => 0
  end

More to be done, e.g. reconstructing multiple patterns in Nat.eqb...

2 files changed, 103 insertions, 9 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6527ba9355..5906d58789 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) =
@@ -290,7 +373,7 @@ let rec build_tree na isgoal e sigma ci cl =
       (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(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 +383,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 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 (hd,rest) -> pat::hd,rest) mat
+        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,can,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 +732,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