diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 34 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 533 |
2 files changed, 370 insertions, 197 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 838926d651..ab1edc0b27 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -40,8 +40,7 @@ induction for objects in type `identᵢ`. Induction scheme for tree and forest. - The definition of principle of mutual induction for tree and forest - over the sort Set is defined by the command: + A mutual induction principle for tree and forest in sort ``Set`` can be defined using the command .. coqtop:: none @@ -193,10 +192,12 @@ command generates the induction principle for each `identᵢ`, following the recursive structure and case analyses of the corresponding function identᵢ’. -Remark: There is a difference between obtaining an induction scheme by -using ``Functional Scheme`` on a function defined by ``Function`` or not. -Indeed, ``Function`` generally produces smaller principles, closer to the -definition written by the user. +.. warning:: + + There is a difference between induction schemes generated by the command + :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, + :cmd:`Function` generally produces smaller principles that are closer to how + a user would implement them. See :ref:`advanced-recursive-functions` for details. .. example:: @@ -257,11 +258,6 @@ definition written by the user. auto with arith. Qed. - Remark: There is a difference between obtaining an induction scheme - for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using - ``Functional Scheme`` after a normal definition using ``Fixpoint`` or - ``Definition``. See :ref:`advanced-recursive-functions` for details. - .. example:: Induction scheme for tree_size. @@ -298,15 +294,15 @@ definition written by the user. | cons t f' => (tree_size t + forest_size f') end. - Remark: Function generates itself non mutual induction principles - tree_size_ind and forest_size_ind: + Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` + generated by ``Function`` are not mutual. .. coqtop:: all Check tree_size_ind. - The definition of mutual induction principles following the recursive - structure of `tree_size` and `forest_size` is defined by the command: + Mutual induction principles following the recursive structure of ``tree_size`` + and ``forest_size`` can be generated by the following command: .. coqtop:: all @@ -352,10 +348,8 @@ having inverted the instance with the tactic `inversion`. .. example:: - Let us consider the relation `Le` over natural numbers and the following - variable: - - .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning + Consider the relation `Le` over natural numbers and the following + parameter ``P``: .. coqtop:: all @@ -363,7 +357,7 @@ having inverted the instance with the tactic `inversion`. | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Axiom P : nat -> nat -> Prop. + Parameter P : nat -> nat -> Prop. To generate the inversion lemma for the instance `(Le (S n) m)` and the sort `Prop`, we do: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3b95a37ed3..5089a1b3e3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -10,15 +10,14 @@ 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 -``Notation`` and ``Infix``. They are described in section :ref:`Notations`. There is also a -variant of ``Notation`` which does not modify the parser. This provides with a -form of abbreviation and it is described in Section :ref:`Abbreviations`. It is +:cmd:`Notation` and :cmd:`Infix`; they will be described in the +:ref:`next section <Notations>`. There is also a +variant of :cmd:`Notation` which does not modify the parser; this provides a +form of :ref:`abbreviation <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 ``Tactic Notation``. -It is described in Section :ref:`TacticNotation`. +different contexts; to achieve this form of overloading, |Coq| offers a notion +of :ref:`interpretation scopes <Scopes>`. +The main command to provide custom notations for tactics is :cmd:`Tactic Notation`. .. coqtop:: none @@ -44,18 +43,18 @@ logical conjunction (and). Such a notation is declared by Notation "A /\ B" := (and A B). -The expression :g:`(and A B)` is the abbreviated term and the string ``"A /\ B"`` +The expression :g:`(and A B)` is the abbreviated term and the string :g:`"A /\ B"` (called a *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 *tokens* separated by spaces. Identifiers in the string (such as ``A`` and ``B``) are the *parameters* -of the notation. They must occur at least once each in the denoted term. The +of the notation. Each of them must occur at least once in the denoted term. The other elements of the string (such as ``/\``) are the *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, +single 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. @@ -66,15 +65,15 @@ example. 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 12.1.7), explicit precedences and associativity rules -have to be given. +expression (see :ref:`ReservingNotations`), explicit precedences and +associativity rules have to be given. .. note:: 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:`ImplicitArguments`), coercions (see Section :ref:`Coercions`), - etc. are resolved at the time of the declaration of the notation. + given. In particular, disambiguation of constants, :ref:`implicit arguments + <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the + time of the declaration of the notation. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -106,13 +105,13 @@ is 100, for example 85 for disjunction and 80 for conjunction [#and_or_levels]_. Similarly, an associativity is needed to decide whether :g:`True /\ False /\ False` defaults to :g:`True /\ (False /\ False)` (right associativity) or to :g:`(True /\ False) /\ False` (left associativity). We may even consider that the -expression is not well- formed and that parentheses are mandatory (this is a “no +expression is not well-formed and that parentheses are mandatory (this is a “no associativity”) [#no_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 ``Notation`` +given between parentheses in a list of modifiers that the :cmd:`Notation` command understands. Here is how the previous examples refine. .. coqtop:: in @@ -120,11 +119,12 @@ command understands. Here is how the previous examples refine. Notation "A /\ B" := (and A B) (at level 80, right associativity). Notation "A \/ B" := (or A B) (at level 85, right associativity). -By default, a notation is considered non associative, but the +By default, a notation is considered nonassociative, but the precedence level is mandatory (except for special cases whose level is -canonical). The level is either a number or the phrase `next level` -whose meaning is obvious. The list of levels already assigned is on -Figure 3.1. +canonical). The level is either a number or the phrase ``next level`` +whose meaning is obvious. +Some :ref:`associativities are predefined <init-notations>` in the +``Notations`` module. .. TODO I don't find it obvious -- CPC @@ -139,14 +139,14 @@ instance define prefix notations. Notation "~ x" := (not x) (at level 75, right associativity). One can also define notations for incomplete terms, with the hole -expected to be inferred at typing time. +expected to be inferred during type checking. .. coqtop:: in Notation "x = y" := (@eq _ x y) (at level 70, no associativity). One can define *closed* notations whose both sides are symbols. In this case, -the default precedence level for the inner subexpression is 200, and the default +the default precedence level for the inner sub-expression is 200, and the default level for the notation itself is 0. .. coqtop:: in @@ -162,7 +162,7 @@ One can also define notations for binders. In the last case though, there is a conflict with the notation for type casts. The notation for types casts, as shown by the command :cmd:`Print Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, -it is necessary to put x at a level below 100, typically 99. Hence, a correct +it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: .. coqtop:: all @@ -176,7 +176,7 @@ Simple factorization rules ~~~~~~~~~~~~~~~~~~~~~~~~~~ Coq extensible parsing is performed by *Camlp5* which is essentially a LL1 -parser: it decides which notation to parse by looking tokens from left to right. +parser: it decides which notation to parse by looking at 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. @@ -186,21 +186,21 @@ rules. Some simple left factorization work has to be done. Here is an example. Notation "x < y < z" := (x < y /\ y < z) (at level 70). In order to factorize the left part of the rules, the subexpression -referred by y has to be at the same level in both rules. However the -default behavior puts 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 y, as follows. +referred to by ``y`` has to be at the same level in both rules. However the +default behavior puts ``y`` at the next level below 70 in the first rule +(``no associativity`` is the default), and at 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 ``y``, as follows. -.. coqtop:: all +.. coqtop:: in Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). 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:`thecoqlibrary`. +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 the chapter on :ref:`thecoqlibrary`. .. cmd:: Print Grammar constr. @@ -209,13 +209,13 @@ predefined notations can be found in Chapter :ref:`thecoqlibrary`. .. cmd:: Print Grammar pattern. This displays the state of the subparser of patterns (the parser used in the - grammar of the match with constructions). + grammar of the ``match with`` constructions). Displaying symbolic notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The command ``Notation`` has an effect both on the Coq parser and on the +The command :cmd:`Notation` has an effect both on the Coq parser and on the Coq printer. For example: .. coqtop:: all @@ -283,7 +283,7 @@ the possible following elements delimited by single quotes: (4 spaces in the example) - well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are - translated into horizontal-orelse-vertical printing boxes; if the + translated into horizontal-or-else-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 “ ``[``” is applied at the beginning of each @@ -295,13 +295,13 @@ the possible following elements delimited by single quotes: of the box, and an extra indentation of the number of spaces given after the “``[``” is applied at the beginning of each newline -Notations do not survive the end of sections. No typing of the denoted -expression is performed at definition time. Type-checking is done only +Notations disappear when a section is closed. No typing of the denoted +expression is performed at definition time. Type checking is done only at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do so, the option ``only parsing`` is allowed in the list of modifiers - of ``Notation``. Conversely, the ``only printing`` modifier can be + of :cmd:`Notation`. Conversely, the ``only printing`` modifier 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. @@ -309,7 +309,7 @@ at the time of use of the notation. The Infix command ~~~~~~~~~~~~~~~~~~ -The ``Infix`` command is a shortening for declaring notations of infix +The :cmd:`Infix` command is a shortening for declaring notations of infix symbols. .. cmd:: Infix "@symbol" := @term ({+, @modifier}). @@ -324,6 +324,8 @@ symbols. Infix "/\" := and (at level 80, right associativity). +.. _ReservingNotations: + Reserving notations ~~~~~~~~~~~~~~~~~~~ @@ -341,14 +343,14 @@ state of Coq. Reserving a notation is also useful for simultaneously defining an inductive type or a recursive constant and a notation for it. -.. note:: The notations mentioned on Figure 3.1 are reserved. Hence +.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence their precedence and associativity cannot be changed. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Thanks to reserved notations, the inductive, co-inductive, record, recursive and -corecursive definitions can benefit of customized notations. To do this, insert +corecursive definitions can benefit from customized notations. To do this, insert a ``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 by :token:`decl_notation` for inductive, @@ -357,17 +359,23 @@ for records. Here are examples: .. coqtop:: in - Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B - where "A /\ B" := (and A B). + Reserved Notation "A & B" (at level 80). + +.. coqtop:: in + + Inductive and' (A B : Prop) : Prop := conj' : A -> B -> A & B + where "A & B" := (and' A B). - Fixpoint plus (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (p+m) - end +.. coqtop:: in + + 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). -Displaying informations about notations +Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. opt:: Printing Notations @@ -391,7 +399,7 @@ Locating notations To know to which notations a given symbol belongs to, use the :cmd:`Locate` command. You can call it on 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 +notation are replaced by “``_``” and where possible single quotes inserted around identifiers or tokens starting with a single quote are dropped. .. coqtop:: all @@ -404,7 +412,7 @@ Notations and binders Notations can include binders. This section lists different ways to deal with binders. For further examples, see also -Section :ref:`RecursiveNotationsWithBinders`. +:ref:`RecursiveNotationsWithBinders`. Binders bound in the notation and parsed as identifiers +++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -490,7 +498,7 @@ the following: This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the -constant :g:`sumbool` (see Section :ref:`specification`). +constant :g:`sumbool` (see :ref:`specification`). Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for @@ -517,7 +525,7 @@ is just an identifier, one could have said ``p at level 99 as strict pattern``. Note also that in the absence of a ``as ident``, ``as strict pattern`` or -``as pattern`` modifiers, the default is to consider subexpressions occurring +``as pattern`` modifiers, the default is to consider sub-expressions occurring in binding position and parsed as terms to be ``as ident``. .. _NotationsWithBinders: @@ -545,7 +553,7 @@ the next command fails because p does not bind in the instance of n. Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). -.. _RecursiveNotationsWithBinders: +.. _RecursiveNotations: Notations with recursive patterns ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -563,7 +571,7 @@ confused with the three-dots notation “``…``” used in this manual to denot a sequence of arbitrary size. On the left-hand side, the part “``x s .. s y``” of the notation parses -any number of time (but at least one time) a sequence of expressions +any number of times (but at least once) a sequence of expressions separated by the sequence of tokens ``s`` (in the example, ``s`` is just “``;``”). The right-hand side must contain a subterm of the form either @@ -572,7 +580,7 @@ called the *iterator* of the recursive notation is an arbitrary expression with distinguished placeholders and where :math:`t` is called the *terminating expression* of the recursive notation. In the example, we choose the names :math:`x` and :math:`y` but in practice they can of course be chosen -arbitrarily. Not atht the placeholder :math:`[~]_I` has to occur only once but +arbitrarily. Note that the placeholder :math:`[~]_I` has to occur only once but :math:`[~]_E` can occur several times. Parsing the notation produces a list of expressions which are used to @@ -595,9 +603,10 @@ and the terminating expression is ``nil``. Here are other examples: (t at level 39). Notations with recursive patterns can be reserved like standard -notations, they can also be declared within interpretation scopes (see -section 12.2). +notations, they can also be declared within +:ref:`interpretation scopes <Scopes>`. +.. _RecursiveNotationsWithBinders: Notations with recursive patterns involving binders ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -605,13 +614,14 @@ Notations with recursive patterns involving binders Recursive notations can also be used with binders. The basic example is: -.. coqtop:: all +.. coqtop:: in Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, y binder, right associativity). -The principle is the same as in Section 12.1.12 except that in the iterator +The principle is the same as in :ref:`RecursiveNotations` +except that in the iterator :math:`φ([~]_E , [~]_I)`, the placeholder :math:`[~]_E` can also occur in position of the binding variable of a ``fun`` or a ``forall``. @@ -620,10 +630,10 @@ binders, ``x`` and ``y`` must be marked as ``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 ``'`` (see Section 2.7.19) is used in the binding list, -the added binders are taken into account too. +generalization operator ``'`` (see :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 binder, +There are two flavors of binder parsing. If ``x`` and ``y`` are marked as binder, then a sequence such as :g:`a b c : T` will be accepted and interpreted as the sequence of binders :g:`(a:T) (b:T) (c:T)`. For instance, in the notation above, the syntax :g:`exists a b : nat, a = b` is valid. @@ -646,7 +656,7 @@ example of recursive notation with closed binders: A recursive pattern for binders can be used in position of a recursive pattern for terms. Here is an example: -.. coqtop:: in +.. coqtop:: in Notation "'FUNAPP' x .. y , f" := (fun x => .. (fun y => (.. (f x) ..) y ) ..) @@ -678,7 +688,7 @@ position of :g:`x`: In addition to ``global``, one can restrict the syntax of a sub-expression by using the entry names ``ident`` or ``pattern`` -already seen in Section :ref:`NotationsWithBinders`, even when the +already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: @@ -687,13 +697,168 @@ side. E.g.: Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +Custom entries +~~~~~~~~~~~~~~ + +.. cmd:: Declare Custom Entry @ident + + This command allows to define new grammar entries, called *custom + entries*, that can later be referred to using the entry name + :n:`custom @ident`. + +.. example:: + + For instance, we may want to define an ad hoc + parser for arithmetical operations and proceed as follows: + + .. coqtop:: all + + Inductive Expr := + | One : Expr + | Mul : Expr -> Expr -> Expr + | Add : Expr -> Expr -> Expr. + + Declare Custom Entry expr. + Notation "[ e ]" := e (e custom expr at level 2). + Notation "1" := One (in custom expr at level 0). + Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + Notation "( x )" := x (in custom expr, x at level 2). + Notation "{ x }" := x (in custom expr, x constr). + Notation "x" := x (in custom expr at level 0, x ident). + + Axiom f : nat -> Expr. + Check fun x y z => [1 + y z + {f x}]. + Unset Printing Notations. + Check fun x y z => [1 + y z + {f x}]. + Set Printing Notations. + Check fun e => match e with + | [1 + 1] => [1] + | [x y + z] => [x + y z] + | y => [y + e] + end. + +Custom entries have levels, like the main grammar of terms and grammar +of patterns have. The lower level is 0 and this is the level used by +default to put rules delimited with tokens on both ends. The level is +left to be inferred by Coq when using :n:`in custom @ident`. The +level is otherwise given explicitly by using the syntax +:n:`in custom @ident at level @num`, where :n:`@num` refers to the level. + +Levels are cumulative: a notation at level ``n`` of which the left end +is a term shall use rules at level less than ``n`` to parse this +sub-term. More precisely, it shall use rules at level strictly less +than ``n`` if the rule is declared with ``right associativity`` and +rules at level less or equal than ``n`` if the rule is declared with +``left associativity``. Similarly, a notation at level ``n`` of which +the right end is a term shall use by default rules at level strictly +less than ``n`` to parse this sub-term if the rule is declared left +associative and rules at level less or equal than ``n`` if the rule is +declared right associative. This is what happens for instance in the +rule + +.. coqtop:: in + + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + +where ``x`` is any expression parsed in entry +``expr`` at level less or equal than ``2`` (including, recursively, +the given rule) and ``y`` is any expression parsed in entry ``expr`` +at level strictly less than ``2``. + +Rules associated to an entry can refer different sub-entries. The +grammar entry name ``constr`` can be used to refer to the main grammar +of term as in the rule + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +which indicates that the subterm ``x`` should be +parsed using the main grammar. If not indicated, the level is computed +as for notations in ``constr``, e.g. using 200 as default level for +inner sub-expressions. The level can otherwise be indicated explicitly +by using ``constr at level n`` for some ``n``, or ``constr at next +level``. + +Conversely, custom entries can be used to parse sub-expressions of the +main grammar, or from another custom entry as is the case in + +.. coqtop:: in + + Notation "[ e ]" := e (e custom expr at level 2). + +to indicate that ``e`` has to be parsed at level ``2`` of the grammar +associated to the custom entry ``expr``. The level can be omitted, as in + +.. coqtop:: in + + Notation "[ e ]" := e (e custom expr)`. + +in which case Coq tries to infer it. + +In the absence of an explicit entry for parsing or printing a +sub-expression of a notation in a custom entry, the default is to +consider that this sub-expression is parsed or printed in the same +custom entry where the notation is defined. In particular, if ``x at +level n`` is used for a sub-expression of a notation defined in custom +entry ``foo``, it shall be understood the same as ``x custom foo at +level n``. + +In general, rules are required to be *productive* on the right-hand +side, i.e. that they are bound to an expression which is not +reduced to a single variable. If the rule is not productive on the +right-hand side, as it is the case above for + +.. coqtop:: in + + Notation "( x )" := x (in custom expr at level 0, x at level 2). + +and + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +it is used as a *grammar coercion* which means that it is used to parse or +print an expression which is not available in the current grammar at the +current level of parsing or printing for this grammar but which is available +in another grammar or in another level of the current grammar. For instance, + +.. coqtop:: in + + Notation "( x )" := x (in custom expr at level 0, x at level 2). + +tells that parentheses can be inserted to parse or print an expression +declared at level ``2`` of ``expr`` whenever this expression is +expected to be used as a subterm at level 0 or 1. This allows for +instance to parse and print :g:`Add x y` as a subterm of :g:`Mul (Add +x y) z` using the syntax ``(x + y) z``. Similarly, + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +gives a way to let any arbitrary expression which is not handled by the +custom entry ``expr`` be parsed or printed by the main grammar of term +up to the insertion of a pair of curly brackets. + +.. cmd:: Print Grammar @ident. + + This displays the state of the grammar for terms and grammar for + patterns associated to the custom entry :token:`ident`. + Summary ~~~~~~~ -**Syntax of notations** +.. _NotationSyntax: + +Syntax of notations ++++++++++++++++++++ -The different syntactic variants of the command Notation are given on the -following figure. The optional :token:`scope` is described in the Section 12.2. +The different syntactic forms taken by the commands declaring +notations are given below. The optional :production:`scope` is described in +:ref:`Scopes`. .. productionlist:: coq notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. @@ -703,33 +868,44 @@ following figure. The optional :token:`scope` is described in the Section 12.2. : | CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : | Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : | CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. + : | [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. - modifiers : at level `natural` - : | `ident` , … , `ident` at level `natural` [`binderinterp`] + modifiers : at level `num` + : in custom `ident` + : in custom `ident` at level `num` + : | `ident` , … , `ident` at level `num` [`binderinterp`] : | `ident` , … , `ident` at next level [`binderinterp`] - : | `ident` ident - : | `ident` global - : | `ident` bigint - : | `ident` [strict] pattern [at level `natural`] - : | `ident` binder - : | `ident` closed binder + : | `ident` `explicit_subentry` : | left associativity : | right associativity : | no associativity : | only parsing : | only printing : | format `string` + explicit_subentry : ident + : | global + : | bigint + : | [strict] pattern [at level `num`] + : | binder + : | closed binder + : | constr [`binderinterp`] + : | constr at level `num` [`binderinterp`] + : | constr at next level [`binderinterp`] + : | custom [`binderinterp`] + : | custom at level `num` [`binderinterp`] + : | custom at next level [`binderinterp`] binderinterp : as ident : | as pattern : | as strict pattern .. note:: No typing of the denoted expression is performed at definition - time. Type-checking is done only at the time of use of the notation. + time. Type checking is done only at the time of use of the notation. -.. note:: Many examples of Notation may be found in the files composing +.. note:: Some examples of Notation may be found in the files composing the initial state of Coq (see directory :file:`$COQLIB/theories/Init`). -.. note:: The notation ``"{ x }"`` has a special status in such a way that +.. note:: The notation ``"{ x }"`` has a special status in the main grammars of + terms and patterns so that complex notations of the form ``"x + { y }"`` or ``"x * { y }"`` can be nested with correct precedences. Especially, every notation involving a pattern of the form ``"{ x }"`` is parsed as a notation where the @@ -743,14 +919,20 @@ following figure. The optional :token:`scope` is described in the Section 12.2. given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). -**Persistence of notations** +Persistence of notations +++++++++++++++++++++++++ -Notations do not survive the end of sections. +Notations disappear when a section is closed. .. cmd:: Local Notation @notation Notations survive modules unless the command ``Local Notation`` is used instead - of ``Notation``. + of :cmd:`Notation`. + +.. cmd:: Local Declare Custom Entry @ident + + Custom entries survive modules unless the command ``Local Declare + Custom Entry`` is used instead of :cmd:`Declare Custom Entry`. .. _Scopes: @@ -758,20 +940,20 @@ Interpretation scopes ---------------------- An *interpretation scope* is a set of notations for terms with their -interpretation. Interpretation scopes provide a weak, purely -syntactical form of notations overloading: the same notation, for -instance the infix symbol ``+`` can be used to denote distinct +interpretations. Interpretation scopes provide a weak, purely +syntactical form of notation overloading: the same notation, for +instance the infix symbol ``+``, can be used to denote distinct definitions of the additive operator. Depending on which interpretation -scopes is currently open, the interpretation is different. +scopes are currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See Figure 12.1 for the syntax of notations including the possibility -to declare them in a given scope. Here is a typical example which +See :ref:`above <NotationSyntax>` 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 ``type_scope``. -.. coqdoc:: +.. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. @@ -781,10 +963,10 @@ declares the notation for conjunction in the scope ``type_scope``. Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -At any time, the interpretation of a notation for term is done within +At any time, the interpretation of a notation for a term is done within a *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 +one defined by (or in) the more recently declared (or opened) 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 @@ -810,7 +992,7 @@ lonely notations. These scopes, in opening order, are ``core_scope``, stack by using the command :n:`Close Scope @scope`. Notice that this command does not only cancel the last :n:`Open Scope @scope` - but all the invocations of it. + but all its invocations. .. note:: ``Open Scope`` and ``Close Scope`` do not survive the end of sections where they occur. When defined outside of a section, they are exported @@ -890,29 +1072,29 @@ Binding arguments of a constant to an interpretation scope 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. + accordingly to the argument scopes bound to this reference. -.. cmdv:: Arguments @qualid : clear scopes + .. cmdv:: Arguments @qualid : clear scopes - Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. + This command can be used to clear argument scopes of :token:`qualid`. -.. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes + .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes - Defines extra argument scopes, to be used in case of coercion to Funclass - (see Chapter :ref:`implicitcoercions`) or with a computed type. + Defines extra argument scopes, to be used in case of coercion to ``Funclass`` + (see the :ref:`implicitcoercions` chapter) or with a computed type. -.. cmdv:: Global Arguments @qualid {+ @name%@scope} + .. cmdv:: Global Arguments @qualid {+ @name%@scope} - This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a - section is closed instead of stopping working at section closing. Without the - ``Global`` modifier, the effect of the command stops when the section it belongs - to ends. + This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a + section is closed instead of stopping working at section closing. Without the + ``Global`` modifier, the effect of the command stops when the section it belongs + to ends. -.. cmdv:: Local Arguments @qualid {+ @name%@scope} + .. cmdv:: Local Arguments @qualid {+ @name%@scope} - This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not - survive modules and files. Without the ``Local`` modifier, the effect of the - command is visible from within other modules or files. + This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not + survive modules and files. Without the ``Local`` modifier, the effect of the + command is visible from within other modules or files. .. seealso:: @@ -947,18 +1129,18 @@ 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 + 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 ``Arguments``). + using the command :cmd:`Arguments`). Whether the argument of a function has some type ``type`` is determined - statically. For instance, if f is a polymorphic function of type :g:`forall - X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, then :g:`a` of - type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted - in scope ``scope``. + statically. For instance, if ``f`` is a polymorphic function of type + :g:`forall X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, + then :g:`a` of type :g:`t` in :g:`f t a` is not recognized as an argument to + be interpreted in scope ``scope``. - More generally, any coercion :n:`@class` (see Chapter :ref:`implicitcoercions`) + More generally, any coercion :n:`@class` (see the :ref:`implicitcoercions` chapter) can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` @@ -980,12 +1162,6 @@ Binding types of arguments to an interpretation scope .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. -.. seealso:: - - :cmd:`About` - The command to show the scopes bound to the arguments of a - function is described in Section 2. - The ``type_scope`` interpretation scope ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -996,7 +1172,7 @@ scope which is temporarily activated each time a subterm of an expression is expected to be a type. It is delimited by the key ``type``, and bound to the coercion class ``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 Ltac goal match (see Section +type of hypotheses within an Ltac goal match (see :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 @@ -1007,7 +1183,7 @@ The ``function_scope`` interpretation scope .. index:: function_scope -The scope ``function_scope`` also has a special status. +The scope ``function_scope`` also has a special status. It is temporarily activated each time the argument of a global reference is recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or :g:`A -> B`. @@ -1017,39 +1193,39 @@ 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 Print -Scopes or Print Scope scope. +For a complete list of notations in each scope, use the commands :cmd:`Print +Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It - is delimited by key ``type``, and bound to the coercion class + is delimited by the key ``type``, and bound to the coercion class ``Sortclass``, as described above. ``function_scope`` - This scope is delimited by key ``function``, and bound to the coercion class + This scope is delimited by the key ``function``, and bound to the coercion class ``Funclass``, as described above. ``nat_scope`` This scope includes the standard arithmetical operators and relations on type nat. Positive numerals in this scope are mapped to their canonical - representent built from :g:`O` and :g:`S`. The scope is delimited by key + representent built from :g:`O` and :g:`S`. The scope is delimited by the key ``nat``, and bound to the type :g:`nat` (see above). ``N_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`N` (binary natural numbers). It is delimited by key ``N`` and comes + type :g:`N` (binary natural numbers). It is delimited by the key ``N`` and comes with an interpretation for numerals as closed terms of type :g:`N`. ``Z_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`Z` (binary integer numbers). It is delimited by key ``Z`` and comes - with an interpretation for numerals as closed term of type :g:`Z`. + type :g:`Z` (binary integer numbers). It is delimited by the key ``Z`` and comes + with an interpretation for numerals as closed terms of type :g:`Z`. ``positive_scope`` This scope includes the standard arithmetical operators and relations on type :g:`positive` (binary strictly positive numbers). It is delimited by key ``positive`` and comes with an interpretation for numerals as closed - term of type :g:`positive`. + terms of type :g:`positive`. ``Q_scope`` This scope includes the standard arithmetical operators and relations on @@ -1066,25 +1242,25 @@ Scopes or Print Scope scope. ``real_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`R` (axiomatic real numbers). It is delimited by key ``R`` and comes + type :g:`R` (axiomatic real numbers). It is delimited by the key ``R`` and comes with an interpretation for numerals using the :g:`IZR` morphism from binary integer numbers to :g:`R`. ``bool_scope`` - This scope includes notations for the boolean operators. It is delimited by + This scope includes notations for the boolean operators. It is delimited by the key ``bool``, and bound to the type :g:`bool` (see above). ``list_scope`` - This scope includes notations for the list operators. It is delimited by key + This scope includes notations for the list operators. It is delimited by the key ``list``, and bound to the type :g:`list` (see above). ``core_scope`` - This scope includes the notation for pairs. It is delimited by key ``core``. + This scope includes the notation for pairs. It is delimited by the key ``core``. ``string_scope`` This scope includes notation for strings as elements of the type string. Special characters and escaping follow Coq conventions on strings (see - Section 1.1). Especially, there is no convention to visualize non + :ref:`lexical-conventions`). Especially, there is no convention to visualize non printable characters of a string. The file :file:`String.v` shows an example that contains quotes, a newline and a beep (i.e. the ASCII character of code 7). @@ -1093,12 +1269,12 @@ Scopes or Print Scope scope. This scope includes interpretation for all strings of the form ``"c"`` where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is a three-digits number (possibly with leading 0's), or of the form - ``""""``. Their respective denotations are the ASCII code of c, the - decimal ASCII code nnn, or the ascii code of the character ``"`` (i.e. + ``""""``. Their respective denotations are the ASCII code of :g:`c`, the + decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e. the ASCII code 34), all of them being represented in the type :g:`ascii`. -Displaying informations about scopes +Displaying information about scopes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Print Visibility @@ -1106,28 +1282,29 @@ Displaying informations about scopes 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. + by the same notation in a more recently opened scope are not displayed. Hence each notation is displayed only once. -.. cmdv:: 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 ofscope is - interpreted. + .. cmdv:: Print Visibility @scope -.. cmdv:: Print Scope scope + This displays the current stack of notations in scopes and lonely + notations assuming that :token:`scope` is pushed on top of the stack. This is + useful to know how a subterm locally occurring in the scope :token:`scope` is + interpreted. - This displays all the notations defined in interpretation scopescope. - It also displays the delimiting key if any and the class to which the - scope is bound, if any. - -.. cmdv:: Print Scopes +.. cmd:: Print Scopes This displays all the notations, delimiting keys and corresponding - class of all the existing interpretation scopes. It also displays the + classes of all the existing interpretation scopes. It also displays the lonely notations. + .. cmdv:: Print Scope @scope + :name: Print Scope + + This displays all the notations defined in the interpretation scope :token:`scope`. + It also displays the delimiting key if any and the class to which the + scope is bound, if any. + .. _Abbreviations: Abbreviations @@ -1166,13 +1343,13 @@ Abbreviations much as possible by the Coq printers unless the modifier ``(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. + An abbreviation is bound to an absolute name as an ordinary definition is + and it also can be referred to by a qualified name. 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 “``_``”). For example: + abbreviation but at the time they are used. Especially, abbreviations + can be bound to terms with holes (i.e. with “``_``”). For example: .. coqtop:: none reset @@ -1182,14 +1359,17 @@ Abbreviations .. coqtop:: in Definition explicit_id (A:Set) (a:A) := a. + + .. coqtop:: in + Notation id := (explicit_id _). .. coqtop:: all Check (id 0). - Abbreviations do not survive the end of sections. No typing of the - denoted expression is performed at definition time. Type-checking is + Abbreviations disappear when a section is closed. No typing of the + denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. .. _TacticNotation: @@ -1197,13 +1377,12 @@ Abbreviations Tactic Notations ----------------- -Tactic notations allow to customize the syntax of the tactics of the -tactic language. Tactic notations obey the following syntax: +Tactic notations allow to customize the syntax of tactics. They have the following syntax: .. productionlist:: coq tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) - tactic_level : (at level `natural`) + tactic_level : (at level `num`) tactic_argument_type : ident | simple_intropattern | reference : | hyp | hyp_list | ne_hyp_list : | constr | uconstr | constr_list | ne_constr_list @@ -1220,7 +1399,7 @@ tactic language. Tactic notations obey the following syntax: a terminal symbol, i.e. a string, 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). + Levels 0 to 5 are available (default is 5). .. cmd:: Print Grammar tactic @@ -1247,12 +1426,12 @@ tactic language. Tactic notations obey the following syntax: * - ``simple_intropattern`` - intro_pattern - - an intro_pattern + - an intro pattern - intros * - ``hyp`` - identifier - - an hypothesis defined in context + - a hypothesis defined in context - clear * - ``reference`` @@ -1301,7 +1480,7 @@ tactic language. Tactic notations obey the following syntax: - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of simple L tac + entry for argument type must include the case of a simple |Ltac| identifier as part of what it parses. This is naturally the case for ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. This is the reason for introducing a special entry ``int_or_var`` which @@ -1315,16 +1494,16 @@ tactic language. Tactic notations obey the following syntax: .. cmdv:: Local Tactic Notation - Tactic notations do not survive the end of sections. They survive - modules unless the command Local Tactic Notation is used instead of - Tactic Notation. + Tactic notations disappear when a section is closed. They survive when + a module is closed unless the command ``Local Tactic Notation`` is used instead + of :cmd:`Tactic Notation`. .. rubric:: Footnotes .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as no associative but the parser on - which Coq is built, namely Camlp4, 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 +.. [#no_associativity] Coq accepts notations declared as nonassociative but the parser on + which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` + is in fact ``left associativity`` for the purposes of parsing |