doc du traducteur + premiere mise a jour du refman

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

1 files changed, 416 insertions, 0 deletions

diff --git a/doc/Translator.tex b/doc/Translator.tex
new file mode 100644
index 0000000000..02cbdf02e8
--- /dev/null
+++ b/doc/Translator.tex
@@ -0,0 +1,416 @@
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
+\documentclass[11pt,a4paper]{article}
+\else
+\documentclass[11pt,a4paper,pdftex]{article}
+\fi
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{pslatex}
+\usepackage{url}
+\usepackage{verbatim}
+
+\title{Translation from Coq V7 to V8}
+\author{The Coq Development Team}
+
+%% Macros etc.
+\catcode`\_=13
+\let\subscr=_
+\def_{\ifmmode\sb\else\subscr\fi}
+
+\def\NT#1{\langle\textit{#1}\rangle}
+\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
+\def\TERM#1{\textsf{\bf #1}}
+\newenvironment{transbox}
+  {\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline}
+  {\end{tabular}\end{center}}
+\def\TRANS#1#2
+  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
+   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} \\}
+\def\TRANSCOM#1#2#3
+  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
+   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} & #3 \\}
+
+%%
+\begin{document}
+\maketitle
+
+\section{Introduction}
+
+The goal of this document is to introduce to the new syntax of Coq on
+simple examples, rather than just giving the new grammar. It is
+strongly recommended to read first the definition of the new syntax
+(in the reference manual), but this document should also be useful for
+the eager user who wants to start with the new syntax quickly.
+
+\section{The new syntax on examples}
+
+The toplevel has an option {\tt -translate} which allows to
+interactively translate commands. All the examples below can be tested
+by entering the V7 commands in the toplevel launched this option. This
+toplevel translator accepts a command, prints the translation on
+standard output (after a \verb+New syntax:+ balise), executes the
+command, and waits for another command. The only requirements is that
+they should be syntactically correct, but they do not have to be
+well-typed.
+
+%%
+
+\subsection{Changes in lexical conventions w.r.t. V7}
+
+\subsubsection{Identifiers}
+
+The lexical conventions changed: \TERM{_} is not a regular identifier
+anymore. It is used in terms as a placeholder for subterms to be inferred
+at type-checking, and in patterns as a non-binding variable.
+
+Furthermore, only letters (unicode letters), digits, single quotes and
+_ are allowed after the first character.
+
+\subsubsection{Quoted string}
+
+Quoted strings are used typically to give a filename (which may not
+be a regular identifier). As before they are written between double
+quotes ("). Unlike for V7, there is no escape character: characters
+are written normaly but the double quote which is doubled.
+
+\subsection{Main changes in terms w.r.t. V7}
+
+
+\subsubsection{Precedence of application}
+
+In the new syntax, parentheses are not really part of the syntax of
+application. The precedence of application (10) is tighter than all
+prefix and infix notations. It makes it possible to remove parentheses
+in many contexts.
+
+\begin{transbox}
+\TRANS{(A x)->(f x)=(g y)}{A x -> f x = g y}
+\TRANS{(f [x]x)}{f (fun x => x)}
+\end{transbox}
+
+
+\subsubsection{Arithmetics and scopes}
+
+The specialized notation for \TERM{Z} and \TERM{R} (introduced by
+symbols \TERM{`} and \TERM{``}) have disappeared. They have been
+replaced by the general notion of scope.
+
+\begin{center}
+\begin{tabular}{l|l|l}
+type & scope name & delimiter \\
+\hline
+types & type_scope & \TERM{T} \\
+\TERM{bool} & bool_scope & \\
+\TERM{nat} & nat_scope & \TERM{nat} \\
+\TERM{Z} & Z_scope & \TERM{Z} \\
+\TERM{R} & R_scope & \TERM{R} \\
+\TERM{positive} & positive_scope & \TERM{P}
+\end{tabular}
+\end{center}
+
+In order to use notations of arithmetics on \TERM{Z}, its scope must be opened with command \verb+Open Scope Z_scope.+ Another possibility is using the scope change notation (\TERM{\%}). The latter notation is to be used when notations of several scopes appear in the same expression.
+
+In examples below, scope changes are not needed if the appropriate scope
+has been opened. Scope nat_scope is opened in the initial state of Coq.
+\begin{transbox}
+\TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}}
+\TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}}
+\TRANSCOM{(0)}{0}{\textrm{nat_scope}}
+\end{transbox}
+
+Below is a table that tells which notation is available in which
+scope. The relative precedences and associativity of operators is the
+same as in usual mathematics. See the reference manual for more
+details. However, it is important to remember that unlike V7, the type
+operators for product and sum are left associative, in order not to
+clash with arithmetic operators.
+
+\begin{center}
+\begin{tabular}{l|l}
+scope & notations \\
+\hline
+nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\
+Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\
+R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq$ \\
+type_scope & $* ~+$ \\
+bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\
+list_scope & $\TERM{::} ~\TERM{++}$
+\end{tabular}
+\end{center}
+(Note: $\leq$ is written \TERM{$<=$})
+
+
+
+\subsubsection{Notation for implicit arguments}
+
+The explicitation of arguments is closer to the \emph{bindings} notation in
+tactics. Argument positions follow the argument names of the head constant.
+
+\begin{transbox}
+\TRANS{f 1!t1 2!t2}{f (x:=t1) (y:=t2)}
+\TRANS{!f t1 t2}{@f t1 t2}
+\end{transbox}
+
+
+\subsubsection{Universal quantification}
+
+The universal quantification and dependent product types are now
+materialized with the \TERM{forall} keyword before the binders and a
+comma after the binders.
+
+The syntax of binders also changed significantly. A binder can simply be
+a name when its type can be inferred. In other cases, the name and the type
+of the variable are put between parentheses. When several consecutive
+variables have the same type, they can be grouped. Finally, if all variables
+have the same type parentheses can be omitted.
+
+\begin{transbox}
+\TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B}
+\TRANS{(x,y:nat)P}{forall (x y :~nat), P ~~\textrm{or}~~ forall x y :~nat, P}
+\TRANS{(x,y:nat;z:A)P}{forall (x y :~nat) (z:A), P}
+\TRANS{(x,y,z,t:?)P}{forall x y z t, P}
+\TRANS{(x,y:nat;z:?)P}{forall (x y :~nat) z, P}
+\end{transbox}
+
+\subsubsection{Abstraction}
+
+The notation for $\lambda$-abstraction follows that of universal
+quantification. The binders are surrounded by keyword \TERM{fun}
+and $\Rightarrow$ (\verb+=>+ in ascii).
+
+\begin{transbox}
+\TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c}
+\end{transbox}
+
+
+\subsubsection{Pattern-matching}
+
+Beside the usage of the keyword pair \TERM{match}/\TERM{with} instead of
+\TERM{Cases}/\TERM{of}, the main change is the notation for the type of
+branches and return type. It is no longer written between \TERM{$<$ $>$} before
+the \TERM{Cases} keyword, but interleaved with the destructured objects.
+
+The idea is that for each destructured object, one may specify a variable
+name to tell how the branches types depend on this destructured objects (case
+of a dependent elimination), and also how they depend on the value of the
+arguments of the inductive type of the destructured objects. The type of
+branches is then given after the keyword \TERM{return}, unless it can be
+inferred.
+
+Moreover, when the destructured object is a variable, one may use this
+variable in the return type.
+
+\begin{transbox}
+\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| (S k) => 1 end}
+\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| .. end}
+\TRANS{<[n:nat](P n)>Cases T of ... end}{match T as n return P n with ... end}
+\TRANS{<[n:nat][p:(even n)]\~{}(odd n)>Cases p of\\~~ ... \\end}{match p in even n return \~{} odd n with\\~~ ...\\end}
+\end{transbox}
+
+
+\subsubsection{Fixpoints and cofixpoints}
+
+An easier syntax for non-mutual fixpoints is provided, making it very close
+to the usual notation for non-recursive functions. The decreasing argument
+is now indicated by an annotation between curly braces, regardless of the
+binders grouping. The annotation can be omitted if the binders introduce only
+one variable. The type of the result can be omitted if inferable.
+
+\begin{transbox}
+\TRANS{Fix plus\{plus [n:nat] : nat -> nat :=\\~~ [m]...\}}{fix plus (n m:nat) \{struct n\}: nat := ...}
+\TRANS{Fix fact\{fact [n:nat]: nat :=\\
+~~Cases n of\\~~~~ O => (1) \\~~| (S k) => (mult n (fact k)) end\}}{fix fact
+  (n:nat) :=\\
+~~match n with \\~~~~0 => 1 \\~~| (S k) => n * fact k end}
+\end{transbox}
+
+There is a syntactic sugar for mutual fixpoints associated to a local
+definition:
+
+\begin{transbox}
+\TRANS{let f := Fix f \{f [x:A] : T := M\} in\\(g (f y))}{let fix f (x:A) : T := M in\\g (f x)}
+\end{transbox}
+
+The same applies to cofixpoints, annotations are not allowed in that case.
+
+\subsubsection{Notation for type cast}
+
+\begin{transbox}
+\TRANS{O :: nat}{0 : nat}
+\end{transbox}
+
+\section{Main changes in tactics w.r.t. V7}
+
+The main change is that all tactic names are lowercase. This also holds for
+Ltac keywords.
+
+\subsubsection{Ltac}
+
+Definitions of macros are introduced by \TERM{Ltac} instead of
+\TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive
+Definition}.
+
+Rules of a match command are not between square brackets anymore.
+
+Context (understand a term with a placeholder) instantiation \TERM{inst}
+became \TERM{context}. Syntax is unified with subterm matching.
+
+\begin{transbox}
+\TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]}
+\end{transbox}
+
+\subsubsection{Named arguments of theorems}
+
+\begin{transbox}
+\TRANS{Apply thm with x:=t 1:=u}{apply thm with (x:=t) (1:=u)}
+\end{transbox}
+
+
+\subsubsection{Occurrences}
+
+To avoid ambiguity between a numeric literal and the optionnal
+occurence numbers of this term, the occurence numbers are put after
+the term itself. This applies to tactic \TERM{pattern} and also
+\TERM{unfold}
+\begin{transbox}
+\TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern (f x at 1 2) (d at 3 4) y z}
+\end{transbox}
+
+
+\subsection{Main changes in vernacular commands w.r.t. V7}
+
+
+\subsubsection{Binders}
+
+The binders of vernacular commands changed in the same way as those of
+fixpoints. This also holds for parameters of inductive definitions.
+
+
+\begin{transbox}
+\TRANS{Definition x [a:A] : T := M}{Definition x (a:A) : T := M}
+\TRANS{Inductive and [A,B:Prop]: Prop := \\~~conj : A->B->(and A B)}%
+      {Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
+\end{transbox}
+
+\subsubsection{Hints}
+
+The syntax of \emph{extern} hints changed: the pattern and the tactic
+to be applied are separated by a \TERM{$\Rightarrow$}.
+\begin{transbox}
+\TRANS{Hint Extern 4 (toto ?) Apply lemma}{Hint Extern 4 (toto _) => apply lemma}
+\end{transbox}
+
+
+
+
+%% Doc of the translator
+\section{A guide to translation}
+
+\subsection{Overview of the translation process}
+
+Tools:
+\begin{itemize}
+\item {\tt coqc -translate}
+is the automatic translator. It is a parser/pretty-printer. This means
+that the translation is made by parsing using a parser of old syntax,
+and every command is printed using the new syntax. Many efforts were
+made to preserve as much as possible the quality of the presentation:
+it avoids expansion of syntax extensions, comments are not discarded
+and placed at the same place.
+\item {\tt tools/check-v8} will help translate developments that
+compile with a Makefile with minimum requirements.
+\end{itemize}
+
+\subsection{What to do before the translation}
+
+First of all, it is mandatory that files compile with the current
+version of Coq with option {\tt -v7}. Translation is a complicated
+task that involves the full compilation of the development. If your
+development was compiled with older versions, first upgrade to Coq V8
+with option {\tt -v7}. If you use a Makefile similar to those produced
+by {\tt coq\_makefile}, you probably just have to do
+
+{\tt make OPT="-opt -v7"} ~~~or~~~ {\tt make OPT="-byte -v7"}
+
+When the development compiles successfully, there are several changes
+that might be necessary for the translation. Essentially, this is
+about syntax extensions (see section below dedicated to porting syntax
+extensions). If you do not use such features, then you can try and
+make the translation.
+
+The preferred way is to use script {\tt check-v8} if your development
+is compiled by a Makfile with the following constraints:
+\begin{itemize}
+\item compilation is achievd by invoke make without arguments
+\item options are passed to Coq with make variable COQFLAGS that
+  includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
+\end{itemize}
+These constraints are met by the makefiles produced by {\tt coq\_makefile}
+
+Otherwise, modify your build program so as to pass option {\tt
+-translate} to program {\tt coqc}. The effect of this option is to
+ouptut the translated source of any {\tt .v} file in a file with
+extension {\tt .v8} located in the same directory than the original
+file.
+
+The following section describes events that may happen during the
+translation and measures to adopt.
+
+\subsection{What may happens during the translation}
+
+Warnings:
+
+...
+
+\subsection{Errors occurring after translation}
+
+Equality in {\tt Z} or {\tt R}...
+
+
+
+\subsection{Particular cases}
+
+\subsubsection{Lexical conventions}
+
+The definition of identifiers changed. Most of those changes are
+handled by the translator. They include:
+\begin{itemize}
+\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt
+x\_}
+\item avoid clash with new keywords by adding a trailing {\tt \_}
+\end{itemize}
+
+If the choices made by translation or in the following cases:
+\begin{itemize}
+\item usage of latin letters
+\item usage if iso-latin characters in notations
+\end{itemize}
+the user should change his development prior to translation.
+
+
+\subsubsection{Syntax extensions}
+
+\paragraph{Notation and Infix}
+
+These commands do not necessarily need to be changed.
+
+Some work will have to be done manually if the notation conflicts with
+the new syntax (for instance, using keywords like {\tt fun} or {\tt
+exists}, overloading of symbols of the old syntax).
+
+
+\paragraph{Grammar and Syntax}
+
+{\tt Grammar} and {\tt Syntax} are not supported by translation. They
+should be replaced by an equivalent {\tt Notation} command and be
+processed as decribed above. Before attempting translation, users
+should verify that compilation with option {\tt -v7} succeeds.
+
+In the cases where {\tt Grammar} and {\tt Syntax} cannot be emulated
+by {\tt Notation}, users have to change manually they development as
+they wish to avoid the use of {\tt Grammar}. If this is not done, the
+translator will simply expand the notations and the output of the
+translator will use the reuglar Coq syntax.
+
+
+\end{document}