diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 70 |
1 files changed, 32 insertions, 38 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 23a970b49..5f6697b4e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -9,15 +9,9 @@ (*i $Id$ i*) (*i*) -open Pp open Names open Term -open Univ -open Sign open Declarations -open Inductive -open Environ -open Typeops (*i*) (*s Safe environments. Since we are now able to type terms, we can define an @@ -27,50 +21,47 @@ open Typeops type safe_environment -val empty_environment : safe_environment +val env_of_safe_env : safe_environment -> Environ.env -val universes : safe_environment -> universes -val context : safe_environment -> context -val named_context : safe_environment -> named_context +val empty_environment : safe_environment +(* Adding and removing local declarations (Local or Variables) *) val push_named_assum : - identifier * constr -> safe_environment -> safe_environment + identifier * types -> safe_environment -> + Univ.constraints * safe_environment val push_named_def : - identifier * constr -> safe_environment -> safe_environment - -val check_and_push_named_assum : identifier * constr -> safe_environment -> - (constr option * types * constraints) * safe_environment -val check_and_push_named_def : - identifier * constr -> safe_environment -> - (constr option * types * constraints) * safe_environment + Univ.constraints * safe_environment +val pop_named_decls : identifier list -> safe_environment -> safe_environment -type local_names = (identifier * variable) list +(* Adding global axioms or definitions *) val add_parameter : - section_path -> constr -> local_names -> safe_environment -> safe_environment + section_path -> constr -> safe_environment -> safe_environment + +(*s Global and local constant declaration. *) + +type constant_entry = { + const_entry_body : constr; + const_entry_type : types option; + const_entry_opaque : bool } + val add_constant : - section_path -> constant_entry -> local_names -> - safe_environment -> safe_environment + section_path -> constant_entry -> safe_environment -> safe_environment val add_discharged_constant : - section_path -> Cooking.recipe -> local_names -> safe_environment -> safe_environment + section_path -> Cooking.recipe -> safe_environment -> safe_environment +(* Adding an inductive type *) val add_mind : - section_path -> mutual_inductive_entry -> local_names -> safe_environment - -> safe_environment -val add_constraints : constraints -> safe_environment -> safe_environment - -val pop_named_decls : identifier list -> safe_environment -> safe_environment - -val lookup_named : identifier -> safe_environment -> constr option * types -val lookup_constant : section_path -> safe_environment -> constant_body -val lookup_mind : section_path -> safe_environment -> mutual_inductive_body -val lookup_mind_specif : inductive -> safe_environment -> inductive_instance + section_path -> Indtypes.mutual_inductive_entry -> safe_environment -> + safe_environment -val export : safe_environment -> dir_path -> compiled_env -val import : compiled_env -> safe_environment -> safe_environment +(* Adding universe constraints *) +val add_constraints : Univ.constraints -> safe_environment -> safe_environment -val env_of_safe_env : safe_environment -> env +(* Loading and saving a module *) +val export : safe_environment -> dir_path -> Environ.compiled_env +val import : Environ.compiled_env -> safe_environment -> safe_environment (*s Typing judgments *) @@ -80,9 +71,12 @@ type judgment val j_val : judgment -> constr val j_type : judgment -> constr -val safe_infer : safe_environment -> constr -> judgment * constraints +(* Safe typing of a term returning a typing judgment and universe + constraints to be added to the environment for the judgment to + hold. It is guaranteed that the constraints are satisfiable + *) +val safe_infer : safe_environment -> constr -> judgment * Univ.constraints val typing : safe_environment -> constr -> judgment -val typing_in_unsafe_env : env -> constr -> judgment |