Add almost empty Classes.tex for documentation of type classes.

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

6 files changed, 68 insertions, 3 deletions

diff --git a/Makefile.common b/Makefile.common
index bfabd8021..cc31e7553 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -75,7 +75,7 @@ REFMANCOQTEXFILES:=\
   doc/refman/RefMan-decl.v.tex \
   doc/refman/Cases.v.tex doc/refman/Coercion.v.tex doc/refman/Extraction.v.tex \
   doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Polynom.v.tex \
-  doc/refman/Setoid.v.tex doc/refman/Helm.tex # doc/refman/Natural.v.tex
+  doc/refman/Setoid.v.tex doc/refman/Helm.tex doc/refman/Classes.v.tex
 
 REFMANTEXFILES:=\
   doc/refman/headers.sty \
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
new file mode 100644
index 000000000..3a90a59f1
--- /dev/null
+++ b/doc/refman/Classes.tex
@@ -0,0 +1,52 @@
+\def\Haskell{\textsc{Haskell}\xspace}
+\def\eol{\setlength\parskip{0pt}\par}
+\def\indent#1{\noindent\kern#1}
+\def\cst#1{\textsf{#1}}
+
+\achapter{\protect{Type Classes}}
+\aauthor{Matthieu Sozeau}
+\label{typeclasses}
+
+\begin{flushleft}
+  \em The status of Type Classes is (extremelly) experimental.
+\end{flushleft}
+
+This chapter presents a quick reference of the commands related to type
+classes. It is not meant as an introduction to type classes altough it
+may become one in the future. For an actual introduction, there is a
+description of the system \cite{sozeau08} and the literature on type
+classes in \Haskell which also applies.
+
+\asection{Class and Instance declarations}
+
+The syntax for class and instance declarations is a mix between the
+record syntax of \Coq~and the type classes syntax of \Haskell:
+\def\kw{\texttt}
+\def\classid{\texttt}
+
+\begin{multicols}{2}{
+\medskip
+  \kw{Class} \classid{Id} $(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n)$ :=
+  \eol\indent{3.00em}$\cst{f}_1 : \phi_1$ ;
+  \eol\indent{4.00em}\vdots
+  \eol\indent{3.00em}$\cst{f}_m : \phi_m$.
+\medskip}
+{
+  
+  \medskip
+  \kw{Instance} \classid{Id} $t_1 \cdots t_n$ :=
+  \eol\indent{3.00em}$\cst{f}_1 := b_1$ ;
+  \eol\indent{4.00em}\vdots
+  \eol\indent{3.00em}$\cst{f}_m := b_m$.
+  \medskip}
+\end{multicols}
+
+\begin{coq_eval}
+  Reset Initial.
+\end{coq_eval}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
+%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index c6b34f771..61ad66a9c 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -17,6 +17,8 @@
 \usepackage{ifpdf}
 \usepackage[headings]{fullpage}
 \usepackage{headers} % in this directory
+\usepackage{multicol}
+\usepackage{xspace}
 
 % for coqide
 \ifpdf   % si on est pas en pdflatex
@@ -99,6 +101,7 @@ Options A and B of the licence are {\em not} elected.}
 \include{AddRefMan-pre}%
 \include{Cases.v}%
 \include{Coercion.v}%
+\include{Classes.v}%
 %%SUPPRIME \include{Natural.v}%
 \include{Omega.v}%
 %%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index cce04b4e2..f49b3c730 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1115,6 +1115,14 @@ Decomposition}},
   series =    {LNCS}
 }
 
+@inproceedings{sozeau08,
+	Author = {Matthieu Sozeau and Nicolas Oury},
+	booktitle = {TPHOLs'08},
+	Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
+	Title = {{F}irst-{C}lass {T}ype {C}lasses},
+	Year = {2008},
+}
+
 @Misc{streicher93semantical,
   author      = {T. Streicher},
   title       = {Semantical Investigations into Intensional Type Theory},
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index 87b72a5c2..9260e7e18 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -43,8 +43,10 @@ The standard library is composed of the following subdirectories:
   \item[Sorting] Sorted list (basic definitions and heapsort
                  correctness). 
   \item[Wellfounded] Well-founded relations (basic results).
-  \item[Program] Tactcis to deal with dependently-typed programs and
+  \item[Program] Tactics to deal with dependently-typed programs and
     their proofs.
+  \item[Classes] Standard type class instances on relations and
+    Coq part of the setoid rewriting tactic.
 \end{description}
 
 
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index aed853655..add14a13b 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -10,7 +10,7 @@
 # En supposant que make fait son boulot, ca fait un tri topologique du
 # graphe des dépendances
 
-LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program"
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes"
 
 rm -f library.files.ls.tmp
 (cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp