From c3e26fca1d077a2b69926df85d05e067882c40b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 Dec 2017 08:33:55 +0100 Subject: Specific type for section definition entries. This allows to statically ensure well-formedness properties. --- library/global.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') diff --git a/library/global.mli b/library/global.mli index 2a646386e..5d7495657 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 * unit Entries.definition_entry) -> Univ.ContextSet.t +val push_named_def : (Id.t * Entries.section_def_entry) -> Univ.ContextSet.t val export_private_constants : in_section:bool -> Safe_typing.private_constants Entries.definition_entry -> -- cgit v1.2.3 From 1de1d505dfd1c5a05a4910cfc872971087de26fb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 19 Dec 2017 10:11:26 +0100 Subject: Let definitions do not create new universe constraints. We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions. --- interp/declare.ml | 19 ++++++++++++------- kernel/entries.ml | 3 +-- kernel/safe_typing.ml | 19 +++---------------- kernel/safe_typing.mli | 2 +- kernel/term_typing.ml | 44 ++++++++++++++++++++++++-------------------- kernel/term_typing.mli | 4 ++-- library/global.ml | 2 +- library/global.mli | 2 +- 8 files changed, 45 insertions(+), 50 deletions(-) (limited to 'library') 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 -> -- cgit v1.2.3