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/proof-engine/vernacular-commands.rst | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'doc/sphinx/proof-engine') 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/proof-engine/vernacular-commands.rst | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'doc/sphinx/proof-engine') 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/proof-engine/vernacular-commands.rst | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'doc/sphinx/proof-engine') 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