Last changes in type class syntax:

- curly braces mandatory for record class instances
- no mention of the unique method for definitional class instances
Turning a record or definition into a class is mostly a 
matter of changing the keywords to 'Class' and 'Instance' now.
Documentation reflects these changes, and was checked once more 
along with setoid_rewrite's and Program's.


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

4 files changed, 54 insertions, 49 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index ecfe48e60..9bcca8589 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -2,7 +2,7 @@
 \def\eol{\setlength\parskip{0pt}\par}
 \def\indent#1{\noindent\kern#1}
 \def\cst#1{\textsf{#1}}
-\def\tele#1{\overrightarrow{#1}}
+\def\tele#1{\ensuremath{\overrightarrow{#1}}}
 
 \achapter{\protect{Type Classes}}
 \aauthor{Matthieu Sozeau}
@@ -20,15 +20,15 @@ classes in \Haskell which also applies.
 \asection{Class and Instance declarations}
 \label{ClassesInstances}
 
-The syntax for class and instance declarations is a mix between the
-record syntax of \Coq~and the type classes syntax of \Haskell:
+The syntax for class and instance declarations is the same as
+record syntax of \Coq:
 \def\kw{\texttt}
 \def\classid{\texttt}
 
 \begin{center}
 \[\begin{array}{l}
-\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n)
-:= \{\\
+\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n) 
+[: \sort] := \{\\
 \begin{array}{p{0em}lcl}
   & \cst{f}_1 & : & \type_1 ; \\
   & \vdots & &  \\
@@ -37,11 +37,11 @@ record syntax of \Coq~and the type classes syntax of \Haskell:
 \end{center}
 \begin{center}
 \[\begin{array}{l}
-\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n :=\\
+\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n := \{\\
 \begin{array}{p{0em}lcl}
   & \cst{f}_1 & := & \term_{f_1} ; \\
   & \vdots & &  \\
-  & \cst{f}_m & := & \term_{f_m}.
+  & \cst{f}_m & := & \term_{f_m} \}.
 \end{array}\end{array}\]
 \end{center}
 \begin{coq_eval}
@@ -67,9 +67,9 @@ leibniz equality on some type. An example implementation is:
 
 \begin{coq_example*}
 Instance unit_EqDec : EqDec unit :=
-  eqb x y := true ;
+{ eqb x y := true ;
   eqb_leibniz x y H := 
-    match x, y return x = y with tt, tt => refl_equal tt end.
+    match x, y return x = y with tt, tt => refl_equal tt end }.
 \end{coq_example*}
 
 If one does not give all the members in the \texttt{Instance}
@@ -78,9 +78,8 @@ inhabitants of the remaining fields, e.g.:
 
 \begin{coq_example*}
 Instance eq_bool : EqDec bool :=
-  eqb x y := if x then y else negb y.
+{ eqb x y := if x then y else negb y }.
 \end{coq_example*}
-
 \begin{coq_example}
 Proof. intros x y H.
   destruct x ; destruct y ; (discriminate || reflexivity). 
@@ -96,7 +95,7 @@ richer facilities for dealing with obligations.
 
 Once a type class is declared, one can use it in class binders:
 \begin{coq_example}
-  Definition neqb {A : Type} {eqa : EqDec A} (x y : A) := negb (eqb x y).
+Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 When one calls a class method, a constraint is generated that is
@@ -106,7 +105,7 @@ satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
 found, an error is raised:
 
 \begin{coq_example}
-  Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
+Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 The algorithm used to solve constraints is a variant of the eauto tactic
@@ -116,7 +115,7 @@ local hypotheses as well as declared lemmas in the
 written:
 
 \begin{coq_example}
-  Definition neqb' (A : Type) (eqa : EqDec A) (x y : A) := negb (eqb x y).
+Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 However, the generalizing binders should be used instead as they have
@@ -142,7 +141,7 @@ binders begining with a backquote \texttt{`} and the codomain of
 
 Following the previous example, one can write:
 \begin{coq_example}
-  Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
+Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 Here \texttt{A} is implicitely generalized, and the resulting function
@@ -164,9 +163,9 @@ the constraints as a binding context before the instance, e.g.:
 
 \begin{coq_example}
 Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
-  eqb x y := match x, y with
+{ eqb x y := match x, y with
   | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
-  end.
+  end }.
 \end{coq_example}
 \begin{coq_eval}
 Admitted.
@@ -182,10 +181,10 @@ One can also parameterize classes by other classes, generating a
 hierarchy of classes and superclasses. In the same way, we give the
 superclasses as a binding context:
 
-\begin{coq_example}
+\begin{coq_example*}
 Class Ord `(E : EqDec A) :=
   { le : A -> A -> bool }.
-\end{coq_example}
+\end{coq_example*}
 
 Contrary to \Haskell, we have no special syntax for superclasses, but
 this declaration is morally equivalent to:
@@ -202,20 +201,18 @@ As we have seen, \texttt{Ord} is encoded as a record type with two parameters:
 a type \texttt{A} and an \texttt{E} of type \texttt{EqDec A}. However, one can
 still use it as if it had a single parameter inside generalizing binders: the
 generalization of superclasses will be done automatically. 
-\begin{coq_example}
-Definition le_eqb `{Ord A} (x y : A) :=
-  andb (le x y) (le y x).
-\end{coq_example}
+\begin{coq_example*}
+Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
+\end{coq_example*}
 
 In some cases, to be able to specify sharing of structures, one may want to give
 explicitely the superclasses. It is is possible to do it directly in regular
 binders, and using the \texttt{!} modifier in class binders. For
 example:
-
-\begin{coq_example}
-Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) :=
+\begin{coq_example*}
+Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := 
   andb (le x y) (neqb x y).
-\end{coq_example}
+\end{coq_example*}
 
 The \texttt{!} modifier switches the way a binder is parsed back to the
 regular interpretation of Coq. In particular, it uses the implicit
@@ -237,7 +234,8 @@ Class Transitive (A : Type) (R : relation A) :=
   transitivity : forall x y z, R x y -> R y z -> R x z.
 \end{coq_example*}
 
-This declares singleton classes for reflexive and transitive relations. 
+This declares singleton classes for reflexive and transitive relations,
+(see \ref{SingletonClass} for an explanation).
 These may be used as part of other classes:
 
 \begin{coq_example*}
@@ -259,7 +257,7 @@ same effect.
 \section{Summary of the commands
 \label{TypeClassCommands}}
 
-\subsection{\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} 
+\subsection{\tt Class {\ident} {\binder$_1$ \ldots~\binder$_n$} 
   : \sort := \{ field$_1$ ; \ldots ; field$_k$ \}.}
 \comindex{Class}
 \label{Class}
@@ -269,7 +267,7 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
 {\tt field$_k$}.
 
 \begin{Variants}
-\item {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} 
+\item \label{SingletonClass} {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} 
     : \sort := \ident$_1$ : \type$_1$.}
   This variant declares a \emph{singleton} class whose only method is
   {\tt \ident$_1$}. This singleton class is a so-called definitional
@@ -286,7 +284,7 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
 
 \subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
   {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}]
-  := field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$}
+  := \{ field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$ \}}
 \comindex{Instance}
 \label{Instance}
 
@@ -302,6 +300,12 @@ An optional \textit{priority} can be declared, 0 being the highest
 priority as for auto hints.
 
 \begin{Variants}
+\item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
+    {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term} 
+  This syntax is used for declaration of singleton class instances. 
+  It does not include curly braces and one need not even mention
+  the unique field name.
+
 \item {\tt Instance Global} One can use the \texttt{Global} modifier on
   instances declared in a section so that their generalization is automatically
   redeclared after the section is closed.
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index dfcebf186..20444dc0a 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -137,18 +137,18 @@ Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
 \end{coq_example}
 
 Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are
-automatically generated by the pattern-matching compilation algorithm):
+automatically generated by the pattern-matching compilation algorithm).
 \begin{coq_example}
-  Obligations.
+  Obligation 1.
 \end{coq_example}
 
-You can use a well-founded order or a measure as termination orders using the syntax:
+One can use a well-founded order or a measure as termination orders using the syntax:
 \begin{coq_eval}
 Reset Initial.
 Require Import Arith.
 Require Import Program.
 \end{coq_eval}
-\begin{coq_example}
+\begin{coq_example*}
 Definition id (n : nat) := n.
 Program Fixpoint div2 (n : nat) {measure id n} :
   { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
@@ -156,7 +156,7 @@ Program Fixpoint div2 (n : nat) {measure id n} :
   | S (S p) => S (div2 p)
   | _ => O
   end.
-\end{coq_example}
+\end{coq_example*}
 
 The \verb|measure| keyword expects a measure function into the naturals, whereas
 \verb|wf| expects a relation.
@@ -270,4 +270,5 @@ Program Fixpoint f (x : A | P) { measure size } :=
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
+%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
 %%% End: 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 502b42b83..8b404f4ef 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -24,7 +24,7 @@ construction allows to define ``signatures''.
 && ~~~~\zeroone{\ident}
        \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
   & & \\
-{\field} & ::= & {\name} : {\type} \\
+{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\
  & $|$ & {\name} {\typecstr} := {\term}
 \end{tabular}
 \end{centerframe}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index c2d20b490..6a80be633 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -482,8 +482,7 @@ can be registered as parametric relations and morphisms.
 \begin{cscexample}[First class setoids]
 
 \begin{coq_example*}
-Require Export Relation_Definitions.
-Require Import Setoid.
+Require Import Relation_Definitions Setoid.
 Record Setoid: Type :=
 { car:Type;
   eq:car->car->Prop;
@@ -494,8 +493,7 @@ Record Setoid: Type :=
 Add Parametric Relation (s : Setoid) : (@car s) (@eq s)
  reflexivity proved by (refl s)
  symmetry proved by (sym s)
- transitivity proved by (trans s)
-as eq_rel.
+ transitivity proved by (trans s) as eq_rel.
 Record Morphism (S1 S2:Setoid): Type :=
 { f:car S1 ->car S2;
   compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }.
@@ -636,13 +634,15 @@ Admitted.
 One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
 declared such a morphism, it will be used by the setoid rewriting tactic
-each time we try to rewrite under a binder. Indeed, when rewriting under
-a lambda, binding variable $x$, say from $P~x$ to $Q~x$ using the
-relation \texttt{iff}, the tactic will generate a proof of
-\texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q x)}
-from the proof of \texttt{iff (P x) (Q x)} and a
-constraint of the form \texttt{Morphism (pointwise\_relation A iff ==> ?) m}
-will be generated for the surrounding morphism \texttt{m}. 
+each time we try to rewrite under an \texttt{all} application (products
+in \Prop{} are implicitely translated to such applications).
+
+Indeed, when rewriting under a lambda, binding variable $x$, say from
+$P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate
+a proof of \texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q
+x)} from the proof of \texttt{iff (P x) (Q x)} and a constraint of the
+form \texttt{Morphism (pointwise\_relation A iff ==> ?) m} will be
+generated for the surrounding morphism \texttt{m}.
 
 Hence, one can add higher-order combinators as morphisms by providing
 signatures using pointwise extension for the relations on the functional
@@ -694,7 +694,7 @@ any rewriting constraints arising from a rewrite using \texttt{iff},
 \texttt{impl} or \texttt{inverse impl} through \texttt{and}.
 
 Sub-relations are implemented in \texttt{Classes.Morphisms} and are a 
-prime example of a completely user-space extension of the algorithm.
+prime example of a mostly user-space extension of the algorithm.
 
 \asection{Constant unfolding}