Merge PR #10291: Controlling typing flags with commands (no attribute)

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

7 files changed, 27 insertions, 1 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index dff19dee5e..8d32684b09 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -66,6 +66,10 @@ type typing_flags = {
   (** If [false] then fixed points and co-fixed points are assumed to
       be total. *)
 
+  check_positive : bool;
+  (** If [false] then inductive types are assumed positive and co-inductive
+      types are assumed productive. *)
+
   check_universes : bool;
   (** If [false] universe constraints are not checked *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7a553700e8..391b139496 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration
 
 let safe_flags oracle = {
   check_guarded = true;
+  check_positive = true;
   check_universes = true;
   conv_oracle = oracle;
   share_reduction = true;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9a75f0b682..655094e88b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -216,6 +216,9 @@ let lookup_named_ctxt id ctxt =
 let fold_constants f env acc =
   Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
 
+let fold_inductives f env acc =
+  Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+
 (* Global constants *)
 
 let lookup_constant_key kn env =
@@ -418,6 +421,7 @@ let set_engagement c env = (* Unsafe *)
 (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
 let same_flags {
      check_guarded;
+     check_positive;
      check_universes;
      conv_oracle;
      indices_matter;
@@ -426,6 +430,7 @@ let same_flags {
      enable_native_compiler;
   } alt =
   check_guarded == alt.check_guarded &&
+  check_positive == alt.check_positive &&
   check_universes == alt.check_universes &&
   conv_oracle == alt.conv_oracle &&
   indices_matter == alt.indices_matter &&
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6cd4f96645..e6d814ac7d 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -176,6 +176,7 @@ val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
 val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b0366d6ec0..aa3ef715db 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -546,7 +546,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let chkpos = (Environ.typing_flags env).check_guarded in
+  let chkpos = (Environ.typing_flags env).check_positive in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
       mie.mind_entry_inds
   in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ea45f699ce..6970a11e72 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,18 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_check_guarded b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_guarded = b } senv
+
+let set_check_positive b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_positive = b } senv
+
+let set_check_universes b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_universes = b } senv
+
 let set_indices_matter indices_matter senv =
   set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2406b6add1..fa53fa33fa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0
 val set_indices_matter : bool -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
+val set_check_guarded : bool -> safe_transformer0
+val set_check_positive : bool -> safe_transformer0
+val set_check_universes : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0
 val set_native_compiler : bool -> safe_transformer0
 val make_sprop_cumulative : safe_transformer0