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 | 63 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
4 files changed, 68 insertions, 37 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..3128e125dd 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -17,48 +17,55 @@ 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 - (* [env'] contains De Bruijn universe variables *) - let poly, env' = + let cb_flags = cb.const_typing_flags in + let env = Environ.set_typing_flags + {env.env_typing_flags with + check_guarded = cb_flags.check_guarded; + check_universes = cb_flags.check_universes; + conv_oracle = cb_flags.conv_oracle;} + env + in + let poly, env = match cb.const_universes with - | Monomorphic ctx -> false, env + | Monomorphic ctx -> + (* Monomorphic universes are stored at the library level, the + ones in const_universes should not be needed *) + false, env | Polymorphic auctx -> let ctx = Univ.AUContext.repr auctx in + (* [env] contains De Bruijn universe variables *) let env = push_context ~strict:false ctx env in true, env in let ty = cb.const_type in - let _ = infer_type env' ty in - let otab = Environ.opaque_tables env' in - let body, env' = match cb.const_body with - | Undef _ | Primitive _ -> None, env' - | Def c -> Some (Mod_subst.force_constr c), env' - | OpaqueDef o -> - let c, u = Opaqueproof.force_proof !indirect_accessor otab o in - let env' = match u, cb.const_universes with - | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env' - | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ -> - push_subgraph local env' - | _ -> assert false - in - Some c, env' + let _ = infer_type env ty in + let otab = Environ.opaque_tables env in + let body, env = match cb.const_body with + | Undef _ | Primitive _ -> None, env + | Def c -> Some (Mod_subst.force_constr c), env + | OpaqueDef o -> + let c, u = Opaqueproof.force_proof !indirect_accessor otab o in + let env = match u, cb.const_universes with + | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env + | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ -> + push_subgraph local env + | _ -> assert false + in + Some c, env in let () = match body with | Some bd -> - let j = infer env' bd in - (try conv_leq env' j.uj_type ty + let j = infer env bd in + (try conv_leq env j.uj_type ty with NotConvertible -> Type_errors.error_actual_type env j ty) | None -> () in - let env = - 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 + () + +let check_constant_declaration env kn cb = + let () = check_constant_declaration env kn cb in + Environ.add_constant kn cb env (** {6 Checking modules } *) diff --git a/checker/values.ml b/checker/values.ml index 8dc09aed87..cc9ac1f834 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; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |