diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 8 | ||||
| -rw-r--r-- | checker/check_stat.ml | 32 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 13 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
4 files changed, 41 insertions, 14 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/checker/values.ml b/checker/values.ml index 8dc09aed87..ac9bc26344 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -219,7 +219,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |