Fix typing_flags in the checker

Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.

5 files changed, 44 insertions, 13 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index f2df99dcd6..d20eea7874 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -142,8 +142,12 @@ let check_inductive env mind mb =
         mind_universes; mind_variance;
         mind_private; mind_typing_flags; }
     =
-    (* Locally set the oracle for further typechecking *)
-    let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in
+    (* Locally set typing flags for further typechecking *)
+    let mb_flags = mb.mind_typing_flags in
+    let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded;
+                                                                  check_positive = mb_flags.check_positive;
+                                                                  check_universes = mb_flags.check_universes;
+                                                                  conv_oracle = mb_flags.conv_oracle} env in
     Indtypes.check_inductive env mind entry
   in
   let check = check mind in
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 62f72c8edc..a67945ae94 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -31,14 +31,31 @@ let pr_engagement env =
     | PredicativeSet -> str "Theory: Set is predicative"
   end
 
-let is_ax _ cb = not (Declareops.constant_has_body cb)
 
-let pr_ax env =
-  let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in
+let pr_assumptions ass axs =
   if axs = [] then
-    str "Axioms: <none>"
+    str ass ++ str ": <none>"
   else
-    hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs)
+    hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
+
+let pr_axioms env =
+  let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in
+  pr_assumptions "Axioms" csts
+
+let pr_type_in_type env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on type-in-type" csts
+
+let pr_unguarded env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts
+
+let pr_nonpositive env =
+  let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
+  pr_assumptions "Inductives whose positivity is assumed" inds
+
 
 let print_context env =
   if !output_context then begin
@@ -47,7 +64,10 @@ let print_context env =
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_ax env)));
+      str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_nonpositive env)))
   end
 
 let stats env =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9b41fbcb7a..09b8c48c15 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -17,9 +17,12 @@ let set_indirect_accessor f = indirect_accessor := f
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  (* Locally set the oracle for further typechecking *)
-  let oracle = env.env_typing_flags.conv_oracle in
-  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
+  (* Locally set typing flags for further typechecking *)
+  let orig_flags = env.env_typing_flags in
+  let cb_flags = cb.const_typing_flags in
+  let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded;
+                                                      check_universes = cb_flags.check_universes;
+                                                      conv_oracle = cb_flags.conv_oracle} env in
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
@@ -57,8 +60,8 @@ let check_constant_declaration env kn cb =
     if poly then add_constant kn cb env
     else add_constant kn cb env'
   in
-  (* Reset the value of the oracle *)
-  Environ.set_oracle env oracle
+  (* Reset the value of the typing flags *)
+  Environ.set_typing_flags orig_flags env
 
 (** {6 Checking modules } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1b17e954b7..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 =
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 } *)