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. --- test-suite/success/typing_flags.v | 54 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index bd20d9c804..a6640a5a03 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -1,4 +1,58 @@ +From Coq Require Import Program.Tactics. +(* Part using attributes *) + +#[typing(guarded=no)] Fixpoint att_f' (n : nat) : nat := att_f' n. +#[typing(guarded=no)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n. + +#[typing(universes=no)] Definition att_T := let t := Type in (t : t). +#[typing(universes=no)] Program Definition p_att_T := let t := Type in (t : t). + +#[typing(positive=no)] +Inductive att_Cor := +| att_Over : att_Cor +| att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor. + +Fail #[typing(guarded=yes)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail #[typing(universes=yes)] Definition f_att_T := let t := Type in (t : t). + +Fail #[typing(positive=yes)] +Inductive f_att_Cor := +| f_att_Over : f_att_Cor +| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. + +Print Assumptions att_f'. +Print Assumptions att_T. +Print Assumptions att_Cor. + +(* Interactive + atts *) + +(* Coq's handling of environments in tactic mode is too broken for this to work yet *) + +(* +#[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. +#[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. +#[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. +*) + +(* Note: this works a bit by chance, the attribute only affects the + kernel call in Defined. Would the tactics perform a check we would + fail. *) +#[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat. +Proof. exact (i_att_f' n). Defined. + +#[typing(guarded=no)] Fixpoint d_att_f' (n : nat) : nat. +Proof. exact (d_att_f' n). Qed. + +(* check regular mode is still safe *) +Fail Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail Definition f_att_T := let t := Type in (t : t). + +Fail Inductive f_att_Cor := +| f_att_Over : f_att_Cor +| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. + +(* Part using Set/Unset *) Print Typing Flags. Unset Guard Checking. Fixpoint f' (n : nat) : nat := f' n. -- cgit v1.2.3 From 454a10da9412a5bd6f3661b1f60e17f08289d0e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 16 Oct 2020 17:13:14 +0200 Subject: [proofs] Support per-definition typing-flags in interactive proofs. Most cases should be accounted in proof code, however be wary of paths where `Global.env ()` is used. --- test-suite/success/typing_flags.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'test-suite/success') diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index a6640a5a03..a5fe676cc1 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -27,13 +27,12 @@ Print Assumptions att_Cor. (* Interactive + atts *) -(* Coq's handling of environments in tactic mode is too broken for this to work yet *) +(* Coq's handling of environments in tactic mode is too broken for + this to work yet, the pretyper doesn't get the right flags *) -(* #[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. #[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. #[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. -*) (* Note: this works a bit by chance, the attribute only affects the kernel call in Defined. Would the tactics perform a check we would -- 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: --- test-suite/success/typing_flags.v | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'test-suite/success') diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index a5fe676cc1..4a20f3379b 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -26,17 +26,11 @@ Print Assumptions att_T. Print Assumptions att_Cor. (* Interactive + atts *) - -(* Coq's handling of environments in tactic mode is too broken for - this to work yet, the pretyper doesn't get the right flags *) - #[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. #[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. #[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. -(* Note: this works a bit by chance, the attribute only affects the - kernel call in Defined. Would the tactics perform a check we would - fail. *) +(* Note: be aware of tactics invoking [Global.env()] if this test fails. *) #[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat. Proof. exact (i_att_f' n). Defined. -- 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. --- test-suite/success/typing_flags.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'test-suite/success') diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index 4a20f3379b..4af2028e38 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -2,21 +2,21 @@ From Coq Require Import Program.Tactics. (* Part using attributes *) -#[typing(guarded=no)] Fixpoint att_f' (n : nat) : nat := att_f' n. -#[typing(guarded=no)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n. +#[bypass_check(guard)] Fixpoint att_f' (n : nat) : nat := att_f' n. +#[bypass_check(guard)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n. -#[typing(universes=no)] Definition att_T := let t := Type in (t : t). -#[typing(universes=no)] Program Definition p_att_T := let t := Type in (t : t). +#[bypass_check(universes)] Definition att_T := let t := Type in (t : t). +#[bypass_check(universes)] Program Definition p_att_T := let t := Type in (t : t). -#[typing(positive=no)] +#[bypass_check(positivity)] Inductive att_Cor := | att_Over : att_Cor | att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor. -Fail #[typing(guarded=yes)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. -Fail #[typing(universes=yes)] Definition f_att_T := let t := Type in (t : t). +Fail #[bypass_check(guard=no)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n. +Fail #[bypass_check(universes=no)] Definition f_att_T := let t := Type in (t : t). -Fail #[typing(positive=yes)] +Fail #[bypass_check(positivity=no)] Inductive f_att_Cor := | f_att_Over : f_att_Cor | f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor. @@ -26,15 +26,15 @@ Print Assumptions att_T. Print Assumptions att_Cor. (* Interactive + atts *) -#[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. -#[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. -#[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. +#[bypass_check(universes=yes)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined. +#[bypass_check(universes=yes)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. +#[bypass_check(universes=yes)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed. (* Note: be aware of tactics invoking [Global.env()] if this test fails. *) -#[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat. +#[bypass_check(guard=yes)] Fixpoint i_att_f' (n : nat) : nat. Proof. exact (i_att_f' n). Defined. -#[typing(guarded=no)] Fixpoint d_att_f' (n : nat) : nat. +#[bypass_check(guard=yes)] Fixpoint d_att_f' (n : nat) : nat. Proof. exact (d_att_f' n). Qed. (* check regular mode is still safe *) -- cgit v1.2.3