diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Classes.tex | 52 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 3 | ||||
| -rw-r--r-- | doc/refman/biblio.bib | 8 | ||||
| -rwxr-xr-x | doc/stdlib/Library.tex | 4 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-files | 2 |
5 files changed, 67 insertions, 2 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}, diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 87b72a5c29..9260e7e189 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 aed8536555..add14a13b8 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 |