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.
---
 vernac/attributes.ml | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

(limited to 'vernac/attributes.ml')

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fdaeedef8c..05d96a1165 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -338,3 +338,46 @@ let uses_parser : string key_parser = fun orig args ->
   |  _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
 
 let using = attribute_of_list ["using",uses_parser]
+
+let process_typing_att ~typing_flags att enable =
+  match att with
+  | "universes" ->
+    { typing_flags with
+      Declarations.check_universes = enable
+    }
+  | "guarded" ->
+    { typing_flags with
+      Declarations.check_guarded = enable
+    }
+  | "positive" ->
+    { typing_flags with
+      Declarations.check_positive = enable
+    }
+  | att ->
+    CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
+
+let process_typing_enable ~key = function
+  | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") ->
+    true
+  | VernacFlagLeaf (FlagIdent "no") ->
+    false
+  | _ ->
+    CErrors.user_err Pp.(str "Ill-formed attribute value, must be " ++ str key ++ str "={yes, no}")
+
+let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args ->
+  let rec flag_parser typing_flags = function
+    | [] -> typing_flags
+    | (typing_att, enable) :: rest ->
+      let enable = process_typing_enable ~key:typing_att enable in
+      let typing_flags = process_typing_att ~typing_flags typing_att enable in
+      flag_parser typing_flags rest
+  in
+  match args with
+  | VernacFlagList atts ->
+    let typing_flags = Global.typing_flags () in
+    flag_parser typing_flags atts
+  | att ->
+    CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
+
+let typing_flags =
+  attribute_of_list ["typing", typing_flags_parser]
-- 
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.
---
 vernac/attributes.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'vernac/attributes.ml')

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 05d96a1165..37895d22f5 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -339,24 +339,25 @@ let uses_parser : string key_parser = fun orig args ->
 
 let using = attribute_of_list ["using",uses_parser]
 
-let process_typing_att ~typing_flags att enable =
+let process_typing_att ~typing_flags att disable =
+  let enable = not disable in
   match att with
   | "universes" ->
     { typing_flags with
       Declarations.check_universes = enable
     }
-  | "guarded" ->
+  | "guard" ->
     { typing_flags with
       Declarations.check_guarded = enable
     }
-  | "positive" ->
+  | "positivity" ->
     { typing_flags with
       Declarations.check_positive = enable
     }
   | att ->
     CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
 
-let process_typing_enable ~key = function
+let process_typing_disable ~key = function
   | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") ->
     true
   | VernacFlagLeaf (FlagIdent "no") ->
@@ -368,8 +369,8 @@ let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args -
   let rec flag_parser typing_flags = function
     | [] -> typing_flags
     | (typing_att, enable) :: rest ->
-      let enable = process_typing_enable ~key:typing_att enable in
-      let typing_flags = process_typing_att ~typing_flags typing_att enable in
+      let disable = process_typing_disable ~key:typing_att enable in
+      let typing_flags = process_typing_att ~typing_flags typing_att disable in
       flag_parser typing_flags rest
   in
   match args with
@@ -380,4 +381,4 @@ let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args -
     CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
 
 let typing_flags =
-  attribute_of_list ["typing", typing_flags_parser]
+  attribute_of_list ["bypass_check", typing_flags_parser]
-- 
cgit v1.2.3