From 3ce18524834bb9ff7a9ea14c3f1659decb63af76 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 25 Jun 2019 11:54:54 +0200 Subject: Do not export side-effects of polymorphic definitions. This is the last call to the kernel that makes a difference between opaque definitions depending on their polymorphic status. --- tactics/declare.ml | 29 ++++++++++------------------- 1 file changed, 10 insertions(+), 19 deletions(-) (limited to 'tactics') diff --git a/tactics/declare.ml b/tactics/declare.ml index c0eae7503c..a37368550b 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -253,37 +253,28 @@ let get_roles export eff = let define_constant ~side_effect ~name cd = let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) - let is_poly de = match de.proof_entry_universes with - | Monomorphic_entry _ -> false - | Polymorphic_entry _ -> true - in let in_section = Lib.sections_are_opened () in - let export, decl = (* We deal with side effects *) - match cd with - | DefinitionEntry de when - not de.proof_entry_opaque || - is_poly de -> + let export, decl = 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 ~in_section (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 = match de.proof_entry_opaque with - | true -> Entries.OpaqueEntry (cast_opaque_proof_entry PureEntry de) - | false -> Entries.DefinitionEntry (cast_proof_entry de) - in + let cd = Entries.DefinitionEntry (cast_proof_entry de) in export, ConstantEntry (PureEntry, cd) - | DefinitionEntry de -> - let () = assert (de.proof_entry_opaque) in + 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 [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) - | ParameterEntry e -> - [], ConstantEntry (PureEntry, Entries.ParameterEntry e) - | PrimitiveEntry e -> - [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) + | ParameterEntry e -> + [], ConstantEntry (PureEntry, Entries.ParameterEntry e) + | PrimitiveEntry e -> + [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) in let kn, eff = Global.add_constant ~side_effect ~in_section name decl in kn, eff, export -- cgit v1.2.3 From 75de485c233dd7bbb6301b49e6702eee205977fb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 25 Jun 2019 12:00:02 +0200 Subject: Further cleanup following the removal of pure opaque definitions. We can statically enforce that opaque definitions are always impure by means of typing, leading to quite a few simplifications. --- tactics/declare.ml | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) (limited to 'tactics') diff --git a/tactics/declare.ml b/tactics/declare.ml index a37368550b..7ad86baa8d 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -205,7 +205,7 @@ let cast_proof_entry e = const_entry_inline_code = e.proof_entry_inline_code; } -let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Proof_global.proof_entry) = +let cast_opaque_proof_entry e = let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false @@ -220,14 +220,8 @@ let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Id.Set.empty, Id.Set.empty else let ids_typ = global_vars_set env typ in - let pf, env = match pure with - | PureEntry -> - let (pf, _), () = Future.force e.proof_entry_body in - pf, env - | EffectEntry -> - let (pf, _), eff = Future.force e.proof_entry_body in - pf, Safe_typing.push_private_constants env eff - in + let (pf, _), eff = Future.force e.proof_entry_body in + let env = Safe_typing.push_private_constants env eff in let vars = global_vars_set env pf in ids_typ, vars in @@ -269,7 +263,7 @@ let define_constant ~side_effect ~name cd = 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 + let de = cast_opaque_proof_entry de in [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) | ParameterEntry e -> [], ConstantEntry (PureEntry, Entries.ParameterEntry e) -- cgit v1.2.3 From d929838be77e30db04cd91201542bb52ed3ff7fd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 25 Jun 2019 20:57:50 +0200 Subject: Similar purity invariants in the kernel. --- tactics/declare.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/declare.ml b/tactics/declare.ml index 7ad86baa8d..b8ba62a5e5 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -289,7 +289,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind | None -> Cmap.empty | Some r -> Cmap.singleton kn r in - let eff = { Evd.seff_private = eff; Evd.seff_roles; } in + let eff = { Evd.seff_private = eff.Entries.seff_wrap; Evd.seff_roles; } in kn, eff (** Declaration of section variables and local definitions *) -- cgit v1.2.3