From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 13:38:22 +0200 Subject: More precise type for universe entries. We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure. --- API/API.mli | 6 ++++-- interp/declare.ml | 17 ++++++++++++++--- kernel/entries.ml | 7 +++++-- kernel/safe_typing.ml | 10 +++++----- kernel/term_typing.ml | 30 +++++++++++++++++++----------- kernel/term_typing.mli | 2 +- proofs/proof_global.ml | 6 +++++- tactics/ind_tables.ml | 8 ++++++-- tactics/tactics.ml | 8 +++++--- vernac/indschemes.ml | 8 ++++++-- vernac/obligations.ml | 4 ++-- vernac/record.ml | 7 +++++-- 12 files changed, 77 insertions(+), 36 deletions(-) diff --git a/API/API.mli b/API/API.mli index bb24d5768f..4d9904b5f5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1345,6 +1345,9 @@ sig type inline = int option type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation + type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1352,8 +1355,7 @@ sig (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : Constr.types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.UContext.t; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline diff --git a/interp/declare.ml b/interp/declare.ml index 154793a32d..f95d025e42 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -63,8 +63,12 @@ let cache_variable ((sp,_),o) = impl, true, poly, ctx | SectionLocalDef (de) -> let univs = Global.push_named_def (id,de) in + let poly = match de.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in Explicit, de.const_entry_opaque, - de.const_entry_polymorphic, univs in + poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; @@ -237,22 +241,29 @@ let declare_constant_common id cst = let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + let univs = + if poly then Polymorphic_const_entry univs + else Monomorphic_const_entry univs + in { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; - const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; const_entry_inline_code = inline} let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = + let is_poly de = match de.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in let export = (* We deal with side effects *) match cd with | DefinitionEntry de when export_seff || not de.const_entry_opaque || - de.const_entry_polymorphic -> + is_poly de -> let bo = de.const_entry_body in let _, seff = Future.force bo in Safe_typing.empty_private_constants <> seff diff --git a/kernel/entries.ml b/kernel/entries.ml index 3fa25c142a..a1ccbdbc1b 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -64,6 +64,10 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation +type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context + type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -71,8 +75,7 @@ type 'a definition_entry = { (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.universe_context; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ed4c7d57ad..074122b03f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,12 +382,12 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c,typ,univs = - match Term_typing.translate_local_def senv.revstruct senv.env id de with - | c, typ, Monomorphic_const ctx -> c, typ, ctx - | _, _, Polymorphic_const _ -> assert false + let open Entries in + let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in + let poly = match de.Entries.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true in - let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with | Def c -> Mod_subst.force_constr c, univs diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cf82d54ec1..9102234657 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -251,8 +251,8 @@ let infer_declaration ~trust env kn dcl = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_polymorphic = false} as c) -> - let env = push_context ~strict:true c.const_entry_universes env in + const_entry_universes = Monomorphic_const_entry univs } as c) -> + let env = push_context ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -271,7 +271,7 @@ let infer_declaration ~trust env kn dcl = c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, - (Monomorphic_const c.const_entry_universes), + (Monomorphic_const univs), c.const_entry_inline_code, c.const_entry_secctx (** Other definitions have to be processed immediately. *) @@ -279,18 +279,22 @@ let infer_declaration ~trust env kn dcl = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let univsctx = Univ.ContextSet.of_context c.const_entry_universes in + let poly, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> false, univs + | 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 env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in - let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let env = push_context_set ~strict:(not poly) ctx env in + let abstract = poly && not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in let typ = match typ with | None -> - if not c.const_entry_polymorphic then (* Old-style polymorphism *) + if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) | Some t -> @@ -461,11 +465,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = - let poly, univs = + let univs = match cb.const_universes with - | Monomorphic_const ctx -> false, ctx + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx | Polymorphic_const auctx -> - true, Univ.AUContext.repr auctx + Polymorphic_const_entry (Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -478,7 +483,6 @@ let constant_entry_of_side_effect cb u = const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } @@ -592,6 +596,10 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; + let univs = match univs with + | Monomorphic_const ctx -> ctx + | Polymorphic_const _ -> assert false + in def, typ, univs (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 77d126074f..29c9918373 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -15,7 +15,7 @@ open Entries type side_effects val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes + constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 52d6787d44..2ade797f63 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in + let univs = + if poly then Entries.Polymorphic_const_entry univs + else Entries.Monomorphic_const_entry univs + in { Entries. const_entry_body = body; const_entry_secctx = section_vars; @@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_inline_code = false; const_entry_opaque = true; const_entry_universes = univs; - const_entry_polymorphic = poly}) + }) fpl initial_goals in let binders = Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 0407c1e36a..7f087ea01a 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -123,14 +123,18 @@ let define internal id c p univs = let ctx = Evd.normalize_evar_universe_context univs in let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let univs = Evd.evar_context_universe_context ctx in + let univs = + if p then Polymorphic_const_entry univs + else Monomorphic_const_entry univs + in let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = None; - const_entry_polymorphic = p; - const_entry_universes = Evd.evar_context_universe_context ctx; + const_entry_universes = univs; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8a95ad177d..cb905e749a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5004,8 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = in let cst = Impargs.with_implicit_protection cst () in let lem = - if const.Entries.const_entry_polymorphic then - let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in + match const.Entries.const_entry_universes with + | Entries.Polymorphic_const_entry uctx -> + let uctx = Univ.ContextSet.of_context uctx in (** Hack: the kernel may generate definitions whose universe variables are not the same as requested in the entry because of constraints delayed in the body, even in polymorphic mode. We mimick what it does for now @@ -5014,7 +5015,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in let u = Univ.UContext.instance uctx in mkConstU (cst, EInstance.make u) - else mkConst cst + | Entries.Monomorphic_const_entry _ -> + mkConst cst in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 3d97a767c8..6ea8bc7f2c 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,13 +109,17 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in + let _, univs = Evd.universe_context ctx in + let univs = + if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs + else Monomorphic_const_entry univs + in let kn = f id (DefinitionEntry { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_polymorphic = Flags.is_universe_polymorphism (); - const_entry_universes = snd (Evd.universe_context ctx); + const_entry_universes = univs; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 10d3317f8d..02067c190e 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -636,12 +636,12 @@ let declare_obligation prg obl body ty uctx = shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in + let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = ty; - const_entry_polymorphic = poly; - const_entry_universes = uctx; + const_entry_universes = univs; const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/vernac/record.ml b/vernac/record.ml index 63ca227862..a2e443e5f7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -322,13 +322,16 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try + let univs = + if poly then Polymorphic_const_entry ctx + else Monomorphic_const_entry ctx + in let entry = { const_entry_body = Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_polymorphic = poly; - const_entry_universes = ctx; + const_entry_universes = univs; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in -- cgit v1.2.3 From 9961577dfbb93f0b691c355ba99822665def037f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 17:00:48 +0200 Subject: Using a record type for Cooking.result. --- kernel/cooking.ml | 22 +++++++++++----- kernel/cooking.mli | 11 +++++--- kernel/term_typing.ml | 71 ++++++++++++++++++++++++++++++++++++--------------- 3 files changed, 74 insertions(+), 30 deletions(-) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 95822fac68..63614e20f7 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -151,9 +151,14 @@ let abstract_constant_body = type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - constant_universes * inline * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : constant_type; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : Context.Named.t option; +} let on_body ml hy f = function | Undef _ as x -> x @@ -254,9 +259,14 @@ let cook_constant ~hcons env { from = cb; info } = | Polymorphic_const auctx -> Polymorphic_const (AUContext.union abs_ctx auctx) in - (body, typ, Option.map projection cb.const_proj, - univs, cb.const_inline_code, - Some const_hyps) + { + cook_body = body; + cook_type = typ; + cook_proj = Option.map projection cb.const_proj; + cook_universes = univs; + cook_inline = cb.const_inline_code; + cook_context = Some const_hyps; + } (* let cook_constant_key = Profile.declare_profile "cook_constant" *) (* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 79a028d760..f386fd9362 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,9 +16,14 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - constant_universes * inline * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : constant_type; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : Context.Named.t option; +} val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9102234657..c809e4791c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -243,7 +243,14 @@ let infer_declaration ~trust env kn dcl = in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, univs, false, ctx + { + Cooking.cook_body = Undef nl; + cook_type = RegularArity t; + cook_proj = None; + cook_universes = univs; + cook_inline = false; + cook_context = ctx; + } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -270,9 +277,14 @@ let infer_declaration ~trust env kn dcl = feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, - (Monomorphic_const univs), - c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = RegularArity typ; + cook_proj = None; + cook_universes = Monomorphic_const univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> @@ -308,7 +320,14 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -328,8 +347,14 @@ let infer_declaration ~trust env kn dcl = Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) in let term, typ = pb.proj_eta in - Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - univs, false, None + { + Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term)); + cook_type = RegularArity typ; + cook_proj = Some pb; + cook_universes = univs; + cook_inline = false; + cook_context = None; + } let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -353,7 +378,9 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = +let build_constant_declaration kn env result = + let open Cooking in + let typ = result.cook_type in let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -380,7 +407,8 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in - match ctx with + let def = result.cook_body in + match result.cook_context with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -423,9 +451,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in + let univs = result.cook_universes in let tps = let res = - match proj with + match result.cook_proj with | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because @@ -438,10 +467,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = None; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env; } in @@ -452,10 +481,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } (*s Global and local constant declaration. *) @@ -579,11 +608,11 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,univs,inline_code,ctx = - infer_declaration ~trust:mb env None (DefinitionEntry centry) in - let typ = type_of_constant_type env typ in - if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin - match def with + let open Cooking in + let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let typ = type_of_constant_type env decl.cook_type in + if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin + match decl.cook_body with | Undef _ -> () | Def _ -> () | OpaqueDef lc -> @@ -596,11 +625,11 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; - let univs = match univs with + let univs = match decl.cook_universes with | Monomorphic_const ctx -> ctx | Polymorphic_const _ -> assert false in - def, typ, univs + decl.cook_body, typ, univs (* Insertion of inductive types. *) -- cgit v1.2.3 From 3c6679676c3963b7c3ec7c1eadbf24ae70311408 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 15:43:40 +0200 Subject: More precise type of entries capturing their lack of side-effects. We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants. --- interp/declare.ml | 6 +++--- kernel/safe_typing.ml | 22 +++++++++++++++------- kernel/safe_typing.mli | 9 ++++++--- kernel/term_typing.ml | 45 ++++++++++++++++++++++++++++++--------------- kernel/term_typing.mli | 18 +++++++++++------- 5 files changed, 65 insertions(+), 35 deletions(-) diff --git a/interp/declare.ml b/interp/declare.ml index f95d025e42..8cafb5f3a6 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 074122b03f..6dbc223952 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 5bb8ceb1a5..2a454400fd 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 c809e4791c..03bd8426fe 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 29c9918373..082ed7ed0d 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 -- cgit v1.2.3 From 3fcf0930874d7200f2503ac7084b1d6669d59540 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Jul 2017 17:46:15 +0200 Subject: Remove a horrendous hack in Declare to retrieve exported side-effects. Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment. --- interp/declare.ml | 80 ++++++++++++++++++++++++-------------------------- kernel/safe_typing.ml | 26 +++++++--------- kernel/safe_typing.mli | 8 +++-- library/global.ml | 1 + library/global.mli | 7 +++-- 5 files changed, 61 insertions(+), 61 deletions(-) diff --git a/interp/declare.ml b/interp/declare.ml index 8cafb5f3a6..d82b8f2158 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -106,10 +106,7 @@ type constant_obj = { cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; - mutable cst_exported : Safe_typing.exported_private_constant list; - (* mutable: to avoid change the libobject API, since cache_function - * does not return an updated object *) - mutable cst_was_seff : bool + cst_was_seff : bool; } type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind @@ -150,15 +147,13 @@ let cache_constant ((sp,kn), obj) = let _,dir,_ = repr_kn kn in let kn' = if obj.cst_was_seff then begin - obj.cst_was_seff <- false; if Global.exists_objlabel (Label.of_id (basename sp)) then constant_of_kn kn else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") end else let () = check_exists sp in - let kn', exported = Global.add_constant dir id obj.cst_decl in - obj.cst_exported <- exported; - kn' in + Global.add_constant dir id obj.cst_decl + in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in @@ -179,7 +174,7 @@ let discharge_constant ((sp, kn), obj) = let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } + Some { obj with cst_was_seff = false; cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = @@ -191,14 +186,13 @@ let dummy_constant cst = { cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; - cst_exported = []; - cst_was_seff = cst.cst_was_seff; + cst_was_seff = false; } let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = - declare_object_full { (default_object "CONSTANT") with +let (inConstant : constant_obj -> obj) = + declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -209,31 +203,14 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f +let update_tables c = + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) + let declare_constant_common id cst = - let update_tables c = -(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) - declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c) in let o = inConstant cst in let _, kn as oname = add_leaf id o in - List.iter (fun (c,ce,role) -> - (* handling of private_constants just exported *) - let o = inConstant { - cst_decl = ConstantEntry (PureEntry, ce); - cst_hyps = [] ; - cst_kind = IsProof Theorem; - cst_locl = false; - cst_exported = []; - cst_was_seff = true; } in - let id = Label.to_id (pi3 (Constant.repr3 c)) in - ignore(add_leaf id o); - update_tables c; - let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in - match role with - | Safe_typing.Subproof -> () - | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) - (outConstant o).cst_exported; pull_to_head oname; let c = Global.constant_of_delta_kn kn in update_tables c; @@ -258,23 +235,42 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true in - let export = (* We deal with side effects *) + let in_section = Lib.sections_are_opened () in + let export, decl = (* We deal with side effects *) match cd with | DefinitionEntry de when export_seff || not de.const_entry_opaque || is_poly de -> - let bo = de.const_entry_body in - let _, seff = Future.force bo in - Safe_typing.empty_private_constants <> seff - | _ -> false + (** This globally defines the side-effects in the environment. We mark + exported constants as being side-effect not to redeclare them at + caching time. *) + let cd, export = Global.export_private_constants ~in_section cd in + export, ConstantEntry (PureEntry, cd) + | _ -> [], ConstantEntry (EffectEntry, cd) + in + let iter_eff (c, cd, role) = + let o = inConstant { + cst_decl = ConstantEntry (PureEntry, cd); + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + cst_was_seff = true + } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] in + let () = List.iter iter_eff export in let cst = { - cst_decl = ConstantEntry (EffectEntry export,cd); + cst_decl = decl; cst_hyps = [] ; cst_kind = kind; cst_locl = local; - cst_exported = []; cst_was_seff = false; } in let kn = declare_constant_common id cst in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6dbc223952..ccd6e9cf97 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -494,11 +494,10 @@ 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 +| EffectEntry : private_constants effect_entry | PureEntry : unit effect_entry type global_declaration = - (* bool: export private constants *) | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe @@ -527,24 +526,21 @@ let add_constant_aux no_section senv (kn, cb) = in senv'' +let export_private_constants ~in_section ce senv = + let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in + let bodies = List.map (fun (kn, cb, _, _) -> (kn, cb)) exported in + let exported = List.map (fun (kn, _, ce, r) -> (kn, ce, r)) exported in + let no_section = not in_section in + let senv = List.fold_left (add_constant_aux no_section) senv bodies in + (ce, exported), senv + let add_constant dir l decl senv = let kn = make_con senv.modpath dir l in let no_section = DirPath.is_empty dir in - let seff_to_export, decl = - match decl with - | ConstantEntry (EffectEntry true, ce) -> - let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (PureEntry, ce) - | _ -> [], decl - in - let senv = - List.fold_left (add_constant_aux no_section) senv - (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in let senv = let cb = match decl with - | ConstantEntry (EffectEntry _, 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 @@ -552,7 +548,7 @@ let add_constant dir l decl senv = let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in add_constant_aux no_section senv (kn, cb) in - (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv + kn, senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2a454400fd..7152261078 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -95,7 +95,7 @@ val push_named_def : (** Insertion of global axioms or definitions *) type 'a effect_entry = -| EffectEntry : bool -> private_constants effect_entry (* bool: export private constants *) +| EffectEntry : private_constants effect_entry | PureEntry : unit effect_entry type global_declaration = @@ -105,11 +105,15 @@ type global_declaration = type exported_private_constant = constant * unit Entries.constant_entry * 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 + (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) val add_constant : DirPath.t -> Label.t -> global_declaration -> - (constant * exported_private_constant list) safe_transformer + constant safe_transformer (** Adding an inductive type *) diff --git a/library/global.ml b/library/global.ml index 5b17855dce..00a3a49862 100644 --- a/library/global.ml +++ b/library/global.ml @@ -86,6 +86,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index 48bcfa989f..c777691d11 100644 --- a/library/global.mli +++ b/library/global.mli @@ -34,9 +34,12 @@ val set_typing_flags : Declarations.typing_flags -> unit val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set +val export_private_constants : in_section:bool -> + Safe_typing.private_constants Entries.constant_entry -> + unit Entries.constant_entry * Safe_typing.exported_private_constant list + val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> - constant * Safe_typing.exported_private_constant list + DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive -- cgit v1.2.3 From ce830b204ad52f8b3655d2cb4672662120d83101 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Jul 2017 00:05:03 +0200 Subject: Further simplication: do not recreate entries for side-effects. This is actually useless, the code does not depend on the value of the entry for side-effects. --- interp/declare.ml | 29 ++++++++++++----------------- kernel/safe_typing.ml | 6 +++--- kernel/safe_typing.mli | 2 +- kernel/term_typing.ml | 6 +++--- kernel/term_typing.mli | 5 +---- 5 files changed, 20 insertions(+), 28 deletions(-) diff --git a/interp/declare.ml b/interp/declare.ml index d82b8f2158..70f422b514 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -102,11 +102,12 @@ let declare_variable id obj = (** Declaration of constants and parameters *) type constant_obj = { - cst_decl : global_declaration; + cst_decl : global_declaration option; + (** [None] when the declaration is a side-effect and has already been defined + in the global environment. *) cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; - cst_was_seff : bool; } type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind @@ -146,13 +147,14 @@ let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in let kn' = - if obj.cst_was_seff then begin + match obj.cst_decl with + | None -> if Global.exists_objlabel (Label.of_id (basename sp)) then constant_of_kn kn else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") - end else + | Some decl -> let () = check_exists sp in - Global.add_constant dir id obj.cst_decl + Global.add_constant dir id decl in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); @@ -174,19 +176,14 @@ let discharge_constant ((sp, kn), obj) = let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_was_seff = false; cst_hyps = new_hyps; cst_decl = new_decl; } + Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = - ConstantEntry - (PureEntry, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) - let dummy_constant cst = { - cst_decl = dummy_constant_entry; + cst_decl = None; cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; - cst_was_seff = false; } let classify_constant cst = Substitute (dummy_constant cst) @@ -249,13 +246,12 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e export, ConstantEntry (PureEntry, cd) | _ -> [], ConstantEntry (EffectEntry, cd) in - let iter_eff (c, cd, role) = + let iter_eff (c, role) = let o = inConstant { - cst_decl = ConstantEntry (PureEntry, cd); + cst_decl = None; cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; - cst_was_seff = true } in let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); @@ -267,11 +263,10 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e in let () = List.iter iter_eff export in let cst = { - cst_decl = decl; + cst_decl = Some decl; cst_hyps = [] ; cst_kind = kind; cst_locl = local; - cst_was_seff = false; } in let kn = declare_constant_common id cst in let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ccd6e9cf97..04051f2e23 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -502,7 +502,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * unit Entries.constant_entry * private_constant_role + constant * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -528,8 +528,8 @@ let add_constant_aux no_section senv (kn, cb) = let export_private_constants ~in_section ce senv = let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in - let bodies = List.map (fun (kn, cb, _, _) -> (kn, cb)) exported in - let exported = List.map (fun (kn, _, ce, r) -> (kn, ce, r)) exported in + let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in + let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let no_section = not in_section in let senv = List.fold_left (add_constant_aux no_section) senv bodies in (ce, exported), senv diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 7152261078..148fdca678 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -103,7 +103,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * unit Entries.constant_entry * private_constant_role + constant * private_constant_role val export_private_constants : in_section:bool -> private_constants Entries.constant_entry -> diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 03bd8426fe..23c5b6f58e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -544,7 +544,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * side_effect_role let export_side_effects mb env ce = match ce with @@ -596,7 +596,7 @@ let export_side_effects mb env ce = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env | Some sl, cbs :: rest -> @@ -604,7 +604,7 @@ let export_side_effects mb env ce = let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, constant_entry_of_side_effect cb u, r) cbs in + kn, cb, r) cbs in translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env in translate_seff trusted seff [] env diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 082ed7ed0d..5914c4a954 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -55,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * 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 @@ -65,9 +65,6 @@ val export_side_effects : structure_body -> env -> side_effects constant_entry -> exported_side_effect list * unit constant_entry -val constant_entry_of_side_effect : - constant_body -> seff_env -> unit constant_entry - val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body -- cgit v1.2.3 From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 18 Jul 2017 18:16:43 +0200 Subject: Statically ensuring that inlined entries out of the kernel have no effects. This was an easy to prove property that I somehow overlooked. --- kernel/safe_typing.mli | 2 +- kernel/term_typing.ml | 2 +- kernel/term_typing.mli | 2 +- proofs/pfedit.ml | 5 ++--- vernac/obligations.ml | 6 ++---- 5 files changed, 7 insertions(+), 10 deletions(-) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 148fdca678..752fdd793e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : Environ.env -> Constr.constr -> private_constants -> Constr.constr val inline_private_constants_in_definition_entry : - Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry val universes_of_private : private_constants -> Univ.universe_context_set list diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 23c5b6f58e..ed53df01f1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -654,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), empty_seff); + (body, ctx'), ()); } let inline_side_effects env body side_eff = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 5914c4a954..24153343e7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr redexes. *) val inline_entry_side_effects : - env -> side_effects definition_entry -> side_effects definition_entry + env -> side_effects definition_entry -> unit definition_entry (** Same as {!inline_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a949c8e911..1937885587 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body - (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in - let (cb, ctx), se = Future.force ce.const_entry_body in + (fun (pt, _) -> pt, ()) } in + let (cb, ctx), () = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Safe_typing.empty_private_constants = se); cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 02067c190e..28aeaa725e 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx = id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, eff = Future.force entry.const_entry_body in - assert(Safe_typing.empty_private_constants = eff); + let body, () = Future.force entry.const_entry_body in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' @@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf = let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in - let (body, cstr), eff = Future.force entry.Entries.const_entry_body in - assert(Safe_typing.empty_private_constants = eff); + let (body, cstr), () = Future.force entry.Entries.const_entry_body in let sigma = Evd.from_ctx (fst uctx) in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) body; -- cgit v1.2.3 From 906b48ff401f22be6059a6cdde8723b858102690 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Jul 2017 14:05:52 +0200 Subject: Avoiding a variable shadowing in the kernel. This ought to ease the understanding of the code. --- kernel/term_typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ed53df01f1..43c099712a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -274,9 +274,9 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let j = infer env body in let _ = judge_of_cast env j DEFAULTcast tyj in j, uctx - | SideEffects trust -> + | SideEffects mb -> let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in + let valid_signatures = check_signatures mb 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 -- cgit v1.2.3