diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-14 23:58:02 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-14 23:58:02 +0100 |
| commit | 52255610a976cae6e93206125c4bb55dc157a96d (patch) | |
| tree | 764697e44c527bf60a72294a6a59ab0943a05bdf | |
| parent | 33c5d8d00cb017c61141ee0d6b7cb8f672a3e691 (diff) | |
| parent | 4ee02719ae211493b2922c04f259062ee230ed5c (diff) | |
Merge PR #6973: [Sphinx] migrate introduction
30 files changed, 2057 insertions, 286 deletions
diff --git a/.gitignore b/.gitignore index b857b754a..267534365 100644 --- a/.gitignore +++ b/.gitignore @@ -53,6 +53,7 @@ _build myocamlbuild_config.ml config/Makefile config/coq_config.ml +config/coq_config.py config/Info-*.plist dev/ocamldebug-coq dev/camlp5.dbg diff --git a/Makefile.doc b/Makefile.doc index a98f35a1c..587c5ccbf 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -70,7 +70,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ + RefMan-pre.tex RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex RefMan-modr.tex \ AsyncProofs.tex RefMan-ssr.tex) \ $(REFMANCOQTEXFILES) \ diff --git a/configure.ml b/configure.ml index 4726831e4..6c052b63b 100644 --- a/configure.ml +++ b/configure.ml @@ -1371,3 +1371,13 @@ let write_macos_metadata exec = let () = if arch = "Darwin" then List.iter write_macos_metadata distributed_exec + +let write_configpy f = + safe_remove f; + let o = open_out f in + let pr s = fprintf o s in + let pr_s = pr "%s = '%s'\n" in + pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure\n"; + pr_s "version" coq_version + +let _ = write_configpy "config/coq_config.py" diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex deleted file mode 100644 index f802a3595..000000000 --- a/doc/refman/RefMan-int.tex +++ /dev/null @@ -1,143 +0,0 @@ -%BEGIN LATEX -\setheaders{Introduction} -%END LATEX -\chapter*{Introduction} -%HEVEA\cutname{introduction.html} - -This document is the Reference Manual of version \coqversion{} of the \Coq\ -proof assistant. A companion volume, the \Coq\ Tutorial, is provided -for the beginners. It is advised to read the Tutorial first. -A book~\cite{CoqArt} on practical uses of the \Coq{} system was published in 2004 and is a good support for both the beginner and -the advanced user. - -%The system \Coq\ is designed to develop mathematical proofs. It can be -%used by mathematicians to develop mathematical theories and by -%computer scientists to write formal specifications, -The \Coq{} system is designed to develop mathematical proofs, and -especially to write formal specifications, programs and to verify that -programs are correct with respect to their specification. It provides -a specification language named \gallina. Terms of \gallina\ can -represent programs as well as properties of these programs and proofs -of these properties. Using the so-called \textit{Curry-Howard - isomorphism}, programs, properties and proofs are formalized in the -same language called \textit{Calculus of Inductive Constructions}, -that is a $\lambda$-calculus with a rich type system. All logical -judgments in \Coq\ are typing judgments. The very heart of the Coq -system is the type-checking algorithm that checks the correctness of -proofs, in other words that checks that a program complies to its -specification. \Coq\ also provides an interactive proof assistant to -build proofs using specific programs called \textit{tactics}. - -All services of the \Coq\ proof assistant are accessible by -interpretation of a command language called \textit{the vernacular}. - -\Coq\ has an interactive mode in which commands are interpreted as the -user types them in from the keyboard and a compiled mode where -commands are processed from a file. - -\begin{itemize} -\item The interactive mode may be used as a debugging mode in which - the user can develop his theories and proofs step by step, - backtracking if needed and so on. The interactive mode is run with - the {\tt coqtop} command from the operating system (which we shall - assume to be some variety of UNIX in the rest of this document). -\item The compiled mode acts as a proof checker taking a file - containing a whole development in order to ensure its correctness. - Moreover, \Coq's compiler provides an output file containing a - compact representation of its input. The compiled mode is run with - the {\tt coqc} command from the operating system. - -\end{itemize} -These two modes are documented in Chapter~\ref{Addoc-coqc}. - -Other modes of interaction with \Coq{} are possible: through an emacs -shell window, an emacs generic user-interface for proof assistant -({\ProofGeneral}~\cite{ProofGeneral}) or through a customized interface -(PCoq~\cite{Pcoq}). These facilities are not documented here. There -is also a \Coq{} Integrated Development Environment described in -Chapter~\ref{Addoc-coqide}. - -\section*{How to read this book} - -This is a Reference Manual, not a User Manual, so it is not made for a -continuous reading. However, it has some structure that is explained -below. - -\begin{itemize} -\item The first part describes the specification language, - Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension} - describe the concrete syntax as well as the meaning of programs, - theorems and proofs in the Calculus of Inductive - Constructions. Chapter~\ref{Theories} describes the standard library - of \Coq. Chapter~\ref{Cic} is a mathematical description of the - formalism. Chapter~\ref{chapter:Modules} describes the module system. - -\item The second part describes the proof engine. It is divided in - five chapters. Chapter~\ref{Vernacular-commands} presents all - commands (we call them \emph{vernacular commands}) that are not - directly related to interactive proving: requests to the - environment, complete or partial evaluation, loading and compiling - files. How to start and stop proofs, do multiple proofs in parallel - is explained in Chapter~\ref{Proof-handling}. In - Chapter~\ref{Tactics}, all commands that realize one or more steps - of the proof are presented: we call them \emph{tactics}. The - language to combine these tactics into complex proof strategies is - given in Chapter~\ref{TacticLanguage}. Examples of tactics are - described in Chapter~\ref{Tactics-examples}. - -%\item The third part describes how to extend the system in two ways: -% adding parsing and pretty-printing rules -% (Chapter~\ref{Addoc-syntax}) and writing new tactics -% (Chapter~\ref{TacticLanguage}). - -\item The third part describes how to extend the syntax of \Coq. It -corresponds to the Chapter~\ref{Addoc-syntax}. - -\item In the fourth part more practical tools are documented. First in - Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode) - and \texttt{coqtop} (interactive mode) with their options is - described. Then, in Chapter~\ref{Utilities}, - various utilities that come with the \Coq\ distribution are - presented. - Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated - development environment. - -\item The fifth part documents a number of advanced features, including - coercions, canonical structures, typeclasses, program extraction, and - specialized solvers and tactics. See the table of contents for a complete - list. -\end{itemize} - -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error -messages. - -\section*{List of additional documentation} - -This manual does not contain all the documentation the user may need -about \Coq{}. Various informations can be found in the following -documents: -\begin{description} - -\item[Tutorial] - A companion volume to this reference manual, the \Coq{} Tutorial, is - aimed at gently introducing new users to developing proofs in \Coq{} - without assuming prior knowledge of type theory. In a second step, the - user can read also the tutorial on recursive types (document {\tt - RecTutorial.ps}). - -\item[Installation] A text file INSTALL that comes with the sources - explains how to install \Coq{}. - -\item[The \Coq{} standard library] -A commented version of sources of the \Coq{} standard library -(including only the specifications, the proofs are removed) -is given in the additional document {\tt Library.ps}. - -\end{description} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index fc1c01cf2..1bd79d511 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -85,7 +85,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX %\defaultheaders -\include{RefMan-int}% Introduction \include{RefMan-pre}% Credits %BEGIN LATEX diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 1ae7a7cd7..9b7b826d5 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -158,11 +158,6 @@ dt > .property { color: #FFFFFF; } -/* FIXME: Specific to the RTD theme */ -a:visited { - color: #2980B9; -} - /* Pygments for Coq is confused by ‘…’ */ code span.error { background: inherit !important; diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib new file mode 100644 index 000000000..4a9bd6c1a --- /dev/null +++ b/doc/sphinx/biblio.bib @@ -0,0 +1,1397 @@ +@String{jfp = "Journal of Functional Programming"} +@String{lncs = "Lecture Notes in Computer Science"} +@String{lnai = "Lecture Notes in Artificial Intelligence"} +@String{SV = "{Sprin-ger-Verlag}"} + +@InProceedings{Aud91, + author = {Ph. Audebaud}, + booktitle = {Proceedings of the sixth Conf. on Logic in Computer Science.}, + publisher = {IEEE}, + title = {Partial {Objects} in the {Calculus of Constructions}}, + year = {1991} +} + +@PhDThesis{Aud92, + author = {Ph. Audebaud}, + school = {{Universit\'e} Bordeaux I}, + title = {Extension du Calcul des Constructions par Points fixes}, + year = {1992} +} + +@InProceedings{Audebaud92b, + author = {Ph. Audebaud}, + booktitle = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, + editor = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, + note = {Also Research Report LIP-ENS-Lyon}, + pages = {21--34}, + title = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, + year = {1992} +} + +@InProceedings{Augustsson85, + author = {L. Augustsson}, + title = {{Compiling Pattern Matching}}, + booktitle = {Conference Functional Programming and +Computer Architecture}, + year = {1985} +} + +@Article{BaCo85, + author = {J.L. Bates and R.L. Constable}, + journal = {ACM transactions on Programming Languages and Systems}, + title = {Proofs as {Programs}}, + volume = {7}, + year = {1985} +} + +@Book{Bar81, + author = {H.P. Barendregt}, + publisher = {North-Holland}, + title = {The Lambda Calculus its Syntax and Semantics}, + year = {1981} +} + +@TechReport{Bar91, + author = {H. Barendregt}, + institution = {Catholic University Nijmegen}, + note = {In Handbook of Logic in Computer Science, Vol II}, + number = {91-19}, + title = {Lambda {Calculi with Types}}, + year = {1991} +} + +@Article{BeKe92, + author = {G. Bellin and J. Ketonen}, + journal = {Theoretical Computer Science}, + pages = {115--142}, + title = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, + volume = {95}, + year = {1992} +} + +@Book{Bee85, + author = {M.J. Beeson}, + publisher = SV, + title = {Foundations of Constructive Mathematics, Metamathematical Studies}, + year = {1985} +} + +@Book{Bis67, + author = {E. Bishop}, + publisher = {McGraw-Hill}, + title = {Foundations of Constructive Analysis}, + year = {1967} +} + +@Book{BoMo79, + author = {R.S. Boyer and J.S. Moore}, + key = {BoMo79}, + publisher = {Academic Press}, + series = {ACM Monograph}, + title = {A computational logic}, + year = {1979} +} + +@MastersThesis{Bou92, + author = {S. Boutin}, + month = sep, + school = {{Universit\'e Paris 7}}, + title = {Certification d'un compilateur {ML en Coq}}, + year = {1992} +} + +@InProceedings{Bou97, + title = {Using reflection to build efficient and certified decision procedure +s}, + author = {S. Boutin}, + booktitle = {TACS'97}, + editor = {Martin Abadi and Takahashi Ito}, + publisher = SV, + series = lncs, + volume = 1281, + year = {1997} +} + +@PhDThesis{Bou97These, + author = {S. Boutin}, + title = {R\'eflexions sur les quotients}, + school = {Paris 7}, + year = 1997, + type = {th\`ese d'Universit\'e}, + month = apr +} + +@Article{Bru72, + author = {N.J. de Bruijn}, + journal = {Indag. Math.}, + title = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}}, + volume = {34}, + year = {1972} +} + + +@InCollection{Bru80, + author = {N.J. de Bruijn}, + booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, + editor = {J.P. Seldin and J.R. Hindley}, + publisher = {Academic Press}, + title = {A survey of the project {Automath}}, + year = {1980} +} + +@TechReport{COQ93, + author = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, + institution = {INRIA}, + month = may, + number = {154}, + title = {{The Coq Proof Assistant User's Guide Version 5.8}}, + year = {1993} +} + +@TechReport{COQ02, + author = {The Coq Development Team}, + institution = {INRIA}, + month = Feb, + number = {255}, + title = {{The Coq Proof Assistant Reference Manual Version 7.2}}, + year = {2002} +} + +@TechReport{CPar93, + author = {C. Parent}, + institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, + month = oct, + note = {Also in~\cite{Nijmegen93}}, + number = {93-29}, + title = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, + year = {1993} +} + +@PhDThesis{CPar95, + author = {C. Parent}, + school = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, + title = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, + year = {1995} +} + +@Book{Caml, + author = {P. Weis and X. Leroy}, + publisher = {InterEditions}, + title = {Le langage Caml}, + year = {1993} +} + +@InProceedings{ChiPotSimp03, + author = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, + title = {Mathematical Quotients and Quotient Types in Coq}, + booktitle = {TYPES}, + crossref = {DBLP:conf/types/2002}, + year = {2002} +} + +@TechReport{CoC89, + author = {Projet Formel}, + institution = {INRIA}, + number = {110}, + title = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, + year = {1989} +} + +@InProceedings{CoHu85a, + author = {Th. Coquand and G. Huet}, + address = {Linz}, + booktitle = {EUROCAL'85}, + publisher = SV, + series = LNCS, + title = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, + volume = {203}, + year = {1985} +} + +@InProceedings{CoHu85b, + author = {Th. Coquand and G. Huet}, + booktitle = {Logic Colloquium'85}, + editor = {The Paris Logic Group}, + publisher = {North-Holland}, + title = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, + year = {1987} +} + +@Article{CoHu86, + author = {Th. Coquand and G. Huet}, + journal = {Information and Computation}, + number = {2/3}, + title = {The {Calculus of Constructions}}, + volume = {76}, + year = {1988} +} + +@InProceedings{CoPa89, + author = {Th. Coquand and C. Paulin-Mohring}, + booktitle = {Proceedings of Colog'88}, + editor = {P. Martin-L\"of and G. Mints}, + publisher = SV, + series = LNCS, + title = {Inductively defined types}, + volume = {417}, + year = {1990} +} + +@Book{Con86, + author = {R.L. {Constable et al.}}, + publisher = {Prentice-Hall}, + title = {{Implementing Mathematics with the Nuprl Proof Development System}}, + year = {1986} +} + +@PhDThesis{Coq85, + author = {Th. Coquand}, + month = jan, + school = {Universit\'e Paris~7}, + title = {Une Th\'eorie des Constructions}, + year = {1985} +} + +@InProceedings{Coq86, + author = {Th. Coquand}, + address = {Cambridge, MA}, + booktitle = {Symposium on Logic in Computer Science}, + publisher = {IEEE Computer Society Press}, + title = {{An Analysis of Girard's Paradox}}, + year = {1986} +} + +@InProceedings{Coq90, + author = {Th. Coquand}, + booktitle = {Logic and Computer Science}, + editor = {P. Oddifredi}, + note = {INRIA Research Report 1088, also in~\cite{CoC89}}, + publisher = {Academic Press}, + title = {{Metamathematical Investigations of a Calculus of Constructions}}, + year = {1990} +} + +@InProceedings{Coq91, + author = {Th. Coquand}, + booktitle = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, + title = {{A New Paradox in Type Theory}}, + month = {August}, + year = {1991} +} + +@InProceedings{Coq92, + author = {Th. Coquand}, + title = {{Pattern Matching with Dependent Types}}, + year = {1992}, + booktitle = {Proceedings of the 1992 Workshop on Types for Proofs and Programs} +} + +@InProceedings{Coquand93, + author = {Th. Coquand}, + booktitle = {Types for Proofs and Programs}, + editor = {H. Barendregt and T. Nipokow}, + publisher = SV, + series = LNCS, + title = {{Infinite objects in Type Theory}}, + volume = {806}, + year = {1993}, + pages = {62-78} +} + +@inproceedings{Corbineau08types, + author = {P. Corbineau}, + title = {A Declarative Language for the Coq Proof Assistant}, + editor = {M. Miculan and I. Scagnetto and F. Honsell}, + booktitle = {TYPES '07, Cividale del Friuli, Revised Selected Papers}, + publisher = {Springer}, + series = LNCS, + volume = {4941}, + year = {2007}, + pages = {69-84}, + ee = {http://dx.doi.org/10.1007/978-3-540-68103-8_5}, +} + +@PhDThesis{Cor97, + author = {C. Cornes}, + month = nov, + school = {{Universit\'e Paris 7}}, + title = {Conception d'un langage de haut niveau de représentation de preuves}, + type = {Th\`ese de Doctorat}, + year = {1997} +} + +@MastersThesis{Cou94a, + author = {J. Courant}, + month = sep, + school = {DEA d'Informatique, ENS Lyon}, + title = {Explicitation de preuves par r\'ecurrence implicite}, + year = {1994} +} + +@book{Cur58, + author = {Haskell B. Curry and Robert Feys and William Craig}, + title = {Combinatory Logic}, + volume = 1, + publisher = "North-Holland", + year = 1958, + note = {{\S{9E}}}, +} + +@InProceedings{Del99, + author = {Delahaye, D.}, + title = {Information Retrieval in a Coq Proof Library using + Type Isomorphisms}, + booktitle = {Proceedings of TYPES '99, L\"okeberg}, + publisher = SV, + series = lncs, + year = {1999}, + url = + "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# + "{\sf TYPES99-SIsos.ps.gz}" +} + +@InProceedings{Del00, + author = {Delahaye, D.}, + title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}}, + booktitle = {Proceedings of Logic for Programming and Automated Reasoning + (LPAR), Reunion Island}, + publisher = SV, + series = LNCS, + volume = {1955}, + pages = {85--95}, + month = {November}, + year = {2000}, + url = + "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# + "{\sf LPAR2000-ltac.ps.gz}" +} + +@InProceedings{DelMay01, + author = {Delahaye, D. and Mayero, M.}, + title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}}, + booktitle = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier}, + publisher = {INRIA}, + month = {Janvier}, + year = {2001}, + url = + "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# + "{\sf JFLA2000-Field.ps.gz}" +} + +@TechReport{Dow90, + author = {G. Dowek}, + institution = {INRIA}, + number = {1283}, + title = {Naming and Scoping in a Mathematical Vernacular}, + type = {Research Report}, + year = {1990} +} + +@Article{Dow91a, + author = {G. Dowek}, + journal = {Compte-Rendus de l'Acad\'emie des Sciences}, + note = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, + number = {12}, + pages = {951--956}, + title = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, + volume = {I, 312}, + year = {1991} +} + +@InProceedings{Dow91b, + author = {G. Dowek}, + booktitle = {Proceedings of Mathematical Foundation of Computer Science}, + note = {Also INRIA Research Report}, + pages = {151--160}, + publisher = SV, + series = LNCS, + title = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, + volume = {520}, + year = {1991} +} + +@PhDThesis{Dow91c, + author = {G. Dowek}, + month = dec, + school = {Universit\'e Paris 7}, + title = {D\'emonstration automatique dans le Calcul des Constructions}, + year = {1991} +} + +@Article{Dow92a, + author = {G. Dowek}, + title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, + year = 1993, + journal = {Theoretical Computer Science}, + volume = 107, + number = 2, + pages = {349-356} +} + +@Article{Dow94a, + author = {G. Dowek}, + journal = {Annals of Pure and Applied Logic}, + volume = {69}, + pages = {135--155}, + title = {Third order matching is decidable}, + year = {1994} +} + +@InProceedings{Dow94b, + author = {G. Dowek}, + booktitle = {Proceedings of the second international conference on typed lambda calculus and applications}, + title = {Lambda-calculus, Combinators and the Comprehension Schema}, + year = {1995} +} + +@InProceedings{Dyb91, + author = {P. Dybjer}, + booktitle = {Logical Frameworks}, + editor = {G. Huet and G. Plotkin}, + pages = {59--79}, + publisher = {Cambridge University Press}, + title = {Inductive sets and families in {Martin-Löf's} + Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, + volume = {14}, + year = {1991} +} + +@Article{Dyc92, + author = {Roy Dyckhoff}, + journal = {The Journal of Symbolic Logic}, + month = sep, + number = {3}, + title = {Contraction-free sequent calculi for intuitionistic logic}, + volume = {57}, + year = {1992} +} + +@MastersThesis{Fil94, + author = {J.-C. Filli\^atre}, + month = sep, + school = {DEA d'Informatique, ENS Lyon}, + title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}}, + year = {1994} +} + +@TechReport{Filliatre95, + author = {J.-C. Filli\^atre}, + institution = {LIP-ENS-Lyon}, + title = {A decision procedure for Direct Predicate Calculus}, + type = {Research report}, + number = {96--25}, + year = {1995} +} + +@Article{Filliatre03jfp, + author = {J.-C. Filliâtre}, + title = {Verification of Non-Functional Programs + using Interpretations in Type Theory}, + journal = jfp, + volume = 13, + number = 4, + pages = {709--745}, + month = jul, + year = 2003, + note = {[English translation of \cite{Filliatre99}]}, + url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, + topics = {team, lri}, + type_publi = {irevcomlec} +} + +@PhDThesis{Filliatre99, + author = {J.-C. Filli\^atre}, + title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, + type = {Thèse de Doctorat}, + school = {Universit\'e Paris-Sud}, + year = 1999, + month = {July}, + url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} +} + +@Unpublished{Filliatre99c, + author = {J.-C. Filli\^atre}, + title = {{Formal Proof of a Program: Find}}, + month = {January}, + year = 2000, + note = {Submitted to \emph{Science of Computer Programming}}, + url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} +} + +@InProceedings{FilliatreMagaud99, + author = {J.-C. Filli\^atre and N. Magaud}, + title = {Certification of sorting algorithms in the system {\Coq}}, + booktitle = {Theorem Proving in Higher Order Logics: + Emerging Trends}, + year = 1999, + url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} +} + +@Unpublished{Fle90, + author = {E. Fleury}, + month = jul, + note = {Rapport de Stage}, + title = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, + year = {1990} +} + +@Book{Fourier, + author = {Jean-Baptiste-Joseph Fourier}, + publisher = {Gauthier-Villars}, + title = {Fourier's method to solve linear + inequations/equations systems.}, + year = {1890} +} + +@InProceedings{Gim94, + author = {E. Gim\'enez}, + booktitle = {Types'94 : Types for Proofs and Programs}, + note = {Extended version in LIP research report 95-07, ENS Lyon}, + publisher = SV, + series = LNCS, + title = {Codifying guarded definitions with recursive schemes}, + volume = {996}, + year = {1994} +} + +@PhDThesis{Gim96, + author = {E. Gim\'enez}, + title = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants}, + school = {\'Ecole Normale Sup\'erieure de Lyon}, + year = {1996} +} + +@TechReport{Gim98, + author = {E. Gim\'enez}, + title = {A Tutorial on Recursive Types in Coq}, + institution = {INRIA}, + year = 1998, + month = mar +} + +@Unpublished{GimCas05, + author = {E. Gim\'enez and P. Cast\'eran}, + title = {A Tutorial on [Co-]Inductive Types in Coq}, + institution = {INRIA}, + year = 2005, + month = jan, + note = {available at \url{http://coq.inria.fr/doc}} +} + +@InProceedings{Gimenez95b, + author = {E. Gim\'enez}, + booktitle = {Workshop on Types for Proofs and Programs}, + series = LNCS, + number = {1158}, + pages = {135-152}, + title = {An application of co-Inductive types in Coq: + verification of the Alternating Bit Protocol}, + editorS = {S. Berardi and M. Coppo}, + publisher = SV, + year = {1995} +} + +@InProceedings{Gir70, + author = {J.-Y. Girard}, + booktitle = {Proceedings of the 2nd Scandinavian Logic Symposium}, + publisher = {North-Holland}, + title = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, + year = {1970} +} + +@PhDThesis{Gir72, + author = {J.-Y. Girard}, + school = {Universit\'e Paris~7}, + title = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, + year = {1972} +} + +@Book{Gir89, + author = {J.-Y. Girard and Y. Lafont and P. Taylor}, + publisher = {Cambridge University Press}, + series = {Cambridge Tracts in Theoretical Computer Science 7}, + title = {Proofs and Types}, + year = {1989} +} + +@TechReport{Har95, + author = {John Harrison}, + title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, + institution = {SRI International Cambridge Computer Science Research Centre,}, + year = 1995, + type = {Technical Report}, + number = {CRC-053}, + abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} +} + +@MastersThesis{Hir94, + author = {D. Hirschkoff}, + month = sep, + school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, + title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, + year = {1994} +} + +@InProceedings{HofStr98, + author = {Martin Hofmann and Thomas Streicher}, + title = {The groupoid interpretation of type theory}, + booktitle = {Proceedings of the meeting Twenty-five years of constructive type theory}, + publisher = {Oxford University Press}, + year = {1998} +} + +@InCollection{How80, + author = {W.A. Howard}, + booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, + editor = {J.P. Seldin and J.R. Hindley}, + note = {Unpublished 1969 Manuscript}, + publisher = {Academic Press}, + title = {The Formulae-as-Types Notion of Constructions}, + year = {1980} +} + +@InProceedings{Hue87tapsoft, + author = {G. Huet}, + title = {Programming of Future Generation Computers}, + booktitle = {Proceedings of TAPSOFT87}, + series = LNCS, + volume = 249, + pages = {276--286}, + year = 1987, + publisher = SV +} + +@InProceedings{Hue87, + author = {G. Huet}, + booktitle = {Programming of Future Generation Computers}, + editor = {K. Fuchi and M. Nivat}, + note = {Also in \cite{Hue87tapsoft}}, + publisher = {Elsevier Science}, + title = {Induction Principles Formalized in the {Calculus of Constructions}}, + year = {1988} +} + +@InProceedings{Hue88, + author = {G. Huet}, + booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, + editor = {R. Narasimhan}, + note = {Also in~\cite{CoC89}}, + publisher = {World Scientific Publishing}, + title = {{The Constructive Engine}}, + year = {1989} +} + +@Unpublished{Hue88b, + author = {G. Huet}, + title = {Extending the Calculus of Constructions with Type:Type}, + year = 1988, + note = {Unpublished} +} + +@Book{Hue89, + editor = {G. Huet}, + publisher = {Addison-Wesley}, + series = {The UT Year of Programming Series}, + title = {Logical Foundations of Functional Programming}, + year = {1989} +} + +@InProceedings{Hue92, + author = {G. Huet}, + booktitle = {Proceedings of 12th FST/TCS Conference, New Delhi}, + pages = {229--240}, + publisher = SV, + series = LNCS, + title = {The Gallina Specification Language : A case study}, + volume = {652}, + year = {1992} +} + +@Article{Hue94, + author = {G. Huet}, + journal = {J. Functional Programming}, + pages = {371--394}, + publisher = {Cambridge University Press}, + title = {Residual theory in $\lambda$-calculus: a formal development}, + volume = {4,3}, + year = {1994} +} + +@InCollection{HuetLevy79, + author = {G. Huet and J.-J. L\'{e}vy}, + title = {Call by Need Computations in Non-Ambigous +Linear Term Rewriting Systems}, + note = {Also research report 359, INRIA, 1979}, + booktitle = {Computational Logic, Essays in Honor of +Alan Robinson}, + editor = {J.-L. Lassez and G. Plotkin}, + publisher = {The MIT press}, + year = {1991} +} + +@Article{KeWe84, + author = {J. Ketonen and R. Weyhrauch}, + journal = {Theoretical Computer Science}, + pages = {297--307}, + title = {A decidable fragment of {P}redicate {C}alculus}, + volume = {32}, + year = {1984} +} + +@Book{Kle52, + author = {S.C. Kleene}, + publisher = {North-Holland}, + series = {Bibliotheca Mathematica}, + title = {Introduction to Metamathematics}, + year = {1952} +} + +@Book{Kri90, + author = {J.-L. Krivine}, + publisher = {Masson}, + series = {Etudes et recherche en informatique}, + title = {Lambda-calcul {types et mod\`eles}}, + year = {1990} +} + +@Book{LE92, + editor = {G. Huet and G. Plotkin}, + publisher = {Cambridge University Press}, + title = {Logical Environments}, + year = {1992} +} + +@Book{LF91, + editor = {G. Huet and G. Plotkin}, + publisher = {Cambridge University Press}, + title = {Logical Frameworks}, + year = {1991} +} + +@Article{Laville91, + author = {A. Laville}, + title = {Comparison of Priority Rules in Pattern +Matching and Term Rewriting}, + journal = {Journal of Symbolic Computation}, + volume = {11}, + pages = {321--347}, + year = {1991} +} + +@InProceedings{LePa94, + author = {F. Leclerc and C. Paulin-Mohring}, + booktitle = {{Types for Proofs and Programs, Types' 93}}, + editor = {H. Barendregt and T. Nipkow}, + publisher = SV, + series = {LNCS}, + title = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, + volume = {806}, + year = {1994} +} + +@TechReport{Leroy90, + author = {X. Leroy}, + title = {The {ZINC} experiment: an economical implementation +of the {ML} language}, + institution = {INRIA}, + number = {117}, + year = {1990} +} + +@InProceedings{Let02, + author = {P. Letouzey}, + title = {A New Extraction for Coq}, + booktitle = {TYPES}, + year = 2002, + crossref = {DBLP:conf/types/2002}, + url = {draft at \url{http://www.irif.fr/~letouzey/download/extraction2002.pdf}} +} + +@PhDThesis{Luo90, + author = {Z. Luo}, + title = {An Extended Calculus of Constructions}, + school = {University of Edinburgh}, + year = {1990} +} + +@inproceedings{Luttik97specificationof, + Author = {Sebastiaan P. Luttik and Eelco Visser}, + Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, + Publisher = {Springer-Verlag}, + Title = {Specification of Rewriting Strategies}, + Year = {1997}} + +@Book{MaL84, + author = {{P. Martin-L\"of}}, + publisher = {Bibliopolis}, + series = {Studies in Proof Theory}, + title = {Intuitionistic Type Theory}, + year = {1984} +} + +@Article{MaSi94, + author = {P. Manoury and M. Simonot}, + title = {Automatizing Termination Proofs of Recursively Defined Functions.}, + journal = {TCS}, + volume = {135}, + number = {2}, + year = {1994}, + pages = {319-343}, +} + +@InProceedings{Miquel00, + author = {A. Miquel}, + title = {A Model for Impredicative Type Systems with Universes, +Intersection Types and Subtyping}, + booktitle = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}}, + publisher = {IEEE Computer Society Press}, + year = {2000} +} + +@PhDThesis{Miquel01a, + author = {A. Miquel}, + title = {Le Calcul des Constructions implicite: syntaxe et s\'emantique}, + month = {dec}, + school = {{Universit\'e Paris 7}}, + year = {2001} +} + +@InProceedings{Miquel01b, + author = {A. Miquel}, + title = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping}, + booktitle = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}}, + publisher = SV, + series = {LNCS}, + number = 2044, + year = {2001} +} + +@InProceedings{MiWer02, + author = {A. Miquel and B. Werner}, + title = {The Not So Simple Proof-Irrelevant Model of CC}, + booktitle = {TYPES}, + year = {2002}, + pages = {240-258}, + ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm}, + crossref = {DBLP:conf/types/2002}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@proceedings{DBLP:conf/types/2002, + editor = {H. Geuvers and F. Wiedijk}, + title = {Types for Proofs and Programs, Second International Workshop, + TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, + Selected Papers}, + booktitle = {TYPES}, + publisher = SV, + series = LNCS, + volume = {2646}, + year = {2003}, + isbn = {3-540-14031-X}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@InProceedings{Moh89a, + author = {C. Paulin-Mohring}, + address = {Austin}, + booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, + month = jan, + publisher = {ACM}, + title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, + year = {1989} +} + +@PhDThesis{Moh89b, + author = {C. Paulin-Mohring}, + month = jan, + school = {{Universit\'e Paris 7}}, + title = {Extraction de programmes dans le {Calcul des Constructions}}, + year = {1989} +} + +@InProceedings{Moh93, + author = {C. Paulin-Mohring}, + booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications}, + editor = {M. Bezem and J.-F. Groote}, + note = {Also LIP research report 92-49, ENS Lyon}, + number = {664}, + publisher = SV, + series = {LNCS}, + title = {{Inductive Definitions in the System Coq - Rules and Properties}}, + year = {1993} +} + +@Book{Moh97, + author = {C. Paulin-Mohring}, + month = jan, + publisher = {{ENS Lyon}}, + title = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, + year = {1997} +} + +@MastersThesis{Mun94, + author = {C. Muñoz}, + month = sep, + school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, + title = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, + year = {1994} +} + +@PhDThesis{Mun97d, + author = {C. Mu{\~{n}}oz}, + title = {Un calcul de substitutions pour la repr\'esentation + de preuves partielles en th\'eorie de types}, + school = {Universit\'e Paris 7}, + year = {1997}, + note = {Version en anglais disponible comme rapport de + recherche INRIA RR-3309}, + type = {Th\`ese de Doctorat} +} + +@Book{NoPS90, + author = {B. {Nordstr\"om} and K. Peterson and J. Smith}, + booktitle = {Information Processing 83}, + publisher = {Oxford Science Publications}, + series = {International Series of Monographs on Computer Science}, + title = {Programming in {Martin-L\"of's} Type Theory}, + year = {1990} +} + +@Article{Nor88, + author = {B. {Nordstr\"om}}, + journal = {BIT}, + title = {Terminating General Recursion}, + volume = {28}, + year = {1988} +} + +@Book{Odi90, + editor = {P. Odifreddi}, + publisher = {Academic Press}, + title = {Logic and Computer Science}, + year = {1990} +} + +@InProceedings{PaMS92, + author = {M. Parigot and P. Manoury and M. Simonot}, + address = {St. Petersburg, Russia}, + booktitle = {Logic Programming and automated reasoning}, + editor = {A. Voronkov}, + month = jul, + number = {624}, + publisher = SV, + series = {LNCS}, + title = {{ProPre : A Programming language with proofs}}, + year = {1992} +} + +@Article{PaWe92, + author = {C. Paulin-Mohring and B. Werner}, + journal = {Journal of Symbolic Computation}, + pages = {607--640}, + title = {{Synthesis of ML programs in the system Coq}}, + volume = {15}, + year = {1993} +} + +@Article{Par92, + author = {M. Parigot}, + journal = {Theoretical Computer Science}, + number = {2}, + pages = {335--356}, + title = {{Recursive Programming with Proofs}}, + volume = {94}, + year = {1992} +} + +@InProceedings{Parent95b, + author = {C. Parent}, + booktitle = {{Mathematics of Program Construction'95}}, + publisher = SV, + series = {LNCS}, + title = {{Synthesizing proofs from programs in +the Calculus of Inductive Constructions}}, + volume = {947}, + year = {1995} +} + +@InProceedings{Prasad93, + author = {K.V. Prasad}, + booktitle = {{Proceedings of CONCUR'93}}, + publisher = SV, + series = {LNCS}, + title = {{Programming with broadcasts}}, + volume = {715}, + year = {1993} +} + +@Book{RC95, + author = {di~Cosmo, R.}, + title = {Isomorphisms of Types: from $\lambda$-calculus to information + retrieval and language design}, + series = {Progress in Theoretical Computer Science}, + publisher = {Birkhauser}, + year = {1995}, + note = {ISBN-0-8176-3763-X} +} + +@TechReport{Rou92, + author = {J. Rouyer}, + institution = {INRIA}, + month = nov, + number = {1795}, + title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}}, + year = {1992} +} + +@Article{Rushby98, + title = {Subtypes for Specifications: Predicate Subtyping in + {PVS}}, + author = {John Rushby and Sam Owre and N. Shankar}, + journal = {IEEE Transactions on Software Engineering}, + pages = {709--720}, + volume = 24, + number = 9, + month = sep, + year = 1998 +} + +@TechReport{Saibi94, + author = {A. Sa\"{\i}bi}, + institution = {INRIA}, + month = dec, + number = {2345}, + title = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, + year = {1994} +} + + +@MastersThesis{Ter92, + author = {D. Terrasse}, + month = sep, + school = {IARFA}, + title = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, + year = {1992} +} + +@TechReport{ThBeKa92, + author = {L. Th\'ery and Y. Bertot and G. Kahn}, + institution = {INRIA Sophia}, + month = may, + number = {1684}, + title = {Real theorem provers deserve real user-interfaces}, + type = {Research Report}, + year = {1992} +} + +@Book{TrDa89, + author = {A.S. Troelstra and D. van Dalen}, + publisher = {North-Holland}, + series = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, + title = {Constructivism in Mathematics, an introduction}, + year = {1988} +} + +@PhDThesis{Wer94, + author = {B. Werner}, + school = {Universit\'e Paris 7}, + title = {Une th\'eorie des constructions inductives}, + type = {Th\`ese de Doctorat}, + year = {1994} +} + +@PhDThesis{Bar99, + author = {B. Barras}, + school = {Universit\'e Paris 7}, + title = {Auto-validation d'un système de preuves avec familles inductives}, + type = {Th\`ese de Doctorat}, + year = {1999} +} + +@Unpublished{ddr98, + author = {D. de Rauglaudre}, + title = {Camlp4 version 1.07.2}, + year = {1998}, + note = {In Camlp4 distribution} +} + +@Article{dowek93, + author = {G. Dowek}, + title = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, + journal = {Journal Logic Computation}, + volume = {3}, + number = {3}, + pages = {287--315}, + month = {June}, + year = {1993} +} + +@InProceedings{manoury94, + author = {P. Manoury}, + title = {{A User's Friendly Syntax to Define +Recursive Functions as Typed $\lambda-$Terms}}, + booktitle = {{Types for Proofs and Programs, TYPES'94}}, + series = {LNCS}, + volume = {996}, + month = jun, + year = {1994} +} + +@TechReport{maranget94, + author = {L. Maranget}, + institution = {INRIA}, + number = {2385}, + title = {{Two Techniques for Compiling Lazy Pattern Matching}}, + year = {1994} +} + +@InProceedings{puel-suarez90, + author = {L.Puel and A. Su\'arez}, + booktitle = {{Conference Lisp and Functional Programming}}, + series = {ACM}, + publisher = SV, + title = {{Compiling Pattern Matching by Term +Decomposition}}, + year = {1990} +} + +@MastersThesis{saidi94, + author = {H. Saidi}, + month = sep, + school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, + title = {R\'esolution d'\'equations dans le syst\`eme T + de G\"odel}, + year = {1994} +} + +@inproceedings{sozeau06, + author = {Matthieu Sozeau}, + title = {Subset Coercions in {C}oq}, + year = {2007}, + booktitle = {TYPES'06}, + pages = {237-252}, + volume = {4502}, + publisher = "Springer", + 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}, + note = {Habilitationsschrift, LMU Munchen.}, + year = {1993} +} + +@Misc{Pcoq, + author = {Lemme Team}, + title = {Pcoq a graphical user-interface for {Coq}}, + note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} +} + +@Misc{ProofGeneral, + author = {David Aspinall}, + title = {Proof General}, + note = {\url{https://proofgeneral.github.io/}} +} + +@Book{CoqArt, + title = {Interactive Theorem Proving and Program Development. + Coq'Art: The Calculus of Inductive Constructions}, + author = {Yves Bertot and Pierre Castéran}, + publisher = {Springer Verlag}, + series = {Texts in Theoretical Computer Science. An EATCS series}, + year = 2004 +} + +@InCollection{wadler87, + author = {P. Wadler}, + title = {Efficient Compilation of Pattern Matching}, + booktitle = {The Implementation of Functional Programming +Languages}, + editor = {S.L. Peyton Jones}, + publisher = {Prentice-Hall}, + year = {1987} +} + +@inproceedings{DBLP:conf/types/CornesT95, + author = {Cristina Cornes and + Delphine Terrasse}, + title = {Automating Inversion of Inductive Predicates in Coq}, + booktitle = {TYPES}, + year = {1995}, + pages = {85-104}, + crossref = {DBLP:conf/types/1995}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/types/1995, + editor = {Stefano Berardi and + Mario Coppo}, + title = {Types for Proofs and Programs, International Workshop TYPES'95, + Torino, Italy, June 5-8, 1995, Selected Papers}, + booktitle = {TYPES}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {1158}, + year = {1996}, + isbn = {3-540-61780-9}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@inproceedings{DBLP:conf/types/McBride00, + author = {Conor McBride}, + title = {Elimination with a Motive}, + booktitle = {TYPES}, + year = {2000}, + pages = {197-216}, + ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, + crossref = {DBLP:conf/types/2000}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@proceedings{DBLP:conf/types/2000, + editor = {Paul Callaghan and + Zhaohui Luo and + James McKinna and + Robert Pollack}, + title = {Types for Proofs and Programs, International Workshop, TYPES + 2000, Durham, UK, December 8-12, 2000, Selected Papers}, + booktitle = {TYPES}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {2277}, + year = {2002}, + isbn = {3-540-43287-6}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@INPROCEEDINGS{sugar, + author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso}, + title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm}, + booktitle = { Proceedings of the ISSAC'91, ACM Press}, + year = {1991}, + pages = {5--4}, + publisher = {} +} + +@article{LeeWerner11, + author = {Gyesik Lee and + Benjamin Werner}, + title = {Proof-irrelevant model of {CC} with predicative induction + and judgmental equality}, + journal = {Logical Methods in Computer Science}, + volume = {7}, + number = {4}, + year = {2011}, + ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@Comment{cross-references, must be at end} + +@Book{Bastad92, + editor = {B. Nordstr\"om and K. Petersson and G. Plotkin}, + publisher = {Available by ftp at site ftp.inria.fr}, + title = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, + year = {1992} +} + +@Book{Nijmegen93, + editor = {H. Barendregt and T. Nipkow}, + publisher = SV, + series = LNCS, + title = {Types for Proofs and Programs}, + volume = {806}, + year = {1994} +} + +@article{ TheOmegaPaper, + author = "W. Pugh", + title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis", + journal = "Communication of the ACM", + pages = "102--114", + year = "1992", +} + +@inproceedings{CSwcu, + hal_id = {hal-00816703}, + url = {http://hal.inria.fr/hal-00816703}, + title = {{Canonical Structures for the working Coq user}}, + author = {Mahboubi, Assia and Tassi, Enrico}, + booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, + publisher = {Springer}, + pages = {19-34}, + address = {Rennes, France}, + volume = {7998}, + editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, + series = {LNCS }, + doi = {10.1007/978-3-642-39634-2\_5 }, + year = {2013}, +} + +@article{CSlessadhoc, + author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, + title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, + journal = {SIGPLAN Not.}, + issue_date = {September 2011}, + volume = {46}, + number = {9}, + month = sep, + year = {2011}, + issn = {0362-1340}, + pages = {163--175}, + numpages = {13}, + url = {http://doi.acm.org/10.1145/2034574.2034798}, + doi = {10.1145/2034574.2034798}, + acmid = {2034798}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, +} + +@inproceedings{CompiledStrongReduction, + author = {Benjamin Gr{\'{e}}goire and + Xavier Leroy}, + editor = {Mitchell Wand and + Simon L. Peyton Jones}, + title = {A compiled implementation of strong reduction}, + booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference + on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania, + USA, October 4-6, 2002.}, + pages = {235--246}, + publisher = {{ACM}}, + year = {2002}, + url = {http://doi.acm.org/10.1145/581478.581501}, + doi = {10.1145/581478.581501}, + timestamp = {Tue, 11 Jun 2013 13:49:16 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{FullReduction, + author = {Mathieu Boespflug and + Maxime D{\'{e}}n{\`{e}}s and + Benjamin Gr{\'{e}}goire}, + editor = {Jean{-}Pierre Jouannaud and + Zhong Shao}, + title = {Full Reduction at Full Throttle}, + booktitle = {Certified Programs and Proofs - First International Conference, {CPP} + 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {7086}, + pages = {362--377}, + publisher = {Springer}, + year = {2011}, + url = {http://dx.doi.org/10.1007/978-3-642-25379-9_26}, + doi = {10.1007/978-3-642-25379-9_26}, + timestamp = {Thu, 17 Nov 2011 13:33:48 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 0bff41a25..12aeee3f9 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -10,7 +10,7 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## # -# Coq 8.5 documentation build configuration file, created by +# Coq documentation build configuration file, created by # sphinx-quickstart on Wed May 11 11:23:13 2016. # # This file is execfile()d with the current directory set to its @@ -32,6 +32,9 @@ sys.setrecursionlimit(1500) # add these directories to sys.path here. If the directory is relative to the # documentation root, use os.path.abspath to make it absolute, like shown here. sys.path.append(os.path.abspath('../tools/')) +sys.path.append(os.path.abspath('../../config/')) + +import coq_config # -- General configuration ------------------------------------------------ @@ -64,7 +67,7 @@ master_doc = 'index' # General information about the project. project = 'Coq' -copyright = '2016, Inria' +copyright = '1999-2018, Inria' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for @@ -72,9 +75,9 @@ author = 'The Coq Development Team' # built documents. # # The short X.Y version. -version = '8.7' +version = coq_config.version # The full version, including alpha/beta/rc tags. -release = '8.7.dev' +release = coq_config.version # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages. @@ -92,7 +95,7 @@ language = None # List of patterns, relative to source directory, that match files and # directories to ignore when looking for source files. # This patterns also effect to html_static_path and html_extra_path -exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store'] +exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store', 'introduction.rst'] # The reST default role (used for this markup: `text`) to use for all # documents. @@ -143,6 +146,14 @@ html_theme = 'sphinx_rtd_theme' # documentation. #html_theme_options = {} +html_context = { + 'display_github': True, + 'github_user': 'coq', + 'github_repo': 'coq', + 'github_version': 'master', + 'conf_py_path': '/doc/sphinx/' +} + # Add any paths that contain custom themes here, relative to this directory. import sphinx_rtd_theme html_theme_path = [sphinx_rtd_theme.get_html_theme_path()] @@ -230,9 +241,6 @@ html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesg # implements a search results scorer. If empty, the default will be used. #html_search_scorer = 'scorer.js' -# Output file base name for HTML help builder. -htmlhelp_basename = 'Coq85doc' - # -- Options for LaTeX output --------------------------------------------- ########################### @@ -264,10 +272,10 @@ latex_additional_files = ["_static/coqnotations.sty"] # Grouping the document tree into LaTeX files. List of tuples # (source start file, target name, title, # author, documentclass [howto, manual, or own class]). -latex_documents = [ - (master_doc, 'Coq85.tex', 'Coq 8.5 Documentation', - 'The Coq Development Team (edited by C. Pit-Claudel)', 'manual'), -] +# latex_documents = [ +# (master_doc, 'CoqRefMan.tex', 'Coq Documentation', +# 'The Coq Development Team', 'manual'), +#] # The name of an image file (relative to this directory) to place at the top of # the title page. @@ -294,10 +302,10 @@ latex_documents = [ # One entry per manual page. List of tuples # (source start file, name, description, authors, manual section). -man_pages = [ - (master_doc, 'coq85', 'Coq 8.5 Documentation', - [author], 1) -] +#man_pages = [ +# (master_doc, 'coq', 'Coq Documentation', +# [author], 1) +#] # If true, show URL addresses after external links. #man_show_urls = False @@ -308,11 +316,11 @@ man_pages = [ # Grouping the document tree into Texinfo files. List of tuples # (source start file, target name, title, author, # dir menu entry, description, category) -texinfo_documents = [ - (master_doc, 'Coq85', 'Coq 8.5 Documentation', - author, 'Coq85', 'One line description of project.', - 'Miscellaneous'), -] +#texinfo_documents = [ +# (master_doc, 'Coq', 'Coq Documentation', +# author, 'Coq', 'One line description of project.', +# 'Miscellaneous'), +#] # Documents to append as an appendix to all manuals. #texinfo_appendices = [] @@ -330,10 +338,10 @@ texinfo_documents = [ # -- Options for Epub output ---------------------------------------------- # Bibliographic Dublin Core info. -epub_title = project -epub_author = author -epub_publisher = author -epub_copyright = copyright +#epub_title = project +#epub_author = author +#epub_publisher = author +#epub_copyright = copyright # The basename for the epub file. It defaults to the project name. #epub_basename = project diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst new file mode 100644 index 000000000..7df6cb36c --- /dev/null +++ b/doc/sphinx/coq-cmdindex.rst @@ -0,0 +1,5 @@ +.. hack to get index in TOC + +----------------- +Command index +----------------- diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst new file mode 100644 index 000000000..100c57b08 --- /dev/null +++ b/doc/sphinx/coq-exnindex.rst @@ -0,0 +1,5 @@ +.. hack to get index in TOC + +---------------------- +Errors, warnings index +---------------------- diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst new file mode 100644 index 000000000..f8046a800 --- /dev/null +++ b/doc/sphinx/coq-optindex.rst @@ -0,0 +1,5 @@ +.. hack to get index in TOC + +----------------- +Option index +----------------- diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst new file mode 100644 index 000000000..588104f46 --- /dev/null +++ b/doc/sphinx/coq-tacindex.rst @@ -0,0 +1,5 @@ +.. hack to get index in TOC + +------------- +Tactic index +------------- diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst new file mode 100644 index 000000000..a991c7f9f --- /dev/null +++ b/doc/sphinx/genindex.rst @@ -0,0 +1,5 @@ +.. hack to get index in TOC + +----- +Index +----- diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index e69de29bb..7b8bc2bae 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -0,0 +1,50 @@ +.. _introduction: + +.. include:: preamble.rst +.. include:: replaces.rst + +Introduction +=========================================== + +.. include:: introduction.rst + +------------------ +Table of contents +------------------ + +.. toctree:: + :caption: The language + +.. toctree:: + :caption: The proof engine + +.. toctree:: + :caption: User extensions + +.. toctree:: + :caption: Practical tools + +.. toctree:: + :caption: Addendum + +.. toctree:: + :caption: Reference + + zebibliography + +.. toctree:: + :caption: Indexes + + genindex + coq-cmdindex + coq-tacindex + coq-optindex + coq-exnindex + +.. No entries yet + * :index:`thmindex` + +This material (the Coq Reference Manual) may be distributed only subject to the +terms and conditions set forth in the Open Publication License, v1.0 or later +(the latest version is presently available at +http://www.opencontent.org/openpub). Options A and B are not elected. diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst new file mode 100644 index 000000000..514745c1b --- /dev/null +++ b/doc/sphinx/introduction.rst @@ -0,0 +1,119 @@ +------------------------ +Introduction +------------------------ + +This document is the Reference Manual of version of the |Coq| proof +assistant. A companion volume, the |Coq| Tutorial, is provided for the +beginners. It is advised to read the Tutorial first. A +book :cite:`CoqArt` on practical uses of the |Coq| system was +published in 2004 and is a good support for both the beginner and the +advanced user. + +The |Coq| system is designed to develop mathematical proofs, and +especially to write formal specifications, programs and to verify that +programs are correct with respect to their specification. It provides a +specification language named |Gallina|. Terms of |Gallina| can represent +programs as well as properties of these programs and proofs of these +properties. Using the so-called *Curry-Howard isomorphism*, programs, +properties and proofs are formalized in the same language called +*Calculus of Inductive Constructions*, that is a +:math:`\lambda`-calculus with a rich type system. All logical judgments +in |Coq| are typing judgments. The very heart of the |Coq| system is the +type-checking algorithm that checks the correctness of proofs, in other +words that checks that a program complies to its specification. |Coq| also +provides an interactive proof assistant to build proofs using specific +programs called *tactics*. + +All services of the |Coq| proof assistant are accessible by interpretation +of a command language called *the vernacular*. + +Coq has an interactive mode in which commands are interpreted as the +user types them in from the keyboard and a compiled mode where commands +are processed from a file. + +- The interactive mode may be used as a debugging mode in which the + user can develop his theories and proofs step by step, backtracking + if needed and so on. The interactive mode is run with the `coqtop` + command from the operating system (which we shall assume to be some + variety of UNIX in the rest of this document). + +- The compiled mode acts as a proof checker taking a file containing a + whole development in order to ensure its correctness. Moreover, + |Coq|’s compiler provides an output file containing a compact + representation of its input. The compiled mode is run with the `coqc` + command from the operating system. + +These two modes are documented in Chapter :ref:`thecoqcommands`. + +Other modes of interaction with |Coq| are possible: through an emacs shell +window, an emacs generic user-interface for proof assistant (Proof +General :cite:`ProofGeneral`) or through a customized +interface (PCoq :cite:`Pcoq`). These facilities are not +documented here. There is also a |Coq| Integrated Development Environment +described in :ref:`coqintegrateddevelopmentenvironment`. + +How to read this book +===================== + +This is a Reference Manual, not a User Manual, so it is not made for a +continuous reading. However, it has some structure that is explained +below. + +- The first part describes the specification language, |Gallina|. + Chapters :ref:`thegallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete + syntax as well as the meaning of programs, theorems and proofs in the + Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the + standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description + of the formalism. Chapter :ref:`themodulesystem` describes the module + system. + +- The second part describes the proof engine. It is divided in five + chapters. Chapter :ref:`vernacularcommands` presents all commands (we + call them *vernacular commands*) that are not directly related to + interactive proving: requests to the environment, complete or partial + evaluation, loading and compiling files. How to start and stop + proofs, do multiple proofs in parallel is explained in + Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that + realize one or more steps of the proof are presented: we call them + *tactics*. The language to combine these tactics into complex proof + strategies is given in Chapter :ref:`thetacticlanguage`. Examples of tactics + are described in Chapter :ref:`detailedexamplesoftactics`. + +- The third part describes how to extend the syntax of |Coq|. It + corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`. + +- In the fourth part more practical tools are documented. First in + Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and + `coqtop` (interactive mode) with their options is described. Then, + in Chapter :ref:`utilities`, various utilities that come with the + |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` + describes the |Coq| integrated development environment. + +- The fifth part documents a number of advanced features, including coercions, + canonical structures, typeclasses, program extraction, and specialized + solvers and tactics. See the table of contents for a complete list. + +At the end of the document, after the global index, the user can find +specific indexes for tactics, vernacular commands, and error messages. + +List of additional documentation +================================ + +This manual does not contain all the documentation the user may need +about |Coq|. Various informations can be found in the following documents: + +Tutorial + A companion volume to this reference manual, the |Coq| Tutorial, is + aimed at gently introducing new users to developing proofs in |Coq| + without assuming prior knowledge of type theory. In a second step, + the user can read also the tutorial on recursive types (document + `RecTutorial.ps`). + +Installation + A text file `INSTALL` that comes with the sources explains how to + install |Coq|. + +The |Coq| standard library + A commented version of sources of the |Coq| standard library + (including only the specifications, the proofs are removed) is given + in the additional document `Library.ps`. diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst new file mode 100644 index 000000000..395f558a8 --- /dev/null +++ b/doc/sphinx/preamble.rst @@ -0,0 +1,92 @@ +.. preamble:: + + \[ + \newcommand{\alors}{\textsf{then}} + \newcommand{\alter}{\textsf{alter}} + \newcommand{\as}{\kw{as}} + \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} + \newcommand{\bool}{\textsf{bool}} + \newcommand{\case}{\kw{case}} + \newcommand{\conc}{\textsf{conc}} + \newcommand{\cons}{\textsf{cons}} + \newcommand{\consf}{\textsf{consf}} + \newcommand{\conshl}{\textsf{cons\_hl}} + \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} + \newcommand{\emptyf}{\textsf{emptyf}} + \newcommand{\End}{\kw{End}} + \newcommand{\endkw}{\kw{end}} + \newcommand{\EqSt}{\textsf{EqSt}} + \newcommand{\even}{\textsf{even}} + \newcommand{\evenO}{\textsf{even_O}} + \newcommand{\evenS}{\textsf{even_S}} + \newcommand{\false}{\textsf{false}} + \newcommand{\filter}{\textsf{filter}} + \newcommand{\Fix}{\kw{Fix}} + \newcommand{\fix}{\kw{fix}} + \newcommand{\for}{\textsf{for}} + \newcommand{\forest}{\textsf{forest}} + \newcommand{\from}{\textsf{from}} + \newcommand{\Functor}{\kw{Functor}} + \newcommand{\haslength}{\textsf{has\_length}} + \newcommand{\hd}{\textsf{hd}} + \newcommand{\ident}{\textsf{ident}} + \newcommand{\In}{\kw{in}} + \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} + \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} + \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} + \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} + \newcommand{\injective}{\kw{injective}} + \newcommand{\kw}[1]{\textsf{#1}} + \newcommand{\lb}{\lambda} + \newcommand{\length}{\textsf{length}} + \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} + \newcommand{\List}{\textsf{list}} + \newcommand{\lra}{\longrightarrow} + \newcommand{\Match}{\kw{match}} + \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} + \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} + \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} + \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} + \newcommand{\mto}{.\;} + \newcommand{\Nat}{\mathbb{N}} + \newcommand{\nat}{\textsf{nat}} + \newcommand{\Nil}{\textsf{nil}} + \newcommand{\nilhl}{\textsf{nil\_hl}} + \newcommand{\nO}{\textsf{O}} + \newcommand{\node}{\textsf{node}} + \newcommand{\nS}{\textsf{S}} + \newcommand{\odd}{\textsf{odd}} + \newcommand{\oddS}{\textsf{odd_S}} + \newcommand{\ovl}[1]{\overline{#1}} + \newcommand{\Pair}{\textsf{pair}} + \newcommand{\Prod}{\textsf{prod}} + \newcommand{\Prop}{\textsf{Prop}} + \newcommand{\return}{\kw{return}} + \newcommand{\Set}{\textsf{Set}} + \newcommand{\si}{\textsf{if}} + \newcommand{\sinon}{\textsf{else}} + \newcommand{\Sort}{\cal S} + \newcommand{\Str}{\textsf{Stream}} + \newcommand{\Struct}{\kw{Struct}} + \newcommand{\subst}[3]{#1\{#2/#3\}} + \newcommand{\tl}{\textsf{tl}} + \newcommand{\tree}{\textsf{tree}} + \newcommand{\true}{\textsf{true}} + \newcommand{\Type}{\textsf{Type}} + \newcommand{\unfold}{\textsf{unfold}} + \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} + \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} + \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} + \newcommand{\WFE}[1]{\WF{E}{#1}} + \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} + \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} + \newcommand{\with}{\kw{with}} + \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} + \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} + \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} + \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} + \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} + \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} + \newcommand{\zeroone}[1]{[{#1}]} + \newcommand{\zeros}{\textsf{zeros}} + \] diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst new file mode 100644 index 000000000..2c38219b9 --- /dev/null +++ b/doc/sphinx/replaces.rst @@ -0,0 +1,78 @@ +.. some handy replacements for common items + +.. role:: smallcaps + +.. |A_1| replace:: `A`\ :math:`_{1}` +.. |A_n| replace:: `A`\ :math:`_{n}` +.. |arg_1| replace:: `arg`\ :math:`_{1}` +.. |arg_n| replace:: `arg`\ :math:`_{n}` +.. |bdi| replace:: :math:`\beta\delta\iota` +.. |binder_1| replace:: `binder`\ :math:`_{1}` +.. |binder_n| replace:: `binder`\ :math:`_{n}` +.. |binders_1| replace:: `binders`\ :math:`_{1}` +.. |binders_n| replace:: `binders`\ :math:`_{n}` +.. |C_1| replace:: `C`\ :math:`_{1}` +.. |c_1| replace:: `c`\ :math:`_{1}` +.. |C_2| replace:: `C`\ :math:`_{2}` +.. |c_i| replace:: `c`\ :math:`_{i}` +.. |c_n| replace:: `c`\ :math:`_{n}` +.. |Cic| replace:: :smallcaps:`Cic` +.. |class_1| replace:: `class`\ :math:`_{1}` +.. |class_2| replace:: `class`\ :math:`_{2}` +.. |Coq| replace:: :smallcaps:`Coq` +.. |CoqIDE| replace:: :smallcaps:`CoqIDE` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}` +.. |Gallina| replace:: :smallcaps:`Gallina` +.. |ident_0| replace:: `ident`\ :math:`_{0}` +.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` +.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`) +.. |ident_1| replace:: `ident`\ :math:`_{1}` +.. |ident_2| replace:: `ident`\ :math:`_{2}` +.. |ident_3| replace:: `ident`\ :math:`_{3}` +.. |ident_i| replace:: `ident`\ :math:`_{i}` +.. |ident_j| replace:: `ident`\ :math:`_{j}` +.. |ident_k| replace:: `ident`\ :math:`_{k}` +.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}` +.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}` +.. |ident_n| replace:: `ident`\ :math:`_{n}` +.. |L_tac| replace:: `L`:sub:`tac` +.. |ML| replace:: :smallcaps:`ML` +.. |mod_0| replace:: `mod`\ :math:`_{0}` +.. |mod_1| replace:: `mod`\ :math:`_{1}` +.. |mod_2| replace:: `mod`\ :math:`_{1}` +.. |mod_n| replace:: `mod`\ :math:`_{n}` +.. |module_0| replace:: `module`\ :math:`_{0}` +.. |module_1| replace:: `module`\ :math:`_{1}` +.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}` +.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}` +.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}` +.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}` +.. |module_n| replace:: `module`\ :math:`_{n}` +.. |module_type_0| replace:: `module_type`\ :math:`_{0}` +.. |module_type_1| replace:: `module_type`\ :math:`_{1}` +.. |module_type_i| replace:: `module_type`\ :math:`_{i}` +.. |module_type_n| replace:: `module_type`\ :math:`_{n}` +.. |N| replace:: ``N`` +.. |nat| replace:: ``nat`` +.. |Ocaml| replace:: :smallcaps:`OCaml` +.. |p_1| replace:: `p`\ :math:`_{1}` +.. |p_i| replace:: `p`\ :math:`_{i}` +.. |p_n| replace:: `p`\ :math:`_{n}` +.. |Program| replace:: :strong:`Program` +.. |t_1| replace:: `t`\ :math:`_{1}` +.. |t_i| replace:: `t`\ :math:`_{i}` +.. |t_m| replace:: `t`\ :math:`_{m}` +.. |t_n| replace:: `t`\ :math:`_{n}` +.. |term_0| replace:: `term`\ :math:`_{0}` +.. |term_1| replace:: `term`\ :math:`_{1}` +.. |term_2| replace:: `term`\ :math:`_{2}` +.. |term_n| replace:: `term`\ :math:`_{n}` +.. |type_0| replace:: `type`\ :math:`_{0}` +.. |type_1| replace:: `type`\ :math:`_{1}` +.. |type_2| replace:: `type`\ :math:`_{2}` +.. |type_3| replace:: `type`\ :math:`_{3}` +.. |type_n| replace:: `type`\ :math:`_{n}` +.. |x_1| replace:: `x`\ :math:`_{1}` +.. |x_i| replace:: `x`\ :math:`_{i}` +.. |x_n| replace:: `x`\ :math:`_{n}` +.. |Z| replace:: ``Z`` diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.rst new file mode 100644 index 000000000..0000caa30 --- /dev/null +++ b/doc/sphinx/zebibliography.rst @@ -0,0 +1,8 @@ +.. _bibliography: + +============ +Bibliography +============ + +.. bibliography:: biblio.bib + :cited: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 18f32d7a8..663ab9d37 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -28,8 +28,10 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes from sphinx.roles import XRefRole from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode +from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index +from sphinx.domains.std import token_xrefs from sphinx.ext.mathbase import MathDirective, displaymath from . import coqdoc @@ -155,6 +157,9 @@ class CoqObject(ObjectDescription): """Create a target and an index entry for name""" if name: target = self._add_target(signode, name) + # remove trailing . , found in commands, but not ... (ellipsis) + if name[-1] == "." and not name[-3:] == "..." : + name = name[0:-1] self._add_index_entry(name, target) return target @@ -173,19 +178,19 @@ class NotationObject(CoqObject): class TacticObject(PlainObject): """An object to represent Coq tactics""" subdomain = "tac" - index_suffix = "(tactic)" + index_suffix = "(tac)" annotation = None class GallinaObject(PlainObject): """An object to represent Coq theorems""" subdomain = "thm" - index_suffix = "(theorem)" + index_suffix = "(thm)" annotation = "Theorem" class VernacObject(NotationObject): """An object to represent Coq commands""" subdomain = "cmd" - index_suffix = "(command)" + index_suffix = "(cmd)" annotation = "Command" def _name_from_signature(self, signature): @@ -193,33 +198,72 @@ class VernacObject(NotationObject): class VernacVariantObject(VernacObject): """An object to represent variants of Coq commands""" - index_suffix = "(command variant)" + index_suffix = "(cmdv)" annotation = "Variant" class TacticNotationObject(NotationObject): """An object to represent Coq tactic notations""" subdomain = "tacn" - index_suffix = "(tactic notation)" + index_suffix = "(tacn)" annotation = None class TacticNotationVariantObject(TacticNotationObject): """An object to represent variants of Coq tactic notations""" - index_suffix = "(tactic variant)" + index_suffix = "(tacnv)" annotation = "Variant" class OptionObject(NotationObject): - """An object to represent variants of Coq options""" + """An object to represent Coq options""" subdomain = "opt" - index_suffix = "(option)" + index_suffix = "(opt)" annotation = "Option" def _name_from_signature(self, signature): return stringify_with_ellipses(signature) +class ProductionObject(NotationObject): + """An object to represent grammar productions""" + subdomain = "prodn" + index_suffix = None + annotation = None + + # override to create link targets for production left-hand sides + def run(self): + env = self.state.document.settings.env + objects = env.domaindata['std']['objects'] + + class ProdnError(Exception): + """Exception for ill-formed prodn""" + pass + + [idx, node] = super().run() + try: + # find LHS of production + inline_lhs = node[0][0][0][0] # may be fragile !!! + lhs_str = str(inline_lhs) + if lhs_str[0:7] != "<inline": + raise ProdnError("Expected atom on LHS") + lhs = inline_lhs[0] + # register link target + subnode = addnodes.production() + subnode['tokenname'] = lhs + idname = 'grammar-token-%s' % subnode['tokenname'] + if idname not in self.state.document.ids: + subnode['ids'].append(idname) + self.state.document.note_implicit_target(subnode, subnode) + objects['token', subnode['tokenname']] = env.docname, idname + subnode.extend(token_xrefs(lhs)) + # patch in link target + inline_lhs['ids'].append(idname) + except ProdnError as err: + getLogger(__name__).warning("Could not create link target for prodn: " + str(err) + + "\nSphinx represents the prodn as: " + str(node) + "\n") + return [idx, node] + class ExceptionObject(NotationObject): """An object to represent Coq errors.""" subdomain = "exn" - index_suffix = "(error)" + index_suffix = "(err)" annotation = "Error" # Uses “exn” since “err” already is a CSS class added by “writer_aux”. @@ -371,6 +415,7 @@ class InferenceDirective(Directive): required_arguments = 1 optional_arguments = 0 has_content = True + final_argument_whitespace = True def make_math_node(self, latex): node = displaymath() @@ -601,11 +646,13 @@ class CoqOptionIndex(CoqSubdomainsIndex): class CoqGallinaIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] -class CoqExceptionIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "exnindex", "Error Index", "errors", ["exn"] +# we specify an index to make productions fit into the framework of notations +# but not likely to include a link to this index +class CoqProductionIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "prodnindex", "Production Index", "productions", ["prodn"] -class CoqWarningIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "warnindex", "Warning Index", "warnings", ["warn"] +class CoqExceptionIndex(CoqSubdomainsIndex): + name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"] class IndexXRefRole(XRefRole): """A link to one of our domain-specific indices.""" @@ -664,8 +711,9 @@ class CoqDomain(Domain): 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), 'thm': ObjType('thm', 'thm'), + 'prodn': ObjType('prodn', 'prodn'), 'exn': ObjType('exn', 'exn'), - 'warn': ObjType('warn', 'warn'), + 'warn': ObjType('warn', 'exn'), 'index': ObjType('index', 'index', searchprio=-1) } @@ -680,6 +728,7 @@ class CoqDomain(Domain): 'tacv': TacticNotationVariantObject, 'opt': OptionObject, 'thm': GallinaObject, + 'prodn' : ProductionObject, 'exn': ExceptionObject, 'warn': WarningObject, } @@ -691,6 +740,7 @@ class CoqDomain(Domain): 'tacn': XRefRole(), 'opt': XRefRole(), 'thm': XRefRole(), + 'prodn' : XRefRole(), 'exn': XRefRole(), 'warn': XRefRole(), # This one is special @@ -704,7 +754,7 @@ class CoqDomain(Domain): 'l': LtacRole, #FIXME unused? } - indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex, CoqWarningIndex] + indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] data_version = 1 initial_data = { @@ -716,6 +766,7 @@ class CoqDomain(Domain): 'tacn': {}, 'opt': {}, 'thm': {}, + 'prodn' : {}, 'exn': {}, 'warn': {}, } @@ -807,6 +858,7 @@ def setup(app): app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) # Add extra styles + app.add_stylesheet("fonts.css") app.add_stylesheet("ansi.css") app.add_stylesheet("coqdoc.css") app.add_javascript("notations.js") diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 72ae8eb6b..5176c51d2 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -15,16 +15,18 @@ grammar TacticNotations; top: blocks EOF; blocks: block ((whitespace)? block)*; -block: atomic | hole | repeat | curlies; +block: atomic | meta | hole | repeat | curlies; repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; whitespace: WHITESPACE; +meta: METACHAR; atomic: ATOM; hole: ID; LGROUP: '{' [+*?]; LBRACE: '{'; RBRACE: '}'; -ATOM: ~[@{} ]+; +METACHAR: '%' [|()]; +ATOM: '@' | ~[@{} ]+; ID: '@' [a-zA-Z0-9_]+; WHITESPACE: ' '+; diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens index 4d41a3883..76ed2b065 100644 --- a/doc/tools/coqrst/notations/TacticNotations.tokens +++ b/doc/tools/coqrst/notations/TacticNotations.tokens @@ -1,8 +1,9 @@ LGROUP=1 LBRACE=2 RBRACE=3 -ATOM=4 -ID=5 -WHITESPACE=6 +METACHAR=4 +ATOM=5 +ID=6 +WHITESPACE=7 '{'=2 '}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py index 4cac071ac..ffa774b9b 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -7,21 +7,24 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\b") - buf.write("&\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") - buf.write("\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\6\5\30\n\5\r\5\16\5\31") - buf.write("\3\6\3\6\6\6\36\n\6\r\6\16\6\37\3\7\6\7#\n\7\r\7\16\7") - buf.write("$\2\2\b\3\3\5\4\7\5\t\6\13\7\r\b\3\2\5\4\2,-AA\6\2\"\"") - buf.write("BB}}\177\177\6\2\62;C\\aac|\2(\2\3\3\2\2\2\2\5\3\2\2\2") - buf.write("\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\3\17") - buf.write("\3\2\2\2\5\22\3\2\2\2\7\24\3\2\2\2\t\27\3\2\2\2\13\33") - buf.write("\3\2\2\2\r\"\3\2\2\2\17\20\7}\2\2\20\21\t\2\2\2\21\4\3") - buf.write("\2\2\2\22\23\7}\2\2\23\6\3\2\2\2\24\25\7\177\2\2\25\b") - buf.write("\3\2\2\2\26\30\n\3\2\2\27\26\3\2\2\2\30\31\3\2\2\2\31") - buf.write("\27\3\2\2\2\31\32\3\2\2\2\32\n\3\2\2\2\33\35\7B\2\2\34") - buf.write("\36\t\4\2\2\35\34\3\2\2\2\36\37\3\2\2\2\37\35\3\2\2\2") - buf.write("\37 \3\2\2\2 \f\3\2\2\2!#\7\"\2\2\"!\3\2\2\2#$\3\2\2\2") - buf.write("$\"\3\2\2\2$%\3\2\2\2%\16\3\2\2\2\6\2\31\37$\2") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\t") + buf.write(".\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3") + buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r") + buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6") + buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+~~\6\2\"\"BB}}\177\177") + buf.write("\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2") + buf.write("\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\3") + buf.write("\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2\13") + buf.write("!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23\t") + buf.write("\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27\7") + buf.write("\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32\n") + buf.write("\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36\37") + buf.write("\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3\2") + buf.write("\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3\2") + buf.write("\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+\7") + buf.write("\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3\2") + buf.write("\2\2\7\2\37!\',\2") return buf.getvalue() @@ -34,9 +37,10 @@ class TacticNotationsLexer(Lexer): LGROUP = 1 LBRACE = 2 RBRACE = 3 - ATOM = 4 - ID = 5 - WHITESPACE = 6 + METACHAR = 4 + ATOM = 5 + ID = 6 + WHITESPACE = 7 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] @@ -46,9 +50,10 @@ class TacticNotationsLexer(Lexer): "'{'", "'}'" ] symbolicNames = [ "<INVALID>", - "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ] + "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "WHITESPACE" ] - ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ] + ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", + "WHITESPACE" ] grammarFileName = "TacticNotations.g" diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens index 4d41a3883..76ed2b065 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -1,8 +1,9 @@ LGROUP=1 LBRACE=2 RBRACE=3 -ATOM=4 -ID=5 -WHITESPACE=6 +METACHAR=4 +ATOM=5 +ID=6 +WHITESPACE=7 '{'=2 '}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py index 357902ddb..c7e28af52 100644 --- a/doc/tools/coqrst/notations/TacticNotationsParser.py +++ b/doc/tools/coqrst/notations/TacticNotationsParser.py @@ -7,28 +7,29 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\b") - buf.write("A\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") - buf.write("\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\5\3\30\n\3\3\3\7\3\33") - buf.write("\n\3\f\3\16\3\36\13\3\3\4\3\4\3\4\3\4\5\4$\n\4\3\5\3\5") - buf.write("\5\5(\n\5\3\5\3\5\3\5\5\5-\n\5\3\5\3\5\3\6\3\6\5\6\63") - buf.write("\n\6\3\6\3\6\5\6\67\n\6\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3") - buf.write("\t\3\t\2\2\n\2\4\6\b\n\f\16\20\2\2\2A\2\22\3\2\2\2\4\25") - buf.write("\3\2\2\2\6#\3\2\2\2\b%\3\2\2\2\n\60\3\2\2\2\f:\3\2\2\2") - buf.write("\16<\3\2\2\2\20>\3\2\2\2\22\23\5\4\3\2\23\24\7\2\2\3\24") - buf.write("\3\3\2\2\2\25\34\5\6\4\2\26\30\5\f\7\2\27\26\3\2\2\2\27") - buf.write("\30\3\2\2\2\30\31\3\2\2\2\31\33\5\6\4\2\32\27\3\2\2\2") - buf.write("\33\36\3\2\2\2\34\32\3\2\2\2\34\35\3\2\2\2\35\5\3\2\2") - buf.write("\2\36\34\3\2\2\2\37$\5\16\b\2 $\5\20\t\2!$\5\b\5\2\"$") - buf.write("\5\n\6\2#\37\3\2\2\2# \3\2\2\2#!\3\2\2\2#\"\3\2\2\2$\7") - buf.write("\3\2\2\2%\'\7\3\2\2&(\7\6\2\2\'&\3\2\2\2\'(\3\2\2\2()") - buf.write("\3\2\2\2)*\7\b\2\2*,\5\4\3\2+-\7\b\2\2,+\3\2\2\2,-\3\2") - buf.write("\2\2-.\3\2\2\2./\7\5\2\2/\t\3\2\2\2\60\62\7\4\2\2\61\63") - buf.write("\5\f\7\2\62\61\3\2\2\2\62\63\3\2\2\2\63\64\3\2\2\2\64") - buf.write("\66\5\4\3\2\65\67\5\f\7\2\66\65\3\2\2\2\66\67\3\2\2\2") - buf.write("\678\3\2\2\289\7\5\2\29\13\3\2\2\2:;\7\b\2\2;\r\3\2\2") - buf.write("\2<=\7\6\2\2=\17\3\2\2\2>?\7\7\2\2?\21\3\2\2\2\t\27\34") - buf.write("#\',\62\66") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\t") + buf.write("F\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") + buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3") + buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'") + buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3") + buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b") + buf.write("\3\b\3\t\3\t\3\n\3\n\3\n\2\2\13\2\4\6\b\n\f\16\20\22\2") + buf.write("\2\2F\2\24\3\2\2\2\4\27\3\2\2\2\6&\3\2\2\2\b(\3\2\2\2") + buf.write("\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2\2\20A\3\2\2\2\22C\3") + buf.write("\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3\26\3\3\2\2\2\27\36") + buf.write("\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2\2\31\32\3\2\2\2\32") + buf.write("\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2\2\2\35 \3\2\2\2\36") + buf.write("\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2\2\2 \36\3\2\2\2!\'") + buf.write("\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2$\'\5\b\5\2%\'\5\n\6") + buf.write("\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2&$\3\2\2\2&%\3\2\2\2") + buf.write("\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*)\3\2\2\2*+\3\2\2\2+") + buf.write(",\3\2\2\2,-\7\t\2\2-/\5\4\3\2.\60\7\t\2\2/.\3\2\2\2/\60") + buf.write("\3\2\2\2\60\61\3\2\2\2\61\62\7\5\2\2\62\t\3\2\2\2\63\65") + buf.write("\7\4\2\2\64\66\5\f\7\2\65\64\3\2\2\2\65\66\3\2\2\2\66") + buf.write("\67\3\2\2\2\679\5\4\3\28:\5\f\7\298\3\2\2\29:\3\2\2\2") + buf.write(":;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2=>\7\t\2\2>\r\3\2\2\2") + buf.write("?@\7\6\2\2@\17\3\2\2\2AB\7\7\2\2B\21\3\2\2\2CD\7\b\2\2") + buf.write("D\23\3\2\2\2\t\31\36&*/\659") return buf.getvalue() @@ -44,8 +45,8 @@ class TacticNotationsParser ( Parser ): literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ] - symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "ATOM", - "ID", "WHITESPACE" ] + symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR", + "ATOM", "ID", "WHITESPACE" ] RULE_top = 0 RULE_blocks = 1 @@ -53,19 +54,21 @@ class TacticNotationsParser ( Parser ): RULE_repeat = 3 RULE_curlies = 4 RULE_whitespace = 5 - RULE_atomic = 6 - RULE_hole = 7 + RULE_meta = 6 + RULE_atomic = 7 + RULE_hole = 8 ruleNames = [ "top", "blocks", "block", "repeat", "curlies", "whitespace", - "atomic", "hole" ] + "meta", "atomic", "hole" ] EOF = Token.EOF LGROUP=1 LBRACE=2 RBRACE=3 - ATOM=4 - ID=5 - WHITESPACE=6 + METACHAR=4 + ATOM=5 + ID=6 + WHITESPACE=7 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) @@ -106,9 +109,9 @@ class TacticNotationsParser ( Parser ): self.enterRule(localctx, 0, self.RULE_top) try: self.enterOuterAlt(localctx, 1) - self.state = 16 + self.state = 18 self.blocks() - self.state = 17 + self.state = 19 self.match(TacticNotationsParser.EOF) except RecognitionException as re: localctx.exception = re @@ -157,24 +160,24 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 19 + self.state = 21 self.block() - self.state = 26 + self.state = 28 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: if _alt==1: - self.state = 21 + self.state = 23 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 20 + self.state = 22 self.whitespace() - self.state = 23 + self.state = 25 self.block() - self.state = 28 + self.state = 30 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) @@ -196,6 +199,10 @@ class TacticNotationsParser ( Parser ): return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0) + def meta(self): + return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0) + + def hole(self): return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0) @@ -225,27 +232,32 @@ class TacticNotationsParser ( Parser ): localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) self.enterRule(localctx, 4, self.RULE_block) try: - self.state = 33 + self.state = 36 self._errHandler.sync(self) token = self._input.LA(1) if token in [TacticNotationsParser.ATOM]: self.enterOuterAlt(localctx, 1) - self.state = 29 + self.state = 31 self.atomic() pass - elif token in [TacticNotationsParser.ID]: + elif token in [TacticNotationsParser.METACHAR]: self.enterOuterAlt(localctx, 2) - self.state = 30 + self.state = 32 + self.meta() + pass + elif token in [TacticNotationsParser.ID]: + self.enterOuterAlt(localctx, 3) + self.state = 33 self.hole() pass elif token in [TacticNotationsParser.LGROUP]: - self.enterOuterAlt(localctx, 3) - self.state = 31 + self.enterOuterAlt(localctx, 4) + self.state = 34 self.repeat() pass elif token in [TacticNotationsParser.LBRACE]: - self.enterOuterAlt(localctx, 4) - self.state = 32 + self.enterOuterAlt(localctx, 5) + self.state = 35 self.curlies() pass else: @@ -303,29 +315,29 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 35 + self.state = 38 self.match(TacticNotationsParser.LGROUP) - self.state = 37 + self.state = 40 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.ATOM: - self.state = 36 + self.state = 39 self.match(TacticNotationsParser.ATOM) - self.state = 39 + self.state = 42 self.match(TacticNotationsParser.WHITESPACE) - self.state = 40 + self.state = 43 self.blocks() - self.state = 42 + self.state = 45 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 41 + self.state = 44 self.match(TacticNotationsParser.WHITESPACE) - self.state = 44 + self.state = 47 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -377,27 +389,27 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 46 + self.state = 49 self.match(TacticNotationsParser.LBRACE) - self.state = 48 + self.state = 51 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 47 + self.state = 50 self.whitespace() - self.state = 50 + self.state = 53 self.blocks() - self.state = 52 + self.state = 55 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 51 + self.state = 54 self.whitespace() - self.state = 54 + self.state = 57 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -434,7 +446,7 @@ class TacticNotationsParser ( Parser ): self.enterRule(localctx, 10, self.RULE_whitespace) try: self.enterOuterAlt(localctx, 1) - self.state = 56 + self.state = 59 self.match(TacticNotationsParser.WHITESPACE) except RecognitionException as re: localctx.exception = re @@ -444,6 +456,43 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx + class MetaContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def METACHAR(self): + return self.getToken(TacticNotationsParser.METACHAR, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_meta + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitMeta" ): + return visitor.visitMeta(self) + else: + return visitor.visitChildren(self) + + + + + def meta(self): + + localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_meta) + try: + self.enterOuterAlt(localctx, 1) + self.state = 61 + self.match(TacticNotationsParser.METACHAR) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + class AtomicContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -468,10 +517,10 @@ class TacticNotationsParser ( Parser ): def atomic(self): localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state) - self.enterRule(localctx, 12, self.RULE_atomic) + self.enterRule(localctx, 14, self.RULE_atomic) try: self.enterOuterAlt(localctx, 1) - self.state = 58 + self.state = 63 self.match(TacticNotationsParser.ATOM) except RecognitionException as re: localctx.exception = re @@ -505,10 +554,10 @@ class TacticNotationsParser ( Parser ): def hole(self): localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state) - self.enterRule(localctx, 14, self.RULE_hole) + self.enterRule(localctx, 16, self.RULE_hole) try: self.enterOuterAlt(localctx, 1) - self.state = 60 + self.state = 65 self.match(TacticNotationsParser.ID) except RecognitionException as re: localctx.exception = re diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py index 80e69d433..c0bcc4af3 100644 --- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py +++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py @@ -39,6 +39,11 @@ class TacticNotationsVisitor(ParseTreeVisitor): return self.visitChildren(ctx) + # Visit a parse tree produced by TacticNotationsParser#meta. + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by TacticNotationsParser#atomic. def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): return self.visitChildren(ctx) @@ -50,4 +55,4 @@ class TacticNotationsVisitor(ParseTreeVisitor): -del TacticNotationsParser
\ No newline at end of file +del TacticNotationsParser diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index d91bbb64c..44212d788 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -42,6 +42,9 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): tags.span(ctx.ID().getText()[1:], _class="hole") + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + tags.span(ctx.METACHAR().getText()[1:], _class="meta") + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): tags.span(" ") # TODO: no need for a <span> here diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 73be6f26e..506240d90 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -12,7 +12,7 @@ from .TacticNotationsParser import TacticNotationsParser from antlr4 import CommonTokenStream, InputStream -SUBSTITUTIONS = [("@bindings_list", "{+ (@id := @val) }"), +SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"), ("@qualid_or_string", "@id|@string")] def substitute(notation): diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index 5d4501892..f6e82fc68 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -41,6 +41,9 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): self.buffer.write("‘{}’".format(ctx.ID().getText()[1:])) + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + self.buffer.write(ctx.METACHAR().getText()[1:]) + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(" ") diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py index cac6aaecb..ea820c719 100644 --- a/doc/tools/coqrst/notations/regexp.py +++ b/doc/tools/coqrst/notations/regexp.py @@ -47,6 +47,9 @@ class TacticNotationsToRegexpVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): self.buffer.write("([^();. \n]+)") # FIXME could allow more things + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + self.buffer.write(re.escape(ctx.METACHAR().getText()[1:])) + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(r"\s+") diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 889bf70a4..26a5f6968 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -20,6 +20,8 @@ from .TacticNotationsVisitor import TacticNotationsVisitor from docutils import nodes from sphinx import addnodes +import sys + class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): def defaultResult(self): return [] @@ -62,6 +64,12 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): node = nodes.inline(hole, token_name, classes=["hole"]) return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + meta = ctx.METACHAR().getText() + metachar = meta[1:] # remove escape char + token_name = metachar + return [nodes.inline(metachar, token_name, classes=["meta"])] + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return [nodes.Text(" ")] |