diff options
| -rw-r--r-- | kernel/safe_typing.ml | 10 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | tactics/declare.ml | 74 |
4 files changed, 47 insertions, 45 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e8adde2605..8db8a044a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -759,7 +759,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 @@ -776,7 +776,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 = @@ -805,8 +805,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 @@ -819,7 +819,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 e6f2fc4a5d..e472dfd5e5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -86,8 +86,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..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 body, export = Global.export_private_constants (body, 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 @@ -377,10 +381,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 eff = get_roles export eff in - let () = List.iter register_side_effect eff in + let ((body, uctx), eff) = Future.force de.proof_entry_body 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 |