diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 42 |
1 files changed, 8 insertions, 34 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ab25090b00..faf434c142 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -14,53 +14,27 @@ open Environ open Declarations open Entries -type side_effects +(** Handlers are used to manage side-effects. The ['a] type stands for the type + of side-effects, and it is parametric because they are only defined later + on. Handlers inline the provided side-effects into the term, and return + the set of additional global constraints that need to be added for the term + to be well typed. *) +type 'a effect_handler = + env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) type _ trust = | Pure : unit trust -| SideEffects : structure_body -> side_effects trust +| SideEffects : 'a effect_handler -> 'a trust val translate_local_def : env -> Id.t -> section_def_entry -> constr * types val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> side_effects proof_output - -val inline_side_effects : env -> constr -> side_effects -> constr -(** Returns the term where side effects have been turned into let-ins or beta - redexes. *) - -val inline_entry_side_effects : - env -> side_effects definition_entry -> unit definition_entry -(** Same as {!inline_side_effects} but applied to entries. Only modifies the - {!Entries.const_entry_body} field. It is meant to get a term out of a not - yet type checked proof. *) - -val empty_seff : side_effects -val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects -val concat_seff : side_effects -> side_effects -> side_effects -(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in - [e1] must be more recent than those of [e2]. *) -val uniq_seff : side_effects -> side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -type exported_side_effect = - Constant.t * constant_body * side_effect_role - -(* Given a constant entry containing side effects it exports them (either - * by re-checking them or trusting them). Returns the constant bodies to - * be pushed in the safe_env by safe typing. The main constant entry - * needs to be translated as usual after this step. *) -val export_side_effects : - structure_body -> env -> side_effects definition_entry -> - exported_side_effect list * unit definition_entry - val translate_mind : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body |