diff options
Diffstat (limited to 'doc/tools/Translator.tex')
| -rw-r--r-- | doc/tools/Translator.tex | 898 |
1 files changed, 898 insertions, 0 deletions
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex new file mode 100644 index 00000000..005ca9c0 --- /dev/null +++ b/doc/tools/Translator.tex @@ -0,0 +1,898 @@ +\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}} +\def\TERM#1{\texttt{#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} + +Coq version 8.0 is a major version and carries major changes: the +concrete syntax was redesigned almost from scratch, and many notions +of the libraries were renamed for uniformisation purposes. We felt +that these changes could discourage users with large theories from +switching to the new version. + +The goal of this document is to introduce these changes on simple +examples (mainly the syntactic changes), and describe the automated +tools to help moving to V8.0. Essentially, it consists of a translator +that takes as input a Coq source file in old syntax and produces a +file in new syntax and adapted to the new standard library. The main +extra features of this translator is that it keeps comments, even +those within expressions\footnote{The position of those comment might +differ slightly since there is no exact matching of positions between +old and new syntax.}. + +The document is organised as follows: first section describes the new +syntax on simple examples. It is very translation-oriented. This +should give users of older versions the flavour of the new syntax, and +allow them to make translation manually on small +examples. Section~\ref{Translation} explains how the translation +process can be automatised for the most part (the boring one: applying +similar changes over thousands of lines of code). We strongly advise +users to follow these indications, in order to avoid many potential +complications of the translation process. + + +\section{The new syntax on examples} + +The goal of this section 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. + +The toplevel has an option {\tt -translate} which allows to +interactively translate commands. 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. + +This interactive translator proved to be useful in two main +usages. First as a ``debugger'' of the translation. Before the +translation, it may help in spotting possible conflicts between the +new syntax and user notations. Or when the translation fails for some +reason, it makes it easy to find the exact reason why it failed and +make attempts in fixing the problem. + +The second usage of the translator is when trying to make the first +proofs in new syntax. Well trained users will automatically think +their scripts in old syntax and might waste much time (and the +intuition of the proof) if they have to search the translation in a +document. Running a translator in the background will allow the user +to instantly have the answer. + +The rest of this section is a description of all the aspects of the +syntax that changed and how they were translated. All the examples +below can be tested by entering the V7 commands in the toplevel +translator. + + +%% + +\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 normally except the double quote which is doubled. + +\begin{transbox} +\TRANS{"abcd$\backslash\backslash$efg"}{"abcd$\backslash$efg"} +\TRANS{"abcd$\backslash$"efg"}{"abcd""efg"} +\end{transbox} + + +\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 \verb|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 & \texttt{+ - * < <= > >=} \\ +Z_scope & \texttt{+ - * / mod < <= > >= ?=} \\ +R_scope & \texttt{+ - * / < <= > >=} \\ +type_scope & \texttt{* +} \\ +bool_scope & \texttt{\&\& || -} \\ +list_scope & \texttt{:: ++} +\end{tabular} +\end{center} + + + +\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 two implicit dependent arguments named \verb+x+ and \verb+y+. +\begin{transbox} +\TRANS{f 1!t1 2!t2 t3}{f (x:=t1) (y:=t2) t3} +\TRANS{!f t1 t2}{@f t1 t2} +\end{transbox} + + +\subsubsection{Inferred subterms} + +Subterms that can be automatically inferred by the type-checker is now +written {\tt _} + +\begin{transbox} +\TRANS{?}{_} +\end{transbox} + +\subsubsection{Universal quantification} + +The universal quantification and dependent product types are now +introduced by the \texttt{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 \texttt{fun} +and \verb+=>+. + +\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 (after the \TERM{as} keyword) 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 (after the \TERM{in} +keyword). 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} + +The annotations of the special pattern-matching operators +(\TERM{if}/\TERM{then}/\TERM{else}) and \TERM{let()} also changed. The +only restriction is that the destructuring \TERM{let} does not allow +dependent case analysis. + +\begin{transbox} +\TRANS{ + \begin{tabular}{@{}l} + <[n:nat;x:(I n)](P n x)>if t then t1 \\ + else t2 + \end{tabular}}% +{\begin{tabular}{@{}l} + if t as x in I n return P n x then t1 \\ + else t2 + \end{tabular}} +\TRANS{<[n:nat](P n)>let (p,q) = t1 in t2}% +{let (p,q) in I n return P n := t1 in t2} +\end{transbox} + + +\subsubsection{Fixpoints and cofixpoints} + +An simpler 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{Renaming of induction tactics} + +\begin{transbox} +\TRANS{NewDestruct}{destruct} +\TRANS{NewInduction}{induction} +\TRANS{Induction}{simple induction} +\TRANS{Destruct}{simple destruct} +\end{transbox} + +\subsubsection{Ltac} + +Definitions of macros are introduced by \TERM{Ltac} instead of +\TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive +Definition}. They are considered recursive by default. + +\begin{transbox} +\TRANS{Meta Definition my_tac t1 t2 := t1; t2.}% +{Ltac my_tac t1 t2 := t1; t2.} +\end{transbox} + +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} +\end{transbox} + +Arguments of macros use the term syntax. If a general Ltac expression +is to be passed, it must be prefixed with ``{\tt ltac :}''. In other +cases, when a \'{} was necessary, it is replaced by ``{\tt constr :}'' + +\begin{transbox} +\TRANS{my_tac '(S x)}{my_tac (S x)} +\TRANS{my_tac (Let x=tac In x)}{my_tac ltac:(let x:=tac in x)} +\TRANS{Let x = '[x](S (S x)) In Apply x}% +{let x := constr:(fun x => S (S x)) in apply x} +\end{transbox} + +{\tt Match Context With} is now called {\tt match goal with}. Its +argument is an Ltac expression by default. + + +\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 optional +occurrence numbers of this term, the occurrence numbers are put after +the term itself and after keyword \TERM{as}. +\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} + + +\subsubsection{{\tt LetTac} and {\tt Pose}} + +Tactic {\tt LetTac} was renamed into {\tt set}, and tactic {\tt Pose} +was a particular case of {\tt LetTac} where the abbreviation is folded +in the conclusion\footnote{There is a tactic called {\tt pose} in V8, +but its behaviour is not to fold the abbreviation at all.}. + +\begin{transbox} +\TRANS{LetTac x = t in H}{set (x := t) in H} +\TRANS{Pose x := t}{set (x := t)} +\end{transbox} + +{\tt LetTac} could be followed by a specification (called a clause) of +the places where the abbreviation had to be folded (hypothese and/or +conclusion). Clauses are the syntactic notion to denote in which parts +of a goal a given transformation shold occur. Its basic notation is +either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |- +\textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all +the hypotheses), or a comma-separated list of either hypothesis name, +or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences +can be specified after every hypothesis after the {\TERM{at}} +keyword. {\em concl} is either empty or \TERM{*}, and can be followed +by occurences. + +\begin{transbox} +\TRANS{in Goal}{in |- *} +\TRANS{in H H1}{in H1, H2 |-} +\TRANS{in H H1 ...}{in * |-} +\TRANS{in H H1 Goal}{in H1, H2 |- *} +\TRANS{in H H1 H2 ... Goal}{in *} +\TRANS{in 1 2 H 3 4 H0 1 3 Goal}{in H at 1 2, H0 at 3 4 |- * at 1 3} +\end{transbox} + +\subsection{Main changes in vernacular commands w.r.t. V7} + + +\subsubsection{Require} + +The default behaviour of {\tt Require} is not to open the loaded +module. + +\begin{transbox} +\TRANS{Require Arith}{Require Import Arith} +\end{transbox} + +\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} + +Both {\tt Hints} and {\tt Hint} commands are beginning with {\tt Hint}. + +Command {\tt HintDestruct} has disappeared. + + +The syntax of \emph{Extern} hints changed: the pattern and the tactic +to be applied are separated by a {\tt =>}. +\begin{transbox} +\TRANS{Hint name := Resolve (f ? x)}% +{Hint Resolve (f _ x)} +\TRANS{Hint name := Extern 4 (toto ?) Apply lemma}% +{Hint Extern 4 (toto _) => apply lemma} +\TRANS{Hints Resolve x y z}{Hint Resolve x y z} +\TRANS{Hints Resolve f : db1 db2}{Hint Resolve f : db1 db2} +\TRANS{Hints Immediate x y z}{Hint Immediate x y z} +\TRANS{Hints Unfold x y z}{Hint Unfold x y z} +%% \TRANS{\begin{tabular}{@{}l} +%% HintDestruct Local Conclusion \\ +%% ~~name (f ? ?) 3 [Apply thm] +%% \end{tabular}}% +%% {\begin{tabular}{@{}l} +%% Hint Local Destuct name := \\ +%% ~~3 Conclusion (f _ _) => apply thm +%% \end{tabular}} +\end{transbox} + + +\subsubsection{Implicit arguments} + + +{\tt Set Implicit Arguments} changed its meaning in V8: the default is +to turn implicit only the arguments that are {\em strictly} implicit +(or rigid), i.e. that remains inferable whatever the other arguments +are. For instance {\tt x} inferable from {\tt P x} is not strictly +inferable since it can disappears if {\tt P} is instanciated by a term +which erases {\tt x}. + +\begin{transbox} +\TRANS{Set Implicit Arguments}% +{\begin{tabular}{l} + Set Implicit Arguments. \\ + Unset Strict Implicits. + \end{tabular}} +\end{transbox} + +However, you may wish to adopt the new semantics of {\tt Set Implicit +Arguments} (for instance because you think that the choice of +arguments it sets implicit is more ``natural'' for you). + + +\subsection{Changes in standard library} + +Many lemmas had their named changed to improve uniformity. The user +generally do not have to care since the translators performs the +renaming. + + Type {\tt entier} from fast_integer.v is renamed into {\tt N} by the +translator. As a consequence, user-defined objects of same name {\tt N} +are systematically qualified even tough it may not be necessary. The +following table lists the main names with which the same problem +arises: +\begin{transbox} +\TRANS{IF}{IF_then_else} +\TRANS{ZERO}{Z0} +\TRANS{POS}{Zpos} +\TRANS{NEG}{Zneg} +\TRANS{SUPERIEUR}{Gt} +\TRANS{EGAL}{Eq} +\TRANS{INFERIEUR}{Lt} +\TRANS{add}{Pplus} +\TRANS{true_sub}{Pminus} +\TRANS{entier}{N} +\TRANS{Un_suivi_de}{Ndouble_plus_one} +\TRANS{Zero_suivi_de}{Ndouble} +\TRANS{Nul}{N0} +\TRANS{Pos}{Npos} +\end{transbox} + + +\subsubsection{Implicit arguments} + +%% Hugo: +Main definitions of standard library have now implicit +arguments. These arguments are dropped in the translated files. This +can exceptionally be a source of incompatibilities which has to be +solved by hand (it typically happens for polymorphic functions applied +to {\tt nil} or {\tt None}). +%% preciser: avant ou apres trad ? + +\subsubsection{Logic about {\tt Type}} + +Many notations that applied to {\tt Set} have been extended to {\tt +Type}, so several definitions in {\tt Type} are superseded by them. + +\begin{transbox} +\TRANS{x==y}{x=y} +\TRANS{(EXT x:Prop | Q)}{exists x:Prop, Q} +\TRANS{identityT}{identity} +\end{transbox} + + + +%% Doc of the translator +\section{A guide to translation} +\label{Translation} + +%%\subsection{Overview of the translation process} + +Here is a short description of the tools involved in the translation process: +\begin{description} +\item{\tt coqc -translate} +is the automatic translator. It is a parser/pretty-printer. This means +that the translation is made by parsing every command using a parser +of old syntax, which is printed using the new syntax. Many efforts +were made to preserve as much as possible of the quality of the +presentation: it avoids expansion of syntax extensions, comments are +not discarded and placed at the same place. +\item{\tt translate-v8} (in the translation package) is a small +shell-script that will help translate developments that compile with a +Makefile with minimum requirements. +\end{description} + +\subsection{Preparation to translation} + +This step is very important because most of work shall be done before +translation. If a problem occurs during translation, it often means +that you will have to modify the original source and restart the +translation process. This also means that it is recommended not to +edit the output of the translator since it would be overwritten if +the translation has to be restarted. + +\subsubsection{Compilation with {\tt coqc -v7}} + +First of all, it is mandatory that files compile with the current +version of Coq (8.0) 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.0 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. + +\subsection{Translation} + +\subsubsection{The general case} + +The preferred way is to use script {\tt translate-v8} if your development +is compiled by a Makefile with the following constraints: +\begin{itemize} +\item compilation is achieved by invoking make without specifying a target +\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. + +\subsubsection{What may happen during the translation} + +This section describes events that may happen during the +translation and measures to adopt. + +These are the warnings that may arise during the translation, but they +generally do not require any modification for the user: +Warnings: +\begin{itemize} +\item {\tt Unable to detect if $id$ denotes a local definition}\\ +This is due to a semantic change in clauses. In a command such as {\tt +simpl in H}, the old semantics were to perform simplification in the +type of {\tt H}, or in its body if it is defined. With the new +semantics, it is performed both in the type and the body (if any). It +might lead to incompatibilities + +\item {\tt Forgetting obsolete module}\\ +Some modules have disappeared in V8.0 (new syntax). The user does not +need to worry about it, since the translator deals with it. + +\item {\tt Replacing obsolete module}\\ +Same as before but with the module that were renamed. Here again, the +translator deals with it. +\end{itemize} + +\subsection{Verification of the translation} + +The shell-script {\tt translate-v8} also renames {\tt .v8} files into +{\tt .v} files (older {\tt .v} files are put in a subdirectory called +{\tt v7}) and tries to recompile them. To do so it invokes {\tt make} +without option (which should cause the compilation using {\tt coqc} +without particular option). + +If compilation fails at this stage, you should refrain from repairing +errors manually on the new syntax, but rather modify the old syntax +script and restart the translation. We insist on that because the +problem encountered can show up in many instances (especially if the +problem comes from a syntactic extension), and fixing the original +sources (for instance the {\tt V8only} parts of notations) once will +solve all occurrences of the problem. + +%%\subsubsection{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 is not satisfactory +or in the following cases: +\begin{itemize} +\item use of latin letters +\item use of iso-latin characters in notations +\end{itemize} +the user should change his development prior to translation. + +\subsubsection{{\tt Case} and {\tt Match}} + +These very low-level case analysis are no longer supported. The +translator tries hard to translate them into a user-friendly one, but +it might lack type information to do so\footnote{The translator tries +to typecheck terms before printing them, but it is not always possible +to determine the context in which terms appearing in tactics +live.}. If this happens, it is preferable to transform it manually +before translation. + +\subsubsection{Syntax extensions with {\tt Grammar} and {\tt Syntax}} + + +{\tt Grammar} and {\tt Syntax} are no longer supported. They +should be replaced by an equivalent {\tt Notation} command and be +processed as described 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 regular Coq syntax. + +\subsubsection{Syntax extensions with {\tt Notation} and {\tt 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, etc.) or if the +precedences are not right. + + Precedence levels are now from 0 to 200. In V8, the precedence and +associativity of an operator cannot be redefined. Typical level are +(refer to the chapter on notations in the Reference Manual for the +full list): + +\begin{center} +\begin{tabular}{|cll|} +\hline +Notation & Precedence & Associativity \\ +\hline +\verb!_ <-> _! & 95 & no \\ +\verb!_ \/ _! & 85 & right \\ +\verb!_ /\ _! & 80 & right \\ +\verb!~ _! & 75 & right \\ +\verb!_ = _!, \verb!_ <> _!, \verb!_ < _!, \verb!_ > _!, + \verb!_ <= _!, \verb!_ >= _! & 70 & no \\ +\verb!_ + _!, \verb!_ - _! & 50 & left \\ +\verb!_ * _!, \verb!_ / _! & 40 & left \\ +\verb!- _! & 35 & right \\ +\verb!_ ^ _! & 30 & left \\ +\hline +\end{tabular} +\end{center} + + + By default, the translator keeps the associativity given in V7 while +the levels are mapped according to the following table: + +\begin{center} +\begin{tabular}{l|l|l} +V7 level & mapped to & associativity \\ +\hline +0 & 0 & no \\ +1 & 20 & left \\ +2 & 30 & right \\ +3 & 40 & left \\ +4 & 50 & left \\ +5 & 70 & no \\ +6 & 80 & right \\ +7 & 85 & right \\ +8 & 90 & right \\ +9 & 95 & no \\ +10 & 100 & left +\end{tabular} +\end{center} + +If this is OK, just simply apply the translator. + + +\paragraph{Associativity conflict} + + Since the associativity of the levels obtained by translating a V7 +level (as shown on table above) cannot be changed, you have to choose +another level with a compatible associativity. + + You can choose any level between 0 and 200, knowing that the +standard operators are already set at the levels shown on the list +above. + +Assume you have a notation +\begin{verbatim} +Infix NONA 2 "=_S" my_setoid_eq. +\end{verbatim} +By default, the translator moves it to level 30 which is right +associative, hence a conflict with the expected no associativity. + +To solve the problem, just add the "V8only" modifier to reset the +level and enforce the associativity as follows: +\begin{verbatim} +Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity). +\end{verbatim} +The translator now knows that it has to translate "=_S" at level 70 +with no associativity. + +Remark: 70 is the "natural" level for relations, hence the choice of 70 +here, but any other level accepting a no-associativity would have been +OK. + +Second example: assume you have a notation +\begin{verbatim} +Infix RIGHTA 1 "o" my_comp. +\end{verbatim} +By default, the translator moves it to level 20 which is left +associative, hence a conflict with the expected right associativity. + +To solve the problem, just add the "V8only" modifier to reset the +level and enforce the associativity as follows: +\begin{verbatim} +Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity). +\end{verbatim} +The translator now knows that it has to translate "o" at level 20 +which has the correct "right associativity". + +Remark: we assumed here that the user wants a strong precedence for +composition, in such a way, say, that "f o g + h" is parsed as +"(f o g) + h". To get "o" binding less than the arithmetical operators, +an appropriated level would have been close of 70, and below, e.g. 65. + + +\paragraph{Conflict: notation hides another notation} + +Remark: use {\tt Print Grammar constr} in V8 to diagnose the overlap +and see the section on factorization in the chapter on notations of +the Reference Manual for hints on how to factorize. + +Example: +\begin{verbatim} +Notation "{ x }" := (my_embedding x) (at level 1). +\end{verbatim} +overlaps in V8 with notation \verb#{ x : A & P }# at level 0 and with +x at level 99. The conflicts can be solved by left-factorizing the +notation as follows: +\begin{verbatim} +Notation "{ x }" := (my_embedding x) (at level 1) + V8only (at level 0, x at level 99). +\end{verbatim} + +\paragraph{Conflict: a notation conflicts with the V8 grammar} + +Again, use the {\tt V8only} modifier to tell the translator to +automatically take in charge the new syntax. + +Example: +\begin{verbatim} +Infix 3 "@" app. +\end{verbatim} +Since {\tt @} is used in the new syntax for deactivating the implicit +arguments, another symbol has to be used, e.g. {\tt @@}. This is done via +the {\tt V8only} option as follows: +\begin{verbatim} +Infix 3 "@" app V8only "@@" (at level 40, left associativity). +\end{verbatim} +or, alternatively by +\begin{verbatim} +Notation "x @ y" := (app x y) (at level 3, left associativity) + V8only "x @@ y" (at level 40, left associativity). +\end{verbatim} + +\paragraph{Conflict: my notation is already defined at another level + (or with another associativity)} + +In V8, the level and associativity of a given notation can no longer +be changed. Then, either you adopt the standard reserved levels and +associativity for this notation (as given on the list above) or you +change your notation. +\begin{itemize} +\item To change the notation, follow the directions in the previous +paragraph +\item To adopt the standard level, just use {\tt V8only} without any +argument. +\end{itemize} + +Example: +\begin{verbatim} +Infix 6 "*" my_mult. +\end{verbatim} +is not accepted as such in V8. Write +\begin{verbatim} +Infix 6 "*" my_mult V8only. +\end{verbatim} +to tell the translator to use {\tt *} at the reserved level (i.e. 40 +with left associativity). Even better, use interpretation scopes (look +at the Reference Manual). + + +\subsubsection{Strict implicit arguments} + +In the case you want to adopt the new semantics of {\tt Set Implicit + Arguments} (only setting rigid arguments as implicit), add the option +{\tt -strict-implicit} to the translator. + +Warning: changing the number of implicit arguments can break the +notations. Then use the {\tt V8only} modifier of {\tt Notation}. + +\end{document} |