diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 52 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
5 files changed, 57 insertions, 22 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a011c81f15..52e47b52ae 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in: 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 -coerce term to its support type. It can be useful in notations, for -example: - -.. coqtop:: all - - Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). - -This notation denotes equality on subset types using equality on their -support types, avoiding uses of proof-irrelevance that would come up -when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts :cmd:`Definition` and :cmd:`Fixpoint` diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index fcf61a5bf4..1a729ced4e 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -42,7 +42,6 @@ Type cast term_cast ::= @term10 : @type | @term10 <: @type | @term10 <<: @type - | @term10 :> The expression :n:`@term10 : @type` is a type cast expression. It enforces the type of :n:`@term10` to be :n:`@type`. @@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`). :n:`@term10 <<: @type` specifies that compilation to OCaml will be used to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`). -:n:`@term10 :>` casts to the support type in Program mode. -See :ref:`syntactic_control`. - .. _gallina-definitions: Top-level definitions diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index fbba6c30b8..e3b014d8d5 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -41,12 +41,54 @@ in :ref:`canonicalstructures`; here only a simple example is given. This command supports the :attr:`local` attribute. When used, the structure is canonical only within the :cmd:`Section` containing it. - Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the - structure :g:`struct` of which the fields are |x_1|, …, |x_n|. - Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be + :token:`qualid` (in :token:`reference`) denotes an object :n:`(Build_struct c__1 … c__n)` in the + structure :g:`struct` for which the fields are :n:`x__1, …, x__n`. + Then, each time an equation of the form :n:`(x__i _)` |eq_beta_delta_iota_zeta| :n:`c__i` has to be solved during the type checking process, :token:`qualid` is used as a solution. - Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| - into a complete structure built on |c_i|. + Otherwise said, :token:`qualid` is canonically used to extend the field :n:`x__i` + into a complete structure built on :n:`c__i` when :n:`c__i` unifies with :n:`(x__i _)`. + + The following kinds of terms are supported for the fields :n:`c__i` of :token:`qualid`: + + * :term:`Constants <constant>` and section variables of an active section, + applied to zero or more arguments. + * :token:`sort`\s. + * Literal functions: `fun … => …`. + * Literal, non-dependent function types, i.e. implications: `… -> …`. + * Variables bound in :token:`qualid`. + + Only the head symbol of an existing instance's field :n:`c__i` + is considered when searching for a canonical extension. + We call this head symbol the *key* and we say ":token:`qualid` *keys* the field :n:`x__i` to :n:`k`" when :n:`c__i`'s + head symbol is :n:`k`. + Keys are the only piece of information that is used for canonical extension. + The keys corresponding to the kinds of terms listed above are: + + * For constants and section variables, potentially applied to arguments: + the constant or variable itself, disregarding any arguments. + * For sorts: the sort itself. + * For literal functions: skip the abstractions and use the key of the body. + * For literal functions types: a disembodied implication key denoted `_ -> _`, disregarding both its + domain and codomain. + * For variables bound in :token:`qualid`: a catch-all key denoted `_`. + + This means that, for example, `(some_constant x1)` and `(some_constant (other_constant y1 y2) x2)` + are not distinct keys. + + Variables bound in :token:`qualid` match any term for the purpose of canonical extension. + This has two major consequences for a field :n:`c__i` keyed to a variable of :token:`qualid`: + + 1. Unless another key—and, thus, instance—matches :n:`c__i`, the instance will always be considered by + unification. + 2. :n:`c__i` will be considered overlapping not distinct from any other canonical instance + that keys :n:`x__i` to one of its own variables. + + A record field :n:`x__i` can only be keyed once to each key. + Coq prints a warning when :token:`qualid` keys :n:`x__i` to a term + whose head symbol is already keyed by an existing canonical instance. + In this case, Coq will not register that :token:`qualid` as a canonical + extension. + (The remaining fields of the instance can still be used for canonical extension.) Canonical structures are particularly useful when mixed with coercions and strict implicit arguments. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 25ac72069b..52cf565998 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1251,6 +1251,10 @@ Notations This command supports the :attr:`deprecated` attribute. + .. exn:: Notation levels must range between 0 and 6. + + The level of a notation must be an integer between 0 and 6 inclusive. + Abbreviations ~~~~~~~~~~~~~ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d212256765..f65361bc64 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1182,7 +1182,7 @@ Here are the syntax elements used by the various notation commands. .. prodn:: syntax_modifier ::= at level @natural | in custom @ident {? at level @natural } - | {+, @ident } at @level + | {+, @ident } {| at @level | in scope @ident } | @ident at @level {? @binder_interp } | @ident @explicit_subentry | @ident @binder_interp @@ -1374,6 +1374,10 @@ interpreted in the scope stack extended with the scope bound to :n:`@scope_key`. Removes the delimiting keys associated with a scope. +The arguments of an :ref:`abbreviation <Abbreviations>` can be interpreted +in a scope stack locally extended with a given scope by using the modifier +:n:`{+, @ident } in scope @scope_name`.s + Binding types or coercion classes to a notation scope ++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1567,7 +1571,7 @@ Displaying information about scopes Abbreviations -------------- -.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( only parsing ) } +.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( {+, @syntax_modifier } ) } :name: Notation (abbreviation) .. todo: for some reason, Sphinx doesn't complain about a duplicate name if |