diff options
| -rw-r--r-- | doc/changelog/02-specification-language/13312-attributes+bool_single.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 49 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 7 |
6 files changed, 76 insertions, 51 deletions
diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst index fa046d968f..f069bc616b 100644 --- a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst +++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst @@ -1,13 +1,17 @@ - **Changed:** - Boolean attributes are now specified using key/value pairs, that is - to say ``attr={yes,no}``. If the value is missing, the default is - ``on``. Old syntax is still supported, but produces the - ``deprecated-attribute-syntax`` warning. - Attributes deprecated are ``universes(monomorphic)``, - ``universes(notemplate)``, ``universes(noncumulative)``, which are - replaced by the corresponding ``universes(polymorphic=no)`` etc... + :term:`Boolean attributes <boolean attribute>` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`, + :attr:`universes(template=no) <universes(template)>` + and :attr:`universes(cumulative=no) <universes(cumulative)>`. Attributes :attr:`program` and :attr:`canonical` are also affected, - with the syntax ``attr(false)`` being deprecated in favor of - ``attr=no``. + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + (`#13312 <https://github.com/coq/coq/pull/13312>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 298ea4b4ab..104f84a253 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -99,15 +99,15 @@ coercions. Enables the program mode, in which 1) typechecking allows subset coercions and 2) the elaboration of pattern matching of :cmd:`Fixpoint` and - :cmd:`Definition` act as if the :attr:`program` attribute had been + :cmd:`Definition` acts as if the :attr:`program` attribute has been used, generating obligations if there are unresolved holes after typechecking. -.. attr:: program +.. attr:: program{? = {| yes | no } } :name: program; Program - Allows using the Program mode on a specific - definition. An alternative syntax is to use the legacy ``Program`` + This :term:`boolean attribute` allows using or disabling the Program mode on a specific + definition. An alternative and commonly used syntax is to use the legacy ``Program`` prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter. .. _syntactic_control: diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index a2ed23335e..3790f36e5a 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,25 +122,32 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. attr:: universes(polymorphic) - :name: universes(polymorphic); Polymorphic +.. attr:: universes(polymorphic{? = {| yes | no } }) + :name: universes(polymorphic); Polymorphic; Monomorphic - This boolean attribute can be used to control whether universe + This :term:`boolean attribute` can be used to control whether universe polymorphism is enabled in the definition of an inductive type. There is also a legacy syntax using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as shown in the examples, is more commonly used. - When ``polymorphic=no`` is set, global universe constraints + When ``universes(polymorphic=no)`` is used, global universe constraints are produced, even when the :flag:`Universe Polymorphism` flag is on. There is also a legacy syntax using the ``Monomorphic`` prefix (see :n:`@legacy_attr`). +.. attr:: universes(monomorphic) + + .. deprecated:: 8.13 + + Use :attr:`universes(polymorphic=no) <universes(polymorphic)>` + instead. + .. flag:: Universe Polymorphism This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(polymorphic)` attribute is - used to override the default. + polymorphic unless the :attr:`universes(polymorphic=no) <universes(polymorphic)>` + attribute is used to override the default. Many other commands can be used to declare universe polymorphic or monomorphic constants depending on whether the :flag:`Universe @@ -168,18 +175,23 @@ attribute is used: Cumulative, NonCumulative ------------------------- -.. attr:: universes(cumulative) - :name: universes(cumulative); Cumulative +.. attr:: universes(cumulative{? = {| yes | no } }) + :name: universes(cumulative); Cumulative; NonCumulative Polymorphic inductive types, coinductive types, variants and - records can be declared cumulative using this attribute or the - legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + records can be declared cumulative using this :term:`boolean attribute` + or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as shown in the examples, is more commonly used. This means that two instances of the same inductive type (family) are convertible based on the universe variances; they do not need to be equal. + When the attribtue is off, the inductive type is non-cumulative + even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. + There is also a legacy syntax using the ``NonCumulative`` prefix + (see :n:`@legacy_attr`). + This means that two instances of the same inductive type (family) are convertible only if all the universes are equal. @@ -192,20 +204,21 @@ Cumulative, NonCumulative .. note:: - ``#[ universes(polymorphic), universes(cumulative) ]`` can be - abbreviated into ``#[ universes(polymorphic, cumulative) ]``. + :n:`#[ universes(polymorphic{? = yes }), universes(cumulative{? = {| yes | no } }) ]` can be + abbreviated into :n:`#[ universes(polymorphic{? = yes }, cumulative{? = {| yes | no } }) ]`. - When the attribtue is off, the inductive type as non-cumulative - even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. - There is also a legacy syntax using the ``NonCumulative`` prefix - (see :n:`@legacy_attr`). +.. attr:: universes(noncumulative) + + .. deprecated:: 8.13 + + Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead. .. flag:: Polymorphic Inductive Cumulativity When this flag is on (it is off by default), it makes all subsequent *polymorphic* inductive definitions cumulative, unless - the :attr:`universes(cumulative)` attribute with setting ``off`` is - used. It has no effect on *monomorphic* inductive definitions. + the :attr:`universes(cumulative=no) <universes(cumulative)>` attribute is + used to override the default. It has no effect on *monomorphic* inductive definitions. Consider the examples below. diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index ea29da6dd4..2b262b89c0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -380,24 +380,22 @@ this attribute`. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. -Boolean attributes take the form ``attr={yes,no}``, when the key is -omitted the default is assumed to be ``yes``. +:gdef:`Boolean attributes <boolean attribute>` take the form :n:`@ident__attr{? = {| yes | no } }`. +When the :n:`{| yes | no }` value is omitted, the default is :n:`yes`. The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: -================ ================================ -Legacy attribute New attribute -================ ================================ -`Local` :attr:`local` -`Global` :attr:`global` -`Polymorphic` :attr:`universes(polymorphic)` -`Monomorphic` :attr:`universes(polymorphic)` -`Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(cumulative)` -`Private` :attr:`private(matching)` -`Program` :attr:`program` -================ ================================ +============================= ================================ +Legacy attribute New attribute +============================= ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic`, `Monomorphic` :attr:`universes(polymorphic)` +`Cumulative`, `NonCumulative` :attr:`universes(cumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +============================= ================================ Attributes appear in the HTML documentation in blue or gray boxes after the label "Attribute". In the pdf, they appear after the diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index b9453650eb..251b5e4955 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -1056,8 +1056,8 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the :attr:`universes(template)` - attribute with the ``=no`` setting. + This can be prevented using the :attr:`universes(template=no) <universes(template)>` + attribute. Template polymorphism and full universe polymorphism (see Chapter :ref:`polymorphicuniverses`) are incompatible, so if the latter is @@ -1075,9 +1075,10 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or the :attr:`universes(template)` attribute: in this case, the warning is not emitted. -.. attr:: universes(template) +.. attr:: universes(template{? = {| yes | no } }) + :name: universes(template) - This boolean attribute can be used to explicitly declare an + This :term:`boolean attribute` can be used to explicitly declare an inductive type as template polymorphic, whether the :flag:`Auto Template Polymorphism` flag is on or off. @@ -1096,6 +1097,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or inductive type to be template polymorphic, even if the :flag:`Auto Template Polymorphism` flag is on. +.. attr:: universes(notemplate) + + .. deprecated:: 8.13 + + Use :attr:`universes(template=no) <universes(template)>` instead. + In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index ec3e3e8aa6..f7ce7f1c6c 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,7 +87,8 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. -.. attr:: canonical +.. attr:: canonical{? = {| yes | no } } + :name: canonical This boolean attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. It is equivalent to having a :cmd:`Canonical @@ -106,7 +107,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. #[canonical=no] Prf_equiv : equivalence Carrier Equal - See :ref:`canonicalstructures` for a more realistic example. + See :ref:`hierarchy_of_structures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -245,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*`` relation ``pair_eq`` whenever the type constructor ``*`` is applied to two types being themselves in the ``EQ`` class. +.. _hierarchy_of_structures: + Hierarchy of structures ---------------------------- |