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...

11 files changed, 227 insertions, 17 deletions

diff --git a/API/API.mli b/API/API.mli
index 99ba3eea47..089cf8b15e 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4339,6 +4339,7 @@ sig
   | Later : [ `thunk ] delay
   val print_universes : bool ref
   val print_evar_arguments : bool ref
+  val print_allow_match_default_clause : bool ref
   val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g
   val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr
   val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit
diff --git a/CHANGES b/CHANGES
index b2b9da8ced..2b057f3632 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,16 @@ Notations
   opened rather than to the latest notations defined independently of
   whether they are in an opened scope or not.
 
+Specification language
+
+- When printing clauses of a "match", clauses with same right-hand
+  side are factorized and the last most factorized clause with no
+  variables, if it exists, is turned into a default clause.
+  Use "Unset Printing Allow Default Clause" do deactivate printing
+  of a default clause.
+  Use "Unset Printing Factorizable Match Patterns" to deactivate
+  factorization of clauses with same right-hand side.
+
 Tactics
 
 - On Linux, "native_compute" calls can be profiled using the "perf"
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6704ed4b7b..1330b3741e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -852,7 +852,7 @@ let rec extern inctx scopes vars r =
                              ) x))
                 tml
     in
-    let eqns = List.map (extern_eqn inctx scopes vars) eqns in
+    let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in
     CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (nal,(na,typopt),tm,b) ->
@@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) = extern_local_binder scopes vars l in
       (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
 
-and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
-  Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl],
-   extern inctx scopes vars c)
+and extern_eqn inctx scopes vars (loc,(ids,pll,c)) =
+  let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
+  Loc.tag ?loc (pll,extern inctx scopes vars c)
 
 and extern_notation (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 72c91db6a0..f311d33b8a 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -93,6 +93,14 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g
 
 type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
 
+type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located
+type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list
+type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list
+
+type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g
+type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g
+type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g
+
 type 'a extended_glob_local_binder_r =
   | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
   | GLocalDef     of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8bf6e48fdb..5a9248d478 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -183,7 +183,9 @@ let with_full_print f a =
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in
   let old_printuniverses = !Constrextern.print_universes in
+  let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
   Constrextern.print_universes := true;
+  Detyping.print_allow_match_default_clause := false;
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
@@ -197,6 +199,7 @@ let with_full_print f a =
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
     Constrextern.print_universes := old_printuniverses;
+    Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
     Dumpglob.continue ();
     res
   with
@@ -206,6 +209,7 @@ let with_full_print f a =
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
 	Constrextern.print_universes := old_printuniverses;
+        Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
 	Dumpglob.continue ();
 	raise reraise
 
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 
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 97fa8e2542..419dcadb4c 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -95,8 +95,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
   
   x : nat
   n, n0 := match x + 0 with
-           | 0 => 0
-           | S _ => 0
+           | 0 | S _ => 0
            end : nat
   e,
   e0 := match x + 0 as y return (y = y) with
@@ -104,8 +103,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
         | S n => eq_refl
         end : x + 0 = x + 0
   n1, n2 := match x with
-            | 0 => 0
-            | S _ => 0
+            | 0 | S _ => 0
             end : nat
   e1, e2 := match x return (x = x) with
             | 0 => eq_refl
@@ -126,3 +124,48 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
         end : p = p /\ p = p
   ============================
   eq_refl = eq_refl
+fun x : comparison => match x with
+                      | Eq => 1
+                      | _ => 0
+                      end
+     : comparison -> nat
+fun x : comparison => match x with
+                      | Eq => 1
+                      | Lt => 0
+                      | Gt => 0
+                      end
+     : comparison -> nat
+fun x : comparison => match x with
+                      | Eq => 1
+                      | Lt | Gt => 0
+                      end
+     : comparison -> nat
+fun x : comparison =>
+match x return nat with
+| Eq => S O
+| Lt => O
+| Gt => O
+end
+     : forall _ : comparison, nat
+fun x : K => match x with
+             | a3 | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a2 => 4
+             | a3 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a2 => 4
+             | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a3 | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 17fee3303d..caf3b28701 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -1,5 +1,7 @@
 (* Cases with let-in in constructors types *)
 
+Unset Printing Allow Match Default Clause.
+
 Inductive t : Set :=
     k : let x := t in x -> x.
 
@@ -184,3 +186,33 @@ let p := fresh "p" in
   |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
   end.
 Show.
+
+Set Printing Allow Match Default Clause.
+
+(***************************************************)
+(* Testing strategy for factorizing cases branches *)
+
+(* Factorization + default clause *)
+Check fun x => match x with Eq => 1 | _ => 0 end.
+
+(* No factorization *)
+Unset Printing Factorizable Match Patterns.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Set Printing Factorizable Match Patterns.
+
+(* Factorization but no default clause *)
+Unset Printing Allow Match Default Clause.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Set Printing Allow Match Default Clause.
+
+(* No factorization in printing all mode *)
+Set Printing All.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Unset Printing All.
+
+(* Several clauses *)
+Inductive K := a1|a2|a3|a4|a5|a6.
+Check fun x => match x with a3 | a4 => 3 | _ => 2 end.
+Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end.
+Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end.
+Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index a1028bda0c..121a369a94 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -37,6 +37,17 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
 Notation plus2 n := (S(S(n)))
+λ n : list(nat), match n with
+                 | 1 :: nil => 0
+                 | _ => 2
+                 end
+     : list(nat) -> nat
+λ n : list(nat),
+match n with
+| 1 :: nil => 0
+| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2
+end
+     : list(nat) -> nat
 λ n : list(nat),
 match n with
 | nil => 2
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4c3eaa0c7b..531398bb0b 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -79,6 +79,13 @@ Notation plus2 n := (S (S n)).
 (* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
 Print plus2.
 Check fun n => match n with list1 => 0 | _ => 2 end.
+Unset Printing Allow Match Default Clause.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+Unset Printing Factorizable Match Patterns.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+Set Printing Allow Match Default Clause.
+Set Printing Factorizable Match Patterns.
+
 End A.
 
 (* This one is not fully satisfactory because binders in the same type