2
How to use the translator
3
=========================
5
(temporary version to be included in the official
6
TeX document describing the translator)
8
The translator is a smart, robust and powerful tool to improve the
9
readibility of your script. The current document describes the
10
possibilities of the translator.
12
In case of problem recompiling the translated files, don't waste time
13
to modify the translated file by hand, read first the following
14
document telling on how to modify the original files to get a smooth
15
uniform safe translation. All 60000 lines of Coq lines on our
16
user-contributions server have been translated without any change
17
afterwards, and 0,5 % of the lines of the original files (mainly
18
notations) had to be modified beforehand to get this result.
24
1) Strict Implicit Arguments
25
2) Implicit Arguments in standard library
28
1) Translating a V7 notation as it was
29
2) Translating a V7 notation which conflicts with the new syntax
30
a) Associativity conflicts
31
b) Conflicts with other notations
32
b1) A notation hides another notation
33
b2) A notation conflicts with the V8 grammar
34
b3) My notation is already defined at another level
35
c) How to use V8only with Distfix ?
36
d) Can I overload a notation in V8, e.g. use "*" and "+" ?
37
3) Using the translator to have simplest notations
38
4) Setting the translator to automatically use new notations that
39
wasn't used in old syntax
40
5) Defining a construction and its notation simultaneously
44
2) Old "Case" and "Match"
45
3) Change of definition or theorem names
46
4) Change of tactic names
48
---------------------------------------------------------------------
53
1) Strict Implicit Arguments
55
"Set Implicit Arguments" changes its meaning in V8: the default is
56
to turn implicit only the arguments that are _strictly_ implicit (or
57
rigid), i.e. that remains inferable whatever the other arguments
58
are. E.g "x" inferable from "P x" is not strictly inferable since it
59
can disappears if "P" is instanciated by a term which erase "x".
61
To respect the old semantics, the default behaviour of the
62
translator is to replace each occurrence "Set Implicit Arguments" by
64
Set Implicit Arguments.
65
Unset Strict Implicits.
67
However, you may wish to adopt the new semantics of "Set Implicit
68
Arguments" (for instance because you think that the choice of
69
arguments it setsimplicit is more "natural" for you). In this case,
70
add the option -strict-implicit to the translator.
72
Warning: Changing the number of implicit arguments can break the
73
notations. Then use the V8only modifier of Notations.
75
2) Implicit Arguments in standard library
77
Main definitions of standard library have now implicit
78
arguments. These arguments are dropped in the translated files. This
79
can exceptionally be a source of incompatibilities which has to be
80
solved by hand (it typically happens for polymorphic functions applied
86
Grammar (on constr) and Syntax are no longer supported. Replace them by
87
Notation before translation.
89
Precedence levels are now from 0 to 200. In V8, the precedence and
90
associativity of an operator cannot be redefined. Typical level are
91
(refer to the chapter on notations in the Reference Manual for the
94
<-> : 95 (no associativity)
95
-> : 90 (right associativity)
96
\/ : 85 (right associativity)
97
/\ : 80 (right associativity)
98
~ : 75 (right associativity)
99
=, <, >, <=, >=, <> : 70 (no associativity)
100
+, - : 50 (left associativity)
101
*, / : 40 (left associativity)
102
^ : 30 (right associativity)
104
1) Translating a V7 notation as it was
106
By default, the translator keeps the associativity given in V7 while
107
the levels are mapped according to the following table:
109
the V7 levels [ 0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10]
110
are resp. mapped in V8 to [ 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
111
with predefined assoc [ No; L; R; L; L; No; R; R; R; No; L]
113
If this is OK for you, just simply apply the translator.
115
2) Translating a V7 notation which conflicts with the new syntax
117
a) Associativity conflict
119
Since the associativity of the levels obtained by translating a V7
120
level (as shown on table above) cannot be changed, you have to choose
121
another level with a compatible associativity.
123
You can choose any level between 0 and 200, knowing that the
124
standard operators are already set at the levels shown on the list
127
Example 1: Assume you have a notation
129
Infix NONA 2 "=_S" my_setoid_eq.
131
By default, the translator moves it to level 30 which is right
132
associative, hence a conflict with the expected no associativity.
134
To solve the problem, just add the "V8only" modifier to reset the
135
level and enforce the associativity as follows:
137
Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
139
The translator now knows that it has to translate "=_S" at level 70
140
with no associativity.
142
Rem: 70 is the "natural" level for relations, hence the choice of 70
143
here, but any other level accepting a no-associativity would have been
146
Example 2: Assume you have a notation
148
Infix RIGHTA 1 "o" my_comp.
150
By default, the translator moves it to level 20 which is left
151
associative, hence a conflict with the expected right associativity.
153
To solve the problem, just add the "V8only" modifier to reset the
154
level and enforce the associativity as follows:
156
Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
158
The translator now knows that it has to translate "o" at level 20
159
which has the correct "right associativity".
161
Rem: We assumed here that the user wants a strong precedence for
162
composition, in such a way, say, that "f o g + h" is parsed as
163
"(f o g) + h". To get "o" binding less than the arithmetical operators,
164
an appropriated level would have been close of 70, and below, e.g. 65.
166
b) Conflicts with other notations
168
Since the new syntax comes with new keywords and new predefined
169
symbols, new conflicts can occur. Again, you can use the option V8only
170
to inform the translator of the new syntax to use.
172
b1) A notation hides another notation
174
Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
175
section on factorization in the chapter on notations of the Reference
176
Manual for hints on how to factorize.
180
Notation "{ x }" := (my_embedding x) (at level 1).
182
overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
183
level 99. The conflicts can be solved by left-factorizing the notation
186
Notation "{ x }" := (my_embedding x) (at level 1)
187
V8only (at level 0, x at level 99).
189
b2) A notation conflicts with the V8 grammar.
191
Again, use the V8only modifier to tell the translator to automatically
192
take in charge the new syntax.
198
Since "@" is used in the new syntax for deactivating the implicit
199
arguments, another symbol has to be used, e.g. "@@". This is done via
200
the V8only option as follows:
202
Infix 3 "@" app V8only "@@" (at level 40, left associativity).
206
Notation "x @ y" := (app x y) (at level 3, left associativity)
207
V8only "x @@ y" (at level 40, left associativity).
209
b3) My notation is already defined at another level (or with another
212
In V8, the level and associativity of a given notation can no longer
213
be changed. Then, either you adopt the standard reserved levels and
214
associativity for this notation (as given on the list above) or you
215
change your notation.
217
- To change the notation, follow the directions in section b2.
219
- To adopt the standard level, just use V8only without any argument.
225
is not accepted as such in V8. Write
227
Infix 6 "*" my_mult V8only.
229
to tell the translator to use "*" at the reserved level (i.e. 40 with
230
left associativity). Even better, use interpretation scopes (look at
231
the Reference Manual).
233
c) How to use V8only with Distfix ?
235
You can't, use Notation instead of Distfix.
237
d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
238
algebraic operations ?
240
Yes, using interpretation scopes (see the corresponding chapter in the
243
3) Using the translator to have simplest notations
245
Thanks to the new syntax, * has now the expected left associativity,
246
and the symbols <, >, <= and >= are now available.
248
Thanks to the interpretation scopes, you can overload the
249
interpretation of these operators with the default interpretation
252
This may be a motivation to use the translator to automatically change
253
the notations while switching to the new syntax.
255
See sections b) and d) above for examples.
257
4) Setting the translator to automatically use new notations that
258
wasn't used in old syntax
260
Thanks to the "Notation" mechanism, defining symbolic notations is
261
simpler than in the previous versions of Coq.
263
Thanks to the new syntax and interpretation scopes, new symbols and
264
overloading is available.
266
This may be a motivation for using the translator to automatically change
267
the notations while switching to the new syntax.
269
Use for that the commands V8Notation and V8Infix.
273
V8Infix "==>" my_relation (at level 65, right associativity).
275
tells the translator to write an infix "==>" instead of my_relation in
276
the translated files.
280
tells the translator to write an infix ">=" instead of my_ge in the
281
translated files and that the level and associativity are the standard
282
one (as defined in the chart above).
284
V8Infix ">=" my_ge : my_scope.
286
tells the translator to write an infix ">=" instead of my_ge in the
287
translated files, that the level and associativity are the standard
288
one (as defined in the chart above), but only if scope my_scope is
289
open or if a delimiting key is available for "my_scope" (see the
292
5) Defining a construction and its notation simultaneously
294
This is permitted by the new syntax. Look at the Reference Manual for
295
explanation. The translator is not fully able to take this in charge...
297
III) Various pitfalls
302
The following identifiers are new keywords
304
"forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
305
"else"; "return"; "mod"; "at"; "let"; "_"; ".("
307
The translator automatically add a "_" to names clashing with a
308
keyword, except for files. Hence users may need to rename the files
309
whose name clashes with a keyword.
311
Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
312
were already keywords
314
2) Old "Case" and "Match"
316
"Case" and "Match" are normally automatically translated into
317
"match" or "match" and "fix", but sometimes it fails to do so. It
318
typically fails when the Case or Match is argument of a tactic whose
319
typing context is unknown because of a preceding Intro/Intros, as e.g. in
321
Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
323
The solution is then to replace the invocation of the sequence of
324
tactics into several invocation of the elementary tactics as follows
326
Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
329
3) Change of definition or theorem names
331
Type "entier" from fast_integer.v is renamed into "N" by the
332
translator. As a consequence, user-defined objects of same name "N"
333
are systematically qualified even tough it may not be necessary. The
334
same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
337
4) Change of tactics names
339
Since tactics names are now lowercase, this can clash with
340
user-defined tactic definitions. To pally this, clashing names are
341
renamed by adding an extra "_" to their name.
343
======================================================================
344
Main examples for new syntax
345
----------------------------
349
Applicative terms don't any longer require to be surrounded by parentheses as
352
"x = f y -> S x = S (f y)"
359
"forall (x y : T) z (v w : V), U"
362
Abstraction is written
366
"fun (x y : T) z (v w : V), U"
369
Pattern-matching is written
371
"match x with c1 x1 x2 => t | c2 y as z => u end"
372
"match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
373
"match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
374
c1 x1 x2, _ => t | c2 y, d z => u end"
376
The last example is the new form of what was written
378
"<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
379
(c1 x1 x2) _ => t | (c2 y) (d z) => u end"
381
Pattern-matching of type with one constructors and no dependencies
382
of the arguments in the resulting type can be written
384
"let (x,y,z) as u return P u := t in v"
386
Local fixpoints are written
388
"fix f (n m:nat) z (x : X) {struct m} : nat := ...
391
and "struct" tells which argument is structurally decreasing.
393
Explicitation of implicit arguments is written
400
The main change is that tactics names are now lowercase. Besides
401
this, the following renaming are applied:
403
"NewDestruct" -> "destruct"
404
"NewInduction" -> "induction"
405
"Induction" -> "simple induction"
406
"Destruct" -> "simple destruct"
408
For tactics with occurrences, the occurrences now comes after and
409
repeated use is separated by comma as in
411
"Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
412
"Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
413
"Simpl 1 3 e" -> "simpl e at 1 3"
417
Definitions are now introduced with keyword "Ltac" (instead of
418
"Tactic"/"Meta" "Definition") and are implicitly recursive
419
("Recursive" is no longer used).
421
The new rule for distinguishing terms from ltac expressions is:
423
Write "ltac:" in front of any tactic in argument position and
424
"constr:" in front of any construction in head position
426
4) Vernacular language
430
The syntax for commands is mainly unchanged. Declaration of
431
assumptions is now done as follows
435
Variables (m n : t) (u v : s) (w : r).
439
Definitions are done as follows
441
Definition f m n : t := ... .
442
Definition f m n := ... .
443
Definition f m n := ... : t.
444
Definition f (m n : u) : t := ... .
445
Definition f (m n : u) := ... : t.
446
Definition f (m n : u) := ... .
447
Definition f a b (p q : v) r s (m n : t) : t := ... .
448
Definition f a b (p q : v) r s (m n : t) := ... .
449
Definition f a b (p q : v) r s (m n : t) := ... : t.
453
Fixpoints are done this way
455
Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
456
Fixpoint f x : v := ... .
457
Fixpoint f (x : t) : v := ... .
459
It is possible to give a concrete notation to a fixpoint as follows
461
Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
469
The syntax for inductive types is as follows
471
Inductive t (a b : u) (d : e) : v :=
472
c1 : w1 | c2 : w2 | ... .
474
Inductive t (a b : u) (d : e) : v :=
475
c1 : w1 | c2 : w2 | ... .
477
Inductive t (a b : u) (d : e) : v :=
478
c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .
480
As seen in the last example, arguments of the constructors can be
481
given before the colon. If the type itself is omitted (allowed only in
482
case the inductive type has no real arguments), this yields an
483
ML-style notation as follows
485
Inductive nat : Set := O | S (n:nat).
486
Inductive bool : Set := true | false.
488
It is even possible to define a syntax at the same time, as follows:
490
Inductive or (A B:Prop) : Prop as "A \/ B":=
491
| or_introl (a:A) : A \/ B
492
| or_intror (b:B) : A \/ B.
494
Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
added
removed
dev/doc/translate.txt
