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

4 files changed, 97 insertions, 4 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 97fa8e254..419dcadb4 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 17fee3303..caf3b2870 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 a1028bda0..121a369a9 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 4c3eaa0c7..531398bb0 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