diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 1431 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 |
2 files changed, 0 insertions, 1432 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex deleted file mode 100644 index 836753db16..0000000000 --- a/doc/refman/RefMan-syn.tex +++ /dev/null @@ -1,1431 +0,0 @@ -\chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}} -%HEVEA\cutname{syntax-extensions.html} - -In this chapter, we introduce advanced commands to modify the way -{\Coq} parses and prints objects, i.e. the translations between the -concrete and internal representations of terms and commands. - -The main commands to provide custom symbolic notations for terms are -{\tt Notation} and {\tt Infix}. They are described in Section -\ref{Notation}. There is also a variant of {\tt Notation} which does -not modify the parser. This provides with a form of abbreviation and -it is described in Section~\ref{Abbreviations}. It is sometimes -expected that the same symbolic notation has different meanings in -different contexts. To achieve this form of overloading, {\Coq} offers -a notion of interpretation scope. This is described in -Section~\ref{scopes}. - -The main command to provide custom notations for tactics is {\tt - Tactic Notation}. It is described in Section~\ref{Tactic-Notation}. - -% No need any more to remind this -%% \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which -%% were present for a while in {\Coq} are no longer available from {\Coq} -%% version 8.0. The underlying AST structure is also no longer available. - -\section[Notations]{Notations\label{Notation} -\comindex{Notation}} - -\subsection{Basic notations} - -A {\em notation} is a symbolic expression denoting some term -or term pattern. - -A typical notation is the use of the infix symbol \verb=/\= to denote -the logical conjunction (\texttt{and}). Such a notation is declared -by - -\begin{coq_example*} -Notation "A /\ B" := (and A B). -\end{coq_example*} - -The expression \texttt{(and A B)} is the abbreviated term and the -string \verb="A /\ B"= (called a {\em notation}) tells how it is -symbolically written. - -A notation is always surrounded by double quotes (except when the -abbreviation has the form of an ordinary applicative expression; see \ref{Abbreviations}). The -notation is composed of {\em tokens} separated by spaces. Identifiers -in the string (such as \texttt{A} and \texttt{B}) are the {\em -parameters} of the notation. They must occur at least once each in the -denoted term. The other elements of the string (such as \verb=/\=) are -the {\em symbols}. - -An identifier can be used as a symbol but it must be surrounded by -simple quotes to avoid the confusion with a parameter. Similarly, -every symbol of at least 3 characters and starting with a simple quote -must be quoted (then it starts by two single quotes). Here is an example. - -\begin{coq_example*} -Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3). -\end{coq_example*} - -%TODO quote the identifier when not in front, not a keyword, as in "x 'U' y" ? - -A notation binds a syntactic expression to a term. Unless the parser -and pretty-printer of {\Coq} already know how to deal with the -syntactic expression (see \ref{ReservedNotation}), explicit precedences and -associativity rules have to be given. - -\Rem The right-hand side of a notation is interpreted at the time the -notation is given. In particular, disambiguation of constants, implicit arguments (see -Section~\ref{Implicit Arguments}), coercions (see -Section~\ref{Coercions}), etc. are resolved at the time of the -declaration of the notation. - -\subsection[Precedences and associativity]{Precedences and associativity\index{Precedences} -\index{Associativity}} - -Mixing different symbolic notations in the same text may cause serious -parsing ambiguity. To deal with the ambiguity of notations, {\Coq} -uses precedence levels ranging from 0 to 100 (plus one extra level -numbered 200) and associativity rules. - -Consider for example the new notation - -\begin{coq_example*} -Notation "A \/ B" := (or A B). -\end{coq_example*} - -Clearly, an expression such as {\tt forall A:Prop, True \verb=/\= A \verb=\/= -A \verb=\/= False} is ambiguous. To tell the {\Coq} parser how to -interpret the expression, a priority between the symbols \verb=/\= and -\verb=\/= has to be given. Assume for instance that we want conjunction -to bind more than disjunction. This is expressed by assigning a -precedence level to each notation, knowing that a lower level binds -more than a higher level. Hence the level for disjunction must be -higher than the level for conjunction. - -Since connectives are not tight articulation points of a text, it -is reasonable to choose levels not so far from the highest level which -is 100, for example 85 for disjunction and 80 for -conjunction\footnote{which are the levels effectively chosen in the -current implementation of {\Coq}}. - -Similarly, an associativity is needed to decide whether {\tt True \verb=/\= -False \verb=/\= False} defaults to {\tt True \verb=/\= (False -\verb=/\= False)} (right associativity) or to {\tt (True -\verb=/\= False) \verb=/\= False} (left associativity). We may -even consider that the expression is not well-formed and that -parentheses are mandatory (this is a ``no associativity'')\footnote{ -{\Coq} accepts notations declared as no associative but the parser on -which {\Coq} is built, namely {\camlpppp}, currently does not implement the -no-associativity and replaces it by a left associativity; hence it is -the same for {\Coq}: no-associativity is in fact left associativity}. -We do not know of a special convention of the associativity of -disjunction and conjunction, so let us apply for instance a right -associativity (which is the choice of {\Coq}). - -Precedence levels and associativity rules of notations have to be -given between parentheses in a list of modifiers that the -\texttt{Notation} command understands. Here is how the previous -examples refine. - -\begin{coq_example*} -Notation "A /\ B" := (and A B) (at level 80, right associativity). -Notation "A \/ B" := (or A B) (at level 85, right associativity). -\end{coq_example*} - -By default, a notation is considered non associative, but the -precedence level is mandatory (except for special cases whose level is -canonical). The level is either a number or the phrase {\tt next -level} whose meaning is obvious. The list of levels already assigned -is on Figure~\ref{init-notations}. - -\subsection{Complex notations} - -Notations can be made from arbitrarily complex symbols. One can for -instance define prefix notations. - -\begin{coq_example*} -Notation "~ x" := (not x) (at level 75, right associativity). -\end{coq_example*} - -One can also define notations for incomplete terms, with the hole -expected to be inferred at typing time. - -\begin{coq_example*} -Notation "x = y" := (@eq _ x y) (at level 70, no associativity). -\end{coq_example*} - -One can define {\em closed} notations whose both sides are symbols. In -this case, the default precedence level for inner subexpression is -200, and the default level for the notation itself is 0. - -\begin{coq_eval} -Set Printing Depth 50. -(********** The following is correct but produces **********) -(**** an incompatibility with the reserved notation ********) -\end{coq_eval} -\begin{coq_example*} -Notation "( x , y )" := (@pair _ _ x y). -\end{coq_example*} - -One can also define notations for binders. - -\begin{coq_eval} -Set Printing Depth 50. -(********** The following is correct but produces **********) -(**** an incompatibility with the reserved notation ********) -\end{coq_eval} -\begin{coq_example*} -Notation "{ x : A | P }" := (sig A (fun x => P)). -\end{coq_example*} - -In the last case though, there is a conflict with the notation for -type casts. The notation for type casts, as shown by the command {\tt Print Grammar -constr} is at level 100. To avoid \verb=x : A= being parsed as a type cast, -it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a -correct definition is the following. - -\begin{coq_example*} -Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). -\end{coq_example*} - -%This change has retrospectively an effect on the notation for notation -%{\tt "{ A } + { B }"}. For the sake of factorization, {\tt A} must be -%put at level 99 too, which gives -% -%\begin{coq_example*} -%Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99). -%\end{coq_example*} - -More generally, it is required that notations are explicitly -factorized on the left. See the next section for more about -factorization. - -\subsection{Simple factorization rules} - -{\Coq} extensible parsing is performed by {\camlpppp} which is -essentially a LL1 parser: it decides which notation to parse by -looking tokens from left to right. Hence, some care has to be taken -not to hide already existing rules by new rules. Some simple left -factorization work has to be done. Here is an example. - -\begin{coq_eval} -(********** The next rule for notation _ < _ < _ produces **********) -(*** Error: Notation _ < _ < _ is already defined at level 70 ... ***) -\end{coq_eval} -\begin{coq_example*} -Notation "x < y" := (lt x y) (at level 70). -Notation "x < y < z" := (x < y /\ y < z) (at level 70). -\end{coq_example*} - -In order to factorize the left part of the rules, the subexpression -referred by {\tt y} has to be at the same level in both rules. However -the default behavior puts {\tt y} at the next level below 70 -in the first rule (no associativity is the default), and at the level -200 in the second rule (level 200 is the default for inner expressions). -To fix this, we need to force the parsing level of {\tt y}, -as follows. - -\begin{coq_example*} -Notation "x < y" := (lt x y) (at level 70). -Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). -\end{coq_example*} - -For the sake of factorization with {\Coq} predefined rules, simple -rules have to be observed for notations starting with a symbol: -e.g. rules starting with ``\{'' or ``('' should be put at level 0. The -list of {\Coq} predefined notations can be found in Chapter~\ref{Theories}. - -The command to display the current state of the {\Coq} term parser is -\comindex{Print Grammar constr} - -\begin{quote} -\tt Print Grammar constr. -\end{quote} - -\variant - -\comindex{Print Grammar pattern} -{\tt Print Grammar pattern.}\\ - -This displays the state of the subparser of patterns (the parser -used in the grammar of the {\tt match} {\tt with} constructions). - -\subsection{Displaying symbolic notations} - -The command \texttt{Notation} has an effect both on the {\Coq} parser and -on the {\Coq} printer. For example: - -\begin{coq_example} -Check (and True True). -\end{coq_example} - -However, printing, especially pretty-printing, also requires some -care. We may want specific indentations, line breaks, alignment if on -several lines, etc. For pretty-printing, {\Coq} relies on {\ocaml} -formatting library, which provides indentation and automatic line -breaks depending on page width by means of {\em formatting boxes}. - -The default printing of notations is rudimentary. For printing a -notation, a formatting box is opened in such a way that if the -notation and its arguments cannot fit on a single line, a line break -is inserted before the symbols of the notation and the arguments on -the next lines are aligned with the argument on the first line. - -A first simple control that a user can have on the printing of a -notation is the insertion of spaces at some places of the -notation. This is performed by adding extra spaces between the symbols -and parameters: each extra space (other than the single space needed -to separate the components) is interpreted as a space to be inserted -by the printer. Here is an example showing how to add spaces around -the bar of the notation. - -\begin{coq_example} -Notation "{{ x : A | P }}" := (sig (fun x : A => P)) - (at level 0, x at level 99). -Check (sig (fun x : nat => x=x)). -\end{coq_example} - -The second, more powerful control on printing is by using the {\tt -format} modifier. Here is an example - -\begin{small} -\begin{coq_example} -Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) -(at level 200, right associativity, format -"'[v ' 'If' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'"). -\end{coq_example} -\end{small} - -\begin{coq_example} -Check - (IF_then_else (IF_then_else True False True) - (IF_then_else True False True) - (IF_then_else True False True)). -\end{coq_example} - -A {\em format} is an extension of the string denoting the notation with -the possible following elements delimited by single quotes: - -\begin{itemize} -\item extra spaces are translated into simple spaces -\item tokens of the form \verb='/ '= are translated into breaking point, - in case a line break occurs, an indentation of the number of spaces - after the ``\verb=/='' is applied (2 spaces in the given example) -\item token of the form \verb='//'= force writing on a new line -\item well-bracketed pairs of tokens of the form \verb='[ '= and \verb=']'= - are translated into printing boxes; in case a line break occurs, - an extra indentation of the number of spaces given after the ``\verb=[='' - is applied (4 spaces in the example) -\item well-bracketed pairs of tokens of the form \verb='[hv '= and \verb=']'= - are translated into horizontal-orelse-vertical printing boxes; - if the content of the box does not fit on a single line, then every breaking - point forces a newline and an extra indentation of the number of spaces - given after the ``\verb=[='' is applied at the beginning of each newline - (3 spaces in the example) -\item well-bracketed pairs of tokens of the form \verb='[v '= and - \verb=']'= are translated into vertical printing boxes; every - breaking point forces a newline, even if the line is large enough to - display the whole content of the box, and an extra indentation of the - number of spaces given after the ``\verb=[='' is applied at the beginning - of each newline -\end{itemize} - -%Thus, for the previous example, we get -%\footnote{The ``@'' is here to shunt -%the notation "'IF' A 'then' B 'else' C" which is defined in {\Coq} -%initial state}: - -Notations do not survive the end of sections. No typing of the denoted -expression is performed at definition time. Type-checking is done only -at the time of use of the notation. - -\Rem -Sometimes, a notation is expected only for the parser. -%(e.g. because -%the underlying parser of {\Coq}, namely {\camlpppp}, is LL1 and some extra -%rules are needed to circumvent the absence of factorization). -To do so, the option {\tt only parsing} is allowed in the list of modifiers of -\texttt{Notation}. - -Conversely, the {\tt only printing} can be used to declare -that a notation should only be used for printing and should not declare a -parsing rule. In particular, such notations do not modify the parser. - -\subsection{The \texttt{Infix} command -\comindex{Infix}} - -The \texttt{Infix} command is a shortening for declaring notations of -infix symbols. Its syntax is - -\begin{quote} -\noindent\texttt{Infix "{\symbolentry}" :=} {\term} {\tt (} \nelist{\em modifier}{,} {\tt )}. -\end{quote} - -and it is equivalent to - -\begin{quote} -\noindent\texttt{Notation "x {\symbolentry} y" := ({\term} x y) (} \nelist{\em modifier}{,} {\tt )}. -\end{quote} - -where {\tt x} and {\tt y} are fresh names. Here is an example. - -\begin{coq_example*} -Infix "/\" := and (at level 80, right associativity). -\end{coq_example*} - -\subsection{Reserving notations -\label{ReservedNotation} -\comindex{Reserved Notation}} - -A given notation may be used in different contexts. {\Coq} expects all -uses of the notation to be defined at the same precedence and with the -same associativity. To avoid giving the precedence and associativity -every time, it is possible to declare a parsing rule in advance -without giving its interpretation. Here is an example from the initial -state of {\Coq}. - -\begin{coq_example} -Reserved Notation "x = y" (at level 70, no associativity). -\end{coq_example} - -Reserving a notation is also useful for simultaneously defining an -inductive type or a recursive constant and a notation for it. - -\Rem The notations mentioned on Figure~\ref{init-notations} are -reserved. Hence their precedence and associativity cannot be changed. - -\subsection{Simultaneous definition of terms and notations -\comindex{Fixpoint {\ldots} where {\ldots}} -\comindex{CoFixpoint {\ldots} where {\ldots}} -\comindex{Inductive {\ldots} where {\ldots}}} - -Thanks to reserved notations, the inductive, co-inductive, record, -recursive and corecursive definitions can benefit of customized -notations. To do this, insert a {\tt where} notation clause after the -definition of the (co)inductive type or (co)recursive term (or after -the definition of each of them in case of mutual definitions). The -exact syntax is given on Figure~\ref{notation-syntax} for inductive, -co-inductive, recursive and corecursive definitions and on -Figure~\ref{record-syntax} for records. Here are examples: - -\begin{coq_eval} -Set Printing Depth 50. -(********** The following is correct but produces an error **********) -(********** because the symbol /\ is already bound **********) -(**** Error: The conclusion of A -> B -> A /\ B is not valid *****) -\end{coq_eval} - -\begin{coq_example*} -Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B -where "A /\ B" := (and A B). -\end{coq_example*} - -\begin{coq_eval} -Set Printing Depth 50. -(********** The following is correct but produces an error **********) -(********** because the symbol + is already bound **********) -(**** Error: no recursive definition *****) -\end{coq_eval} - -\begin{coq_example*} -Fixpoint plus (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (p+m) - end -where "n + m" := (plus n m). -\end{coq_example*} - -\subsection{Displaying informations about notations -\optindex{Printing Notations}} - -To deactivate the printing of all notations, use the command -\begin{quote} -\tt Unset Printing Notations. -\end{quote} -To reactivate it, use the command -\begin{quote} -\tt Set Printing Notations. -\end{quote} -The default is to use notations for printing terms wherever possible. - -\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}. - -\subsection{Locating notations -\comindex{Locate} -\label{LocateSymbol}} - -To know to which notations a given symbol belongs to, use the command -\begin{quote} -\tt Locate {\symbolentry} -\end{quote} -where symbol is any (composite) symbol surrounded by double quotes. To locate -a particular notation, use a string where the variables of the -notation are replaced by ``\_'' and where possible single quotes -inserted around identifiers or tokens starting with a single quote are -dropped. - -\Example -\begin{coq_example} -Locate "exists". -Locate "exists _ .. _ , _". -\end{coq_example} - -\SeeAlso Section \ref{Locate}. - -\begin{figure} -\begin{small} -\begin{centerframe} -\begin{tabular}{lcl} -{\sentence} & ::= & - \zeroone{\tt Local} \texttt{Notation} {\str} \texttt{:=} {\term} - \zeroone{\modifiers} \zeroone{:{\scope}} .\\ - & $|$ & - \zeroone{\tt Local} \texttt{Infix} {\str} \texttt{:=} {\qualid} - \zeroone{\modifiers} \zeroone{:{\scope}} .\\ - & $|$ & - \zeroone{\tt Local} \texttt{Reserved Notation} {\str} - \zeroone{\modifiers} .\\ - & $|$ & {\tt Inductive} - \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\ - & $|$ & {\tt CoInductive} - \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\ - & $|$ & {\tt Fixpoint} - \nelist{{\fixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\ - & $|$ & {\tt CoFixpoint} - \nelist{{\cofixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\ -\\ -{\declnotation} & ::= & - \zeroone{{\tt where} \nelist{{\str} {\tt :=} {\term} \zeroone{:{\scope}}}{\tt and}}. -\\ -\\ -{\modifiers} - & ::= & {\tt at level} {\naturalnumber} \\ - & $|$ & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \zeroone{\binderinterp}\\ - & $|$ & \nelist{\ident}{,} {\tt at next level} \zeroone{\binderinterp}\\ - & $|$ & {\ident} {\binderinterp} \\ - & $|$ & {\ident} {\tt ident} \\ - & $|$ & {\ident} {\tt global} \\ - & $|$ & {\ident} {\tt bigint} \\ - & $|$ & {\ident} \zeroone{{\tt strict}} {\tt pattern} \zeroone{{\tt at level} {\naturalnumber}}\\ - & $|$ & {\ident} {\tt binder} \\ - & $|$ & {\ident} {\tt closed binder} \\ - & $|$ & {\tt left associativity} \\ - & $|$ & {\tt right associativity} \\ - & $|$ & {\tt no associativity} \\ - & $|$ & {\tt only parsing} \\ - & $|$ & {\tt only printing} \\ - & $|$ & {\tt format} {\str} \\ -\\ -\\ -{\binderinterp} - & ::= & {\tt as ident} \\ - & $|$ & {\tt as pattern} \\ - & $|$ & {\tt as strict pattern} \\ -\end{tabular} -\end{centerframe} -\end{small} -\caption{Syntax of the variants of {\tt Notation}} -\label{notation-syntax} -\end{figure} - -\subsection{Notations and binders} - -Notations can include binders. This section lists -different ways to deal with binders. For further examples, see also -Section~\ref{RecursiveNotationsWithBinders}. - -\subsubsection{Binders bound in the notation and parsed as identifiers} - -Here is the basic example of a notation using a binder: - -\begin{coq_example*} -Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) - (at level 200, x ident, A at level 200, right associativity). -\end{coq_example*} - -The binding variables in the right-hand side that occur as a parameter -of the notation (here {\tt x}) dynamically bind all the occurrences -in their respective binding scope after instantiation of the -parameters of the notation. This means that the term bound to {\tt B} can -refer to the variable name bound to {\tt x} as shown in the following -application of the notation: - -\begin{coq_example} -Check sigma z : nat, z = 0. -\end{coq_example} - -Notice the modifier {\tt x ident} in the declaration of the -notation. It tells to parse {\tt x} as a single identifier. - -\subsubsection{Binders bound in the notation and parsed as patterns} - -In the same way as patterns can be used as binders, as in {\tt fun - '(x,y) => x+y} or {\tt fun '(existT \_ x \_) => x}, notations can be -defined so that any pattern (in the sense of the entry {\pattern} of -Figure~\ref{term-syntax-aux}) can be used in place of the -binder. Here is an example: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Notation "'subset' ' p , P " := (sig (fun p => P)) - (at level 200, p pattern, format "'subset' ' p , P"). -\end{coq_example*} - -\begin{coq_example} -Check subset '(x,y), x+y=0. -\end{coq_example} - -The modifier {\tt p pattern} in the declaration of the notation -tells to parse $p$ as a pattern. Note that a single -variable is both an identifier and a pattern, so, e.g., the following -also works: - -% Note: we rely on the notation of the standard library which does not -% print the expected output, so we hide the output. -\begin{coq_example} -Check subset 'x, x=0. -\end{coq_example} - -If one wants to prevent such a notation to be used for printing when the -pattern is reduced to a single identifier, one has to use instead -the modifier {\tt p strict pattern}. For parsing, however, a {\tt - strict pattern} will continue to include the case of a -variable. Here is an example showing the difference: - -\begin{coq_example*} -Notation "'subset_bis' ' p , P" := (sig (fun p => P)) - (at level 200, p strict pattern). -Notation "'subset_bis' p , P " := (sig (fun p => P)) - (at level 200, p ident). -\end{coq_example*} - -\begin{coq_example} -Check subset_bis 'x, x=0. -\end{coq_example} - -The default level for a {\tt pattern} is 0. One can use a different level by -using {\tt pattern at level} $n$ where the scale is the same as the one for -terms (Figure~\ref{init-notations}). - -\subsubsection{Binders bound in the notation and parsed as terms} - -Sometimes, for the sake of factorization of rules, a binder has to be -parsed as a term. This is typically the case for a notation such as -the following: - -\begin{coq_eval} -Set Printing Depth 50. -(********** The following is correct but produces **********) -(**** an incompatibility with the reserved notation ********) -\end{coq_eval} -\begin{coq_example*} -Notation "{ x : A | P }" := (sig (fun x : A => P)) - (at level 0, x at level 99 as ident). -\end{coq_example*} - -This is so because the grammar also contains rules starting with -{\tt \{} and followed by a term, such as the rule for the notation - {\tt \{ A \} + \{ B \}} for the constant {\tt - sumbool}~(see Section~\ref{sumbool}). - -Then, in the rule, {\tt x ident} is replaced by {\tt x at level 99 as - ident} meaning that {\tt x} is parsed as a term at level 99 (as done -in the notation for {\tt sumbool}), but that this term has actually to -be an identifier. - -The notation {\tt \{ x | P \}} is already defined in the standard -library with the {\tt as ident} modifier. We cannot redefine it but -one can define an alternative notation, say {\tt \{ p such that P }\}, -using instead {\tt as pattern}. - -% Note, this conflicts with the default rule in the standard library, so -% we don't show the -\begin{coq_example*} -Notation "{ p 'such' 'that' P }" := (sig (fun p => P)) - (at level 0, p at level 99 as pattern). -\end{coq_example*} - -Then, the following works: -\begin{coq_example} -Check {(x,y) such that x+y=0}. -\end{coq_example} - -To enforce that the pattern should not be used for printing when it -is just an identifier, one could have said {\tt p at level - 99 as strict pattern}. - -Note also that in the absence of a {\tt as ident}, {\tt as strict - pattern} or {\tt as pattern} modifiers, the default is to consider -subexpressions occurring in binding position and parsed as terms to be -{\tt as ident}. - -\subsubsection{Binders not bound in the notation} -\label{NotationsWithBinders} - -We can also have binders in the right-hand side of a notation which -are not themselves bound in the notation. In this case, the binders -are considered up to renaming of the internal binder. E.g., for the -notation - -\begin{coq_example*} -Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200). -\end{coq_example*} -the next command fails because {\tt p} does not bind in -the instance of {\tt n}. -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -% (********** The following produces **********) -% (**** The reference p was not found in the current environment ********) -\begin{coq_example} -Fail Check (exists_different p). -\end{coq_example} - -\subsection{Notations with recursive patterns} -\label{RecursiveNotations} - -A mechanism is provided for declaring elementary notations with -recursive patterns. The basic example is: - -\begin{coq_example*} -Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). -\end{coq_example*} - -On the right-hand side, an extra construction of the form {\tt ..} $t$ -{\tt ..} can be used. Notice that {\tt ..} is part of the {\Coq} -syntax and it must not be confused with the three-dots notation -$\ldots$ used in this manual to denote a sequence of arbitrary size. - -On the left-hand side, the part ``$x$ $s$ {\tt ..} $s$ $y$'' of the -notation parses any number of time (but at least one time) a sequence -of expressions separated by the sequence of tokens $s$ (in the -example, $s$ is just ``{\tt ;}''). - -The right-hand side must contain a subterm of the form either -$\phi(x,${\tt ..} $\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..} -$\phi(x,t)$ {\tt ..}$)$ where $\phi([~]_E,[~]_I)$, called the {\em - iterator} of the recursive notation is an arbitrary expression with -distinguished placeholders and -where $t$ is called the {\tt terminating expression} of the recursive -notation. In the example, we choose the name s$x$ and $y$ but in -practice they can of course be chosen arbitrarily. Note that the -placeholder $[~]_I$ has to occur only once but the $[~]_E$ can occur -several times. - -Parsing the notation produces a list of expressions which are used to -fill the first placeholder of the iterating pattern which itself is -repeatedly nested as many times as the length of the list, the second -placeholder being the nesting point. In the innermost occurrence of the -nested iterating pattern, the second placeholder is finally filled with the -terminating expression. - -In the example above, the iterator $\phi([~]_E,[~]_I)$ is {\tt cons - $[~]_E$ $[~]_I$} and the terminating expression is {\tt nil}. Here are -other examples: -\begin{coq_example*} -Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0). -Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := - (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z)) - (pair .. (pair (pair a u) (pair b u)) .. (pair c u))) - (t at level 39). -\end{coq_example*} - -Recursive patterns can occur several times on the right-hand side. -Here is an example: - -\begin{coq_example*} -Notation "[> a , .. , b <]" := - (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). -\end{coq_example*} - -Notations with recursive patterns can be reserved like standard -notations, they can also be declared within interpretation scopes (see -section \ref{scopes}). - -\subsection{Notations with recursive patterns involving binders} -\label{RecursiveNotationsWithBinders} - -Recursive notations can also be used with binders. The basic example is: - -\begin{coq_example*} -Notation "'exists' x .. y , p" := - (ex (fun x => .. (ex (fun y => p)) ..)) - (at level 200, x binder, y binder, right associativity). -\end{coq_example*} - -The principle is the same as in Section~\ref{RecursiveNotations} -except that in the iterator $\phi([~]_E,[~]_I)$, the placeholder $[~]_E$ can -also occur in position of the binding variable of a {\tt - fun} or a {\tt forall}. - -To specify that the part ``$x$ {\tt ..} $y$'' of the notation -parses a sequence of binders, $x$ and $y$ must be marked as {\tt - binder} in the list of modifiers of the notation. The -binders of the parsed sequence are used to fill the occurrences of the first -placeholder of the iterating pattern which is repeatedly nested as many times -as the number of binders generated. If ever the generalization -operator {\tt `} (see Section~\ref{implicit-generalization}) is used -in the binding list, the added binders are taken into account too. - -Binders parsing exist in two flavors. If $x$ and $y$ are marked as -{\tt binder}, then a sequence such as {\tt a b c : T} will be accepted -and interpreted as the sequence of binders {\tt (a:T) (b:T) - (c:T)}. For instance, in the notation above, the syntax {\tt exists - a b : nat, a = b} is valid. - -The variables $x$ and $y$ can also be marked as {\tt closed binder} in -which case only well-bracketed binders of the form {\tt (a b c:T)} or -{\tt \{a b c:T\}} etc. are accepted. - -With closed binders, the recursive sequence in the left-hand side can -be of the more general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an -arbitrary sequence of tokens. With open binders though, $s$ has to be -empty. Here is an example of recursive notation with closed binders: - -\begin{coq_example*} -Notation "'mylet' f x .. y := t 'in' u":= - (let f := fun x => .. (fun y => t) .. in u) - (at level 200, x closed binder, y closed binder, right associativity). -\end{coq_example*} - -A recursive pattern for binders can be used in position of a recursive -pattern for terms. Here is an example: - -\begin{coq_example*} -Notation "'FUNAPP' x .. y , f" := - (fun x => .. (fun y => (.. (f x) ..) y ) ..) - (at level 200, x binder, y binder, right associativity). -\end{coq_example*} - -If an occurrence of the $[~]_E$ is not in position of a binding -variable but of a term, it is the name used in the binding which is -used. Here is an example: - -\begin{coq_example*} -Notation "'exists_non_null' x .. y , P" := - (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) - (at level 200, x binder). -\end{coq_example*} - -\subsection{Predefined entries} - -By default, sub-expressions are parsed as terms and the corresponding -grammar entry is called {\tt constr}. However, one may sometimes want -to restrict the syntax of terms in a notation. For instance, the -following notation will accept to parse only global reference in -position of {\tt x}: - -\begin{coq_example*} -Notation "'apply' f a1 .. an" := (.. (f a1) .. an) - (at level 10, f global, a1, an at level 9). -\end{coq_example*} - -In addition to {\tt global}, one can restrict the syntax of a -sub-expression by using the entry names {\tt ident} or {\tt pattern} -already seen in Section~\ref{NotationsWithBinders}, even when the -corresponding expression is not used as a binder in the right-hand -side. E.g.: - -\begin{coq_example*} -Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) - (at level 10, f ident, a1, an at level 9). -\end{coq_example*} - -\subsection{Summary} - -\paragraph{Syntax of notations} - -The different syntactic variants of the command \texttt{Notation} are -given on Figure~\ref{notation-syntax}. The optional {\tt :{\scope}} is -described in the Section~\ref{scopes}. - -\Rem No typing of the denoted expression is performed at definition -time. Type-checking is done only at the time of use of the notation. - -\Rem Many examples of {\tt Notation} may be found in the files -composing the initial state of {\Coq} (see directory {\tt -\$COQLIB/theories/Init}). - -\Rem The notation \verb="{ x }"= has a special status in such a way -that complex notations of the form \verb="x + { y }"= or -\verb="x * { y }"= can be nested with correct precedences. Especially, -every notation involving a pattern of the form \verb="{ x }"= is -parsed as a notation where the pattern \verb="{ x }"= has been simply -replaced by \verb="x"= and the curly brackets are parsed separately. -E.g. \verb="y + { z }"= is not parsed as a term of the given form but -as a term of the form \verb="y + z"= where \verb=z= has been parsed -using the rule parsing \verb="{ x }"=. Especially, level and -precedences for a rule including patterns of the form \verb="{ x }"= -are relative not to the textual notation but to the notation where the -curly brackets have been removed (e.g. the level and the associativity -given to some notation, say \verb="{ y } & { z }"= in fact applies to -the underlying \verb="{ x }"=-free rule which is \verb="y & z"=). - -\paragraph{Persistence of notations} - -Notations do not survive the end of sections. They survive modules -unless the command {\tt Local Notation} is used instead of {\tt -Notation}. - -\section[Interpretation scopes]{Interpretation scopes\index{Interpretation scopes} -\label{scopes}} -% Introduction - -An {\em interpretation scope} is a set of notations for terms with -their interpretation. Interpretation scopes provide a weak, -purely syntactical form of notation overloading: the same notation, for -instance the infix symbol \verb=+=, can be used to denote distinct -definitions of the additive operator. Depending on which interpretation -scope is currently open, the interpretation is different. -Interpretation scopes can include an interpretation for -numerals and strings. However, this is only made possible at the -{\ocaml} level. - -See Figure \ref{notation-syntax} for the syntax of notations including -the possibility to declare them in a given scope. Here is a typical -example which declares the notation for conjunction in the scope {\tt -type\_scope}. - -\begin{verbatim} -Notation "A /\ B" := (and A B) : type_scope. -\end{verbatim} - -\Rem A notation not defined in a scope is called a {\em lonely} notation. - -\subsection{Global interpretation rules for notations} - -At any time, the interpretation of a notation for term is done within -a {\em stack} of interpretation scopes and lonely notations. In case a -notation has several interpretations, the actual interpretation is the -one defined by (or in) the more recently declared (or open) lonely -notation (or interpretation scope) which defines this notation. -Typically if a given notation is defined in some scope {\scope} but -has also an interpretation not assigned to a scope, then, if {\scope} -is open before the lonely interpretation is declared, then the lonely -interpretation is used (and this is the case even if the -interpretation of the notation in {\scope} is given after the lonely -interpretation: otherwise said, only the order of lonely -interpretations and opening of scopes matters, and not the declaration -of interpretations within a scope). - -The initial state of {\Coq} declares three interpretation scopes and -no lonely notations. These scopes, in opening order, are {\tt -core\_scope}, {\tt type\_scope} and {\tt nat\_scope}. - -The command to add a scope to the interpretation scope stack is -\comindex{Open Scope} -\comindex{Close Scope} -\begin{quote} -{\tt Open Scope} {\scope}. -\end{quote} -It is also possible to remove a scope from the interpretation scope -stack by using the command -\begin{quote} -{\tt Close Scope} {\scope}. -\end{quote} -Notice that this command does not only cancel the last {\tt Open Scope -{\scope}} but all the invocations of it. - -\Rem {\tt Open Scope} and {\tt Close Scope} do not survive the end of -sections where they occur. When defined outside of a section, they are -exported to the modules that import the module where they occur. - -\begin{Variants} - -\item {\tt Local Open Scope} {\scope}. - -\item {\tt Local Close Scope} {\scope}. - -These variants are not exported to the modules that import the module -where they occur, even if outside a section. - -\item {\tt Global Open Scope} {\scope}. - -\item {\tt Global Close Scope} {\scope}. - -These variants survive sections. They behave as if {\tt Global} were -absent when not inside a section. - -\end{Variants} - -\subsection{Local interpretation rules for notations} - -In addition to the global rules of interpretation of notations, some -ways to change the interpretation of subterms are available. - -\subsubsection{Local opening of an interpretation scope -\label{scopechange} -\index{\%} -\comindex{Delimit Scope} -\comindex{Undelimit Scope}} - -It is possible to locally extend the interpretation scope stack using -the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey} -for atomic terms), where {\delimkey} is a special identifier called -{\em delimiting key} and bound to a given scope. - -In such a situation, the term {\term}, and all its subterms, are -interpreted in the scope stack extended with the scope bound to -{\delimkey}. - -To bind a delimiting key to a scope, use the command - -\begin{quote} -\texttt{Delimit Scope} {\scope} \texttt{with} {\ident} -\end{quote} - -To remove a delimiting key of a scope, use the command - -\begin{quote} -\texttt{Undelimit Scope} {\scope} -\end{quote} - -\subsubsection{Binding arguments of a constant to an interpretation scope -\comindex{Arguments}} - -It is possible to set in advance that some arguments of a given -constant have to be interpreted in a given scope. The command is -\begin{quote} -{\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -\end{quote} -where the list is a prefix of the list of the arguments of {\qualid} eventually -annotated with their {\scope}. Grouping round parentheses can be used to -decorate multiple arguments with the same scope. {\scope} can be either a scope -name or its delimiting key. For example the following command puts the first two -arguments of {\tt plus\_fct} in the scope delimited by the key {\tt F} ({\tt - Rfun\_scope}) and the last argument in the scope delimited by the key {\tt R} -({\tt R\_scope}). - -\begin{coq_example*} -Arguments plus_fct (f1 f2)%F x%R. -\end{coq_example*} - -The {\tt Arguments} command accepts scopes decoration to all grouping -parentheses. In the following example arguments {\tt A} and {\tt B} -are marked as maximally inserted implicit arguments and are -put into the {\tt type\_scope} scope. - -\begin{coq_example*} -Arguments respectful {A B}%type (R R')%signature _ _. -\end{coq_example*} - -When interpreting a term, if some of the arguments of {\qualid} are -built from a notation, then this notation is interpreted in the scope -stack extended by the scope bound (if any) to this argument. The -effect of the scope is limited to the argument itself. It does not propagate -to subterms but the subterms that, after interpretation of the -notation, turn to be themselves arguments of a reference are -interpreted accordingly to the arguments scopes bound to this reference. - -Arguments scopes can be cleared with the following command: - -\begin{quote} -{\tt Arguments {\qualid} : clear scopes} -\end{quote} - -Extra argument scopes, to be used in case of coercion to Funclass -(see Chapter~\ref{Coercions-full}) or with a computed type, -can be given with - -\begin{quote} -{\tt Arguments} {\qualid} \nelist{\textunderscore {\tt \%} \scope}{} {\tt : extra scopes.} -\end{quote} - -\begin{Variants} -\item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} - -This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -but survives when a section is closed instead -of stopping working at section closing. Without the {\tt Global} modifier, -the effect of the command stops when the section it belongs to ends. - -\item {\tt Local Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} - -This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -but does not survive modules and files. -Without the {\tt Local} modifier, the effect of the command is -visible from within other modules or files. - -\end{Variants} - -\SeeAlso The command to show the scopes bound to the arguments of a -function is described in Section~\ref{About}. - -\subsubsection{Binding types of arguments to an interpretation scope} - -When an interpretation scope is naturally associated to a type -(e.g. the scope of operations on the natural numbers), it may be -convenient to bind it to this type. When a scope {\scope} is bound to -a type {\type}, any new function defined later on gets its arguments -of type {\type} interpreted by default in scope {\scope} (this default -behavior can however be overwritten by explicitly using the command -{\tt Arguments}). - -Whether the argument of a function has some type {\type} is determined -statically. For instance, if {\tt f} is a polymorphic function of type -{\tt forall X:Type, X -> X} and type {\tt t} is bound to a scope -{\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not -recognized as an argument to be interpreted in scope {\scope}. - -\comindex{Bind Scope} -\label{bindscope} -More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be -bound to an interpretation scope. The command to do it is -\begin{quote} -{\tt Bind Scope} {\scope} \texttt{with} {\class} -\end{quote} - -\Example -\begin{coq_example} -Parameter U : Set. -Bind Scope U_scope with U. -Parameter Uplus : U -> U -> U. -Parameter P : forall T:Set, T -> U -> Prop. -Parameter f : forall T:Set, T -> U. -Infix "+" := Uplus : U_scope. -Unset Printing Notations. -Open Scope nat_scope. (* Define + on the nat as the default for + *) -Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). -\end{coq_example} - -\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on -interpretation. See the next section. - -\SeeAlso The command to show the scopes bound to the arguments of a -function is described in Section~\ref{About}. - -\Rem In notations, the subterms matching the identifiers of the -notations are interpreted in the scope in which the identifiers -occurred at the time of the declaration of the notation. Here is an -example: - -\begin{coq_example} -Parameter g : bool -> bool. -Notation "@@" := true (only parsing) : bool_scope. -Notation "@@" := false (only parsing): mybool_scope. - -(* Defining a notation while the argument of g is bound to bool_scope *) -Bind Scope bool_scope with bool. -Notation "# x #" := (g x) (at level 40). -Check # @@ #. -(* Rebinding the argument of g to mybool_scope has no effect on the notation *) -Arguments g _%mybool_scope. -Check # @@ #. -(* But we can force the scope *) -Delimit Scope mybool_scope with mybool. -Check # @@%mybool #. -\end{coq_example} - -\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}} - -The scope {\tt type\_scope} has a special status. It is a primitive -interpretation scope which is temporarily activated each time a -subterm of an expression is expected to be a type. It is delimited by -the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also -used in certain situations where an expression is statically known to -be a type, including the conclusion and the type of hypotheses within -an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal}) -the statement of a theorem, the type of -a definition, the type of a binder, the domain and codomain of -implication, the codomain of products, and more generally any type -argument of a declared or defined constant. - -\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}} - -The scope {\tt function\_scope} also has a special status. -It is temporarily activated each time the argument of a global reference is -recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}. - -\subsection{Interpretation scopes used in the standard library of {\Coq}} - -We give an overview of the scopes used in the standard library of -{\Coq}. For a complete list of notations in each scope, use the -commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. - -\subsubsection{\tt type\_scope} - -This scope includes infix {\tt *} for product types and infix {\tt +} for -sum types. It is delimited by key {\tt type}, and bound to the coercion class -{\tt Sortclass}, as described at \ref{bindscope}. - -\subsubsection{\tt nat\_scope} - -This scope includes the standard arithmetical operators and relations on -type {\tt nat}. Positive numerals in this scope are mapped to their -canonical representent built from {\tt O} and {\tt S}. The scope is -delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}). - -\subsubsection{\tt N\_scope} - -This scope includes the standard arithmetical operators and relations on -type {\tt N} (binary natural numbers). It is delimited by key {\tt N} -and comes with an interpretation for numerals as closed term of type {\tt N}. - -\subsubsection{\tt Z\_scope} - -This scope includes the standard arithmetical operators and relations on -type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} -and comes with an interpretation for numerals as closed term of type {\tt Z}. - -\subsubsection{\tt positive\_scope} - -This scope includes the standard arithmetical operators and relations on -type {\tt positive} (binary strictly positive numbers). It is -delimited by key {\tt positive} and comes with an interpretation for -numerals as closed term of type {\tt positive}. - -\subsubsection{\tt Q\_scope} - -This scope includes the standard arithmetical operators and relations on -type {\tt Q} (rational numbers defined as fractions of an integer and -a strictly positive integer modulo the equality of the -numerator-denominator cross-product). As for numerals, only $0$ and -$1$ have an interpretation in scope {\tt Q\_scope} (their -interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively). - -\subsubsection{\tt Qc\_scope} - -This scope includes the standard arithmetical operators and relations on the -type {\tt Qc} of rational numbers defined as the type of irreducible -fractions of an integer and a strictly positive integer. - -\subsubsection{\tt real\_scope} - -This scope includes the standard arithmetical operators and relations on -type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R} -and comes with an interpretation for numerals using the {\tt IZR} -morphism from binary integer numbers to {\tt R}. - -\subsubsection{\tt bool\_scope} - -This scope includes notations for the boolean operators. It is -delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}). - -\subsubsection{\tt list\_scope} - -This scope includes notations for the list operators. It is -delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}). - -\subsubsection{\tt function\_scope} - -This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, -as described at \ref{bindscope}. - -\subsubsection{\tt core\_scope} - -This scope includes the notation for pairs. It is delimited by key {\tt core}. - -\subsubsection{\tt string\_scope} - -This scope includes notation for strings as elements of the type {\tt -string}. Special characters and escaping follow {\Coq} conventions -on strings (see Section~\ref{strings}). Especially, there is no -convention to visualize non printable characters of a string. The -file {\tt String.v} shows an example that contains quotes, a newline -and a beep (i.e. the ASCII character of code 7). - -\subsubsection{\tt char\_scope} - -This scope includes interpretation for all strings of the form -\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form -\verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly -with leading 0's), or of the form \verb!""""!. Their respective -denotations are the ASCII code of $c$, the decimal ASCII code $nnn$, -or the ASCII code of the character \verb!"! (i.e. the ASCII code -34), all of them being represented in the type {\tt ascii}. - -\subsection{Displaying informations about scopes} - -\subsubsection{\tt Print Visibility\comindex{Print Visibility}} - -This displays the current stack of notations in scopes and lonely -notations that is used to interpret a notation. The top of the stack -is displayed last. Notations in scopes whose interpretation is hidden -by the same notation in a more recently open scope are not -displayed. Hence each notation is displayed only once. - -\variant - -{\tt Print Visibility {\scope}}\\ - -This displays the current stack of notations in scopes and lonely -notations assuming that {\scope} is pushed on top of the stack. This -is useful to know how a subterm locally occurring in the scope of -{\scope} is interpreted. - -\subsubsection{\tt Print Scope {\scope}\comindex{Print Scope}} - -This displays all the notations defined in interpretation scope -{\scope}. It also displays the delimiting key if any and the class to -which the scope is bound, if any. - -\subsubsection{\tt Print Scopes\comindex{Print Scopes}} - -This displays all the notations, delimiting keys and corresponding -class of all the existing interpretation scopes. -It also displays the lonely notations. - -\section[Abbreviations]{Abbreviations\index{Abbreviations} -\label{Abbreviations} -\comindex{Notation}} - -An {\em abbreviation} is a name, possibly applied to arguments, that -denotes a (presumably) more complex expression. Here are examples: - -\begin{coq_eval} -Require Import List. -Require Import Relations. -Set Printing Notations. -\end{coq_eval} -\begin{coq_example} -Notation Nlist := (list nat). -Check 1 :: 2 :: 3 :: nil. -Notation reflexive R := (forall x, R x x). -Check forall A:Prop, A <-> A. -Check reflexive iff. -\end{coq_example} - -An abbreviation expects no precedence nor associativity, since it -is parsed as usual application. Abbreviations are used as -much as possible by the {\Coq} printers unless the modifier -\verb=(only parsing)= is given. - -Abbreviations are bound to an absolute name as an ordinary -definition is, and they can be referred by qualified names too. - -Abbreviations are syntactic in the sense that they are bound to -expressions which are not typed at the time of the definition of the -abbreviation but at the time it is used. Especially, abbreviations can -be bound to terms with holes (i.e. with ``\_''). The general syntax -for abbreviations is -\begin{quote} -\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident}{} \texttt{:=} {\term} - \zeroone{{\tt (only parsing)}}~\verb=.= -\end{quote} - -\Example -\begin{coq_eval} -Set Strict Implicit. -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Definition explicit_id (A:Set) (a:A) := a. -Notation id := (explicit_id _). -Check (id 0). -\end{coq_example} - -Abbreviations do not survive the end of sections. No typing of the denoted -expression is performed at definition time. Type-checking is done only -at the time of use of the abbreviation. - -%\Rem \index{Syntactic Definition} % -%Abbreviations are similar to the {\em syntactic -%definitions} available in versions of {\Coq} prior to version 8.0, -%except that abbreviations are used for printing (unless the modifier -%\verb=(only parsing)= is given) while syntactic definitions were not. - -\section{Tactic Notations -\label{Tactic-Notation} -\comindex{Tactic Notation}} - -Tactic notations allow to customize the syntax of the tactics of the -tactic language. -%% \footnote{Tactic notations are just a simplification of -%% the {\tt Grammar tactic simple\_tactic} command that existed in -%% versions prior to version 8.0.} -Tactic notations obey the following syntax: -\medskip - -\noindent -\begin{tabular}{lcl} -{\sentence} & ::= & \zeroone{\tt Local} \texttt{Tactic Notation} \zeroone{\taclevel} \sequence{\proditem}{} \\ -& & \texttt{:= {\tac} .}\\ -{\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ -{\taclevel} & ::= & {\tt (at level} {\naturalnumber}{\tt )} \\ -{\tacargtype}\!\! & ::= & -%{\tt preident} $|$ -{\tt ident} $|$ -{\tt simple\_intropattern} $|$ -{\tt reference} \\ & $|$ & -{\tt hyp} $|$ -{\tt hyp\_list} $|$ -{\tt ne\_hyp\_list} \\ & $|$ & -% {\tt quantified\_hypothesis} \\ & $|$ & -{\tt constr} $|$ {\tt uconstr} $|$ -{\tt constr\_list} $|$ -{\tt ne\_constr\_list} \\ & $|$ & -%{\tt castedopenconstr} $|$ -{\tt integer} $|$ -{\tt integer\_list} $|$ -{\tt ne\_integer\_list} \\ & $|$ & -{\tt int\_or\_var} $|$ -{\tt int\_or\_var\_list} $|$ -{\tt ne\_int\_or\_var\_list} \\ & $|$ & -{\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)} - -\end{tabular} -\medskip - -A tactic notation {\tt Tactic Notation {\taclevel} -{\sequence{\proditem}{}} := {\tac}} extends the parser and -pretty-printer of tactics with a new rule made of the list of -production items. It then evaluates into the tactic expression -{\tac}. For simple tactics, it is recommended to use a terminal -symbol, i.e. a {\str}, for the first production item. The tactic -level indicates the parsing precedence of the tactic notation. This -information is particularly relevant for notations of tacticals. -Levels 0 to 5 are available (default is 0). -To know the parsing precedences of the -existing tacticals, use the command -\comindex{Print Grammar tactic} - {\tt Print Grammar tactic.} - -Each type of tactic argument has a specific semantic regarding how it -is parsed and how it is interpreted. The semantic is described in the -following table. The last command gives examples of tactics which -use the corresponding kind of argument. - -\medskip -\noindent -\begin{tabular}{l|l|l|l} -Tactic argument type & parsed as & interpreted as & as in tactic \\ -\hline & & & \\ -{\tt\small ident} & identifier & a user-given name & {\tt intro} \\ -{\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\ -{\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\ -%% quantified_hypothesis actually not supported -%%{\tt\small quantified\_hypothesis} & identifier or integer & a named or non dep. hyp. of the goal & {\tt intros until}\\ -{\tt\small reference} & qualified identifier & a global reference of term & {\tt unfold}\\ -{\tt\small constr} & term & a term & {\tt exact} \\ -{\tt\small uconstr} & term & an untyped term & {\tt refine} \\ -%% castedopenconstr actually not supported -%%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\ -{\tt\small integer} & integer & an integer & \\ -{\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\ -{\tt\small tactic} & tactic at level 5 & a tactic & \\ -{\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\ -{\tt\small {\nterm{entry}}\_list} & list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted & \\ -{\tt\small ne\_{\nterm{entry}}\_list} & non-empty list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted& \\ -\end{tabular} - -\Rem In order to be bound in tactic definitions, each syntactic entry -for argument type must include the case of simple {\ltac} identifier -as part of what it parses. This is naturally the case for {\tt ident}, -{\tt simple\_intropattern}, {\tt reference}, {\tt constr}, ... but not -for {\tt integer}. This is the reason for introducing a special entry -{\tt int\_or\_var} which evaluates to integers only but which -syntactically includes identifiers in order to be usable in tactic -definitions. - -\Rem The {\tt {\nterm{entry}}\_list} and {\tt ne\_{\nterm{entry}}\_list} -entries can be used in primitive tactics or in other notations at -places where a list of the underlying entry can be used: {\nterm{entry}} is -either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or -{\tt\small int\_or\_var}. - -Tactic notations do not survive the end of sections. They survive -modules unless the command {\tt Local Tactic Notation} is used instead -of {\tt Tactic Notation}. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index e63e6731ec..9545a47c9b 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -109,7 +109,6 @@ Options A and B of the licence are {\em not} elected.} \include{RefMan-ssr} \part{User extensions} -\include{RefMan-syn.v}% The Syntax and the Grammar commands %%SUPPRIME \include{RefMan-tus.v}% Writing tactics \include{RefMan-sch.v}% The Scheme commands |