path: root/doc/Translator.tex

\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}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage{fullpage}

\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{type} \\
\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$ stands for \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. The example below assumes \verb+f+ is a function with 2
dependent arguments named \verb+x+ and \verb+y+, and a third
non-dependent argument.
\begin{transbox}
\TRANS{f 1!t1 2!t2 3!t3}{f (x:=t1) (y:=t2) (1:=t3)}
\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 single fixpoints (defining one
variable) 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}

\subsection{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 ({\em bindings})}

\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 and after keyword \TERM{as}. 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/translate-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 are ready to
try and make the translation.

The preferred way is to use script {\tt translate-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}