From a7af2f6571d007b6f83a1ec9252b52f69907a965 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 30 Jan 2020 23:34:49 +0100 Subject: export_private_constants doesn't use the [constr in_univ_ctx] argument --- kernel/safe_typing.ml | 10 +++++----- kernel/safe_typing.mli | 4 ++-- library/global.mli | 4 ++-- tactics/declare.ml | 6 +++--- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f6f2058c13..2047fd5fc5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -757,7 +757,7 @@ let translate_direct_opaque env kn ce = let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } -let export_side_effects mb env (b_ctx, eff) = +let export_side_effects mb env eff = let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl @@ -774,7 +774,7 @@ let export_side_effects mb env (b_ctx, eff) = in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, b_ctx + | [] -> List.rev acc | eff :: rest -> if Int.equal sl 0 then let env, cb = @@ -803,8 +803,8 @@ let push_opaque_proof pf senv = let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in senv, o -let export_private_constants ce senv = - let exported, ce = export_side_effects senv.revstruct senv.env ce in +let export_private_constants eff senv = + let exported = export_side_effects senv.revstruct senv.env eff in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> let local = empty_private c.const_universes in @@ -817,7 +817,7 @@ let export_private_constants ce senv = let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) let senv = List.fold_left add_constant_aux senv bodies in - (ce, exported), senv + exported, senv let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 92bbd264fa..c879481c66 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -84,8 +84,8 @@ type side_effect_declaration = type exported_private_constant = Constant.t val export_private_constants : - private_constants Entries.proof_output -> - (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer + private_constants -> + exported_private_constant list safe_transformer (** returns the main constant *) val add_constant : diff --git a/library/global.mli b/library/global.mli index a38fde41a5..b6bd69c17c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -47,8 +47,8 @@ val push_named_def : (Id.t * Entries.section_def_entry) -> unit val push_section_context : (Name.t array * Univ.UContext.t) -> unit val export_private_constants : - Safe_typing.private_constants Entries.proof_output -> - Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list + Safe_typing.private_constants -> + Safe_typing.exported_private_constant list val add_constant : Id.t -> Safe_typing.global_declaration -> Constant.t diff --git a/tactics/declare.ml b/tactics/declare.ml index c7581fb0e0..e1d2ccc3eb 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -299,7 +299,7 @@ let define_constant ~name cd = if not de.proof_entry_opaque then (* This globally defines the side-effects in the environment. *) let body, eff = Future.force de.proof_entry_body in - let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in + let export = Global.export_private_constants eff.Evd.seff_private in let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in @@ -377,8 +377,8 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.proof_entry_body in - let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in + let ((body, uctx), eff) = Future.force de.proof_entry_body in + let export = Global.export_private_constants eff.Evd.seff_private in let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.proof_entry_universes with -- cgit v1.2.3 From c20fe3443f905dfea3ff746407cd1649ed8867ff Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 30 Jan 2020 23:40:08 +0100 Subject: Factorize export_private_constants + register_side_effect --- tactics/declare.ml | 72 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 37 insertions(+), 35 deletions(-) diff --git a/tactics/declare.ml b/tactics/declare.ml index e1d2ccc3eb..ce2f3ec2c5 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -160,6 +160,18 @@ let register_side_effect (c, role) = | None -> () | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let export_side_effects eff = + let export = Global.export_private_constants eff.Evd.seff_private in + let export = get_roles export eff in + List.iter register_side_effect export + let record_aux env s_ty s_bo = let open Environ in let in_ty = keep_hyps env s_ty in @@ -278,13 +290,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo opaque_entry_universes = univs; } -let get_roles export eff = - let map c = - let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in - (c, role) - in - List.map map export - let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = @@ -293,37 +298,36 @@ let is_unsafe_typing_flags () = let define_constant ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - let export, decl, unsafe = match cd with - | DefinitionEntry de -> - (* We deal with side effects *) - if not de.proof_entry_opaque then - (* This globally defines the side-effects in the environment. *) - let body, eff = Future.force de.proof_entry_body in - let export = Global.export_private_constants eff.Evd.seff_private in - let export = get_roles export eff in - let de = { de with proof_entry_body = Future.from_val (body, ()) } in - let cd = Entries.DefinitionEntry (cast_proof_entry de) in - export, ConstantEntry cd, false - else - let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.proof_entry_body map in - let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry EffectEntry de in - [], OpaqueEntry de, false - | ParameterEntry e -> - [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) - | PrimitiveEntry e -> - [], ConstantEntry (Entries.PrimitiveEntry e), false + let decl, unsafe = match cd with + | DefinitionEntry de -> + (* We deal with side effects *) + if not de.proof_entry_opaque then + let body, eff = Future.force de.proof_entry_body in + (* This globally defines the side-effects in the environment + and registers their libobjects. *) + let () = export_side_effects eff in + let de = { de with proof_entry_body = Future.from_val (body, ()) } in + let cd = Entries.DefinitionEntry (cast_proof_entry de) in + ConstantEntry cd, false + else + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.proof_entry_body map in + let de = { de with proof_entry_body = body } in + let de = cast_opaque_proof_entry EffectEntry de in + OpaqueEntry de, false + | ParameterEntry e -> + ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) + | PrimitiveEntry e -> + ConstantEntry (Entries.PrimitiveEntry e), false in let kn = Global.add_constant name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); - kn, export + kn let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = check_exists name in - let kn, export = define_constant ~name cd in - (* Register the libobjects attached to the constants and its subproofs *) - let () = List.iter register_side_effect export in + let kn = define_constant ~name cd in + (* Register the libobjects attached to the constants *) let () = register_constant kn kind local in kn @@ -378,9 +382,7 @@ let declare_variable ~name ~kind d = (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) let ((body, uctx), eff) = Future.force de.proof_entry_body in - let export = Global.export_private_constants eff.Evd.seff_private in - let eff = get_roles export eff in - let () = List.iter register_side_effect eff in + let () = export_side_effects eff in let poly, univs = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx -- cgit v1.2.3