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. --- interp/declare.ml | 10 +++++++++- kernel/entries.ml | 8 ++++++++ kernel/safe_typing.ml | 2 +- kernel/safe_typing.mli | 2 +- kernel/term_typing.ml | 10 ++++++++++ kernel/term_typing.mli | 2 +- library/global.mli | 2 +- 7 files changed, 31 insertions(+), 5 deletions(-) diff --git a/interp/declare.ml b/interp/declare.ml index 8781c8719..ae28c4b90 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -231,7 +231,15 @@ 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 univs = Global.push_named_def (id,de) in + let body = Future.chain de.const_entry_body (fun (body, ()) -> body) 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 diff --git a/kernel/entries.ml b/kernel/entries.ml index ca79de404..35a158682 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -81,6 +81,14 @@ type 'a definition_entry = { const_entry_opaque : bool; const_entry_inline_code : bool } +type section_def_entry = { + secdef_body : constr Univ.in_universe_context_set Future.computation; + 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 *) type parameter_entry = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fa984515a..4fbe02cf5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -384,7 +384,7 @@ 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.const_entry_universes with + let poly = match de.Entries.secdef_universes with | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fbc398a2a..faa758d07 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 * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer + Id.t * Entries.section_def_entry -> Univ.ContextSet.t safe_transformer (** Insertion of global axioms or definitions *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 761eab511..c2c65d6d4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -607,6 +607,16 @@ 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 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_opaque = false; + const_entry_inline_code = false; + } in let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in let typ = decl.cook_type in if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index c771452a1..4b893b056 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -18,7 +18,7 @@ type _ trust = | Pure : unit trust | SideEffects : structure_body -> side_effects trust -val translate_local_def : env -> Id.t -> unit definition_entry -> +val translate_local_def : env -> Id.t -> section_def_entry -> constant_def * types * Univ.ContextSet.t val translate_local_assum : env -> types -> types 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