1
\ifx\pdfoutput\undefined % si on est pas en pdflatex
2
\documentclass[11pt,a4paper]{article}
4
\documentclass[11pt,a4paper,pdftex]{article}
6
\usepackage[latin1]{inputenc}
7
\usepackage[T1]{fontenc}
16
\title{Translation from Coq V7 to V8}
17
\author{The Coq Development Team}
22
\def_{\ifmmode\sb\else\subscr\fi}
24
\def\NT#1{\langle\textit{#1}\rangle}
25
\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
26
%\def\TERM#1{\textsf{\bf #1}}
27
\def\TERM#1{\texttt{#1}}
28
\newenvironment{transbox}
29
{\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline}
30
{\end{tabular}\end{center}}
32
{\begin{tabular}[t]{@{}l@{}}#1\end{tabular} &
33
\begin{tabular}[t]{@{}l@{}}#2\end{tabular} \\}
35
{\begin{tabular}[t]{@{}l@{}}#1\end{tabular} &
36
\begin{tabular}[t]{@{}l@{}}#2\end{tabular} & #3 \\}
44
\section{Introduction}
46
Coq version 8.0 is a major version and carries major changes: the
47
concrete syntax was redesigned almost from scratch, and many notions
48
of the libraries were renamed for uniformisation purposes. We felt
49
that these changes could discourage users with large theories from
50
switching to the new version.
52
The goal of this document is to introduce these changes on simple
53
examples (mainly the syntactic changes), and describe the automated
54
tools to help moving to V8.0. Essentially, it consists of a translator
55
that takes as input a Coq source file in old syntax and produces a
56
file in new syntax and adapted to the new standard library. The main
57
extra features of this translator is that it keeps comments, even
58
those within expressions\footnote{The position of those comment might
59
differ slightly since there is no exact matching of positions between
62
The document is organised as follows: first section describes the new
63
syntax on simple examples. It is very translation-oriented. This
64
should give users of older versions the flavour of the new syntax, and
65
allow them to make translation manually on small
66
examples. Section~\ref{Translation} explains how the translation
67
process can be automatised for the most part (the boring one: applying
68
similar changes over thousands of lines of code). We strongly advise
69
users to follow these indications, in order to avoid many potential
70
complications of the translation process.
73
\section{The new syntax on examples}
75
The goal of this section is to introduce to the new syntax of Coq on
76
simple examples, rather than just giving the new grammar. It is
77
strongly recommended to read first the definition of the new syntax
78
(in the reference manual), but this document should also be useful for
79
the eager user who wants to start with the new syntax quickly.
81
The toplevel has an option {\tt -translate} which allows to
82
interactively translate commands. This toplevel translator accepts a
83
command, prints the translation on standard output (after a %
84
\verb+New syntax:+ balise), executes the command, and waits for another
85
command. The only requirements is that they should be syntactically
86
correct, but they do not have to be well-typed.
88
This interactive translator proved to be useful in two main
89
usages. First as a ``debugger'' of the translation. Before the
90
translation, it may help in spotting possible conflicts between the
91
new syntax and user notations. Or when the translation fails for some
92
reason, it makes it easy to find the exact reason why it failed and
93
make attempts in fixing the problem.
95
The second usage of the translator is when trying to make the first
96
proofs in new syntax. Well trained users will automatically think
97
their scripts in old syntax and might waste much time (and the
98
intuition of the proof) if they have to search the translation in a
99
document. Running a translator in the background will allow the user
100
to instantly have the answer.
102
The rest of this section is a description of all the aspects of the
103
syntax that changed and how they were translated. All the examples
104
below can be tested by entering the V7 commands in the toplevel
110
\subsection{Changes in lexical conventions w.r.t. V7}
112
\subsubsection{Identifiers}
114
The lexical conventions changed: \TERM{_} is not a regular identifier
115
anymore. It is used in terms as a placeholder for subterms to be inferred
116
at type-checking, and in patterns as a non-binding variable.
118
Furthermore, only letters (Unicode letters), digits, single quotes and
119
_ are allowed after the first character.
121
\subsubsection{Quoted string}
123
Quoted strings are used typically to give a filename (which may not
124
be a regular identifier). As before they are written between double
125
quotes ("). Unlike for V7, there is no escape character: characters
126
are written normally except the double quote which is doubled.
129
\TRANS{"abcd$\backslash\backslash$efg"}{"abcd$\backslash$efg"}
130
\TRANS{"abcd$\backslash$"efg"}{"abcd""efg"}
134
\subsection{Main changes in terms w.r.t. V7}
137
\subsubsection{Precedence of application}
139
In the new syntax, parentheses are not really part of the syntax of
140
application. The precedence of application (10) is tighter than all
141
prefix and infix notations. It makes it possible to remove parentheses
145
\TRANS{(A x)->(f x)=(g y)}{A x -> f x = g y}
146
\TRANS{(f [x]x)}{f (fun x => x)}
150
\subsubsection{Arithmetics and scopes}
152
The specialized notation for \TERM{Z} and \TERM{R} (introduced by
153
symbols \TERM{`} and \TERM{``}) have disappeared. They have been
154
replaced by the general notion of scope.
157
\begin{tabular}{l|l|l}
158
type & scope name & delimiter \\
160
types & type_scope & \TERM{type} \\
161
\TERM{bool} & bool_scope & \\
162
\TERM{nat} & nat_scope & \TERM{nat} \\
163
\TERM{Z} & Z_scope & \TERM{Z} \\
164
\TERM{R} & R_scope & \TERM{R} \\
165
\TERM{positive} & positive_scope & \TERM{P}
169
In order to use notations of arithmetics on \TERM{Z}, its scope must
170
be opened with command \verb+Open Scope Z_scope.+ Another possibility
171
is using the scope change notation (\TERM{\%}). The latter notation is
172
to be used when notations of several scopes appear in the same
175
In examples below, scope changes are not needed if the appropriate scope
176
has been opened. Scope \verb|nat_scope| is opened in the initial state of Coq.
178
\TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}}
179
\TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}}
180
\TRANSCOM{(0)}{0}{\textrm{nat_scope}}
183
Below is a table that tells which notation is available in which
184
scope. The relative precedences and associativity of operators is the
185
same as in usual mathematics. See the reference manual for more
186
details. However, it is important to remember that unlike V7, the type
187
operators for product and sum are left-associative, in order not to
188
clash with arithmetic operators.
194
nat_scope & \texttt{+ - * < <= > >=} \\
195
Z_scope & \texttt{+ - * / mod < <= > >= ?=} \\
196
R_scope & \texttt{+ - * / < <= > >=} \\
197
type_scope & \texttt{* +} \\
198
bool_scope & \texttt{\&\& || -} \\
199
list_scope & \texttt{:: ++}
205
\subsubsection{Notation for implicit arguments}
207
The explicitation of arguments is closer to the \emph{bindings}
208
notation in tactics. Argument positions follow the argument names of
209
the head constant. The example below assumes \verb+f+ is a function
210
with two implicit dependent arguments named \verb+x+ and \verb+y+.
212
\TRANS{f 1!t1 2!t2 t3}{f (x:=t1) (y:=t2) t3}
213
\TRANS{!f t1 t2}{@f t1 t2}
217
\subsubsection{Inferred subterms}
219
Subterms that can be automatically inferred by the type-checker is now
226
\subsubsection{Universal quantification}
228
The universal quantification and dependent product types are now
229
introduced by the \texttt{forall} keyword before the binders and a
230
comma after the binders.
232
The syntax of binders also changed significantly. A binder can simply be
233
a name when its type can be inferred. In other cases, the name and the type
234
of the variable are put between parentheses. When several consecutive
235
variables have the same type, they can be grouped. Finally, if all variables
236
have the same type, parentheses can be omitted.
239
\TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B}
240
\TRANS{(x,y:nat)P}{forall (x y :~nat), P ~~\textrm{or}~~ forall x y :~nat, P}
241
\TRANS{(x,y:nat;z:A)P}{forall (x y :~nat) (z:A), P}
242
\TRANS{(x,y,z,t:?)P}{forall x y z t, P}
243
\TRANS{(x,y:nat;z:?)P}{forall (x y :~nat) z, P}
246
\subsubsection{Abstraction}
248
The notation for $\lambda$-abstraction follows that of universal
249
quantification. The binders are surrounded by keyword \texttt{fun}
253
\TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c}
257
\subsubsection{Pattern-matching}
259
Beside the usage of the keyword pair \TERM{match}/\TERM{with} instead of
260
\TERM{Cases}/\TERM{of}, the main change is the notation for the type of
261
branches and return type. It is no longer written between \TERM{$<$ $>$} before
262
the \TERM{Cases} keyword, but interleaved with the destructured objects.
264
The idea is that for each destructured object, one may specify a
265
variable name (after the \TERM{as} keyword) to tell how the branches
266
types depend on this destructured objects (case of a dependent
267
elimination), and also how they depend on the value of the arguments
268
of the inductive type of the destructured objects (after the \TERM{in}
269
keyword). The type of branches is then given after the keyword
270
\TERM{return}, unless it can be inferred.
272
Moreover, when the destructured object is a variable, one may use this
273
variable in the return type.
276
\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| S k => 1 end}
277
\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| ... end}
278
\TRANS{<[n:nat](P n)>Cases T of ... end}{match T as n return P n with ... end}
279
\TRANS{<[n:nat][p:(even n)]\~{}(odd n)>Cases p of\\~~ ... \\end}{match p in even n return \~{} odd n with\\~~ ...\\end}
282
The annotations of the special pattern-matching operators
283
(\TERM{if}/\TERM{then}/\TERM{else}) and \TERM{let()} also changed. The
284
only restriction is that the destructuring \TERM{let} does not allow
285
dependent case analysis.
289
\begin{tabular}{@{}l}
290
<[n:nat;x:(I n)](P n x)>if t then t1 \\
293
{\begin{tabular}{@{}l}
294
if t as x in I n return P n x then t1 \\
297
\TRANS{<[n:nat](P n)>let (p,q) = t1 in t2}%
298
{let (p,q) in I n return P n := t1 in t2}
302
\subsubsection{Fixpoints and cofixpoints}
304
An simpler syntax for non-mutual fixpoints is provided, making it very close
305
to the usual notation for non-recursive functions. The decreasing argument
306
is now indicated by an annotation between curly braces, regardless of the
307
binders grouping. The annotation can be omitted if the binders introduce only
308
one variable. The type of the result can be omitted if inferable.
311
\TRANS{Fix plus\{plus [n:nat] : nat -> nat :=\\~~ [m]...\}}{fix plus (n m:nat) \{struct n\}: nat := ...}
312
\TRANS{Fix fact\{fact [n:nat]: nat :=\\
313
~~Cases n of\\~~~~ O => (1) \\~~| (S k) => (mult n (fact k)) end\}}{fix fact
315
~~match n with \\~~~~0 => 1 \\~~| (S k) => n * fact k end}
318
There is a syntactic sugar for single fixpoints (defining one
319
variable) associated to a local definition:
322
\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)}
325
The same applies to cofixpoints, annotations are not allowed in that case.
327
\subsubsection{Notation for type cast}
330
\TRANS{O :: nat}{0 : nat}
333
\subsection{Main changes in tactics w.r.t. V7}
335
The main change is that all tactic names are lowercase. This also holds for
338
\subsubsection{Renaming of induction tactics}
341
\TRANS{NewDestruct}{destruct}
342
\TRANS{NewInduction}{induction}
343
\TRANS{Induction}{simple induction}
344
\TRANS{Destruct}{simple destruct}
349
Definitions of macros are introduced by \TERM{Ltac} instead of
350
\TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive
351
Definition}. They are considered recursive by default.
354
\TRANS{Meta Definition my_tac t1 t2 := t1; t2.}%
355
{Ltac my_tac t1 t2 := t1; t2.}
358
Rules of a match command are not between square brackets anymore.
360
Context (understand a term with a placeholder) instantiation \TERM{inst}
361
became \TERM{context}. Syntax is unified with subterm matching.
364
\TRANS{Match t With [C[x=y]] -> Inst C[y=x]}%
365
{match t with context C[x=y] => context C[y=x] end}
368
Arguments of macros use the term syntax. If a general Ltac expression
369
is to be passed, it must be prefixed with ``{\tt ltac :}''. In other
370
cases, when a \'{} was necessary, it is replaced by ``{\tt constr :}''
373
\TRANS{my_tac '(S x)}{my_tac (S x)}
374
\TRANS{my_tac (Let x=tac In x)}{my_tac ltac:(let x:=tac in x)}
375
\TRANS{Let x = '[x](S (S x)) In Apply x}%
376
{let x := constr:(fun x => S (S x)) in apply x}
379
{\tt Match Context With} is now called {\tt match goal with}. Its
380
argument is an Ltac expression by default.
383
\subsubsection{Named arguments of theorems ({\em bindings})}
386
\TRANS{Apply thm with x:=t 1:=u}{apply thm with (x:=t) (1:=u)}
390
\subsubsection{Occurrences}
392
To avoid ambiguity between a numeric literal and the optional
393
occurrence numbers of this term, the occurrence numbers are put after
394
the term itself and after keyword \TERM{as}.
396
\TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern f x at 1 2, d at 3 4, y, z}
400
\subsubsection{{\tt LetTac} and {\tt Pose}}
402
Tactic {\tt LetTac} was renamed into {\tt set}, and tactic {\tt Pose}
403
was a particular case of {\tt LetTac} where the abbreviation is folded
404
in the conclusion\footnote{There is a tactic called {\tt pose} in V8,
405
but its behaviour is not to fold the abbreviation at all.}.
408
\TRANS{LetTac x = t in H}{set (x := t) in H}
409
\TRANS{Pose x := t}{set (x := t)}
412
{\tt LetTac} could be followed by a specification (called a clause) of
413
the places where the abbreviation had to be folded (hypothese and/or
414
conclusion). Clauses are the syntactic notion to denote in which parts
415
of a goal a given transformation shold occur. Its basic notation is
416
either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |-
417
\textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all
418
the hypotheses), or a comma-separated list of either hypothesis name,
419
or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences
420
can be specified after every hypothesis after the {\TERM{at}}
421
keyword. {\em concl} is either empty or \TERM{*}, and can be followed
425
\TRANS{in Goal}{in |- *}
426
\TRANS{in H H1}{in H1, H2 |-}
427
\TRANS{in H H1 ...}{in * |-}
428
\TRANS{in H H1 Goal}{in H1, H2 |- *}
429
\TRANS{in H H1 H2 ... Goal}{in *}
430
\TRANS{in 1 2 H 3 4 H0 1 3 Goal}{in H at 1 2, H0 at 3 4 |- * at 1 3}
433
\subsection{Main changes in vernacular commands w.r.t. V7}
436
\subsubsection{Require}
438
The default behaviour of {\tt Require} is not to open the loaded
442
\TRANS{Require Arith}{Require Import Arith}
445
\subsubsection{Binders}
447
The binders of vernacular commands changed in the same way as those of
448
fixpoints. This also holds for parameters of inductive definitions.
452
\TRANS{Definition x [a:A] : T := M}{Definition x (a:A) : T := M}
453
\TRANS{Inductive and [A,B:Prop]: Prop := \\~~conj : A->B->(and A B)}%
454
{Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
457
\subsubsection{Hints}
459
Both {\tt Hints} and {\tt Hint} commands are beginning with {\tt Hint}.
461
Command {\tt HintDestruct} has disappeared.
464
The syntax of \emph{Extern} hints changed: the pattern and the tactic
465
to be applied are separated by a {\tt =>}.
467
\TRANS{Hint name := Resolve (f ? x)}%
468
{Hint Resolve (f _ x)}
469
\TRANS{Hint name := Extern 4 (toto ?) Apply lemma}%
470
{Hint Extern 4 (toto _) => apply lemma}
471
\TRANS{Hints Resolve x y z}{Hint Resolve x y z}
472
\TRANS{Hints Resolve f : db1 db2}{Hint Resolve f : db1 db2}
473
\TRANS{Hints Immediate x y z}{Hint Immediate x y z}
474
\TRANS{Hints Unfold x y z}{Hint Unfold x y z}
475
%% \TRANS{\begin{tabular}{@{}l}
476
%% HintDestruct Local Conclusion \\
477
%% ~~name (f ? ?) 3 [Apply thm]
479
%% {\begin{tabular}{@{}l}
480
%% Hint Local Destuct name := \\
481
%% ~~3 Conclusion (f _ _) => apply thm
486
\subsubsection{Implicit arguments}
489
{\tt Set Implicit Arguments} changed its meaning in V8: the default is
490
to turn implicit only the arguments that are {\em strictly} implicit
491
(or rigid), i.e. that remains inferable whatever the other arguments
492
are. For instance {\tt x} inferable from {\tt P x} is not strictly
493
inferable since it can disappears if {\tt P} is instanciated by a term
494
which erases {\tt x}.
497
\TRANS{Set Implicit Arguments}%
499
Set Implicit Arguments. \\
500
Unset Strict Implicits.
504
However, you may wish to adopt the new semantics of {\tt Set Implicit
505
Arguments} (for instance because you think that the choice of
506
arguments it sets implicit is more ``natural'' for you).
509
\subsection{Changes in standard library}
511
Many lemmas had their named changed to improve uniformity. The user
512
generally do not have to care since the translators performs the
515
Type {\tt entier} from fast_integer.v is renamed into {\tt N} by the
516
translator. As a consequence, user-defined objects of same name {\tt N}
517
are systematically qualified even tough it may not be necessary. The
518
following table lists the main names with which the same problem
521
\TRANS{IF}{IF_then_else}
525
\TRANS{SUPERIEUR}{Gt}
527
\TRANS{INFERIEUR}{Lt}
529
\TRANS{true_sub}{Pminus}
531
\TRANS{Un_suivi_de}{Ndouble_plus_one}
532
\TRANS{Zero_suivi_de}{Ndouble}
538
\subsubsection{Implicit arguments}
541
Main definitions of standard library have now implicit
542
arguments. These arguments are dropped in the translated files. This
543
can exceptionally be a source of incompatibilities which has to be
544
solved by hand (it typically happens for polymorphic functions applied
545
to {\tt nil} or {\tt None}).
546
%% preciser: avant ou apres trad ?
548
\subsubsection{Logic about {\tt Type}}
550
Many notations that applied to {\tt Set} have been extended to {\tt
551
Type}, so several definitions in {\tt Type} are superseded by them.
555
\TRANS{(EXT x:Prop | Q)}{exists x:Prop, Q}
556
\TRANS{identityT}{identity}
561
%% Doc of the translator
562
\section{A guide to translation}
565
%%\subsection{Overview of the translation process}
567
Here is a short description of the tools involved in the translation process:
569
\item{\tt coqc -translate}
570
is the automatic translator. It is a parser/pretty-printer. This means
571
that the translation is made by parsing every command using a parser
572
of old syntax, which is printed using the new syntax. Many efforts
573
were made to preserve as much as possible of the quality of the
574
presentation: it avoids expansion of syntax extensions, comments are
575
not discarded and placed at the same place.
576
\item{\tt translate-v8} (in the translation package) is a small
577
shell-script that will help translate developments that compile with a
578
Makefile with minimum requirements.
581
\subsection{Preparation to translation}
583
This step is very important because most of work shall be done before
584
translation. If a problem occurs during translation, it often means
585
that you will have to modify the original source and restart the
586
translation process. This also means that it is recommended not to
587
edit the output of the translator since it would be overwritten if
588
the translation has to be restarted.
590
\subsubsection{Compilation with {\tt coqc -v7}}
592
First of all, it is mandatory that files compile with the current
593
version of Coq (8.0) with option {\tt -v7}. Translation is a
594
complicated task that involves the full compilation of the
595
development. If your development was compiled with older versions,
596
first upgrade to Coq V8.0 with option {\tt -v7}. If you use a Makefile
597
similar to those produced by {\tt coq\_makefile}, you probably just
600
{\tt make OPT="-opt -v7"} ~~~or~~~ {\tt make OPT="-byte -v7"}
602
When the development compiles successfully, there are several changes
603
that might be necessary for the translation. Essentially, this is
604
about syntax extensions (see section below dedicated to porting syntax
605
extensions). If you do not use such features, then you are ready to
606
try and make the translation.
608
\subsection{Translation}
610
\subsubsection{The general case}
612
The preferred way is to use script {\tt translate-v8} if your development
613
is compiled by a Makefile with the following constraints:
615
\item compilation is achieved by invoking make without specifying a target
616
\item options are passed to Coq with make variable COQFLAGS that
617
includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
619
These constraints are met by the makefiles produced by {\tt coq\_makefile}
621
Otherwise, modify your build program so as to pass option {\tt
622
-translate} to program {\tt coqc}. The effect of this option is to
623
ouptut the translated source of any {\tt .v} file in a file with
624
extension {\tt .v8} located in the same directory than the original
627
\subsubsection{What may happen during the translation}
629
This section describes events that may happen during the
630
translation and measures to adopt.
632
These are the warnings that may arise during the translation, but they
633
generally do not require any modification for the user:
636
\item {\tt Unable to detect if $id$ denotes a local definition}\\
637
This is due to a semantic change in clauses. In a command such as {\tt
638
simpl in H}, the old semantics were to perform simplification in the
639
type of {\tt H}, or in its body if it is defined. With the new
640
semantics, it is performed both in the type and the body (if any). It
641
might lead to incompatibilities
643
\item {\tt Forgetting obsolete module}\\
644
Some modules have disappeared in V8.0 (new syntax). The user does not
645
need to worry about it, since the translator deals with it.
647
\item {\tt Replacing obsolete module}\\
648
Same as before but with the module that were renamed. Here again, the
649
translator deals with it.
652
\subsection{Verification of the translation}
654
The shell-script {\tt translate-v8} also renames {\tt .v8} files into
655
{\tt .v} files (older {\tt .v} files are put in a subdirectory called
656
{\tt v7}) and tries to recompile them. To do so it invokes {\tt make}
657
without option (which should cause the compilation using {\tt coqc}
658
without particular option).
660
If compilation fails at this stage, you should refrain from repairing
661
errors manually on the new syntax, but rather modify the old syntax
662
script and restart the translation. We insist on that because the
663
problem encountered can show up in many instances (especially if the
664
problem comes from a syntactic extension), and fixing the original
665
sources (for instance the {\tt V8only} parts of notations) once will
666
solve all occurrences of the problem.
668
%%\subsubsection{Errors occurring after translation}
669
%%Equality in {\tt Z} or {\tt R}...
671
\subsection{Particular cases}
673
\subsubsection{Lexical conventions}
675
The definition of identifiers changed. Most of those changes are
676
handled by the translator. They include:
678
\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt
680
\item avoid clash with new keywords by adding a trailing {\tt \_}
683
If the choices made by translation is not satisfactory
684
or in the following cases:
686
\item use of latin letters
687
\item use of iso-latin characters in notations
689
the user should change his development prior to translation.
691
\subsubsection{{\tt Case} and {\tt Match}}
693
These very low-level case analysis are no longer supported. The
694
translator tries hard to translate them into a user-friendly one, but
695
it might lack type information to do so\footnote{The translator tries
696
to typecheck terms before printing them, but it is not always possible
697
to determine the context in which terms appearing in tactics
698
live.}. If this happens, it is preferable to transform it manually
701
\subsubsection{Syntax extensions with {\tt Grammar} and {\tt Syntax}}
704
{\tt Grammar} and {\tt Syntax} are no longer supported. They
705
should be replaced by an equivalent {\tt Notation} command and be
706
processed as described above. Before attempting translation, users
707
should verify that compilation with option {\tt -v7} succeeds.
709
In the cases where {\tt Grammar} and {\tt Syntax} cannot be emulated
710
by {\tt Notation}, users have to change manually they development as
711
they wish to avoid the use of {\tt Grammar}. If this is not done, the
712
translator will simply expand the notations and the output of the
713
translator will use the regular Coq syntax.
715
\subsubsection{Syntax extensions with {\tt Notation} and {\tt Infix}}
717
These commands do not necessarily need to be changed.
719
Some work will have to be done manually if the notation conflicts with
720
the new syntax (for instance, using keywords like {\tt fun} or {\tt
721
exists}, overloading of symbols of the old syntax, etc.) or if the
722
precedences are not right.
724
Precedence levels are now from 0 to 200. In V8, the precedence and
725
associativity of an operator cannot be redefined. Typical level are
726
(refer to the chapter on notations in the Reference Manual for the
730
\begin{tabular}{|cll|}
732
Notation & Precedence & Associativity \\
734
\verb!_ <-> _! & 95 & no \\
735
\verb!_ \/ _! & 85 & right \\
736
\verb!_ /\ _! & 80 & right \\
737
\verb!~ _! & 75 & right \\
738
\verb!_ = _!, \verb!_ <> _!, \verb!_ < _!, \verb!_ > _!,
739
\verb!_ <= _!, \verb!_ >= _! & 70 & no \\
740
\verb!_ + _!, \verb!_ - _! & 50 & left \\
741
\verb!_ * _!, \verb!_ / _! & 40 & left \\
742
\verb!- _! & 35 & right \\
743
\verb!_ ^ _! & 30 & left \\
749
By default, the translator keeps the associativity given in V7 while
750
the levels are mapped according to the following table:
753
\begin{tabular}{l|l|l}
754
V7 level & mapped to & associativity \\
770
If this is OK, just simply apply the translator.
773
\paragraph{Associativity conflict}
775
Since the associativity of the levels obtained by translating a V7
776
level (as shown on table above) cannot be changed, you have to choose
777
another level with a compatible associativity.
779
You can choose any level between 0 and 200, knowing that the
780
standard operators are already set at the levels shown on the list
783
Assume you have a notation
785
Infix NONA 2 "=_S" my_setoid_eq.
787
By default, the translator moves it to level 30 which is right
788
associative, hence a conflict with the expected no associativity.
790
To solve the problem, just add the "V8only" modifier to reset the
791
level and enforce the associativity as follows:
793
Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
795
The translator now knows that it has to translate "=_S" at level 70
796
with no associativity.
798
Remark: 70 is the "natural" level for relations, hence the choice of 70
799
here, but any other level accepting a no-associativity would have been
802
Second example: assume you have a notation
804
Infix RIGHTA 1 "o" my_comp.
806
By default, the translator moves it to level 20 which is left
807
associative, hence a conflict with the expected right associativity.
809
To solve the problem, just add the "V8only" modifier to reset the
810
level and enforce the associativity as follows:
812
Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
814
The translator now knows that it has to translate "o" at level 20
815
which has the correct "right associativity".
817
Remark: we assumed here that the user wants a strong precedence for
818
composition, in such a way, say, that "f o g + h" is parsed as
819
"(f o g) + h". To get "o" binding less than the arithmetical operators,
820
an appropriated level would have been close of 70, and below, e.g. 65.
823
\paragraph{Conflict: notation hides another notation}
825
Remark: use {\tt Print Grammar constr} in V8 to diagnose the overlap
826
and see the section on factorization in the chapter on notations of
827
the Reference Manual for hints on how to factorize.
831
Notation "{ x }" := (my_embedding x) (at level 1).
833
overlaps in V8 with notation \verb#{ x : A & P }# at level 0 and with
834
x at level 99. The conflicts can be solved by left-factorizing the
837
Notation "{ x }" := (my_embedding x) (at level 1)
838
V8only (at level 0, x at level 99).
841
\paragraph{Conflict: a notation conflicts with the V8 grammar}
843
Again, use the {\tt V8only} modifier to tell the translator to
844
automatically take in charge the new syntax.
850
Since {\tt @} is used in the new syntax for deactivating the implicit
851
arguments, another symbol has to be used, e.g. {\tt @@}. This is done via
852
the {\tt V8only} option as follows:
854
Infix 3 "@" app V8only "@@" (at level 40, left associativity).
858
Notation "x @ y" := (app x y) (at level 3, left associativity)
859
V8only "x @@ y" (at level 40, left associativity).
862
\paragraph{Conflict: my notation is already defined at another level
863
(or with another associativity)}
865
In V8, the level and associativity of a given notation can no longer
866
be changed. Then, either you adopt the standard reserved levels and
867
associativity for this notation (as given on the list above) or you
868
change your notation.
870
\item To change the notation, follow the directions in the previous
872
\item To adopt the standard level, just use {\tt V8only} without any
880
is not accepted as such in V8. Write
882
Infix 6 "*" my_mult V8only.
884
to tell the translator to use {\tt *} at the reserved level (i.e. 40
885
with left associativity). Even better, use interpretation scopes (look
886
at the Reference Manual).
889
\subsubsection{Strict implicit arguments}
891
In the case you want to adopt the new semantics of {\tt Set Implicit
892
Arguments} (only setting rigid arguments as implicit), add the option
893
{\tt -strict-implicit} to the translator.
895
Warning: changing the number of implicit arguments can break the
896
notations. Then use the {\tt V8only} modifier of {\tt Notation}.
added
removed
tools/Translator.tex
