diff options
24 files changed, 332 insertions, 148 deletions
diff --git a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh new file mode 100644 index 0000000000..3bdbcf7d6e --- /dev/null +++ b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then + + overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single + overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single + +fi diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst new file mode 100644 index 0000000000..f069bc616b --- /dev/null +++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst @@ -0,0 +1,17 @@ +- **Changed:** + :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 :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/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..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,33 +122,37 @@ 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 :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 ``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`). - 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. +.. attr:: universes(monomorphic) -.. flag:: Universe Polymorphism + .. deprecated:: 8.13 - This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(monomorphic)` attribute is - used. + Use :attr:`universes(polymorphic=no) <universes(polymorphic)>` + instead. -.. attr:: universes(monomorphic) - :name: universes(monomorphic); Monomorphic +.. flag:: Universe Polymorphism - 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`). + This flag is off by default. When it is on, new declarations are + 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 -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. @@ -171,19 +175,27 @@ Polymorphism` flag is on or the :attr:`universes(polymorphic)` or 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. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + 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. + + .. 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 @@ -192,26 +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 } }) ]`. -.. flag:: Polymorphic Inductive Cumulativity +.. attr:: universes(noncumulative) - 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. + .. deprecated:: 8.13 -.. attr:: universes(noncumulative) - :name: universes(noncumulative); NonCumulative + Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead. - 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`). +.. flag:: Polymorphic Inductive Cumulativity - This means that two instances of the same inductive type (family) - are convertible only if all the universes are equal. + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + 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/changes.rst b/doc/sphinx/changes.rst index de5dbe79cc..4d59fc0513 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -533,8 +533,8 @@ Flags, options and attributes - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)` and :attr:`universes(notemplate)` instead + Use :attr:`universes(polymorphic)`, ``universes(monomorphic)``, + :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** :flag:`Hide Obligations` flag @@ -545,7 +545,7 @@ Flags, options and attributes <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). - **Added:** New attributes supported when defining an inductive type - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`universes(cumulative)`, ``universes(noncumulative)`` and :attr:`private(matching)`, which correspond to legacy attributes ``Cumulative``, ``NonCumulative``, and the previously undocumented ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 5406da38a1..2b262b89c0 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 } @@ -379,21 +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. +: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(monomorphic)` -`Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(noncumulative)` -`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/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..251b5e4955 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,7 +1056,7 @@ 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)` + This can be prevented using the :attr:`universes(template=no) <universes(template)>` attribute. Template polymorphism and full universe polymorphism (see Chapter @@ -1077,11 +1075,12 @@ 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 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 :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. .. exn:: template and polymorphism not compatible @@ -1094,11 +1093,15 @@ 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. + 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. + .. 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. + .. 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 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: diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index 48120503af..f7ce7f1c6c 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,29 +87,27 @@ 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(false) +.. attr:: canonical{? = {| yes | no } } + :name: canonical - To prevent a field from being involved in the inference of - canonical instances, its declaration can be annotated with the - :attr:`canonical(false)` attribute (cf. the syntax of - :n:`@record_field`). + This boolean attribute can decorate a :cmd:`Definition` or + :cmd:`Let` command. It is equivalent to having a :cmd:`Canonical + Structure` declaration just after the command. - .. example:: + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with + ``canonical=no`` (cf. the syntax of :n:`@record_field`). - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. - - .. coqdoc:: + .. example:: - #[canonical(false)] Prf_equiv : equivalence Carrier Equal + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. - See :ref:`canonicalstructures` for a more realistic example. + .. coqdoc:: -.. attr:: canonical + #[canonical=no] Prf_equiv : equivalence Carrier Equal - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. + See :ref:`hierarchy_of_structures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -248,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 ---------------------------- @@ -331,7 +331,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }. Arguments Mixin {e le} _. diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 033ece04de..b5d57f92e9 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -764,6 +764,7 @@ attribute: [ attr_value: [ | "=" string +| "=" IDENT | "(" attribute_list ")" | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index dfd3a18908..c9d70a88fc 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -383,6 +383,7 @@ attribute: [ attr_value: [ | "=" string +| "=" ident | "(" LIST0 attribute SEP "," ")" ] diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out new file mode 100644 index 0000000000..25572ee2aa --- /dev/null +++ b/test-suite/output/attributes.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +Attribute for canonical specified twice. +The command has indeed failed with message: +key 'polymorphic' has been already set. +The command has indeed failed with message: +Invalid value 'foo' for key polymorphic +use one of {yes, no} +The command has indeed failed with message: +Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead. +The command has indeed failed with message: +Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead. diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v new file mode 100644 index 0000000000..aef05e6cd4 --- /dev/null +++ b/test-suite/output/attributes.v @@ -0,0 +1,9 @@ +Fail #[canonical=yes, canonical=no] Definition a := 3. + +Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3. + +Fail #[universes(polymorphic=foo)] Definition a := 3. + +Fail #[universes(polymorphic(foo))] Definition a := 3. + +Fail #[universes(polymorphic(foo,bar))] Definition a := 3. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index 656362b8fc..d11ae20b8d 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -37,7 +37,7 @@ Module Yes. End Yes. Module No. - #[universes(notemplate)] + #[universes(template=no)] Inductive Box (A:Type) : Type := box : A -> Box A. About Box. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index b403fc120c..b866c4b074 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -16,11 +16,16 @@ Definition ι T (x: T) := x. Check ι _ ι. +#[universes(polymorphic=no)] +Definition ιι T (x: T) := x. + +Fail Check ιι _ ιι. + #[program] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. -#[program(true)] +#[program=yes] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. @@ -43,3 +48,14 @@ Export Set Foo. Fail #[ export ] Export Foo. (* Attribute for Locality specified twice *) + +(* Tests for deprecated attribute syntax *) +Set Warnings "-deprecated-attribute-syntax". + +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + +#[universes(monomorphic)] +Definition ιιι T (x: T) := x. +Fail Check ιιι _ ιιι. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index efba6d332a..fdaeedef8c 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -11,13 +11,29 @@ open CErrors (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +let pr_vernac_flag_leaf = function + | FlagIdent b -> Pp.str b + | FlagString s -> Pp.(quote (str s)) + +let rec pr_vernac_flag_value = let open Pp in function + | VernacFlagEmpty -> mt () + | VernacFlagLeaf l -> str "=" ++ pr_vernac_flag_leaf l + | VernacFlagList s -> surround (prlist_with_sep pr_comma pr_vernac_flag s) +and pr_vernac_flag (s, arguments) = + let open Pp in + str s ++ (pr_vernac_flag_value arguments) + let warn_unsupported_attributes = CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError (fun atts -> @@ -105,16 +121,82 @@ let single_key_parser ~name ~key v prev args = assert_once ~name prev; v -let bool_attribute ~name ~on ~off : bool option attribute = - attribute_of_list [(on, single_key_parser ~name ~key:on true); - (off, single_key_parser ~name ~key:off false)] +let pr_possible_values ~values = + Pp.(str "{" ++ prlist_with_sep pr_comma str (List.map fst values) ++ str "}") + +(** [key_value_attribute ~key ~default ~values] parses a attribute [key=value] + with possible [key] [value] in [values], [default] is for compatibility for users + doing [qualif(key)] which is parsed as [qualif(key=default)] *) +let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option attribute = + let parser = function + | Some v -> + CErrors.user_err Pp.(str "key '" ++ str key ++ str "' has been already set.") + | None -> + begin function + | VernacFlagLeaf (FlagIdent b) -> + begin match CList.assoc_f String.equal b values with + | exception Not_found -> + CErrors.user_err + Pp.(str "Invalid value '" ++ str b ++ str "' for key " ++ str key ++ fnl () ++ + str "use one of " ++ pr_possible_values ~values) + | value -> value + end + | VernacFlagEmpty -> + default + | err -> + CErrors.user_err + Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try " + ++ str key ++ str "=" ++ pr_possible_values ~values ++ str " instead.") + end + in + attribute_of_list [key, parser] + +let bool_attribute ~name : bool option attribute = + let values = ["yes", true; "no", false] in + key_value_attribute ~key:name ~default:true ~values + +let legacy_bool_attribute ~name ~on ~off : bool option attribute = + attribute_of_list + [(on, single_key_parser ~name ~key:on true); + (off, single_key_parser ~name ~key:off false)] + +(* important note: we use on as the default for the new bool_attribute ! *) +let deprecated_bool_attribute_warning = + CWarnings.create + ~name:"deprecated-attribute-syntax" + ~category:"parsing" + ~default:CWarnings.Enabled + (fun name -> + Pp.(str "Syntax for switching off boolean attributes has been updated, use " ++ str name ++ str "=no instead.")) + +let deprecated_bool_attribute ~name ~on ~off : bool option attribute = + bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function + | None, None -> + None + | None, Some v -> + deprecated_bool_attribute_warning name; + Some v + | Some v, None -> Some v + | Some v1, Some v2 -> + CErrors.user_err + Pp.(str "attribute " ++ str name ++ + str ": cannot specify legacy and modern syntax at the same time.") + ) (* Variant of the [bool] attribute with only two values (bool has three). *) let get_bool_value ~key ~default = function | VernacFlagEmpty -> default - | VernacFlagList [ "true", VernacFlagEmpty ] -> true - | VernacFlagList [ "false", VernacFlagEmpty ] -> false + | VernacFlagList [ "true", VernacFlagEmpty ] -> + deprecated_bool_attribute_warning key; + true + | VernacFlagList [ "false", VernacFlagEmpty ] -> + deprecated_bool_attribute_warning key; + false + | VernacFlagLeaf (FlagIdent "yes") -> + true + | VernacFlagLeaf (FlagIdent "no") -> + false | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.") let enable_attribute ~key ~default : bool attribute = @@ -161,18 +243,37 @@ let () = let open Goptions in let program = enable_attribute ~key:"program" ~default:(fun () -> !program_mode) -let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" - -let option_locality = +(* This is a bit complex as the grammar in g_vernac.mlg doesn't + distingish between the boolean and ternary case.*) +let option_locality_parser = let name = "Locality" in attribute_of_list [ - ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal); - ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal); - ("export", single_key_parser ~name ~key:"export" Goptions.OptExport); - ] >>= function + ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal) + ; ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal) + ; ("export", single_key_parser ~name ~key:"export" Goptions.OptExport) + ] + +let option_locality = + option_locality_parser >>= function | None -> return Goptions.OptDefault | Some l -> return l +(* locality is supposed to be true when local, false when global *) +let locality = + let locality_to_bool = + function + | Goptions.OptLocal -> + true + | Goptions.OptGlobal -> + false + | Goptions.OptExport -> + CErrors.user_err Pp.(str "export attribute not supported here") + | Goptions.OptDefault -> + CErrors.user_err Pp.(str "default attribute not supported here") + in + option_locality_parser >>= function l -> + return (Option.map locality_to_bool l) + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] @@ -188,12 +289,17 @@ let is_universe_polymorphism = fun () -> !b let polymorphic_base = - bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function + deprecated_bool_attribute + ~name:"Polymorphism" + ~on:"polymorphic" ~off:"monomorphic" >>= function | Some b -> return b | None -> return (is_universe_polymorphism()) let template = - qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") + qualify_attribute ukey + (deprecated_bool_attribute + ~name:"Template" + ~on:"template" ~off:"notemplate") let polymorphic = qualify_attribute ukey polymorphic_base @@ -201,12 +307,12 @@ let polymorphic = let deprecation_parser : Deprecation.t key_parser = fun orig args -> assert_once ~name:"deprecation" orig; match args with - | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] - | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> + | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ; "note", VernacFlagLeaf (FlagString note) ] + | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ; "since", VernacFlagLeaf (FlagString since) ] -> Deprecation.make ~since ~note () - | VernacFlagList [ "since", VernacFlagLeaf since ] -> + | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ] -> Deprecation.make ~since () - | VernacFlagList [ "note", VernacFlagLeaf note ] -> + | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ] -> Deprecation.make ~note () | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") @@ -218,7 +324,7 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] -let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] +let vernac_monomorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagLeaf (FlagIdent "no")] let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) @@ -228,7 +334,7 @@ let canonical_instance = let uses_parser : string key_parser = fun orig args -> assert_once ~name:"using" orig; match args with - | VernacFlagLeaf str -> str + | VernacFlagLeaf (FlagString str) -> str | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute") let using = attribute_of_list ["using",uses_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 1969665082..03a14a03ff 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -9,13 +9,19 @@ (************************************************************************) (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +val pr_vernac_flag : vernac_flag -> Pp.t + type +'a attribute (** The type of attributes. When parsing attributes if an ['a attribute] is present then an ['a] value will be produced. @@ -82,10 +88,19 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute (** Make an attribute from a list of key parsers together with their associated key. *) -val bool_attribute : name:string -> on:string -> off:string -> bool option attribute -(** Define boolean attribute [name] with value [true] when [on] is - provided and [false] when [off] is provided. The attribute may only - be set once for a command. *) +(** Define boolean attribute [name], of the form [name={yes,no}]. The + attribute may only be set once for a command. *) +val bool_attribute : name:string -> bool option attribute + +val deprecated_bool_attribute + : name:string + -> on:string + -> off:string + -> bool option attribute +(** Define boolean attribute [name] with will be set when [on] is + provided and unset when [off] is provided. The attribute may only + be set once for a command; this attribute both accepts the old [on] + [off] syntax and new attribute syntax [on=yes] [on=no] *) val qualify_attribute : string -> 'a attribute -> 'a attribute (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att] diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1aff76114b..116cfc6413 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -119,7 +119,8 @@ GRAMMAR EXTEND Gram ] ; attr_value: - [ [ "=" ; v = string -> { VernacFlagLeaf v } + [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) } + | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) } | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } | -> { VernacFlagEmpty } ] ] @@ -136,7 +137,7 @@ GRAMMAR EXTEND Gram | IDENT "Cumulative" -> { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) } | IDENT "NonCumulative" -> - { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) } + { ("universes", VernacFlagList ["cumulative", VernacFlagLeaf (FlagIdent "no")]) } | IDENT "Private" -> { ("private", VernacFlagList ["matching", VernacFlagEmpty]) } | IDENT "Program" -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 442269ebda..4cee4f7a47 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1331,20 +1331,10 @@ let pr_control_flag (p : control_flag) = let pr_vernac_control flags = Pp.prlist pr_control_flag flags -let rec pr_vernac_flag (k, v) = - let k = keyword k in - let open Attributes in - match v with - | VernacFlagEmpty -> k - | VernacFlagLeaf v -> k ++ str " = " ++ qs v - | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )" -and pr_vernac_flags m = - prlist_with_sep (fun () -> str ", ") pr_vernac_flag m - let pr_vernac_attributes = function | [] -> mt () - | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () + | flags -> str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut () let pr_vernac ({v = {control; attrs; expr}} as v) = tag_vernac v diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4e52af7959..0f63dfe5ce 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -674,13 +674,19 @@ let is_polymorphic_inductive_cumulativity = let polymorphic_cumulative = let error_poly_context () = user_err - Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context."); + Pp.(str "The cumulative attribute can only be used in a polymorphic context."); in let open Attributes in let open Notations in + (* EJGA: this seems redudant with code in attributes.ml *) qualify_attribute "universes" - (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" - ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative") + (deprecated_bool_attribute + ~name:"Polymorphism" + ~on:"polymorphic" ~off:"monomorphic" + ++ + deprecated_bool_attribute + ~name:"Cumulativity" + ~on:"cumulative" ~off:"noncumulative") >>= function | Some poly, Some cum -> (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive |