summaryrefslogtreecommitdiff
path: root/doc/tools/Translator.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/Translator.tex')
-rw-r--r--doc/tools/Translator.tex898
1 files changed, 0 insertions, 898 deletions
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
deleted file mode 100644
index 005ca9c0..00000000
--- a/doc/tools/Translator.tex
+++ /dev/null
@@ -1,898 +0,0 @@
-\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}