diff options
-rw-r--r-- | interp/declare.ml | 6 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 22 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 9 | ||||
-rw-r--r-- | kernel/term_typing.ml | 45 | ||||
-rw-r--r-- | kernel/term_typing.mli | 18 |
5 files changed, 65 insertions, 35 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index f95d025e4..8cafb5f3a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -184,7 +184,7 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry - (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) + (PureEntry, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -220,7 +220,7 @@ let declare_constant_common id cst = List.iter (fun (c,ce,role) -> (* handling of private_constants just exported *) let o = inConstant { - cst_decl = ConstantEntry (false, ce); + cst_decl = ConstantEntry (PureEntry, ce); cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; @@ -270,7 +270,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e | _ -> false in let cst = { - cst_decl = ConstantEntry (export,cd); + cst_decl = ConstantEntry (EffectEntry export,cd); cst_hyps = [] ; cst_kind = kind; cst_locl = local; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 074122b03..6dbc22395 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -383,7 +383,8 @@ 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.revstruct senv.env id de 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 @@ -492,12 +493,17 @@ let add_field ((l,sfb) as field) gn senv = let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) +type 'a effect_entry = +| EffectEntry : bool -> private_constants effect_entry +| PureEntry : unit effect_entry + type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + (* bool: export private constants *) + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + constant * unit Entries.constant_entry * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -526,10 +532,10 @@ let add_constant dir l decl senv = let no_section = DirPath.is_empty dir in let seff_to_export, decl = match decl with - | ConstantEntry (true, ce) -> + | ConstantEntry (EffectEntry true, ce) -> let exports, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) + exports, ConstantEntry (PureEntry, ce) | _ -> [], decl in let senv = @@ -538,8 +544,10 @@ let add_constant dir l decl senv = let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (EffectEntry _, ce) -> + Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce + | ConstantEntry (PureEntry, ce) -> + Term_typing.translate_constant Term_typing.Pure senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5bb8ceb1a..2a454400f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -94,13 +94,16 @@ val push_named_def : (** Insertion of global axioms or definitions *) +type 'a effect_entry = +| EffectEntry : bool -> private_constants effect_entry (* bool: export private constants *) +| PureEntry : unit effect_entry + type global_declaration = - (* bool: export private constants *) - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + constant * unit Entries.constant_entry * private_constant_role (** 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 c809e4791..03bd8426f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -77,6 +77,10 @@ end type side_effects = SideEffects.t +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + let uniq_seff_rev = SideEffects.repr let uniq_seff l = List.rev (SideEffects.repr l) @@ -232,7 +236,7 @@ let abstract_constant_universes abstract uctx = let sbst, auctx = Univ.abstract_universes uctx in sbst, Polymorphic_const auctx -let infer_declaration ~trust env kn dcl = +let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -264,15 +268,22 @@ let infer_declaration ~trust env kn dcl = let tyj = infer_type env typ in let proofterm = Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> - let body, uctx, signatures = - inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in - let env = push_context_set uctx env in - let j = + let j, uctx = match trust with + | Pure -> + let env = push_context_set uctx env in + let j = infer env body in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + | SideEffects trust -> + let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in + let valid_signatures = check_signatures trust signatures in + let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in - unzip ectx j in - let _ = judge_of_cast env j DEFAULTcast tyj in + let j = unzip ectx j in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + in let c = hcons_constr j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in @@ -296,8 +307,11 @@ let infer_declaration ~trust env kn dcl = | Polymorphic_const_entry univs -> true, univs in let univsctx = Univ.ContextSet.of_context univs in - let body, ctx, _ = inline_side_effects env body - (Univ.ContextSet.union univsctx ctx) side_eff in + let ctx = Univ.ContextSet.union univsctx ctx in + let body, ctx, _ = match trust with + | Pure -> body, ctx, [] + | SideEffects _ -> inline_side_effects env body ctx side_eff + in let env = push_context_set ~strict:(not poly) ctx env in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = @@ -507,7 +521,7 @@ let constant_entry_of_side_effect cb u = | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, empty_seff); + const_entry_body = Future.from_val (pt, ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = @@ -530,17 +544,18 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * unit constant_entry * side_effect_role let export_side_effects mb env ce = match ce with - | ParameterEntry _ | ProjectionEntry _ -> [], ce + | ParameterEntry e -> [], ParameterEntry e + | ProjectionEntry e -> [], ProjectionEntry e | DefinitionEntry c -> let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~pure:true body - (fun (b_ctx, _) -> b_ctx, empty_seff) } in + (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -580,7 +595,7 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in + let cb = translate_constant Pure env kn ce in (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 29c991837..082ed7ed0 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -14,7 +14,11 @@ open Entries type side_effects -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> +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.universe_context val translate_local_assum : env -> types -> types @@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + 'a trust -> env -> constant -> 'a constant_entry -> constant_body type side_effect_role = @@ -51,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * unit constant_entry * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -59,10 +63,10 @@ type exported_side_effect = * needs to be translated as usual after this step. *) val export_side_effects : structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * side_effects constant_entry + exported_side_effect list * unit constant_entry val constant_entry_of_side_effect : - constant_body -> seff_env -> side_effects constant_entry + constant_body -> seff_env -> unit constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -71,8 +75,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> - side_effects constant_entry -> Cooking.result +val infer_declaration : trust:'a trust -> env -> constant option -> + 'a constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body |