diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 59 |
1 files changed, 35 insertions, 24 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576..6a0ff072 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,19 +1,27 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term +open Constr open Environ open Declarations open Entries -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes +type side_effects + +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + +val translate_local_def : env -> Id.t -> section_def_entry -> + constr * types val translate_local_assum : env -> types -> types @@ -24,15 +32,24 @@ val inline_side_effects : env -> constr -> side_effects -> constr redexes. *) val inline_entry_side_effects : - env -> side_effects definition_entry -> side_effects definition_entry + 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 uniq_seff : side_effects -> side_effects +val empty_seff : side_effects +val add_seff : side_effect -> 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_effect list +(** Return the list of individual side-effects in the order of their + creation. *) + +val equal_eff : side_effect -> side_effect -> bool val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body type side_effect_role = @@ -40,31 +57,25 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + 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 constant_entry -> - exported_side_effect list * side_effects constant_entry - -val constant_entry_of_side_effect : - constant_body -> seff_env -> side_effects constant_entry + structure_body -> env -> side_effects definition_entry -> + exported_side_effect list * unit definition_entry val translate_mind : - env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body + env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body -val translate_recipe : env -> constant -> Cooking.recipe -> constant_body +val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> - side_effects constant_entry -> Cooking.result +val infer_declaration : trust:'a trust -> env -> + 'a constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body - -val set_suggest_proof_using : - (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit + Constant.t -> env -> Cooking.result -> constant_body |