diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 52 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
2 files changed, 53 insertions, 7 deletions
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/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 |