diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/README.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/_static/notations.css | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 84 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 57 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 54 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 55 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 286 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 42 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 61 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 52 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 261 |
20 files changed, 611 insertions, 393 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 01240a062c..a20b74822c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the ``:undocumented:`` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type @@ -382,7 +382,7 @@ DO DON'T .. code:: - This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + This is equivalent to ``Axiom`` :token:`ident` : :token:`term`. .. diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 86914a71df..11f0cdc008 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the ``:undocumented:`` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type @@ -138,7 +138,7 @@ DO DON'T .. code:: - This is equivalent to ``Axiom`` :token`ident` : :token:`term`. + This is equivalent to ``Axiom`` :token:`ident` : :token:`term`. .. diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index f899945a35..dcb47d1786 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -60,9 +60,10 @@ margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */ } -.notation .hole { +.notation .hole, .std-token .pre { color: #4e9a06; font-style: italic; + font-weight: bold; } /***********************/ diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index cb267576b2..7b8a86d1ab 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -31,9 +31,9 @@ A variable pattern matches any value, and the identifier is bound to that value. The pattern “``_``” (called “don't care” or “wildcard” symbol) also matches any value, but does not bind anything. It may occur an arbitrary number of times in a pattern. Alias patterns written -:n:`(@pattern as @identifier)` are also accepted. This pattern matches the -same values as ``pattern`` does and ``identifier`` is bound to the matched -value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A +:n:`(@pattern as @ident)` are also accepted. This pattern matches the +same values as :token:`pattern` does and :token:`ident` is bound to the matched +value. A pattern of the form :n:`@pattern | @pattern` is called disjunctive. A list of patterns separated with commas is also considered as a pattern and is called *multiple pattern*. However multiple patterns can only occur at the root of pattern matching equations. Disjunctions of diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index f523a39477..e93b01f14d 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -28,7 +28,7 @@ Generating ML Code .. note:: - In the following, a qualified identifier `qualid` + In the following, a qualified identifier :token:`qualid` can be used to refer to any kind of |Coq| global "object" : constant, inductive type, inductive constructor or module name. @@ -47,30 +47,30 @@ extraction. They both display extracted term(s) inside |Coq|. All the following commands produce real ML files. User can choose to produce one monolithic file or one file per |Coq| library. -.. cmd:: Extraction "@file" {+ @qualid } +.. cmd:: Extraction @string {+ @qualid } Recursive extraction of all the mentioned objects and all - their dependencies in one monolithic `file`. + their dependencies in one monolithic file :token:`string`. Global and local identifiers are renamed according to the chosen ML language to fulfill its syntactic conventions, keeping original names as much as possible. .. cmd:: Extraction Library @ident - Extraction of the whole |Coq| library ``ident.v`` to an ML module - ``ident.ml``. In case of name clash, identifiers are here renamed + Extraction of the whole |Coq| library :n:`@ident.v` to an ML module + :n:`@ident.ml`. In case of name clash, identifiers are here renamed using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent renaming. .. cmd:: Recursive Extraction Library @ident - Extraction of the |Coq| library ``ident.v`` and all other modules - ``ident.v`` depends on. + Extraction of the |Coq| library :n:`@ident.v` and all other modules + :n:`@ident.v` depends on. .. cmd:: Separate Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all - their dependencies, just as ``Extraction "file"``, + their dependencies, just as :n:`Extraction @string {+ @qualid }`, but instead of producing one monolithic file, this command splits the produced code in separate ML files, one per corresponding Coq ``.v`` file. This command is hence quite similar to @@ -164,7 +164,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: .. cmd:: Extraction Inline {+ @qualid } In addition to the automatic inline feature, the constants - mentionned by this command will always be inlined during extraction. + mentioned by this command will always be inlined during extraction. .. cmd:: Extraction NoInline {+ @qualid } @@ -214,9 +214,9 @@ principles of extraction (logical parts and types). .. cmd:: Extraction Implicit @qualid [ {+ @ident } ] This experimental command allows declaring some arguments of - `qualid` as implicit, i.e. useless in extracted code and hence to - be removed by extraction. Here `qualid` can be any function or - inductive constructor, and the given `ident` are the names of + :token:`qualid` as implicit, i.e. useless in extracted code and hence to + be removed by extraction. Here :token:`qualid` can be any function or + inductive constructor, and the given :token:`ident` are the names of the concerned arguments. In fact, an argument can also be referred by a number indicating its position, starting from 1. @@ -253,7 +253,7 @@ what ML term corresponds to a given axiom. .. cmd:: Extract Constant @qualid => @string Give an ML extraction for the given constant. - The `string` may be an identifier or a quoted string. + The :token:`string` may be an identifier or a quoted string. .. cmd:: Extract Inlined Constant @qualid => @string @@ -315,24 +315,24 @@ native boolean type instead of the |Coq| one. The syntax is the following: .. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first `string`) and all its - constructors (all the `string` between square brackets). In this form, + extractions for the type itself (first :token:`string`) and all its + constructors (all the :token:`string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string - Same as before, with a final extra `string` that indicates how to + Same as before, with a final extra :token:`string` that indicates how to perform pattern matching over this inductive type. In this form, the ML extraction could be an arbitrary type. - For an inductive type with `k` constructors, the function used to - emulate the pattern matching should expect `(k+1)` arguments, first the `k` + For an inductive type with :math:`k` constructors, the function used to + emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k` branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no arguments is considered to have one unit argument, in order to block early evaluation of the branch: ``| O => bar`` leads to the functional - form ``(fun () -> bar)``. For instance, when extracting ``nat`` + form ``(fun () -> bar)``. For instance, when extracting :g:`nat` into |OCaml| ``int``, the code to be provided has type: ``(unit->'a)->(int->'a)->int->'a``. @@ -410,6 +410,52 @@ It is possible to instruct the extraction not to use particular filenames. For |OCaml|, a typical use of these commands is ``Extraction Blacklist String List``. +Additional settings +~~~~~~~~~~~~~~~~~~~ + +.. opt:: Extraction File Comment @string + :name: Extraction File Comment + + Provides a comment that is included at the beginning of the output files. + +.. opt:: Extraction Flag @num + :name: Extraction Flag + + Controls which optimizations are used during extraction, providing a finer-grained + control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. + Keeping an option off keeps the extracted ML more similar to the Coq term. + Values are: + + +-----+-------+----------------------------------------------------------------+ + | Bit | Value | Optimization (default is on unless noted otherwise) | + +-----+-------+----------------------------------------------------------------+ + | 0 | 1 | Remove local dummy variables | + +-----+-------+----------------------------------------------------------------+ + | 1 | 2 | Use special treatment for fixpoints | + +-----+-------+----------------------------------------------------------------+ + | 2 | 4 | Simplify case with iota-redux | + +-----+-------+----------------------------------------------------------------+ + | 3 | 8 | Factor case branches as functions | + +-----+-------+----------------------------------------------------------------+ + | 4 | 16 | (not available, default false) | + +-----+-------+----------------------------------------------------------------+ + | 5 | 32 | Simplify case as function of one argument | + +-----+-------+----------------------------------------------------------------+ + | 6 | 64 | Simplify case by swapping case and lambda | + +-----+-------+----------------------------------------------------------------+ + | 7 | 128 | Some case optimization | + +-----+-------+----------------------------------------------------------------+ + | 8 | 256 | Push arguments inside a letin | + +-----+-------+----------------------------------------------------------------+ + | 9 | 512 | Use linear let reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + | 10 | 1024 | Use linear beta reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + +.. flag:: Extraction TypeExpand + + If set, fully expand Coq types in ML. See the Coq source code to learn more. + Differences between |Coq| and ML type systems ---------------------------------------------- diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c8fb4bd00e..64e2d7c4ab 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -25,10 +25,10 @@ typed modulo insertion of appropriate coercions. We allow to write: Classes ------- -A class with `n` parameters is any defined name with a type -:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort. Thus a class with +A class with :math:`n` parameters is any defined name with a type +:n:`forall (@ident__1 : @type__1)..(@ident__n:@type__n), @sort`. Thus a class with parameters is considered as a single class and not as a family of -classes. An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`. +classes. An object of a class is any term of type :n:`@class @term__1 .. @term__n`. In addition to these user-defined classes, we have two built-in classes: @@ -40,20 +40,20 @@ In addition to these user-defined classes, we have two built-in classes: Formally, the syntax of a classes is defined as: .. productionlist:: - class: qualid - : | `Sortclass` - : | `Funclass` + class: `qualid` + : | Sortclass + : | Funclass Coercions --------- A name ``f`` can be declared as a coercion between a source user-defined class -``C`` with `n` parameters and a target class ``D`` if one of these +``C`` with :math:`n` parameters and a target class ``D`` if one of these conditions holds: * ``D`` is a user-defined class, then the type of ``f`` must have the form - :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m` + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where :math:`m` is the number of parameters of ``D``. * ``D`` is ``Funclass``, then the type of ``f`` must have the form :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`. @@ -124,7 +124,7 @@ Declaring Coercions .. cmd:: Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion between + Declares the construction denoted by :token:`qualid` as a coercion between the two given classes. .. exn:: @qualid not declared. @@ -159,23 +159,18 @@ Declaring Coercions .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to + Declares the construction denoted by :token:`qualid` as a coercion local to the current section. - .. cmdv:: Coercion @ident := @term + .. cmdv:: Coercion @ident := @term {? @type } - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines :token:`ident` just like :n:`Definition @ident := term {? @type }`, + and then declares :token:`ident` as a coercion between it source and its target. - .. cmdv:: Coercion @ident := @term : @type + .. cmdv:: Local Coercion @ident := @term {? @type } - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. - - .. cmdv:: Local Coercion @ident := @term - - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, + and then declares :token:`ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from @@ -207,10 +202,10 @@ grammar of inductive types from Figure :ref:`vernacular` as follows: \comindex{CoInductive \mbox{\rm (and coercions)}} .. productionlist:: - inductive : `Inductive` ind_body `with` ... `with` ind_body - : | `CoInductive` ind_body `with` ... `with` ind_body - ind_body : ident [binders] : term := [[|] constructor | ... | constructor] - constructor : ident [binders] [:[>] term] + inductive : Inductive `ind_body` with ... with `ind_body` + : | CoInductive `ind_body` with ... with `ind_body` + ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ] + constructor : `ident` [ `binders` ] [:[>] `term` ] Especially, if the extra ``>`` is present in a constructor declaration, this constructor is declared as a coercion. @@ -285,19 +280,21 @@ Activating the Printing of Coercions Classes as Records ------------------ +.. index:: :> (coercion) + We allow the definition of *Structures with Inheritance* (or classes as records) by extending the existing :cmd:`Record` macro. Its new syntax is: .. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` + The first identifier :token:`ident` is the name of the defined record and + :token:`sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be :n:`Build_@ident` if not given). + The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform + field type. Note that the fields always verify the uniform inheritance condition. If the optional ``>`` is given before the record name, then the constructor name is automatically declared as a coercion from the class of the last field type to the record name diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d219ebd0d..fd66de427c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -248,7 +248,7 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. -.. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with +.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with the ``zify`` tactic. .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index e7a8c238ac..ed2e1ea58c 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -81,7 +81,7 @@ performed using :ref:`typeclasses`. produces a goal which states that :math:`c` is not zero. * `variables` is the list of the variables in the decreasing order in - which they will be used in the Buchberger algorithm. If `variables` = `(@nil R)`, + which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`, then `lvar` is replaced by all the variables which are not in `parameters`. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index cc8870e2e4..56f84d0ff0 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -95,6 +95,14 @@ coercions. (the option is on by default). Coercion of subset types and pairs is still active in this case. +.. flag:: Program Mode + + Enables the program mode, in which 1) typechecking allows subset coercions and + 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and + :cmd:`Program Definition` act + like Program Fixpoint/Definition, generating obligations if there are + unresolved holes after typechecking. + .. _syntactic_control: Syntactic control over equalities @@ -102,7 +110,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern matching if a return or in clause is specified. Likewise, the +pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -118,8 +126,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in: else S (pred n). The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not -produce an equality, contrary to the let pattern construct :g:`let ’(x1, -..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +produce an equality, contrary to the let pattern construct +:g:`let '(x1,..., xn) := t in b`. +Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for example: @@ -180,7 +189,7 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term The optional order annotation follows the grammar: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 5bab63f6d0..99d689132d 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -376,8 +376,8 @@ The syntax for adding a new ring is sign :n:`@term` allows :tacn:`ring_simplify` to use a minus operation when outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The - term `:n:`@term` is a proof that a given sign function indicates expressions - that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See + term :token:`term` is a proof that a given sign function indicates expressions + that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. div :n:`@term` @@ -476,8 +476,8 @@ So now, what is the scheme for a normalization proof? Let p be the polynomial expression that the user wants to normalize. First a little piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|- -equivalent to ``(PEeval`` `v` `ap`\ ``)``. Then we replace it by ``(Pphi_dev`` `v` -``(norm`` `ap`\ ``))``, using the main correctness theorem and we reduce it to a +equivalent to `(PEeval v ap)`. Then we replace it by `(Pphi_dev v (norm ap))`, +using the main correctness theorem and we reduce it to a concrete expression `p’`, which is the concrete normal form of `p`. This is summarized in this diagram: ========= ====== ==== @@ -540,15 +540,15 @@ Dealing with fields .. tacv:: field [{* @term}] - decides the equality of two terms modulo - field operations and the equalities defined - by the :n:`@term`\ s. Each :n:`@term` has to be a proof of some equality - `m` ``=`` `p`, where `m` is a monomial (after “abstraction”), `p` a polynomial - and ``=`` the corresponding equality of the field structure. + This tactic decides the equality of two terms modulo + field operations and the equalities defined + by the :token:`term`\s. Each :token:`term` has to be a proof of some equality + :g:`m = p`, where :g:`m` is a monomial (after “abstraction”), :g:`p` a polynomial + and :g:`=` the corresponding equality of the field structure. .. note:: - rewriting works with the equality `m` ``=`` `p` only if `p` is a polynomial since + Rewriting works with the equality :g:`m = p` only if :g:`p` is a polynomial since rewriting is handled by the underlying ring tactic. .. tacv:: field_simplify @@ -562,27 +562,28 @@ Dealing with fields .. tacv:: field_simplify [{* @term }] - performs the simplification in the conclusion of the goal using the equalities - defined by the :n:`@term`\ s. + This variant performs the simplification in the conclusion of the goal using the equalities + defined by the :token:`term`\s. .. tacv:: field_simplify [{* @term }] {* @term } - performs the simplification in the terms :n:`@terms` of the conclusion of the goal - using the equalities defined by :n:`@term`\ s inside the brackets. + This variant performs the simplification in the terms :token:`term`\s of the conclusion of the goal + using the equalities defined by :token:`term`\s inside the brackets. -.. tacv :: field_simplify in @ident +.. tacv:: field_simplify in @ident - performs the simplification in the assumption :n:`@ident`. + This variant performs the simplification in the assumption :token:`ident`. -.. tacv :: field_simplify [{* @term }] in @ident +.. tacv:: field_simplify [{* @term }] in @ident - performs the simplification - in the assumption :n:`@ident` using the equalities defined by the :n:`@term`\ s. + This variant performs the simplification + in the assumption :token:`ident` using the equalities defined by the :token:`term`\s. .. tacv:: field_simplify [{* @term }] {* @term } in @ident - performs the simplification in the :n:`@term`\ s of the assumption :n:`@ident` using the - equalities defined by the :n:`@term`\ s inside the brackets. + This variant performs the simplification in the :token:`term`\s of the + assumption :token:`ident` using the + equalities defined by the :token:`term`\s inside the brackets. .. tacv:: field_simplify_eq @@ -591,18 +592,17 @@ Dealing with fields .. tacv:: field_simplify_eq [ {* @term }] - performs the simplification in - the conclusion of the goal using the equalities defined by - :n:`@term`\ s. + This variant performs the simplification in + the conclusion of the goal using the equalities defined by :token:`term`\s. .. tacv:: field_simplify_eq in @ident - performs the simplification in the assumption :n:`@ident`. + This variant performs the simplification in the assumption :token:`ident`. .. tacv:: field_simplify_eq [{* @term}] in @ident - performs the simplification in the assumption :n:`@ident` using the equalities defined by - :n:`@terms`\ s and removing the denominator. + This variant performs the simplification in the assumption :token:`ident` + using the equalities defined by :token:`term`\s and removing the denominator. Adding a new field structure diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 882798205b..43d302114e 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -228,6 +228,8 @@ mechanism if available, as shown in the example. Substructures ~~~~~~~~~~~~~ +.. index:: :> (substructure) + Substructures are components of a class which are instances of a class themselves. They often arise when using classes for logical properties, e.g.: @@ -459,12 +461,12 @@ type, like: This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -Options -~~~~~~~ +Settings +~~~~~~~~ .. flag:: Typeclasses Dependency Order - This option (on by default since 8.6) respects the dependency order + This flag (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in @@ -473,7 +475,7 @@ Options .. flag:: Typeclasses Filtered Unification - This option, available since Coq 8.6 and off by default, switches the + This flag, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a hint, we first check that the goal *matches* syntactically the inferred or specified pattern of the hint, and only then try to @@ -481,13 +483,13 @@ Options improve performance by calling unification less often, matching syntactic patterns being very quick. This also provides more control on the triggering of instances. For example, forcing a constant to - explicitely appear in the pattern will make it never apply on a goal + explicitly appear in the pattern will make it never apply on a goal where there is a hole in that place. .. flag:: Typeclasses Limit Intros - This option (on by default) controls the ability to apply hints while + This flag (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction. @@ -501,16 +503,16 @@ Options .. flag:: Typeclass Resolution For Conversion - This option (on by default) controls the use of typeclass resolution + This flag (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type - inference. With this option on, when a unification fails, typeclass + inference. With this flag on, when a unification fails, typeclass resolution is tried before launching unification once again. .. flag:: Typeclasses Strict Resolution - Typeclass declarations introduced when this option is set have a - stricter resolution behavior (the option is off by default). When + Typeclass declarations introduced when this flag is set have a + stricter resolution behavior (the flag is off by default). When looking for unifications of a goal with an instance of this class, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be @@ -526,26 +528,40 @@ Options .. flag:: Typeclasses Unique Instances - Typeclass declarations introduced when this option is set have a more - efficient resolution behavior (the option is off by default). When a + Typeclass declarations introduced when this flag is set have a more + efficient resolution behavior (the flag is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. +.. flag:: Typeclasses Iterative Deepening + + When this flag is set, the proof search strategy is breadth-first search. + Otherwise, the search strategy is depth-first search. The default is off. + :cmd:`Typeclasses eauto` is another way to set this flag. + +.. opt:: Typeclasses Depth @num + :name: Typeclasses Depth + + Sets the maximum proof search depth. The default is unbounded. + :cmd:`Typeclasses eauto` is another way to set this option. + .. flag:: Typeclasses Debug Controls whether typeclass resolution steps are shown during search. Setting this flag - also sets :opt:`Typeclasses Debug Verbosity` to 1. + also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto` + is another way to set this flag. .. opt:: Typeclasses Debug Verbosity @num :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving - of goals. Setting this option also sets :flag:`Typeclasses Debug`. + of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this + option to 0 turns that option off. .. flag:: Refine Instance Mode - This option allows to switch the behavior of instance declarations made through + This flag allows to switch the behavior of instance declarations made through the Instance command. + When it is on (the default), instances that have unsolved holes in @@ -558,14 +574,17 @@ Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth + :name: Typeclasses eauto This command allows more global customization of the typeclass resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is - printed. + printed. This value can also be set with :flag:`Typeclasses Debug`. + ``dfs, bfs`` This sets the search strategy to depth-first search (the - default) or breadth-first search. + default) or breadth-first search. This value can also be set with + :flag:`Typeclasses Iterative Deepening`. - + ``depth`` This sets the depth limit of the search. + + ``depth`` This sets the depth limit of the search. This value can also be set with + :opt:`Typeclasses Depth`. diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index d98b8641e9..e681d0f3ff 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -147,7 +147,7 @@ exclude_patterns = [ # The reST default role (used for this markup: `text`) to use for all # documents. -#default_role = None +default_role = 'literal' # Use the Coq domain primary_domain = 'coq' diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..10650af1d1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,8 +97,8 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 562ed48171..376a6b8eed 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -46,25 +46,26 @@ in which case the correctness of :n:`@type__3` may rely on the instance :n:`@ter The set of rational numbers may be defined as: - .. coqtop:: reset all + .. coqtop:: reset all - Record Rat : Set := mkRat - {sign : bool; - top : nat; - bottom : nat; - Rat_bottom_cond : 0 <> bottom; - Rat_irred_cond : - forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. + Record Rat : Set := mkRat + { sign : bool + ; top : nat + ; bottom : nat + ; Rat_bottom_cond : 0 <> bottom + ; Rat_irred_cond : + forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 + }. -Remark here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` and ``Rat_irred_cond`` -depends on both ``top`` and ``bottom``. + Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` + and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``. Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: -:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`. +:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`. -To build an object of type :n:`@ident`, one should provide the constructor -:n:`@ident₀` with the appropriate number of terms filling the fields of the record. +To build an object of type :token:`ident`, one should provide the constructor +:n:`@ident__0` with the appropriate number of terms filling the fields of the record. .. example:: @@ -129,7 +130,7 @@ This syntax can also be used for pattern matching. end). The macro generates also, when it is possible, the projection -functions for destructuring an object of type `\ident`. These +functions for destructuring an object of type :token:`ident`. These projection functions are given the names of the corresponding fields. If a field is named `_` then no projection is built for it. In our example: @@ -163,17 +164,17 @@ available: .. _record_projections_grammar: .. productionlist:: terms - projection : projection `.` ( `qualid` ) - : | projection `.` ( `qualid` `arg` … `arg` ) - : | projection `.` ( @`qualid` `term` … `term` ) + projection : `term` `.` ( `qualid` ) + : | `term` `.` ( `qualid` `arg` … `arg` ) + : | `term` `.` ( @`qualid` `term` … `term` ) Syntax of Record projections -The corresponding grammar rules are given in the preceding grammar. When `qualid` -denotes a projection, the syntax `term.(qualid)` is equivalent to `qualid term`, -the syntax `term.(qualid` |arg_1| |arg_n| `)` to `qualid` |arg_1| `…` |arg_n| `term`, -and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` |term_n| `term`. -In each case, `term` is the object projected and the +The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` +denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`, +the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`. +and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`. +In each case, :token:`term` is the object projected and the other arguments are the parameters of the inductive type. @@ -197,22 +198,22 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name `ident` already exists in the environment (see :cmd:`Axiom`). - #. The body of `ident` uses an incorrect elimination for - `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). - #. The type of the projections `ident` depends on previous + #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The body of :token:`ident` uses an incorrect elimination for + :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). + #. The type of the projections :token:`ident` depends on previous projections which themselves could not be defined. .. exn:: Records declared with the keyword Record or Structure cannot be recursive. - The record name `ident` appears in the type of its fields, but uses - the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. + The record name :token:`ident` appears in the type of its fields, but uses + the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. .. exn:: Cannot handle mutually (co)inductive records. - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section @@ -308,7 +309,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the :flag`Printing Primitive Projection Parameters` option +projection if the :flag:`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -380,7 +381,7 @@ we have the following equivalence | right _ => false end). -Notice that the printing uses the :g:`if` syntax because `sumbool` is +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is declared as such (see :ref:`controlling-match-pp`). .. _irrefutable-patterns: @@ -653,8 +654,7 @@ with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the -presence of partial application of `wrong` in the body of -`wrong` : +presence of partial application of :g:`wrong` in the body of :g:`wrong`: .. coqtop:: all @@ -699,21 +699,22 @@ used by ``Function``. A more precise description is given below. .. cmdv:: Function @ident {* @binder } : @type := @term - Defines the not recursive function `ident` as if declared with `Definition`. Moreover - the following are defined: + Defines the not recursive function :token:`ident` as if declared with + :cmd:`Definition`. Moreover the following are defined: - + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern - matching structure of `term` (see :cmd:`Inductive`); - + The inductive `R_ident` corresponding to the graph of `ident` (silently); - + `ident_complete` and `ident_correct` which are inversion information - linking the function and its graph. + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. .. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term - Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined: + Defines the structural recursive function :token:`ident` as if declared + with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of `ident`: `ident_equation`. + + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term Function @ident {* @binder } { wf @term @ident } : @type := @term @@ -722,16 +723,16 @@ used by ``Function``. A more precise description is given below. of the standard library must be loaded for this feature. The ``{}`` annotation is mandatory and must be one of the following: - + ``{measure`` `term` `ident` ``}`` with `ident` being the decreasing argument - and `term` being a function from type of `ident` to ``nat`` for which - value on the decreasing argument decreases (for the ``lt`` order on ``nat``) - at each recursive call of `term`. Parameters of the function are - bound in `term`\ ; - + ``{wf`` `term` `ident` ``}`` with `ident` being the decreasing argument and - `term` an ordering relation on the type of `ident` (i.e. of type + + :n:`{measure @term @ident }` with :token:`ident` being the decreasing argument + and :token:`term` being a function from type of :token:`ident` to :g:`nat` for which + value on the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + at each recursive call of :token:`term`. Parameters of the function are + bound in :token:`term`; + + :n:`{wf @term @ident }` with :token:`ident` being the decreasing argument and + :token:`term` an ordering relation on the type of :token:`ident` (i.e. of type `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases at each recursive call of `term`. The order must be well-founded. - Parameters of the function are bound in `term`. + decreases at each recursive call of :token:`term`. The order must be well-founded. + Parameters of the function are bound in :token:`term`. Depending on the annotation, the user is left with some proof obligations that will be used to define the function. These proofs @@ -770,42 +771,42 @@ Section :ref:`gallina-definitions`). .. cmd:: End @ident - This command closes the section named `ident`. After closing of the - section, the local declarations (variables and local definitions) get - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. + This command closes the section named :token:`ident`. After closing of the + section, the local declarations (variables and local definitions) get + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Section s1. + Section s1. - Variables x y : nat. + Variables x y : nat. - Let y' := y. + Let y' := y. - Definition x' := S x. + Definition x' := S x. - Definition x'' := x' + y'. + Definition x'' := x' + y'. - Print x'. + Print x'. - End s1. + End s1. - Print x'. + Print x'. - Print x''. + Print x''. - Notice the difference between the value of `x’` and `x’’` inside section - `s1` and outside. + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. - .. exn:: This is not the last opened section. - :undocumented: + .. exn:: This is not the last opened section. + :undocumented: .. note:: - Most commands, like ``Hint``, ``Notation``, option management, … which + Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which appear inside a section are canceled when the section is closed. @@ -816,26 +817,26 @@ The module system provides a way of packaging related elements together, as well as a means of massive abstraction. .. productionlist:: modules - module_type : qualid - : | `module_type` with Definition qualid := term - : | `module_type` with Module qualid := qualid - : | qualid qualid … qualid - : | !qualid qualid … qualid - module_binding : ( [Import|Export] ident … ident : module_type ) + module_type : `qualid` + : | `module_type` with Definition `qualid` := `term` + : | `module_type` with Module `qualid` := `qualid` + : | `qualid` `qualid` … `qualid` + : | !`qualid` `qualid` … `qualid` + module_binding : ( [Import|Export] `ident` … `ident` : `module_type` ) module_bindings : `module_binding` … `module_binding` - module_expression : qualid … qualid - : | !qualid … qualid + module_expression : `qualid` … `qualid` + : | !`qualid` … `qualid` Syntax of modules In the syntax of module application, the ! prefix indicates that any `Inline` directive in the type of the functor arguments will be ignored -(see the ``Module Type`` command below). +(see the :cmd:`Module Type` command below). .. cmd:: Module @ident - This command is used to start an interactive module named `ident`. + This command is used to start an interactive module named :token:`ident`. .. cmdv:: Module @ident {* @module_binding} @@ -848,21 +849,22 @@ In the syntax of module application, the ! prefix indicates that any .. cmdv:: Module @ident {* @module_binding} : @module_type - Starts an interactive functor with parameters given by the list of `module binding`, and output module - type `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_bindings`, and output module type :token:`module_type`. .. cmdv:: Module @ident <: {+<: @module_type } - Starts an interactive module satisfying each `module_type`. + Starts an interactive module satisfying each :token:`module_type`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. - Starts an interactive functor with parameters given by the list of `module_binding`. The output module type - is verified against each `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_binding`. The output module type + is verified against each :token:`module_type`. .. cmdv:: Module [ Import | Export ] - Behaves like ``Module``, but automatically imports or exports the module. + Behaves like :cmd:`Module`, but automatically imports or exports the module. Reserved commands inside an interactive module ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -913,7 +915,7 @@ Reserved commands inside an interactive module .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`. - The body is checked against each |module_type_i|. + The body is checked against each :n:`@module_type__i`. .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression} @@ -1052,8 +1054,8 @@ specification: the y component is dropped as well as the body of x. End SIG. -The definition of ``N`` using the module type expression ``SIG`` with -``Definition T := nat`` is equivalent to the following one: +The definition of :g:`N` using the module type expression :g:`SIG` with +:g:`Definition T := nat` is equivalent to the following one: .. coqtop:: all @@ -1138,7 +1140,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. #. Modules and module types can be nested components of each other. #. One can have sections inside a module or a module type, but not a module or a module type inside a section. - #. Commands like ``Hint`` or ``Notation`` can also appear inside modules and + #. Commands like :cmd:`Hint` or :cmd:`Notation` can also appear inside modules and module types. Note that in case of a module definition like: :: @@ -1157,73 +1159,73 @@ component is equal ``nat`` and hence ``M1.T`` as specified. .. cmd:: Import @qualid - If `qualid` denotes a valid basic module (i.e. its module type is a - signature), makes its components available by their short names. + If :token:`qualid` denotes a valid basic module (i.e. its module type is a + signature), makes its components available by their short names. - .. example:: + .. example:: - .. coqtop:: reset all + .. coqtop:: reset all - Module Mod. + Module Mod. - Definition T:=nat. + Definition T:=nat. - Check T. + Check T. - End Mod. + End Mod. - Check Mod.T. + Check Mod.T. - Fail Check T. + Fail Check T. - Import Mod. + Import Mod. - Check T. + Check T. - Some features defined in modules are activated only when a module is - imported. This is for instance the case of notations (see :ref:`Notations`). + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). - Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` - command. Such declarations are only accessible through their fully - qualified name. + Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Module A. + Module A. - Module B. + Module B. - Local Definition T := nat. + Local Definition T := nat. - End B. + End B. - End A. + End A. - Import A. + Import A. - Fail Check B.T. + Fail Check B.T. - .. cmdv:: Export @qualid - :name: Export + .. cmdv:: Export @qualid + :name: Export - When the module containing the command Export qualid - is imported, qualid is imported as well. + When the module containing the command ``Export`` qualid + is imported, qualid is imported as well. - .. exn:: @qualid is not a module. - :undocumented: + .. exn:: @qualid is not a module. + :undocumented: - .. warn:: Trying to mask the absolute name @qualid! - :undocumented: + .. warn:: Trying to mask the absolute name @qualid! + :undocumented: .. cmd:: Print Module @ident - Prints the module type and (optionally) the body of the module :n:`@ident`. + Prints the module type and (optionally) the body of the module :token:`ident`. .. cmd:: Print Module Type @ident - Prints the module type corresponding to :n:`@ident`. + Prints the module type corresponding to :token:`ident`. .. flag:: Short Module Printing @@ -1374,7 +1376,7 @@ OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object files as described above. The OCaml loadpath is managed using the option ``-I`` `path` (in the OCaml world, there is neither a notion of logical name prefix nor a way to access files in -subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in +subdirectories of path). See the command :cmd:`Declare ML Module` in :ref:`compiled-files` to understand the need of the OCaml loadpath. See :ref:`command-line-options` for a more general view over the |Coq| command @@ -1515,7 +1517,6 @@ possible, the correct argument will be automatically generated. .. exn:: Cannot infer a term for this placeholder. :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments) - :undocumented: |Coq| was not able to deduce an instantiation of a “_”. @@ -1803,20 +1804,20 @@ Explicit applications In presence of non-strict or contextual argument, or in presence of partial applications, the synthesis of implicit arguments may fail, so one may have to give explicitly certain implicit arguments of an -application. The syntax for this is ``(`` `ident` ``:=`` `term` ``)`` where `ident` is the +application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the name of the implicit argument and term is its corresponding explicit term. Alternatively, one can locally deactivate the hiding of implicit -arguments of a function by using the notation `@qualid` |term_1| … |term_n|. +arguments of a function by using the notation :n:`@qualid {+ @term }`. This syntax extension is given in the following grammar: .. _explicit_app_grammar: .. productionlist:: explicit_apps - term : @ qualid term … `term` - : | @ qualid - : | qualid `argument` … `argument` + term : @ `qualid` `term` … `term` + : | @ `qualid` + : | `qualid` `argument` … `argument` argument : `term` - : | (ident := `term`) + : | (`ident` := `term`) Syntax for explicitly giving implicit arguments @@ -2208,13 +2209,10 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). -In the general case, when an existential variable ``?``\ `ident` appears +In the general case, when an existential variable :n:`?@ident` appears outside of its context of definition, its instance, written under the -form - -| ``{`` :n:`{*; @ident:=@term}` ``}`` - -is appending to its name, indicating how the variables of its defining context are instantiated. +form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +how the variables of its defining context are instantiated. The variables of the context of the existential variables which are instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index de9e327740..9bc67147f7 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -198,10 +198,10 @@ and ``coqtop``, unless stated otherwise: :-type-in-type: Collapse the universe hierarchy of |Coq|. .. warning:: This makes the logic inconsistent. -:-mangle-names *ident*: Experimental: Do not depend on this option. Replace +:-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, - etc. The command ``Set Mangle Names`` turns the behavior on in a document, - and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature + etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on, + and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0ea8c7be2d..1071682ead 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1208,7 +1208,7 @@ Interactive debugger .. flag:: Ltac Debug - This option governs the step-by-step debugger that comes with the |Ltac| interpreter + This option governs the step-by-step debugger that comes with the |Ltac| interpreter. When the debugger is activated, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3ca0ffe678..9fbac95f0c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -157,14 +157,24 @@ compatible with the rest of |Coq|, up to a few discrepancies: (see :ref:`pattern_conditional_ssr`). To use the generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. -+ The following two options can be unset to disable the incompatible - rewrite syntax and allow reserved identifiers to appear in scripts. ++ The following flags can be unset to make |SSR| more compatible with + parts of Coq: - .. coqtop:: in +.. flag:: SsrRewrite + + Controls whether the incompatible rewrite syntax is enabled (the default). + Disabling the flag makes the syntax compatible with other parts of Coq. + +.. flag:: SsrIdents - Unset SsrRewrite. - Unset SsrIdents. + Controls whether tactics can refer to |SSR|-generated variables that are + in the form _xxx_. Scripts with explicit references to such variables + are fragile; they are prone to failure if the proof is later modified or + if the details of variable name generation change in future releases of Coq. + The default is on, which gives an error message when the user tries to + create such identifiers. Disabling the flag generates a warning instead, + increasing compatibility with other parts of Coq. |Gallina| extensions -------------------- @@ -3063,6 +3073,17 @@ An :token:`r_item` can be: rewrite -[f y x]/(y + _). +.. flag:: SsrOldRewriteGoalsOrder + + Controls the order in which generated subgoals (side conditions) + are added to the + proof context. The flag is off by default, which puts subgoals generated + by conditional rules first, followed by the main goal. When it is on, + the main goal appears first. If your proofs are organized to complete + proving the main goal before side conditions, turning the flag on will save you + from having to add :tacn:`last first` tactics that would be needed + to keep the main goal as the currently focused goal. + Remarks and examples ~~~~~~~~~~~~~~~~~~~~ @@ -5428,6 +5449,17 @@ right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr prenex implicits declaration see :ref:`parametric_polymorphism_ssr` +Settings +~~~~~~~~ + +.. flag:: Debug Ssreflect + + *Developer only.* Print debug information on reflect. + +.. flag:: Debug SsrMatching + + *Developer only.* Print debug information on SSR matching. + .. rubric:: Footnotes .. [#1] Unfortunately, even after a call to the Set Printing All command, diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 150aadc15a..ad80cb62e1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,6 +264,11 @@ Applying theorems This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. + .. flag:: Debug Unification + + Enables printing traces of unification steps used during + elaboration/typechecking and the :tacn:`refine` tactic. + .. tacn:: apply @term :name: apply @@ -606,6 +611,10 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). +.. flag:: Debug Tactic Unification + + Enables printing traces of unification steps in tactic unification. + Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: @@ -2096,9 +2105,9 @@ and an explanation of the underlying technique. Part of the behavior of the ``inversion`` tactic is to generate equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they - relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort - :g:`Prop`). This behavior can be turned off by using the option - :flag`Keep Proof Equalities`. + relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort + :g:`Prop`). This behavior can be turned off by using the + :flag:`Keep Proof Equalities` setting. .. tacv:: inversion @num @@ -2534,6 +2543,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. unresolved bindings into existential variables, if any, instead of failing. It has the same variants as :tacn:`rewrite` has. + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + .. tacn:: replace @term with @term’ :name: replace @@ -4503,3 +4519,42 @@ user-defined tactics. significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been completely revised to get a very compact and readable version. + +Delaying solving unification constraints +---------------------------------------- + +.. tacn:: solve_constraints + :name: solve_constraints + :undocumented: + +.. flag:: Solve Unification Constraints + + By default, after each tactic application, postponed typechecking unification + problems are resolved using heuristics. Unsetting this flag disables this + behavior, allowing tactics to leave unification constraints unsolved. Use the + :tacn:`solve_constraints` tactic at any point to solve the constraints. + +Proof maintenance +----------------- + +*Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such +as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps +may explicitly refer to these names. However, future versions of Coq may not assign +names exactly the same way, which could cause the proof to fail because the +new names don't match the explicit references in the proof. + +The following "Mangle Names" settings let users find all the +places where proofs rely on automatically generated names, which can +then be named explicitly to avoid any incompatibility. These +settings cause Coq to generate different names, producing errors for +references to automatically generated names. + +.. flag:: Mangle Names + + When set, generated names use the prefix specified in the following + option instead of the default prefix. + +.. opt:: Mangle Names Prefix @string + :name: Mangle Names Prefix + + Specifies the prefix to use when generating names. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4bc85f386d..a98a46ba21 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -274,8 +274,8 @@ Requests to the environment This searches for all statements or types of definition that contains a subterm that matches the pattern - `term_pattern` (holes of the pattern are either denoted by `_` or by - `?ident` when non linear patterns are expected). + :token:`term_pattern` (holes of the pattern are either denoted by `_` or by + :n:`?@ident` when non linear patterns are expected). .. cmdv:: Search { + [-]@term_pattern_string } @@ -580,7 +580,7 @@ file is a particular case of module called *library file*. replayed nor rechecked. To locate the file in the file system, :n:`@qualid` is decomposed under the - form `dirpath.ident` and the file `ident.vo` is searched in the physical + form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical directory of the file system that is mapped in |Coq| loadpath to the logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between physical directories and logical names at the time of requiring the @@ -611,7 +611,7 @@ file is a particular case of module called *library file*. .. cmdv:: Require [Import | Export] {+ @qualid } This loads the - modules named by the :n:`qualid` sequence and their recursive + modules named by the :token:`qualid` sequence and their recursive dependencies. If ``Import`` or ``Export`` is given, it also imports these modules and all the recursive dependencies that were marked or transitively marked @@ -620,8 +620,8 @@ file is a particular case of module called *library file*. .. cmdv:: From @dirpath Require @qualid This command acts as :cmd:`Require`, but picks - any library whose absolute name is of the form dirpath.dirpath’.qualid - for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library + any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` + for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library comes from a given package by making explicit its absolute root. .. exn:: Cannot load qualid: no physical path bound to dirpath. @@ -637,21 +637,21 @@ file is a particular case of module called *library file*. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the - one already loaded in the current |Coq| session. Probably `ident.v` was + one already loaded in the current |Coq| session. Probably :n:`@ident.v` was not properly recompiled with the last version of the file containing - module :n:`@qualid`. + module :token:`qualid`. .. exn:: Bad magic number. - The file `ident.vo` was found but either it is not a + The file :n:`@ident.vo` was found but either it is not a |Coq| compiled module, or it was compiled with an incompatible version of |Coq|. - .. exn:: The file `ident.vo` contains library dirpath and not library dirpath’. + .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’. - The library file `dirpath’` is indirectly required by the + The library file :n:`@dirpath’` is indirectly required by the ``Require`` command but it is bound in the current loadpath to the - file `ident.vo` which was bound to a different library name `dirpath` at + file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at the time it was compiled. @@ -675,10 +675,10 @@ file is a particular case of module called *library file*. .. cmd:: Declare ML Module {+ @string } This commands loads the OCaml compiled files - with names given by the :n:`@string` sequence + with names given by the :token:`string` sequence (dynamic link). It is mainly used to load tactics dynamically. The files are searched into the current OCaml loadpath (see the - command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`). + command :cmd:`Add ML Path`). Loading of OCaml files is only possible under the bytecode version of ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter :ref:`thecoqcommands`), or when |Coq| has been compiled with a @@ -698,9 +698,9 @@ file is a particular case of module called *library file*. .. cmd:: Print ML Modules - This prints the name of all OCaml modules loaded with ``Declare - ML Module``. To know from where these module were loaded, the user - should use the command ``Locate File`` (see :ref:`here <locate-file>`) + This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. + To know from where these module were loaded, the user + should use the command :cmd:`Locate File`. .. _loadpath: @@ -721,7 +721,7 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Cd @string - This command changes the current directory according to :n:`@string` which + This command changes the current directory according to :token:`string` which can be any valid path. .. cmdv:: Cd @@ -732,24 +732,24 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Add LoadPath @string as @dirpath This command is equivalent to the command line option - ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current + :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. .. cmdv:: Add LoadPath @string - Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but + Performs as :n:`Add LoadPath @string @dirpath` but for the empty directory path. .. cmd:: Add Rec LoadPath @string as @dirpath This command is equivalent to the command line option - ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its + :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. .. cmdv:: Add Rec LoadPath @string - Works as :cmd:`Add Rec LoadPath` :n:`@string` as :n:`@dirpath` but for the empty + Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty logical directory path. @@ -792,7 +792,7 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Locate File @string This command displays the location of file string in the current - loadpath. Typically, string is a .cmo or .vo or .v file. + loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file. .. cmd:: Locate Library @dirpath @@ -858,7 +858,7 @@ interactively, they cannot be part of a vernacular file loaded via state label is an integer which grows after each successful command. It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see above), the :cmd:`BackTo` command now handles proof states. For that, it may - have to undo some extra commands and end on a state `num′ ≤ num` if + have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. .. cmdv:: Backtrack @num @num @num @@ -1157,7 +1157,7 @@ described first. This command allows giving a short name to a reduction expression, for instance lazy beta delta [foo bar]. This short name can then be used - in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command + in :n:`Eval @ident in` or ``eval`` directives. This command accepts the Local modifier, for discarding this reduction name at the end of the file or module. For the moment the name cannot be qualified. In @@ -1165,7 +1165,7 @@ described first. functor applications will be refused if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but nothing prevents the user to also perform a - ``Ltac`` `ident` ``:=`` `convtactic`. + :n:`Ltac @ident := @convtactic`. .. seealso:: :ref:`performingcomputations` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index c0e57aab53..a54da6faf2 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1040,6 +1040,8 @@ interpreted in the scope stack extended with the scope bound tokey. To remove a delimiting key of a scope, use the command :n:`Undelimit Scope @scope` +.. _ArgumentScopes: + Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1307,6 +1309,65 @@ Displaying information about scopes It also displays the delimiting key if any and the class to which the scope is bound, if any. +Impact of scopes on printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When several notations are available for printing the same expression, +Coq will use the following rules for printing priorities: + +- If two notations are available in different scopes which are open, + the notation in the more recently opened scope takes precedence. + +- If two notations are available in the same scope, the more recently + defined (or imported) notation takes precedence. + +- Abbreviations and lonely notations, both of which have no scope, + take precedence over a notation in an open scope if and only if the + abbreviation or lonely notation was defined (or imported) more + recently than when the corresponding scope was open. They take + precedence over any notation not in an open scope, whether this scope + has a delimiter or not. + +- A scope is *active* for printing a term either because it was opened + with :cmd:`Open Scope`, or the term is the immediate argument of a + constant which temporarily opens a scope for this argument (see + :ref:`Arguments <ArgumentScopes>`) in which case this temporary + scope is the most recent open one. + +- In case no abbreviation, nor lonely notation, nor notation in an + explicitly open scope, nor notation in a temporarily open scope of + arguments, has been found, notations in those closed scopes which + have a delimiter are considered, giving priority to the most + recently defined (or imported) ones. The corresponding delimiter is + inserted, making the corresponding scope the most recent explicitly + open scope for all subterms of the current term. As an exception to + the insertion of the corresponding delimiter, when an expression is + statically known to be in a position expecting a type and the + notation is from scope ``type_scope``, and the latter is closed, the + delimiter is not inserted. This is because expressions statically + known to be in a position expecting a type are by default + interpreted with `type_scope` temporarily activated. Expressions + statically known to be in a position expecting a type typically + include being on the right-hand side of `:`, `<:`, `<<:` and after + the comma in a `forall` expression. + +- As a refinement of the previous rule, in the case of applied global + references, notations in a non-opened scope with delimiter + specifically defined for this applied global reference take priority + over notations in a non-opened scope with delimiter for generic + applications. For instance, in the presence of ``Notation "f ( x + )" := (f x) (at level 10, format "f ( x )") : app_scope`` and + ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") : + mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being + bound to a delimiter *and* both not opened, the latter, more + specific notation will always take precedence over the first, more + generic one. + +- A scope can be closed by using :cmd:`Close Scope` and its delimiter + removed by using :cmd:`Undelimit Scope`. To remove automatic + temporary opening of scopes for arguments of a constant, use + :ref:`Arguments <ArgumentScopes>`. + .. _Abbreviations: Abbreviations @@ -1380,147 +1441,147 @@ Numeral notations .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. :name: Numeral Notation - This command allows the user to customize the way numeral literals - are parsed and printed. + This command allows the user to customize the way numeral literals + are parsed and printed. - The token :n:`@ident__1` should be the name of an inductive type, - while :n:`@ident__2` and :n:`@ident__3` should be the names of the - parsing and printing functions, respectively. The parsing function - :n:`@ident__2` should have one of the following types: + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: - * :n:`Decimal.int -> @ident__1` - * :n:`Decimal.int -> option @ident__1` - * :n:`Decimal.uint -> @ident__1` - * :n:`Decimal.uint -> option @ident__1` - * :n:`Z -> @ident__1` - * :n:`Z -> option @ident__1` + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` - And the printing function :n:`@ident__3` should have one of the - following types: + And the printing function :n:`@ident__3` should have one of the + following types: - * :n:`@ident__1 -> Decimal.int` - * :n:`@ident__1 -> option Decimal.int` - * :n:`@ident__1 -> Decimal.uint` - * :n:`@ident__1 -> option Decimal.uint` - * :n:`@ident__1 -> Z` - * :n:`@ident__1 -> option Z` + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` - When parsing, the application of the parsing function - :n:`@ident__2` to the number will be fully reduced, and universes - of the resulting term will be refreshed. + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). - When a literal larger than :token:`num` is parsed, a warning - message about possible stack overflow, resulting from evaluating - :n:`@ident__2`, will be displayed. + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). - When a literal :g:`m` larger than :token:`num` is parsed, the - result will be :n:`(@ident__2 m)`, without reduction of this - application to a normal form. Here :g:`m` will be a - :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the - type of the parsing function :n:`@ident__2`. This allows for a - more compact representation of literals in types such as :g:`nat`, - and limits parse failures due to stack overflow. Note that a - warning will be emitted when an integer larger than :token:`num` - is parsed. Note that :n:`(abstract after @num)` has no effect - when :n:`@ident__2` lands in an :g:`option` type. + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. - .. exn:: Cannot interpret this number as a value of type @type + .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support - the given numeral. This error is given when the interpretation - function returns :g:`None`, or if the interpretation is registered - for only non-negative integers, and the given numeral is negative. + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. - .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The parsing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The printing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @type is not an inductive type. + .. exn:: @type is not an inductive type. - Numeral notations can only be declared for inductive types with no - arguments. + Numeral notations can only be declared for inductive types with no + arguments. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a numeral notation. - Parsing functions must always return ground terms, made up of - applications of constructors and inductive types. Parsing - functions may not return terms containing axioms, bare - (co)fixpoints, lambdas, etc. + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a numeral notation. - Parsing functions expected to return an :g:`option` must always - return a concrete :g:`Some` or :g:`None` when applied to a - concrete numeral expressed as a decimal. They may not return - opaque constants. + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. - .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. - The inductive type used to register the numeral notation is no - longer available in the environment. Most likely, this is because - the numeral notation was declared inside a functor for an - inductive type inside the functor. This use case is not currently - supported. + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. - Alternatively, you might be trying to use a primitive token - notation from a plugin which forgot to specify which module you - must :g:`Require` for access to that notation. + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. - .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`Numeral Notation` must be a single - identifier. + The type passed to :cmd:`Numeral Notation` must be a single + identifier. - .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`Numeral Notation` must be single - identifiers. + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. - .. exn:: The reference @ident was not found in the current environment. + .. exn:: The reference @ident was not found in the current environment. - Identifiers passed to :cmd:`Numeral Notation` must exist in the - global environment. + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. - .. exn:: @ident is bound to a notation that does not denote a reference. + .. exn:: @ident is bound to a notation that does not denote a reference. - Identifiers passed to :cmd:`Numeral Notation` must be global - references, or notations which denote to single identifiers. + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. - .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(warning after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. - .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(abstract after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. - Typically, this indicates that the fully computed representation - of numerals can be so large that non-tail-recursive OCaml - functions run out of stack space when trying to walk them. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. - For example + For example - .. coqtop:: all + .. coqtop:: all - Check 90000. + Check 90000. - .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. - As noted above, the :n:`(abstract after @num)` directive has no - effect when :n:`@ident__2` lands in an :g:`option` type. + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. String notations ----------------- |