From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Nov 2020 20:21:36 +0100 Subject: [attributes] Deprecate `attr(true)` syntax in favor of booelan attributes. We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog. --- doc/sphinx/language/core/basic.rst | 7 +++++-- doc/sphinx/language/core/coinductive.rst | 6 ++---- doc/sphinx/language/core/definitions.rst | 2 +- doc/sphinx/language/core/inductive.rst | 24 ++++++++++-------------- doc/sphinx/language/core/records.rst | 6 ++---- doc/sphinx/language/core/variants.rst | 6 ++---- 6 files changed, 22 insertions(+), 29 deletions(-) (limited to 'doc/sphinx/language/core') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 5406da38a1..af5c47dba8 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -379,6 +379,9 @@ 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``. + The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: @@ -388,9 +391,9 @@ Legacy attribute New attribute `Local` :attr:`local` `Global` :attr:`global` `Polymorphic` :attr:`universes(polymorphic)` -`Monomorphic` :attr:`universes(monomorphic)` +`Monomorphic` :attr:`universes(polymorphic)` `Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(noncumulative)` +`NonCumulative` :attr:`universes(cumulative)` `Private` :attr:`private(matching)` `Program` :attr:`program` ================ ================================ diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 3e2ecdc0f0..43bbc8b40d 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -26,10 +26,8 @@ More information on co-inductive definitions can be found in For co-inductive types, the only elimination principle is case analysis. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)`, :attr:`private(matching)` - and :attr:`using` attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`private(matching)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 79489c85f6..57771c9036 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,7 +90,7 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`program` (see :ref:`program_definition`), :attr:`canonical` and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index ad7d6f3963..b9453650eb 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,10 +32,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -1058,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(notemplate)` - attribute. + This can be prevented using the :attr:`universes(template)` + attribute with the ``=no`` setting. Template polymorphism and full universe polymorphism (see Chapter :ref:`polymorphicuniverses`) are incompatible, so if the latter is @@ -1079,9 +1077,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or .. attr:: universes(template) - This attribute can be used to explicitly declare an inductive type - as template polymorphic, whether the :flag:`Auto Template - Polymorphism` flag is on or off. + This 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. .. exn:: template and polymorphism not compatible @@ -1094,11 +1092,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or The attribute was used but the inductive definition does not satisfy the criterion to be template polymorphic. -.. attr:: universes(notemplate) - - This attribute can be used to prevent an inductive type to be - template polymorphic, even if the :flag:`Auto Template - Polymorphism` flag is on. + When ``universes(template=no)`` is used, it will prevent an + inductive type to be template polymorphic, even if the :flag:`Auto + Template Polymorphism` flag is on. 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 diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index e6df3ee9f5..7eedbcd59a 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -53,10 +53,8 @@ expressions. In this sense, the :cmd:`Record` construction allows defining :cmd:`Record` and :cmd:`Structure` are synonyms. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 645986be9c..6ac6626dbe 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -17,10 +17,8 @@ Variants this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. .. exn:: The @natural th argument of @ident must be @ident in @type. :undocumented: -- cgit v1.2.3 From 3b479357d8c5c1a655b2b8257f14a8cafe7621fc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 14 Nov 2020 16:01:00 +0100 Subject: Run doc_grammar for #13312. --- doc/sphinx/language/core/basic.rst | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/sphinx/language/core') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index af5c47dba8..ea29da6dd4 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -369,6 +369,7 @@ this attribute`. attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr } attribute ::= @ident {? @attr_value } attr_value ::= = @string + | = @ident | ( {*, @attribute } ) legacy_attr ::= {| Local | Global } | {| Polymorphic | Monomorphic } -- cgit v1.2.3 From ca42305f1ed1699065cffdef7d96bf5fcc0069be Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 14 Nov 2020 18:44:57 +0100 Subject: Review commit: improving the doc of boolean attributes. --- doc/sphinx/language/core/basic.rst | 26 ++++++++++++-------------- doc/sphinx/language/core/inductive.rst | 15 +++++++++++---- 2 files changed, 23 insertions(+), 18 deletions(-) (limited to 'doc/sphinx/language/core') 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 ` 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) ` + 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) ` 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 -- cgit v1.2.3