diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-14 15:43:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:33 +0200 |
| commit | 3c6679676c3963b7c3ec7c1eadbf24ae70311408 (patch) | |
| tree | 1de23a7b0802e899d2bf3d8f189f31f7f8e0f745 /kernel/safe_typing.mli | |
| parent | 9961577dfbb93f0b691c355ba99822665def037f (diff) | |
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.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5bb8ceb1a..2a454400f 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) *) |