diff options
-rw-r--r-- | interp/declare.ml | 19 | ||||
-rw-r--r-- | kernel/entries.ml | 3 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 19 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
-rw-r--r-- | kernel/term_typing.ml | 44 | ||||
-rw-r--r-- | kernel/term_typing.mli | 4 | ||||
-rw-r--r-- | library/global.ml | 2 | ||||
-rw-r--r-- | library/global.mli | 2 |
8 files changed, 45 insertions, 50 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index ae28c4b90..5be07e09e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -231,19 +231,24 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let (de, eff) = Global.export_private_constants ~in_section:true de in let () = List.iter register_side_effect eff in - let body = Future.chain de.const_entry_body (fun (body, ()) -> body) in + (** The body should already have been forced upstream because it is a + section-local definition, but it's not enforced by typing *) + let (body, uctx), () = Future.force de.const_entry_body in + let poly, univs = match de.const_entry_universes with + | Monomorphic_const_entry uctx -> false, uctx + | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx + in + let univs = Univ.ContextSet.union uctx univs in + (** We must declare the universe constraints before type-checking the + term. *) + let () = Global.push_context_set (not poly) univs in let se = { secdef_body = body; secdef_secctx = de.const_entry_secctx; - secdef_universes = de.const_entry_universes; secdef_feedback = de.const_entry_feedback; secdef_type = de.const_entry_type; } in - let univs = Global.push_named_def (id, se) in - let poly = match de.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true - in + let () = Global.push_named_def (id, se) in Explicit, de.const_entry_opaque, poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); diff --git a/kernel/entries.ml b/kernel/entries.ml index 35a158682..36b75668b 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -82,11 +82,10 @@ type 'a definition_entry = { const_entry_inline_code : bool } type section_def_entry = { - secdef_body : constr Univ.in_universe_context_set Future.computation; + secdef_body : constr; secdef_secctx : Context.Named.t option; secdef_feedback : Stateid.t option; secdef_type : types option; - secdef_universes : constant_universes_entry; } type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4fbe02cf5..93b8e278f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,22 +382,9 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let open Entries in - let c,typ,univs = Term_typing.translate_local_def senv.env id de in - let poly = match de.Entries.secdef_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true - in - let c, univs = match c with - | Def c -> Mod_subst.force_constr c, univs - | OpaqueDef o -> - Opaqueproof.force_proof (Environ.opaque_tables senv.env) o, - Univ.ContextSet.union univs - (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o) - | _ -> assert false in - let senv' = push_context_set poly univs senv in - let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in - univs, {senv' with env=env''} + let c, typ = Term_typing.translate_local_def senv.env id de in + let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in + { senv with env = env'' } let push_named_assum ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index faa758d07..757b803a3 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -90,7 +90,7 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * Entries.section_def_entry -> Univ.ContextSet.t safe_transformer + Id.t * Entries.section_def_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c2c65d6d4..2e4426d62 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -227,17 +227,14 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes abstract = function +let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx | Polymorphic_const_entry uctx -> - if not abstract then - Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx) - else - let sbst, auctx = Univ.abstract_universes uctx in - sbst, Polymorphic_const auctx + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx -let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = +let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -245,10 +242,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env in let j = infer env t in - let abstract = not (Option.is_empty kn) in - let usubst, univs = - abstract_constant_universes abstract uctx - in + let usubst, univs = abstract_constant_universes uctx in let c = Typeops.assumption_of_judgment env j in let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in { @@ -316,12 +310,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | SideEffects _ -> inline_side_effects env body ctx side_eff in let env = push_context_set ~strict:(not poly) ctx env in - let abstract = not (Option.is_empty kn) in let ctx = if poly then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) else Monomorphic_const_entry ctx in - let usubst, univs = abstract_constant_universes abstract ctx in + let usubst, univs = abstract_constant_universes ctx in let j = infer env body in let typ = match typ with | None -> @@ -493,7 +486,7 @@ let build_constant_declaration kn env result = let translate_constant mb env kn ce = build_constant_declaration kn env - (infer_declaration ~trust:mb env (Some kn) ce) + (infer_declaration ~trust:mb env ce) let constant_entry_of_side_effect cb u = let univs = @@ -607,17 +600,17 @@ let translate_recipe env kn r = let translate_local_def env id centry = let open Cooking in - let body = Future.chain centry.secdef_body (fun body -> body, ()) in + let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in let centry = { const_entry_body = body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; - const_entry_universes = centry.secdef_universes; + const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty; const_entry_opaque = false; const_entry_inline_code = false; } in - let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in + let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in let typ = decl.cook_type in if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin match decl.cook_body with @@ -629,11 +622,22 @@ let translate_local_def env id centry = (Opaqueproof.force_proof (opaque_tables env) lc) in record_aux env ids_typ ids_def end; - let univs = match decl.cook_universes with - | Monomorphic_const ctx -> ctx + let () = match decl.cook_universes with + | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx) | Polymorphic_const _ -> assert false in - decl.cook_body, typ, univs + let c = match decl.cook_body with + | Def c -> Mod_subst.force_constr c + | OpaqueDef o -> + let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in + let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + (** Let definitions are ensured to have no extra constraints coming from + the body by virtue of the typing of [Entries.section_def_entry]. *) + let () = assert (Univ.ContextSet.is_empty cst) in + p + | Undef _ -> assert false + in + c, typ (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 4b893b056..7bc029010 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -19,7 +19,7 @@ type _ trust = | SideEffects : structure_body -> side_effects trust val translate_local_def : env -> Id.t -> section_def_entry -> - constant_def * types * Univ.ContextSet.t + constr * types val translate_local_assum : env -> types -> types @@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> Constant.t option -> +val infer_declaration : trust:'a trust -> env -> 'a constant_entry -> Cooking.result val build_constant_declaration : diff --git a/library/global.ml b/library/global.ml index ce37dfecf..ed847b7cd 100644 --- a/library/global.ml +++ b/library/global.ml @@ -81,7 +81,7 @@ let globalize_with_summary fs f = let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize (Safe_typing.push_named_def d) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) diff --git a/library/global.mli b/library/global.mli index 5d7495657..03bc945da 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.section_def_entry) -> Univ.ContextSet.t +val push_named_def : (Id.t * Entries.section_def_entry) -> unit val export_private_constants : in_section:bool -> Safe_typing.private_constants Entries.definition_entry -> |