Documentation or-pattern

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

3 files changed, 119 insertions, 36 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index a05231cd1..dfe9e94c2 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -1,5 +1,5 @@
 \achapter{Extended pattern-matching}\defaultheaders
-\aauthor{Cristina Cornes}
+\aauthor{Cristina Cornes and Hugo Herbelin}
 
 \label{Mult-match-full}
 \ttindex{Cases}
@@ -17,32 +17,38 @@ pattern. It is recommended to start variable names by a lowercase
 letter.
 
 If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor
-symbol and $\vec{x}$ is a linear vector of variables, it is called
-{\em simple}: it is the kind of pattern recognized by the basic
-version of {\tt match}. If a pattern is
-not simple we call it {\em nested}.
+symbol and $\vec{x}$ is a linear vector of (distinct) variables, it is
+called {\em simple}: it is the kind of pattern recognized by the basic
+version of {\tt match}. On the opposite, if it is a variable $x$ or
+has the form $(c~\vec{p})$ with $p$ not only made of variables, the
+pattern is called {\em nested}.
 
 A variable pattern matches any value, and the identifier is bound to
 that value. The pattern ``\texttt{\_}'' (called ``don't care'' or
-``wildcard'' symbol) also matches any value, but does not bind anything. It
-may occur an arbitrary number of times in a pattern. Alias patterns
-written \texttt{(}{\sl pattern} \texttt{as} {\sl identifier}\texttt{)} are
-also accepted. This pattern matches the same values as {\sl pattern}
-does and {\sl identifier} is bound to the matched value.  A list of
-patterns separated with commas 
-is also considered as a pattern and is called {\em multiple
-pattern}.
+``wildcard'' symbol) also matches any value, but does not bind
+anything. It may occur an arbitrary number of times in a
+pattern. Alias patterns written \texttt{(}{\sl pattern} \texttt{as}
+{\sl identifier}\texttt{)} are also accepted. This pattern matches the
+same values as {\sl pattern} does and {\sl identifier} is bound to the
+matched value.  
+A pattern of the form {\pattern}{\tt |}{\pattern} is called
+disjunctive. A list of patterns separated with commas is also
+considered as a pattern and is called {\em multiple pattern}. However
+multiple patterns can only occur at the root of pattern-matching
+equations. Disjunctions of {\em multiple pattern} are allowed though.
 
 Since extended {\tt match} expressions are compiled into the primitive
 ones, the expressiveness of the theory remains the same. Once the
-stage of parsing has finished only simple patterns remain. An easy way
-to see the result of the expansion is by printing the term with
-\texttt{Print} if the term is a constant, or using the command
+stage of parsing has finished only simple patterns remain.  Re-nesting
+of pattern is performed at printing time. An easy way to see the
+result of the expansion is to toggle off the nesting performed at
+printing (use here {\tt Set Printing Matching}), then by printing the term
+with \texttt{Print} if the term is a constant, or using the command
 \texttt{Check}.
 
 The extended \texttt{match} still accepts an optional {\em elimination
 predicate} given after the keyword \texttt{return}.  Given a pattern
-matching expression, if all the right hand sides of \texttt{=>} ({\em
+matching expression, if all the right-hand-sides of \texttt{=>} ({\em
 rhs} in short) have the same type, then this type can be sometimes
 synthesized, and so we can omit the \texttt{return} part. Otherwise 
 the predicate after \texttt{return} has to be provided, like for the basic
@@ -64,7 +70,9 @@ Fixpoint max (n m:nat) {struct m} : nat :=
   end.
 \end{coq_example}
 
-Using multiple patterns in the definition allows to write:
+\paragraph{Multiple patterns}
+
+Using multiple patterns in the definition of {\tt max} allows to write:
 
 \begin{coq_example}
 Reset max.
@@ -89,7 +97,9 @@ Check (fun x:nat => match x return nat with
                     end).
 \end{coq_example}
 
-We can also use ``\texttt{as} patterns'' to associate a name to a
+\paragraph{Aliasing subpatterns}
+
+We can also use ``\texttt{as} {\ident}'' to associate a name to a
 sub-pattern:
 
 \begin{coq_example}
@@ -102,6 +112,8 @@ Fixpoint max (n m:nat) {struct n} : nat :=
   end.
 \end{coq_example}
 
+\paragraph{Nested patterns}
+
 Here is now an example of nested patterns:
 
 \begin{coq_example}
@@ -157,7 +169,6 @@ Fixpoint lef (n m:nat) {struct m} : bool :=
   end.
 \end{coq_example}
 
-
 Here the last pattern superposes with the first two. Because
 of the priority rule, the last pattern 
 will be used only for values that do not match neither the  first nor
@@ -180,12 +191,50 @@ Check (fun x:nat =>
          end).
 \end{coq_example}
 
+\paragraph{Disjunctive patterns}
+
+Multiple patterns that share the same right-hand-side can be
+factorized using the notation \nelist{\multpattern}{\tt |}. For instance,
+{\tt max} can be rewritten as follows:
+
+\begin{coq_eval}
+Reset max.
+\end{coq_eval}
+\begin{coq_example}
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n, m with
+  | S n', S m' => S (max n' m')
+  | 0, p | p, 0 => p
+  end.
+\end{coq_example}
+
+Similarly, factorization of (non necessary multiple) patterns
+that share the same variables is possible by using the notation
+\nelist{\pattern}{\tt |}. Here is an example:
+
+\begin{coq_example}
+Definition filter_2_4 (n:nat) : nat :=
+  match n with
+  | 2 as m | 4 as m => m
+  | _ => 0
+  end.
+\end{coq_example}
+
+Here is another example using disjunctive subpatterns.
+
+\begin{coq_example}
+Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
+  match p with
+  | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
+  | _ => (0,0)
+  end.
+\end{coq_example}
+
 \asection{About patterns of parametric types}
 When matching objects of a parametric type, constructors in patterns
 {\em do not expect} the parameter arguments. Their value is deduced
 during expansion.
-
-Consider for example the polymorphic lists:
+Consider for example the type of polymorphic lists:
 
 \begin{coq_example}
 Inductive List (A:Set) : Set :=
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 503d7571d..73fb391dd 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -223,13 +223,14 @@ To deactivate the printing of projections, use
 \label{Mult-match}}
 
 The basic version of \verb+match+ allows pattern-matching on simple
-patterns. As an extension, multiple and nested patterns are
-allowed, as in ML-like languages.
+patterns. As an extension, multiple nested patterns or disjunction of
+patterns are allowed, as in ML-like languages.
 
 The extension just acts as a macro that is expanded during parsing
 into a sequence of {\tt match} on simple patterns. Especially, a
-construction defined using the extended {\tt match} is printed under
-its expanded form.
+construction defined using the extended {\tt match} is generally
+printed under its expanded form (see~\texttt{Set Printing Matching} in
+section~\ref{SetPrintingMatching}).
 
 \SeeAlso chapter \ref{Mult-match-full}.
 
@@ -330,11 +331,40 @@ The general equivalence for an inductive type with one constructors {\tt C} is
 $\equiv$~
 {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
 
-\subsection{Options for pretty-printing of {\tt match}
+\subsection{Controlling pretty-printing of {\tt match} expressions
 \label{printing-options}}
 
-There are three options controlling the pretty-printing of {\tt match}
-expressions.
+The following commands give some control over the pretty-printing of
+{\tt match} expressions.
+
+\subsubsection{Printing nested patterns
+\label{SetPrintingMatching}
+\comindex{Set Printing Matching}
+\comindex{Unset Printing Matching}
+\comindex{Test Printing Matching}}
+
+The Calculus of Inductive Constructions knows pattern-matching only
+over simple patterns. It is however convenient to re-factorize nested
+pattern-matching into a single pattern-matching over a nested pattern.
+{\Coq}'s printer try to do such limited re-factorization.
+
+\begin{quote}
+{\tt Set Printing Matching.}
+\end{quote}
+This tells {\Coq} to try to use nested patterns. This is the default
+behavior.
+
+\begin{quote}
+{\tt Unset Printing Matching.}
+\end{quote}
+This tells {\Coq} to print only simple pattern-matching problems in
+the same way as the {\Coq} kernel handles them.
+
+\begin{quote}
+{\tt Test Printing Matching.}
+\end{quote}
+This tells if the printing matching mode is on or off. The default is
+on.
 
 \subsubsection{Printing of wildcard pattern
 \comindex{Set Printing Wildcard}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index c2869fd3d..e80a53f5b 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -308,7 +308,9 @@ chapter \ref{Addoc-syntax}.
 &&\\
 {\returntype} & ::= & {\tt return} {\term} \\
 &&\\
-{\eqn} & ::= & \nelist{\pattern}{\tt ,} {\tt =>} {\term}\\
+{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\
+&&\\
+{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
 &&\\
 {\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
  & $|$ & {\pattern} {\tt as} {\ident}             \\
@@ -316,7 +318,9 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\qualid}                              \\
  & $|$ & {\tt \_}                                  \\
  & $|$ & {\num}                                 \\
- & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     
+ & $|$ & {\tt (} \nelist{\orpattern}{,} {\tt )}     \\
+\\
+{\orpattern} & ::= & \nelist{\pattern}{\tt |}\\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of terms (continued)}
@@ -515,10 +519,11 @@ The expression {\tt match} {\term$_0$} {\returntype} {\tt with}
 {\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$}
 {\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em
 pattern-matching} over the term {\term$_0$} (expected to be of an
-inductive type $I$). {\term$_1$}\ldots{\term$_n$} are called branches. In
+inductive type $I$). 
+The terms {\term$_1$}\ldots{\term$_n$} are called branches. In
 a simple pattern \qualid~\nelist{\ident}{}, the qualified identifier
 {\qualid} is intended to
-be a constructor. There should be a branch for every constructor of
+be a constructor. There should be one branch for every constructor of
 $I$.
 
 The {\returntype} is used to compute the resulting type of the whole
@@ -530,9 +535,8 @@ annotation has to be given when the resulting type of the whole {\tt
 match} depends on the actual {\term$_0$} matched.
 
 There are specific notations for case analysis on types with one or
-two constructors: {\tt if / then / else} and
-{\tt let (}\ldots{\tt ) :=} \ldots {\tt in}\ldots. \SeeAlso
-section~\ref{Mult-match} for details and examples.
+two constructors: {\tt if {\ldots} then {\ldots} else {\ldots}} and
+{\tt let (}\nelist{\ldots}{,}{\tt ) :=} {\ldots} {\tt in} {\ldots}.
 
 \SeeAlso Section~\ref{Mult-match} for details and examples.