diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.mli | 2 | ||||
| -rw-r--r-- | kernel/entries.ml | 7 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 20 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 60 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 10 |
6 files changed, 54 insertions, 51 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 21c477578c..98bf713082 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -203,7 +203,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) - | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) + | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. The {!mkApp} constructor also enforces the following invariant: diff --git a/kernel/entries.ml b/kernel/entries.ml index ca79de404d..36b75668b2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -81,6 +81,13 @@ type 'a definition_entry = { const_entry_opaque : bool; const_entry_inline_code : bool } +type section_def_entry = { + secdef_body : constr; + secdef_secctx : Context.Named.t option; + secdef_feedback : Stateid.t option; + secdef_type : types option; +} + 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 5150ad4113..93b8e278fa 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,23 +382,9 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let open Entries in - let trust = Term_typing.SideEffects senv.revstruct in - let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in - let poly = match de.Entries.const_entry_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 a30bb37e64..757b803a39 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 * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer + Id.t * Entries.section_def_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) @@ -106,8 +106,8 @@ type exported_private_constant = Constant.t * private_constant_role val export_private_constants : in_section:bool -> - private_constants Entries.constant_entry -> - (unit Entries.constant_entry * exported_private_constant list) safe_transformer + private_constants Entries.definition_entry -> + (unit Entries.definition_entry * exported_private_constant list) safe_transformer (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 70dd6438d4..2e4426d621 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 = @@ -533,14 +526,10 @@ type side_effect_role = type exported_side_effect = Constant.t * constant_body * side_effect_role -let export_side_effects mb env ce = - match ce with - | ParameterEntry e -> [], ParameterEntry e - | ProjectionEntry e -> [], ProjectionEntry e - | DefinitionEntry c -> +let export_side_effects mb env c = let { const_entry_body = body } = c in let _, eff = Future.force body in - let ce = DefinitionEntry { c with + let ce = { c with const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = @@ -609,9 +598,19 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) -let translate_local_def mb env id centry = +let translate_local_def env id centry = let open Cooking in - let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) 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 = Monomorphic_const_entry Univ.ContextSet.empty; + const_entry_opaque = false; + const_entry_inline_code = false; + } 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 @@ -623,11 +622,22 @@ let translate_local_def mb 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 55da4197e2..7bc029010f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -18,8 +18,8 @@ type _ trust = | Pure : unit trust | SideEffects : structure_body -> side_effects trust -val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> - constant_def * types * Univ.ContextSet.t +val translate_local_def : env -> Id.t -> section_def_entry -> + constr * types val translate_local_assum : env -> types -> types @@ -62,8 +62,8 @@ type exported_side_effect = * be pushed in the safe_env by safe typing. The main constant entry * needs to be translated as usual after this step. *) val export_side_effects : - structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * unit constant_entry + structure_body -> env -> side_effects definition_entry -> + exported_side_effect list * unit definition_entry val translate_mind : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body @@ -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 : |