From 14150241cfd016c7f64974cc5c58bb116689f3c1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 Jul 2020 18:17:24 +0200 Subject: [vernac] Allow to control typing flags with attributes. The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks. --- doc/sphinx/language/core/inductive.rst | 26 +++++++++++-------------- doc/sphinx/proof-engine/vernacular-commands.rst | 15 ++++++++++++++ 2 files changed, 26 insertions(+), 15 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 9fda2ab1fa..f277997094 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -31,8 +31,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(template)`, :attr:`universes(cumulative)`, and - :attr:`private(matching)` attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`typing(positive)`, 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. @@ -49,10 +49,12 @@ Inductive types .. exn:: Non strictly positive occurrence of @ident in @type. - The types of the constructors have to satisfy a *positivity condition* - (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. The positivity checking can be disabled using - the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`). + The types of the constructors have to satisfy a *positivity + condition* (see Section :ref:`positivity`). This condition + ensures the soundness of the inductive definition. The + positivity checking can be disabled using the :flag:`Positivity + Checking` flag or the :attr:`typing(positive)` attribute (see + :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. @@ -848,9 +850,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive I : Prop := not_I_I (not_I : I -> False) : I. - Set Positivity Checking. + #[typing(positive=no)] Inductive I : Prop := not_I_I (not_I : I -> False) : I. .. coqtop:: all @@ -884,9 +884,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive Lam := lam (_ : Lam -> Lam). - Set Positivity Checking. + #[typing(positive=no)] Inductive Lam := lam (_ : Lam -> Lam). .. coqtop:: all @@ -915,9 +913,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. - Set Positivity Checking. + #[typing(positive=no)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. .. coqtop:: all diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e7db9cfaca..b8160b7966 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1152,6 +1152,11 @@ Controlling Typing Flags anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by :cmd:`Print Assumptions`. +.. attr:: typing(guarded) + + Similar to :flag:`Guard Checking`, but on a per-declaration + basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``. + .. flag:: Positivity Checking This flag can be used to enable/disable the positivity checking of inductive @@ -1159,6 +1164,11 @@ Controlling Typing Flags break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by :cmd:`Print Assumptions`. +.. attr:: typing(positive) + + Similar to :flag:`Positivity Checking`, but on a per-declaration basis. + Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``. + .. flag:: Universe Checking This flag can be used to enable/disable the checking of universes, providing a @@ -1167,6 +1177,11 @@ Controlling Typing Flags :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line argument (see :ref:`command-line-options`). +.. attr:: typing(universes) + + Similar to :flag:`Universe Checking`, but on a per-declaration basis. + Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``. + .. cmd:: Print Typing Flags Print the status of the three typing flags: guard checking, positivity checking -- cgit v1.2.3 From 50af46a596af607493ce46da782389e8a82e8354 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Nov 2020 23:25:17 +0100 Subject: [attributes] [doc] Documentation review by Théo. Co-authored-by: --- doc/sphinx/language/core/coinductive.rst | 3 ++- doc/sphinx/language/core/definitions.rst | 8 +++++--- doc/sphinx/language/core/inductive.rst | 10 ++++++---- doc/sphinx/proof-engine/vernacular-commands.rst | 15 +++++++++------ 4 files changed, 22 insertions(+), 14 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 43bbc8b40d..e9737f8712 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`private(matching)`, and :attr:`using` attributes. + :attr:`private(matching)`, :attr:`typing(universes)`, + :attr:`typing(positive)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 57771c9036..95bb1b0e0c 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,8 +90,9 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`program` (see :ref:`program_definition`), - :attr:`canonical` and :attr:`using` attributes. + :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, + :attr:`typing(universes)`, :attr:`typing(guarded)`, and + :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. @@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - This command accepts the :attr:`using` attribute. + This command accepts the :attr:`typing(universes)`, + :attr:`typing(guarded)`, and :attr:`using` attributes. .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index f277997094..86de059f28 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,7 +32,8 @@ Inductive types This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`typing(positive)`, and :attr:`private(matching)` attributes. + :attr:`typing(positive)`, :attr:`typing(universes)`, 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. @@ -51,8 +52,8 @@ Inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition - ensures the soundness of the inductive definition. The - positivity checking can be disabled using the :flag:`Positivity + ensures the soundness of the inductive definition. + Positivity checking can be disabled using the :flag:`Positivity Checking` flag or the :attr:`typing(positive)` attribute (see :ref:`controlling-typing-flags`). @@ -392,7 +393,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. - This command accepts the :attr:`program` attribute. + This command accepts the :attr:`program`, + :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes. To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index b8160b7966..08534c9e07 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1152,10 +1152,11 @@ Controlling Typing Flags anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by :cmd:`Print Assumptions`. -.. attr:: typing(guarded) +.. attr:: typing(guarded{? = {| yes | no } }) + :name: typing(guarded) Similar to :flag:`Guard Checking`, but on a per-declaration - basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``. + basis. Disable guard checking locally with ``typing(guarded=no)``. .. flag:: Positivity Checking @@ -1164,10 +1165,11 @@ Controlling Typing Flags break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by :cmd:`Print Assumptions`. -.. attr:: typing(positive) +.. attr:: typing(positive{? = {| yes | no } }) + :name: typing(positive) Similar to :flag:`Positivity Checking`, but on a per-declaration basis. - Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``. + Disable positivity checking locally with ``typing(positive=no)``. .. flag:: Universe Checking @@ -1177,10 +1179,11 @@ Controlling Typing Flags :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line argument (see :ref:`command-line-options`). -.. attr:: typing(universes) +.. attr:: typing(universes{? = {| yes | no } }) + :name: typing(universes) Similar to :flag:`Universe Checking`, but on a per-declaration basis. - Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``. + Disable universe checking locally with ``typing(universe=no)``. .. cmd:: Print Typing Flags -- cgit v1.2.3 From 1f0f1ae93f757be8101d598f8aaf5b564bde9dcd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Nov 2020 21:32:37 +0100 Subject: [attributes] [typing] Rename `typing` to `bypass_check` As discussed in the Coq meeting. --- doc/sphinx/language/core/coinductive.rst | 4 ++-- doc/sphinx/language/core/definitions.rst | 6 +++--- doc/sphinx/language/core/inductive.rst | 12 ++++++------ doc/sphinx/proof-engine/vernacular-commands.rst | 18 +++++++++--------- 4 files changed, 20 insertions(+), 20 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index e9737f8712..cf46580bdb 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -27,8 +27,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`private(matching)`, :attr:`typing(universes)`, - :attr:`typing(positive)`, and :attr:`using` attributes. + :attr:`private(matching)`, :attr:`bypass_check(universes)`, + :attr:`bypass_check(positivity)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 95bb1b0e0c..76aa543b8b 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -91,7 +91,7 @@ Section :ref:`typing-rules`. These commands also support the :attr:`universes(polymorphic)`, :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, - :attr:`typing(universes)`, :attr:`typing(guarded)`, and + :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. @@ -163,8 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - This command accepts the :attr:`typing(universes)`, - :attr:`typing(guarded)`, and :attr:`using` attributes. + This command accepts the :attr:`bypass_check(universes)`, + :attr:`bypass_check(guard)`, and :attr:`using` attributes. .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 86de059f28..4bee7cc1b1 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,7 +32,7 @@ Inductive types This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`typing(positive)`, :attr:`typing(universes)`, and + :attr:`bypass_check(positivity)`, :attr:`bypass_check(universes)`, and :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. @@ -54,7 +54,7 @@ Inductive types condition* (see Section :ref:`positivity`). This condition ensures the soundness of the inductive definition. Positivity checking can be disabled using the :flag:`Positivity - Checking` flag or the :attr:`typing(positive)` attribute (see + Checking` flag or the :attr:`bypass_check(positivity)` attribute (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. @@ -394,7 +394,7 @@ constructions. to :n:`fun {* @binder } => @term`. This command accepts the :attr:`program`, - :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes. + :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes. To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They @@ -852,7 +852,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - #[typing(positive=no)] Inductive I : Prop := not_I_I (not_I : I -> False) : I. + #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I. .. coqtop:: all @@ -886,7 +886,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - #[typing(positive=no)] Inductive Lam := lam (_ : Lam -> Lam). + #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam). .. coqtop:: all @@ -915,7 +915,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - #[typing(positive=no)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. + #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. .. coqtop:: all diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 08534c9e07..e866e4c624 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1152,11 +1152,11 @@ Controlling Typing Flags anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by :cmd:`Print Assumptions`. -.. attr:: typing(guarded{? = {| yes | no } }) - :name: typing(guarded) +.. attr:: bypass_check(guard{? = {| yes | no } }) + :name: bypass_check(guard) Similar to :flag:`Guard Checking`, but on a per-declaration - basis. Disable guard checking locally with ``typing(guarded=no)``. + basis. Disable guard checking locally with ``bypass_check(guard)``. .. flag:: Positivity Checking @@ -1165,11 +1165,11 @@ Controlling Typing Flags break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by :cmd:`Print Assumptions`. -.. attr:: typing(positive{? = {| yes | no } }) - :name: typing(positive) +.. attr:: bypass_check(positivity{? = {| yes | no } }) + :name: bypass_check(positivity) Similar to :flag:`Positivity Checking`, but on a per-declaration basis. - Disable positivity checking locally with ``typing(positive=no)``. + Disable positivity checking locally with ``bypass_check(positivity)``. .. flag:: Universe Checking @@ -1179,11 +1179,11 @@ Controlling Typing Flags :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line argument (see :ref:`command-line-options`). -.. attr:: typing(universes{? = {| yes | no } }) - :name: typing(universes) +.. attr:: bypass_check(universes{? = {| yes | no } }) + :name: bypass_check(universes) Similar to :flag:`Universe Checking`, but on a per-declaration basis. - Disable universe checking locally with ``typing(universe=no)``. + Disable universe checking locally with ``bypass_check(universes)``. .. cmd:: Print Typing Flags -- cgit v1.2.3