1
\chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}}
3
In this chapter, we introduce advanced commands to modify the way
4
{\Coq} parses and prints objects, i.e. the translations between the
5
concrete and internal representations of terms and commands. The main
6
commands are {\tt Notation} and {\tt Infix} which are described in
7
section \ref{Notation}. It also happens that the same symbolic
8
notation is expected in different contexts. To achieve this form of
9
overloading, {\Coq} offers a notion of interpretation scope. This is
10
described in Section~\ref{scopes}.
12
\Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which
13
were present for a while in {\Coq} are no longer available from {\Coq}
14
version 8.0. The underlying AST structure is also no longer available.
15
The functionalities of the command {\tt Syntactic Definition} are
16
still available, see Section~\ref{Abbreviations}.
18
\section[Notations]{Notations\label{Notation}
21
\subsection{Basic notations}
23
A {\em notation} is a symbolic abbreviation denoting some term
26
A typical notation is the use of the infix symbol \verb=/\= to denote
27
the logical conjunction (\texttt{and}). Such a notation is declared
31
Notation "A /\ B" := (and A B).
34
The expression \texttt{(and A B)} is the abbreviated term and the
35
string \verb="A /\ B"= (called a {\em notation}) tells how it is
38
A notation is always surrounded by double quotes (excepted when the
39
abbreviation is a single ident, see \ref{Abbreviations}). The
40
notation is composed of {\em tokens} separated by spaces. Identifiers
41
in the string (such as \texttt{A} and \texttt{B}) are the {\em
42
parameters} of the notation. They must occur at least once each in the
43
denoted term. The other elements of the string (such as \verb=/\=) are
46
An identifier can be used as a symbol but it must be surrounded by
47
simple quotes to avoid the confusion with a parameter. Similarly,
48
every symbol of at least 3 characters and starting with a simple quote
49
must be quoted (then it starts by two single quotes). Here is an example.
52
Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
55
%TODO quote the identifier when not in front, not a keyword, as in "x 'U' y" ?
57
A notation binds a syntactic expression to a term. Unless the parser
58
and pretty-printer of {\Coq} already know how to deal with the
59
syntactic expression (see \ref{ReservedNotation}), explicit precedences and
60
associativity rules have to be given.
62
\subsection[Precedences and associativity]{Precedences and associativity\index{Precedences}
63
\index{Associativity}}
65
Mixing different symbolic notations in a same text may cause serious
66
parsing ambiguity. To deal with the ambiguity of notations, {\Coq}
67
uses precedence levels ranging from 0 to 100 (plus one extra level
68
numbered 200) and associativity rules.
70
Consider for example the new notation
73
Notation "A \/ B" := (or A B).
76
Clearly, an expression such as {\tt forall A:Prop, True \verb=/\= A \verb=\/=
77
A \verb=\/= False} is ambiguous. To tell the {\Coq} parser how to
78
interpret the expression, a priority between the symbols \verb=/\= and
79
\verb=\/= has to be given. Assume for instance that we want conjunction
80
to bind more than disjunction. This is expressed by assigning a
81
precedence level to each notation, knowing that a lower level binds
82
more than a higher level. Hence the level for disjunction must be
83
higher than the level for conjunction.
85
Since connectives are the less tight articulation points of a text, it
86
is reasonable to choose levels not so far from the higher level which
87
is 100, for example 85 for disjunction and 80 for
88
conjunction\footnote{which are the levels effectively chosen in the
89
current implementation of {\Coq}}.
91
Similarly, an associativity is needed to decide whether {\tt True \verb=/\=
92
False \verb=/\= False} defaults to {\tt True \verb=/\= (False
93
\verb=/\= False)} (right associativity) or to {\tt (True
94
\verb=/\= False) \verb=/\= False} (left associativity). We may
95
even consider that the expression is not well-formed and that
96
parentheses are mandatory (this is a ``no associativity'')\footnote{
97
{\Coq} accepts notations declared as no associative but the parser on
98
which {\Coq} is built, namely {\camlpppp}, currently does not implement the
99
no-associativity and replace it by a left associativity; hence it is
100
the same for {\Coq}: no-associativity is in fact left associativity}.
101
We don't know of a special convention of the associativity of
102
disjunction and conjunction, let's apply for instance a right
103
associativity (which is the choice of {\Coq}).
105
Precedence levels and associativity rules of notations have to be
106
given between parentheses in a list of modifiers that the
107
\texttt{Notation} command understands. Here is how the previous
111
Notation "A /\ B" := (and A B) (at level 80, right associativity).
112
Notation "A \/ B" := (or A B) (at level 85, right associativity).
115
By default, a notation is considered non associative, but the
116
precedence level is mandatory (except for special cases whose level is
117
canonical). The level is either a number or the mention {\tt next
118
level} whose meaning is obvious. The list of levels already assigned
119
is on Figure~\ref{init-notations}.
121
\subsection{Complex notations}
123
Notations can be made from arbitraly complex symbols. One can for
124
instance define prefix notations.
127
Notation "~ x" := (not x) (at level 75, right associativity).
130
One can also define notations for incomplete terms, with the hole
131
expected to be inferred at typing time.
134
Notation "x = y" := (@eq _ x y) (at level 70, no associativity).
137
One can define {\em closed} notations whose both sides are symbols. In
138
this case, the default precedence level for inner subexpression is 200.
141
Set Printing Depth 50.
142
(********** The following is correct but produces **********)
143
(**** an incompatibility with the reserved notation ********)
146
Notation "( x , y )" := (@pair _ _ x y) (at level 0).
149
One can also define notations for binders.
152
Set Printing Depth 50.
153
(********** The following is correct but produces **********)
154
(**** an incompatibility with the reserved notation ********)
157
Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0).
160
In the last case though, there is a conflict with the notation for
161
type casts. This last notation, as shown by the command {\tt Print Grammar
162
constr} is at level 100. To avoid \verb=x : A= being parsed as a type cast,
163
it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a
164
correct definition is
167
Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99).
170
%This change has retrospectively an effect on the notation for notation
171
%{\tt "{ A } + { B }"}. For the sake of factorization, {\tt A} must be
172
%put at level 99 too, which gives
174
%\begin{coq_example*}
175
%Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99).
178
See the next section for more about factorization.
180
\subsection{Simple factorization rules}
182
{\Coq} extensible parsing is performed by Camlp5 which is essentially a
183
LL1 parser. Hence, some care has to be taken not to hide already
184
existing rules by new rules. Some simple left factorization work has
185
to be done. Here is an example.
188
(********** The next rule for notation _ < _ < _ produces **********)
189
(*** Error: Notation _ < _ < _ is already defined at level 70 ... ***)
192
Notation "x < y" := (lt x y) (at level 70).
193
Notation "x < y < z" := (x < y /\ y < z) (at level 70).
196
In order to factorize the left part of the rules, the subexpression
197
referred by {\tt y} has to be at the same level in both rules. However
198
the default behavior puts {\tt y} at the next level below 70
199
in the first rule (no associativity is the default), and at the level
200
200 in the second rule (level 200 is the default for inner expressions).
201
To fix this, we need to force the parsing level of {\tt y},
205
Notation "x < y" := (lt x y) (at level 70).
206
Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
209
For the sake of factorization with {\Coq} predefined rules, simple
210
rules have to be observed for notations starting with a symbol:
211
e.g. rules starting with ``\{'' or ``('' should be put at level 0. The
212
list of {\Coq} predefined notations can be found in Chapter~\ref{Theories}.
214
The command to display the current state of the {\Coq} term parser is
215
\comindex{Print Grammar constr}
218
\tt Print Grammar constr.
223
\comindex{Print Grammar pattern}
224
{\tt Print Grammar pattern.}\\
226
This displays the state of the subparser of patterns (the parser
227
used in the grammar of the {\tt match} {\tt with} constructions).
229
\subsection{Displaying symbolic notations}
231
The command \texttt{Notation} has an effect both on the {\Coq} parser and
232
on the {\Coq} printer. For example:
235
Check (and True True).
238
However, printing, especially pretty-printing, requires
239
more care than parsing. We may want specific indentations,
240
line breaks, alignment if on several lines, etc.
242
The default printing of notations is very rudimentary. For printing a
243
notation, a {\em formatting box} is opened in such a way that if the
244
notation and its arguments cannot fit on a single line, a line break
245
is inserted before the symbols of the notation and the arguments on
246
the next lines are aligned with the argument on the first line.
248
A first, simple control that a user can have on the printing of a
249
notation is the insertion of spaces at some places of the
250
notation. This is performed by adding extra spaces between the symbols
251
and parameters: each extra space (other than the single space needed
252
to separate the components) is interpreted as a space to be inserted
253
by the printer. Here is an example showing how to add spaces around
254
the bar of the notation.
257
Notation "{{ x : A | P }}" := (sig (fun x : A => P))
258
(at level 0, x at level 99).
259
Check (sig (fun x : nat => x=x)).
262
The second, more powerful control on printing is by using the {\tt
263
format} modifier. Here is an example
267
Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
268
(at level 200, right associativity, format
269
"'[v ' 'If' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'").
273
A {\em format} is an extension of the string denoting the notation with
274
the possible following elements delimited by single quotes:
277
\item extra spaces are translated into simple spaces
278
\item tokens of the form \verb='/ '= are translated into breaking point,
279
in case a line break occurs, an indentation of the number of spaces
280
after the ``\verb=/='' is applied (2 spaces in the given example)
281
\item token of the form \verb='//'= force writing on a new line
282
\item well-bracketed pairs of tokens of the form \verb='[ '= and \verb=']'=
283
are translated into printing boxes; in case a line break occurs,
284
an extra indentation of the number of spaces given after the ``\verb=[=''
285
is applied (4 spaces in the example)
286
\item well-bracketed pairs of tokens of the form \verb='[hv '= and \verb=']'=
287
are translated into horizontal-orelse-vertical printing boxes;
288
if the content of the box does not fit on a single line, then every breaking
289
point forces a newline and an extra indentation of the number of spaces
290
given after the ``\verb=[='' is applied at the beginning of each newline
291
(3 spaces in the example)
292
\item well-bracketed pairs of tokens of the form \verb='[v '= and
293
\verb=']'= are translated into vertical printing boxes; every
294
breaking point forces a newline, even if the line is large enough to
295
display the whole content of the box, and an extra indentation of the
296
number of spaces given after the ``\verb=[='' is applied at the beginning
300
Thus, for the previous example, we get
301
%\footnote{The ``@'' is here to shunt
302
%the notation "'IF' A 'then' B 'else' C" which is defined in {\Coq}
305
Notations do not survive the end of sections. No typing of the denoted
306
expression is performed at definition time. Type-checking is done only
307
at the time of use of the notation.
311
(IF_then_else (IF_then_else True False True)
312
(IF_then_else True False True)
313
(IF_then_else True False True)).
317
Sometimes, a notation is expected only for the parser.
319
%the underlying parser of {\Coq}, namely {\camlpppp}, is LL1 and some extra
320
%rules are needed to circumvent the absence of factorization).
321
To do so, the option {\em only parsing} is allowed in the list of modifiers of
324
\subsection{The \texttt{Infix} command
327
The \texttt{Infix} command is a shortening for declaring notations of
328
infix symbols. Its syntax is
331
\noindent\texttt{Infix "{\symbolentry}" :=} {\qualid} {\tt (} \nelist{\em modifier}{,} {\tt )}.
334
and it is equivalent to
337
\noindent\texttt{Notation "x {\symbolentry} y" := ({\qualid} x y) (} \nelist{\em modifier}{,} {\tt )}.
340
where {\tt x} and {\tt y} are fresh names distinct from {\qualid}. Here is an example.
343
Infix "/\" := and (at level 80, right associativity).
346
\subsection{Reserving notations
347
\label{ReservedNotation}
348
\comindex{ReservedNotation}}
350
A given notation may be used in different contexts. {\Coq} expects all
351
uses of the notation to be defined at the same precedence and with the
352
same associativity. To avoid giving the precedence and associativity
353
every time, it is possible to declare a parsing rule in advance
354
without giving its interpretation. Here is an example from the initial
358
Reserved Notation "x = y" (at level 70, no associativity).
361
Reserving a notation is also useful for simultaneously defined an
362
inductive type or a recursive constant and a notation for it.
364
\Rem The notations mentioned on Figure~\ref{init-notations} are
365
reserved. Hence their precedence and associativity cannot be changed.
367
\subsection{Simultaneous definition of terms and notations
368
\comindex{Fixpoint {\ldots} where {\ldots}}
369
\comindex{CoFixpoint {\ldots} where {\ldots}}
370
\comindex{Inductive {\ldots} where {\ldots}}}
372
Thanks to reserved notations, the inductive, coinductive, recursive
373
and corecursive definitions can benefit of customized notations. To do
374
this, insert a {\tt where} notation clause after the definition of the
375
(co)inductive type or (co)recursive term (or after the definition of
376
each of them in case of mutual definitions). The exact syntax is given
377
on Figure~\ref{notation-syntax}. Here are examples:
380
Set Printing Depth 50.
381
(********** The following is correct but produces an error **********)
382
(********** because the symbol /\ is already bound **********)
383
(**** Error: The conclusion of A -> B -> A /\ B is not valid *****)
387
Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B
388
where "A /\ B" := (and A B).
392
Set Printing Depth 50.
393
(********** The following is correct but produces an error **********)
394
(********** because the symbol + is already bound **********)
395
(**** Error: no recursive definition *****)
399
Fixpoint plus (n m:nat) {struct n} : nat :=
404
where "n + m" := (plus n m).
407
\subsection{Displaying informations about notations
408
\comindex{Set Printing Notations}
409
\comindex{Unset Printing Notations}}
411
To deactivate the printing of all notations, use the command
413
\tt Unset Printing Notations.
415
To reactivate it, use the command
417
\tt Set Printing Notations.
419
The default is to use notations for printing terms wherever possible.
421
\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}.
423
\subsection{Locating notations
425
\label{LocateSymbol}}
427
To know to which notations a given symbol belongs to, use the command
429
\tt Locate {\symbolentry}
431
where symbol is any (composite) symbol surrounded by quotes. To locate
432
a particular notation, use a string where the variables of the
433
notation are replaced by ``\_''.
438
Locate "'exists' _ , _".
441
\SeeAlso Section \ref{Locate}.
448
\zeroone{\tt Local} \texttt{Notation} {\str} \texttt{:=} {\term}
449
\zeroone{\modifiers} \zeroone{:{\scope}} .\\
451
\zeroone{\tt Local} \texttt{Infix} {\str} \texttt{:=} {\qualid}
452
\zeroone{\modifiers} \zeroone{:{\scope}} .\\
454
\zeroone{\tt Local} \texttt{Reserved Notation} {\str}
455
\zeroone{\modifiers} .\\
456
& $|$ & {\tt Inductive}
457
\nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
458
& $|$ & {\tt CoInductive}
459
\nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
460
& $|$ & {\tt Fixpoint}
461
\nelist{{\fixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
462
& $|$ & {\tt CoFixpoint}
463
\nelist{{\cofixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
465
{\declnotation} & ::= &
466
\zeroone{{\tt where} {\str} {\tt :=} {\term} \zeroone{:{\scope}}} .
470
& ::= & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \\
471
& $|$ & \nelist{\ident}{,} {\tt at next level} \\
472
& $|$ & {\tt at level} {\naturalnumber} \\
473
& $|$ & {\tt left associativity} \\
474
& $|$ & {\tt right associativity} \\
475
& $|$ & {\tt no associativity} \\
476
& $|$ & {\ident} {\tt ident} \\
477
& $|$ & {\ident} {\tt global} \\
478
& $|$ & {\ident} {\tt bigint} \\
479
& $|$ & {\tt only parsing} \\
480
& $|$ & {\tt format} {\str}
484
\caption{Syntax of the variants of {\tt Notation}}
485
\label{notation-syntax}
488
\subsection{Notations with recursive patterns}
490
An experimental mechanism is provided for declaring elementary
491
notations including recursive patterns. The basic syntax is
498
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
501
On the right-hand-side, an extra construction of the form {\tt ..} ($f$
502
$t_1$ $\ldots$ $t_n$) {\tt ..} can be used. Notice that {\tt ..} is part of
503
the {\Coq} syntax while $\ldots$ is just a meta-notation of this
504
manual to denote a sequence of terms of arbitrary size.
506
This extra construction enclosed within {\tt ..}, let's call it $t$,
507
must be one of the argument of an applicative term of the form {\tt
508
($f$ $u_1$ $\ldots$ $u_n$)}. The sequences $t_1$ $\ldots$ $t_n$ and
509
$u_1$ $\ldots$ $u_n$ must coincide everywhere but in two places. In
510
one place, say the terms of indice $i$, we must have $u_i = t$. In the
511
other place, say the terms of indice $j$, both $u_j$ and $t_j$ must be
512
variables, say $x$ and $y$ which are bound by the notation string on
513
the left-hand-side of the declaration. The variables $x$ and $y$ in
514
the string must occur in a substring of the form "$x$ $s$ {\tt ..} $s$
515
$y$" where {\tt ..} is part of the syntax and $s$ is two times the
516
same sequence of terminal symbols (i.e. symbols which are not
519
These invariants must be satisfied in order the notation to be
520
correct. The term $t_i$ is the {\em terminating} expression of
521
the notation and the pattern {\tt ($f$ $u_1$ $\ldots$ $u_{i-1}$ {\rm [I]}
522
$u_{i+1}$ $\ldots$ $u_{j-1}$ {\rm [E]} $u_{j+1}$ $\ldots$ $u_{n}$)} is the
523
{\em iterating pattern}. The hole [I] is the {\em iterative} place
524
and the hole [E] is the {\em enumerating} place. Remark that if $j<i$, the
525
iterative place comes after the enumerating place accordingly.
527
The notation parses sequences of tokens such that the subpart "$x$ $s$
528
{\tt ..} $s$ $y$" parses any number of time (but at least one time) a
529
sequence of expressions separated by the sequence of tokens $s$. The
530
parsing phase produces a list of expressions which
531
are used to fill in order the holes [E] of the iterating pattern
532
which is nested as many time as the length of the list, the hole [I]
533
being the nesting point. In the innermost occurrence of the nested
534
iterating pattern, the hole [I] is finally filled with the terminating
537
In the example above, $f$ is {\tt cons}, $n=3$ (because {\tt cons} has
538
a hidden implicit argument!), $i=3$ and $j=2$. The {\em terminating}
539
expression is {\tt nil} and the {\em iterating pattern} is {\tt cons
540
{\rm [E] [I]}}. Finally, the sequence $s$ is made of the single token
541
``{\tt ;}''. Here is another example.
543
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
546
Notations with recursive patterns can be reserved like standard
547
notations, they can also be declared within interpretation scopes (see
548
section \ref{scopes}).
550
\subsection{Notations and binders}
552
Notations can be defined for binders as in the example:
555
Set Printing Depth 50.
556
(********** The following is correct but produces **********)
557
(**** an incompatibility with the reserved notation ********)
560
Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0).
563
The binding variables in the left-hand-side that occur as a parameter
564
of the notation naturally bind all their occurrences appearing in
565
their respective scope after instantiation of the parameters of the
568
Contrastingly, the binding variables that are not a parameter of the
569
notation do not capture the variables of same name that
570
could appear in their scope after instantiation of the
571
notation. E.g., for the notation
574
Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200).
576
the next command fails because {\tt p} does not bind in
577
the instance of {\tt n}.
579
Set Printing Depth 50.
580
(********** The following produces **********)
581
(**** The reference p was not found in the current environment ********)
584
Check (exists_different p).
587
\Rem Binding variables must not necessarily be parsed using the
588
{\tt ident} entry. For factorization purposes, they can be said to be
589
parsed at another level (e.g. {\tt x} in \verb="{ x : A | P }"= must be
590
parsed at level 99 to be factorized with the notation
591
\verb="{ A } + { B }"= for which {\tt A} can be any term).
592
However, even if parsed as a term, this term must at the end be effectively
597
\paragraph{Syntax of notations}
599
The different syntactic variants of the command \texttt{Notation} are
600
given on Figure~\ref{notation-syntax}. The optional {\tt :{\scope}} is
601
described in the Section~\ref{scopes}.
603
\Rem No typing of the denoted expression is performed at definition
604
time. Type-checking is done only at the time of use of the notation.
606
\Rem Many examples of {\tt Notation} may be found in the files
607
composing the initial state of {\Coq} (see directory {\tt
608
\$COQLIB/theories/Init}).
610
\Rem The notation \verb="{ x }"= has a special status in such a way
611
that complex notations of the form \verb="x + { y }"= or
612
\verb="x * { y }"= can be nested with correct precedences. Especially,
613
every notation involving a pattern of the form \verb="{ x }"= is
614
parsed as a notation where the pattern \verb="{ x }"= has been simply
615
replaced by \verb="x"= and the curly brackets are parsed separately.
616
E.g. \verb="y + { z }"= is not parsed as a term of the given form but
617
as a term of the form \verb="y + z"= where \verb=z= has been parsed
618
using the rule parsing \verb="{ x }"=. Especially, level and
619
precedences for a rule including patterns of the form \verb="{ x }"=
620
are relative not to the textual notation but to the notation where the
621
curly brackets have been removed (e.g. the level and the associativity
622
given to some notation, say \verb="{ y } & { z }"= in fact applies to
623
the underlying \verb="{ x }"=-free rule which is \verb="y & z"=).
625
\paragraph{Persistence of notations}
627
Notations do not survive the end of sections. They survive modules
628
unless the command {\tt Local Notation} is used instead of {\tt
631
\section[Interpretation scopes]{Interpretation scopes\index{Interpretation scopes}
635
An {\em interpretation scope} is a set of notations for terms with
636
their interpretation. Interpretation scopes provides with a weak,
637
purely syntactical form of notations overloading: a same notation, for
638
instance the infix symbol \verb=+= can be used to denote distinct
639
definitions of an additive operator. Depending on which interpretation
640
scopes is currently open, the interpretation is different.
641
Interpretation scopes can include an interpretation for
642
numerals and strings. However, this is only made possible at the
645
See Figure \ref{notation-syntax} for the syntax of notations including
646
the possibility to declare them in a given scope. Here is a typical
647
example which declares the notation for conjunction in the scope {\tt
651
Notation "A /\ B" := (and A B) : type_scope.
654
\Rem A notation not defined in a scope is called a {\em lonely} notation.
656
\subsection{Global interpretation rules for notations}
658
At any time, the interpretation of a notation for term is done within
659
a {\em stack} of interpretation scopes and lonely notations. In case a
660
notation has several interpretations, the actual interpretation is the
661
one defined by (or in) the more recently declared (or open) lonely
662
notation (or interpretation scope) which defines this notation.
663
Typically if a given notation is defined in some scope {\scope} but
664
has also an interpretation not assigned to a scope, then, if {\scope}
665
is open before the lonely interpretation is declared, then the lonely
666
interpretation is used (and this is the case even if the
667
interpretation of the notation in {\scope} is given after the lonely
668
interpretation: otherwise said, only the order of lonely
669
interpretations and opening of scopes matters, and not the declaration
670
of interpretations within a scope).
672
The initial state of {\Coq} declares three interpretation scopes and
673
no lonely notations. These scopes, in opening order, are {\tt
674
core\_scope}, {\tt type\_scope} and {\tt nat\_scope}.
676
The command to add a scope to the interpretation scope stack is
677
\comindex{Open Scope}
678
\comindex{Close Scope}
680
{\tt Open Scope} {\scope}.
682
It is also possible to remove a scope from the interpretation scope
683
stack by using the command
685
{\tt Close Scope} {\scope}.
687
Notice that this command does not only cancel the last {\tt Open Scope
688
{\scope}} but all the invocation of it.
690
\Rem {\tt Open Scope} and {\tt Close Scope} do not survive the end of
691
sections where they occur. When defined outside of a section, they are
692
exported to the modules that import the module where they occur.
696
\item {\tt Local Open Scope} {\scope}.
698
\item {\tt Local Close Scope} {\scope}.
700
These variants are not exported to the modules that import the module
701
where they occur, even if outside a section.
705
\subsection{Local interpretation rules for notations}
707
In addition to the global rules of interpretation of notations, some
708
ways to change the interpretation of subterms are available.
710
\subsubsection{Local opening of an interpretation scope
713
\comindex{Delimit Scope}}
715
It is possible to locally extend the interpretation scope stack using
716
the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
717
for atomic terms), where {\delimkey} is a special identifier called
718
{\em delimiting key} and bound to a given scope.
720
In such a situation, the term {\term}, and all its subterms, are
721
interpreted in the scope stack extended with the scope bound to
724
To bind a delimiting key to a scope, use the command
727
\texttt{Delimit Scope} {\scope} \texttt{with} {\ident}
730
\subsubsection{Binding arguments of a constant to an interpretation scope
731
\comindex{Arguments Scope}}
733
It is possible to set in advance that some arguments of a given
734
constant have to be interpreted in a given scope. The command is
736
{\tt Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
738
where the list is a list made either of {\tt \_} or of a scope name.
739
Each scope in the list is bound to the corresponding parameter of
740
{\qualid} in order. When interpreting a term, if some of the
741
arguments of {\qualid} are built from a notation, then this notation
742
is interpreted in the scope stack extended by the scopes bound (if any)
746
\item {\tt Global Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
748
This behaves like {\tt Arguments Scope} {\qualid} {\tt [
749
\nelist{\optscope}{} ]} but survives when a section is closed instead
750
of stopping working at section closing.
752
\item {\tt Local Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
754
This is a synonym of {\tt Arguments Scope} {\qualid} {\tt [
755
\nelist{\optscope}{} ]}: if in a section, the effect of the command
756
stops when the section it belongs to ends.
760
\SeeAlso The command to show the scopes bound to the arguments of a
761
function is described in Section~\ref{About}.
763
\subsubsection{Binding types of arguments to an interpretation scope}
765
When an interpretation scope is naturally associated to a type
766
(e.g. the scope of operations on the natural numbers), it may be
767
convenient to bind it to this type. The effect of this is that any
768
argument of a function that syntactically expects a parameter of this
769
type is interpreted using scope. More precisely, it applies only if
770
this argument is built from a notation, and if so, this notation is
771
interpreted in the scope stack extended by this particular scope. It
772
does not apply to the subterms of this notation (unless the
773
interpretation of the notation itself expects arguments of the same
774
type that would trigger the same scope).
776
\comindex{Bind Scope}
777
More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
778
bound to an interpretation scope. The command to do it is
780
{\tt Bind Scope} {\scope} \texttt{with} {\class}
786
Bind Scope U_scope with U.
787
Parameter Uplus : U -> U -> U.
788
Parameter P : forall T:Set, T -> U -> Prop.
789
Parameter f : forall T:Set, T -> U.
790
Infix "+" := Uplus : U_scope.
791
Unset Printing Notations.
792
Open Scope nat_scope. (* Define + on the nat as the default for + *)
793
Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
796
\Rem The scope {\tt type\_scope} has also a local effect on
797
interpretation. See the next section.
799
\SeeAlso The command to show the scopes bound to the arguments of a
800
function is described in Section~\ref{About}.
802
\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}}
804
The scope {\tt type\_scope} has a special status. It is a primitive
805
interpretation scope which is temporarily activated each time a
806
subterm of an expression is expected to be a type. This includes goals
807
and statements, types of binders, domain and codomain of implication,
808
codomain of products, and more generally any type argument of a
809
declared or defined constant.
811
\subsection{Interpretation scopes used in the standard library of {\Coq}}
813
We give an overview of the scopes used in the standard library of
814
{\Coq}. For a complete list of notations in each scope, use the
815
commands {\tt Print Scopes} or {\tt Print Scopes {\scope}}.
817
\subsubsection{\tt type\_scope}
819
This includes infix {\tt *} for product types and infix {\tt +} for
820
sum types. It is delimited by key {\tt type}.
822
\subsubsection{\tt nat\_scope}
824
This includes the standard arithmetical operators and relations on
825
type {\tt nat}. Positive numerals in this scope are mapped to their
826
canonical representent built from {\tt O} and {\tt S}. The scope is
827
delimited by key {\tt nat}.
829
\subsubsection{\tt N\_scope}
831
This includes the standard arithmetical operators and relations on
832
type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
833
and comes with an interpretation for numerals as closed term of type {\tt Z}.
835
\subsubsection{\tt Z\_scope}
837
This includes the standard arithmetical operators and relations on
838
type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z}
839
and comes with an interpretation for numerals as closed term of type {\tt Z}.
841
\subsubsection{\tt positive\_scope}
843
This includes the standard arithmetical operators and relations on
844
type {\tt positive} (binary strictly positive numbers). It is
845
delimited by key {\tt positive} and comes with an interpretation for
846
numerals as closed term of type {\tt positive}.
848
\subsubsection{\tt Q\_scope}
850
This includes the standard arithmetical operators and relations on
851
type {\tt Q} (rational numbers defined as fractions of an integer and
852
a strictly positive integer modulo the equality of the
853
numerator-denominator cross-product). As for numerals, only $0$ and
854
$1$ have an interpretation in scope {\tt Q\_scope} (their
855
interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively).
857
\subsubsection{\tt Qc\_scope}
859
This includes the standard arithmetical operators and relations on the
860
type {\tt Qc} of rational numbers defined as the type of irreducible
861
fractions of an integer and a strictly positive integer.
863
\subsubsection{\tt real\_scope}
865
This includes the standard arithmetical operators and relations on
866
type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
867
and comes with an interpretation for numerals as term of type {\tt
868
R}. The interpretation is based on the binary decomposition. The
869
numeral 2 is represented by $1+1$. The interpretation $\phi(n)$ of an
870
odd positive numerals greater $n$ than 3 is {\tt 1+(1+1)*$\phi((n-1)/2)$}.
871
The interpretation $\phi(n)$ of an even positive numerals greater $n$
872
than 4 is {\tt (1+1)*$\phi(n/2)$}. Negative numerals are represented as the
873
opposite of the interpretation of their absolute value. E.g. the
874
syntactic object {\tt -11} is interpreted as {\tt
875
-(1+(1+1)*((1+1)*(1+(1+1))))} where the unit $1$ and all the operations are
878
\subsubsection{\tt bool\_scope}
880
This includes notations for the boolean operators. It is
881
delimited by key {\tt bool}.
883
\subsubsection{\tt list\_scope}
885
This includes notations for the list operators. It is
886
delimited by key {\tt list}.
888
\subsubsection{\tt core\_scope}
890
This includes the notation for pairs. It is delimited by key {\tt core}.
892
\subsubsection{\tt string\_scope}
894
This includes notation for strings as elements of the type {\tt
895
string}. Special characters and escaping follow {\Coq} conventions
896
on strings (see Section~\ref{strings}). Especially, there is no
897
convention to visualize non printable characters of a string. The
898
file {\tt String.v} shows an example that contains quotes, a newline
899
and a beep (i.e. the ascii character of code 7).
901
\subsubsection{\tt char\_scope}
903
This includes interpretation for all strings of the form
904
\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form
905
\verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly
906
with leading 0's), or of the form \verb!""""!. Their respective
907
denotations are the ascii code of $c$, the decimal ascii code $nnn$,
908
or the ascii code of the character \verb!"! (i.e. the ascii code
909
34), all of them being represented in the type {\tt ascii}.
911
\subsection{Displaying informations about scopes}
913
\subsubsection{\tt Print Visibility}
915
This displays the current stack of notations in scopes and lonely
916
notations that is used to interpret a notation. The top of the stack
917
is displayed last. Notations in scopes whose interpretation is hidden
918
by the same notation in a more recently open scope are not
919
displayed. Hence each notation is displayed only once.
923
{\tt Print Visibility {\scope}}\\
925
This displays the current stack of notations in scopes and lonely
926
notations assuming that {\scope} is pushed on top of the stack. This
927
is useful to know how a subterm locally occurring in the scope of
928
{\scope} is interpreted.
930
\subsubsection{\tt Print Scope {\scope}}
932
This displays all the notations defined in interpretation scope
933
{\scope}. It also displays the delimiting key if any and the class to
934
which the scope is bound, if any.
936
\subsubsection{\tt Print Scopes}
938
This displays all the notations, delimiting keys and corresponding
939
class of all the existing interpretation scopes.
940
It also displays the lonely notations.
942
\section[Abbreviations]{Abbreviations\index{Abbreviations}
943
\label{Abbreviations}
946
An {\em abbreviation} is a name, possibly applied to arguments, that
947
denotes a (presumably) more complex expression. Here are examples:
951
Require Import Relations.
952
Set Printing Notations.
955
Notation Nlist := (list nat).
956
Check 1 :: 2 :: 3 :: nil.
957
Notation reflexive R := (forall x, R x x).
958
Check forall A:Prop, A <-> A.
962
An abbreviation expects no precedence nor associativity, since it
963
follows the usual syntax of application. Abbreviations are used as
964
much as possible by the {\Coq} printers unless the modifier
965
\verb=(only parsing)= is given.
967
Abbreviations are bound to an absolute name as an ordinary
968
definition is, and they can be referred by qualified names too.
970
Abbreviations are syntactic in the sense that they are bound to
971
expressions which are not typed at the time of the definition of the
972
abbreviation but at the time it is used. Especially, abbreviations can
973
be bound to terms with holes (i.e. with ``\_''). The general syntax
976
\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term}
977
\zeroone{{\tt (only parsing)}}~\verb=.=
986
Definition explicit_id (A:Set) (a:A) := a.
987
Notation id := (explicit_id _).
991
Abbreviations do not survive the end of sections. No typing of the denoted
992
expression is performed at definition time. Type-checking is done only
993
at the time of use of the abbreviation.
995
%\Rem \index{Syntactic Definition} %
996
%Abbreviations are similar to the {\em syntactic
997
%definitions} available in versions of {\Coq} prior to version 8.0,
998
%except that abbreviations are used for printing (unless the modifier
999
%\verb=(only parsing)= is given) while syntactic definitions were not.
1001
\section{Tactic Notations}
1003
Tactic notations allow to customize the syntax of the tactics of the
1004
tactic language\footnote{Tactic notations are just a simplification of
1005
the {\tt Grammar tactic simple\_tactic} command that existed in
1006
versions prior to version 8.0.}. Tactic notations obey the following
1011
\begin{tabular}{lcl}
1012
{\sentence} & ::= & \texttt{Tactic Notation} \zeroone{\taclevel} \nelist{\proditem}{} \\
1013
& & \texttt{:= {\tac} .}\\
1014
{\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\
1015
{\taclevel} & ::= & {\tt (at level} {\naturalnumber}{\tt )} \\
1016
{\tacargtype} & ::= &
1019
{\tt simple\_intropattern} $|$
1020
{\tt reference} \\ & $|$ &
1023
{\tt ne\_hyp\_list} \\ & $|$ &
1024
% {\tt quantified\_hypothesis} \\ & $|$ &
1026
{\tt constr\_list} $|$
1027
{\tt ne\_constr\_list} \\ & $|$ &
1028
%{\tt castedopenconstr} $|$
1030
{\tt integer\_list} $|$
1031
{\tt ne\_integer\_list} \\ & $|$ &
1032
{\tt int\_or\_var} $|$
1033
{\tt int\_or\_var\_list} $|$
1034
{\tt ne\_int\_or\_var\_list} \\ & $|$ &
1035
{\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)}
1040
A tactic notation {\tt Tactic Notation {\taclevel}
1041
{\sequence{\proditem}{}} := {\tac}} extends the parser and
1042
pretty-printer of tactics with a new rule made of the list of
1043
production items. It then evaluates into the tactic expression
1044
{\tac}. For simple tactics, it is recommended to use a terminal
1045
symbol, i.e. a {\str}, for the first production item. The tactic
1046
level indicates the parsing precedence of the tactic notation. This
1047
information is particularly relevant for notations of tacticals.
1048
Levels 0 to 5 are available (default is 0).
1049
To know the parsing precedences of the
1050
existing tacticals, use the command {\tt Print Grammar tactic.}
1052
Each type of tactic argument has a specific semantic regarding how it
1053
is parsed and how it is interpreted. The semantic is described in the
1054
following table. The last command gives examples of tactics which
1055
use the corresponding kind of argument.
1059
\begin{tabular}{l|l|l|l}
1060
Tactic argument type & parsed as & interpreted as & as in tactic \\
1062
{\tt\small ident} & identifier & a user-given name & {\tt intro} \\
1063
{\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\
1064
{\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\
1065
%% quantified_hypothesis actually not supported
1066
%%{\tt\small quantified\_hypothesis} & identifier or integer & a named or non dep. hyp. of the goal & {\tt intros until}\\
1067
{\tt\small reference} & qualified identifier & a global reference of term & {\tt unfold}\\
1068
{\tt\small constr} & term & a term & {\tt exact} \\
1069
%% castedopenconstr actually not supported
1070
%%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
1071
{\tt\small integer} & integer & an integer & \\
1072
{\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\
1073
{\tt\small tactic} & tactic at level 5 & a tactic & \\
1074
{\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\
1075
{\tt\small {\nterm{entry}}\_list} & list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted & \\
1076
{\tt\small ne\_{\nterm{entry}}\_list} & non-empty list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted& \\
1079
\Rem In order to be bound in tactic definitions, each syntactic entry
1080
for argument type must include the case of simple {\ltac} identifier
1081
as part of what it parses. This is naturally the case for {\tt ident},
1082
{\tt simple\_intropattern}, {\tt reference}, {\tt constr}, ... but not
1083
for {\tt integer}. This is the reason for introducing a special entry
1084
{\tt int\_or\_var} which evaluates to integers only but which
1085
syntactically includes identifiers in order to be usable in tactic
1088
\Rem The {\tt {\nterm{entry}}\_list} and {\tt ne\_{\nterm{entry}}\_list}
1089
entries can be used in primitive tactics or in other notations at
1090
places where a list of the underlying entry can be used: {\nterm{entry}} is
1091
either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
1092
{\tt\small int\_or\_var}.
1094
% $Id: RefMan-syn.tex 11784 2009-01-14 11:36:32Z herbelin $
1096
%%% Local Variables:
1098
%%% TeX-master: "Reference-Manual"
added
removed
doc/refman/RefMan-syn.tex
