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/addendum/type-classes.rst | 7 ++-- doc/sphinx/addendum/universe-polymorphism.rst | 54 ++++++++++++--------------- 2 files changed, 27 insertions(+), 34 deletions(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 2474c784b8..22527dc379 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -320,10 +320,9 @@ Summary of the commands maintained. Like any command declaring a record, 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(polymorphic)`, :attr:`universes(template)`, + :attr:`universes(cumulative)`, and :attr:`private(matching)` + attributes. .. cmd:: Existing Class @qualid diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 064107d088..a2ed23335e 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -125,30 +125,27 @@ Polymorphic, Monomorphic .. attr:: universes(polymorphic) :name: universes(polymorphic); Polymorphic - This attribute can be used to declare universe polymorphic - definitions and inductive types. There is also a legacy syntax - using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as - shown in the examples, is more commonly used. + This 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 + 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`). .. flag:: Universe Polymorphism This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(monomorphic)` attribute is - used. - -.. attr:: universes(monomorphic) - :name: universes(monomorphic); Monomorphic - - This attribute can be used to declare universe monomorphic - definitions and inductive types (i.e. 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`). + polymorphic unless the :attr:`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 -Polymorphism` flag is on or the :attr:`universes(polymorphic)` or -:attr:`universes(monomorphic)` attributes are used: +Polymorphism` flag is on or the :attr:`universes(polymorphic)` +attribute is used: - :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe polymorphic constants. @@ -183,6 +180,9 @@ Cumulative, NonCumulative are convertible based on the universe variances; they do not need to be equal. + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. + .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, @@ -195,23 +195,17 @@ Cumulative, NonCumulative ``#[ universes(polymorphic), universes(cumulative) ]`` can be abbreviated into ``#[ universes(polymorphic, cumulative) ]``. + 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`). + .. 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(noncumulative)` attribute is used. It has no - effect on *monomorphic* inductive definitions. - -.. attr:: universes(noncumulative) - :name: universes(noncumulative); NonCumulative - - Declares 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`). - - This means that two instances of the same inductive type (family) - are convertible only if all the universes are equal. + the :attr:`universes(cumulative)` attribute with setting ``off`` is + used. It has no effect on *monomorphic* inductive definitions. Consider the examples below. -- 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/addendum/program.rst | 8 ++--- doc/sphinx/addendum/universe-polymorphism.rst | 49 +++++++++++++++++---------- 2 files changed, 35 insertions(+), 22 deletions(-) (limited to 'doc/sphinx/addendum') 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) ` + 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) ` + 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) ` 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) ` attribute is + used to override the default. It has no effect on *monomorphic* inductive definitions. Consider the examples below. -- cgit v1.2.3 From 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Nov 2020 15:57:37 +0100 Subject: [attributes] Update error message referring to deprecated syntax. --- doc/sphinx/addendum/universe-polymorphism.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 3790f36e5a..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -195,7 +195,7 @@ Cumulative, NonCumulative This means that two instances of the same inductive type (family) are convertible only if all the universes are equal. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + .. exn:: The cumulative attribute can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, i.e. either having the :flag:`Universe Polymorphism` flag on, or -- cgit v1.2.3