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

3 files changed, 63 insertions, 0 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
new file mode 100644
index 0000000000..3a90a59f19
--- /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 c6b34f7711..61ad66a9cd 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 cce04b4e24..f49b3c7306 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},