diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 9 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 48 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 3 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 84 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 10 |
5 files changed, 71 insertions, 83 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 1e6bc14935..8c4bd16ae3 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -102,11 +102,10 @@ type 'a const_entry_body = 'a proof_output Future.computation (** Dummy wrapper type discriminable from unit *) type 'a seff_wrap = { seff_wrap : 'a } -type _ constant_entry = - | DefinitionEntry : definition_entry -> unit constant_entry - | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry - | ParameterEntry : parameter_entry -> unit constant_entry - | PrimitiveEntry : primitive_entry -> unit constant_entry +type constant_entry = + | DefinitionEntry : definition_entry -> constant_entry + | ParameterEntry : parameter_entry -> constant_entry + | PrimitiveEntry : primitive_entry -> constant_entry (** {6 Modules } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4dbc009324..43aafac809 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -299,13 +299,6 @@ let lift_constant c = in { c with const_body = body } -let map_constant f c = - let body = match c.const_body with - | OpaqueDef o -> OpaqueDef (f o) - | Def _ | Undef _ | Primitive _ as body -> body - in - { c with const_body = body } - let push_private_constants env eff = let eff = side_effects_of_private_constants eff in let add_if_undefined env eff = @@ -585,7 +578,8 @@ type 'a effect_entry = | PureEntry : unit effect_entry type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration type exported_private_constant = Constant.t @@ -765,17 +759,14 @@ let export_side_effects mb env (b_ctx, eff) = if Int.equal sl 0 then let env, cb = let kn = eff.seff_constant in - let ce = constant_entry_of_side_effect eff in - let open Entries in - let cb = match ce with - | DefinitionEff ce -> + let ce = constant_entry_of_side_effect eff in + let open Entries in + let cb = match ce with + | DefinitionEff ce -> Term_typing.translate_constant env kn (DefinitionEntry ce) - | OpaqueEff ce -> - Term_typing.translate_constant env kn (OpaqueEntry ce) - in - let map ctx = match ce with - | OpaqueEff e -> - let body = Future.force e.Entries.opaque_entry_body in + | OpaqueEff ce -> + let cb, ctx = Term_typing.translate_opaque env kn ce in + let body = Future.force ce.Entries.opaque_entry_body in let handle _env c () = (c, Univ.ContextSet.empty, 0) in let (c, u) = Term_typing.check_delayed handle ctx body in let () = match u with @@ -783,10 +774,8 @@ let export_side_effects mb env (b_ctx, eff) = | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) in - c - | _ -> assert false + { cb with const_body = OpaqueDef c } in - let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) in @@ -826,23 +815,18 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan let kn = Constant.make2 senv.modpath l in let cb = match decl with - | ConstantEntry (EffectEntry, Entries.OpaqueEntry e) -> + | OpaqueEntry ce -> let handle env body eff = let body, uctx, signatures = inline_side_effects env body eff in let trusted = check_signatures senv.revstruct signatures in body, uctx, trusted in - let cb = Term_typing.translate_constant senv.env kn (Entries.OpaqueEntry e) in - let ctx = match cb.const_body with - | OpaqueDef ctx -> ctx - | _ -> assert false - in + let cb, ctx = Term_typing.translate_opaque senv.env kn ce in let map pf = Term_typing.check_delayed handle ctx pf in - let pf = Future.chain e.Entries.opaque_entry_body map in + let pf = Future.chain ce.Entries.opaque_entry_body map in { cb with const_body = OpaqueDef pf } - | ConstantEntry (PureEntry, ce) -> - let cb = Term_typing.translate_constant senv.env kn ce in - map_constant (fun _ -> assert false) cb + | ConstantEntry ce -> + Term_typing.translate_constant senv.env kn ce in let senv = let senv, cb, delayed_cst = match cb.const_body with @@ -870,7 +854,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan let senv = match decl with - | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> + | ConstantEntry (Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ }) -> if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1b55293f1c..6e5c9c55ae 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -78,7 +78,8 @@ type 'a effect_entry = | PureEntry : unit effect_entry type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration type exported_private_constant = Constant.t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1e0db8026f..f85b3db413 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -64,7 +64,7 @@ type typing_context = | MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option | PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option -let infer_declaration (type a) env (dcl : a constant_entry) = +let infer_declaration env (dcl : constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -112,47 +112,6 @@ let infer_declaration (type a) env (dcl : a constant_entry) = cook_relevance = Sorts.Relevant; } - (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, - so we delay the typing and hash consing of its body. *) - - | OpaqueEntry ({ opaque_entry_type = typ; - opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> - let env = push_context_set ~strict:true univs env in - let { opaque_entry_feedback = feedback_id; _ } = c in - let tyj = Typeops.infer_type env typ in - let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in - let def = OpaqueDef context in - { - Cooking.cook_body = def; - cook_type = tyj.utj_val; - cook_universes = Monomorphic univs; - cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = false; - cook_context = Some c.opaque_entry_secctx; - } - - (** Similar case for polymorphic entries. *) - - | OpaqueEntry ({ opaque_entry_type = typ; - opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let { opaque_entry_feedback = feedback_id; _ } = c in - let env = push_context ~strict:false uctx env in - let tj = Typeops.infer_type env typ in - let sbst, auctx = Univ.abstract_universes nas uctx in - let usubst = Univ.make_instance_subst sbst in - let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in - let def = OpaqueDef context in - let typ = Vars.subst_univs_level_constr usubst tj.utj_val in - { - Cooking.cook_body = def; - cook_type = typ; - cook_universes = Polymorphic auctx; - cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = false; - cook_context = Some c.opaque_entry_secctx; - } - - (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in @@ -189,6 +148,43 @@ let infer_declaration (type a) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } +(** Definition is opaque (Qed), so we delay the typing of its body. *) +let infer_opaque env = function + | ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> + let env = push_context_set ~strict:true univs env in + let { opaque_entry_feedback = feedback_id; _ } = c in + let tyj = Typeops.infer_type env typ in + let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef () in + { + Cooking.cook_body = def; + cook_type = tyj.utj_val; + cook_universes = Monomorphic univs; + cook_relevance = Sorts.relevance_of_sort tyj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + }, context + + | ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { opaque_entry_feedback = feedback_id; _ } = c in + let env = push_context ~strict:false uctx env in + let tj = Typeops.infer_type env typ in + let sbst, auctx = Univ.abstract_universes nas uctx in + let usubst = Univ.make_instance_subst sbst in + let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef () in + let typ = Vars.subst_univs_level_constr usubst tj.utj_val in + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + }, context + let check_section_variables env declared_set typ body = let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env body in @@ -297,6 +293,10 @@ let translate_constant env _kn ce = build_constant_declaration env (infer_declaration env ce) +let translate_opaque env _kn ce = + let def, ctx = infer_opaque env ce in + build_constant_declaration env def, ctx + let translate_local_assum env t = let j = Typeops.infer env t in let t = Typeops.assumption_of_judgment env j in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index f82312245b..c9f6d66e36 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,8 +30,12 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - env -> Constant.t -> 'a constant_entry -> - typing_context constant_body + env -> Constant.t -> constant_entry -> + 'a constant_body + +val translate_opaque : + env -> Constant.t -> 'a opaque_entry -> + unit constant_body * typing_context val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body @@ -40,7 +44,7 @@ val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (C (** Internal functions, mentioned here for debug purpose only *) val infer_declaration : env -> - 'a constant_entry -> typing_context Cooking.result + constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |