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. --- kernel/safe_typing.mli | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'kernel/safe_typing.mli') 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) *) -- 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. --- kernel/safe_typing.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'kernel/safe_typing.mli') 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 *) -- 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. --- kernel/safe_typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/safe_typing.mli') 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 -> -- 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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/safe_typing.mli') 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 -- cgit v1.2.3