diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 62 |
1 files changed, 46 insertions, 16 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index c5e43e42a..b614a368c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -val sideff_of_con : safe_environment -> constant -> Declarations.side_effect -val sideff_of_scheme : - string -> safe_environment -> (inductive * constant) list -> - Declarations.side_effect +type private_constant +type private_constants + +type private_constant_role = + | Subproof + | Schema of inductive * string + +val side_effects_of_private_constants : + private_constants -> Entries.side_effects + +val empty_private_constants : private_constants +val add_private : private_constant -> private_constants -> private_constants +val concat_private : private_constants -> private_constants -> private_constants + +val private_con_of_con : safe_environment -> constant -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant + +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 + +val universes_of_private : private_constants -> Univ.universe_context_set list val is_curmod_library : safe_environment -> bool @@ -58,19 +78,30 @@ val is_joined_environment : safe_environment -> bool val push_named_assum : flags:Declarations.typing_flags -> - (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 + (Id.t * Term.types * bool (* polymorphic *)) + Univ.in_universe_context_set -> safe_transformer0 + +(** Returns the full universe context necessary to typecheck the definition + (futures are forced) *) val push_named_def : flags:Declarations.typing_flags -> - Id.t * Entries.definition_entry -> safe_transformer0 + Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry * Declarations.typing_flags + (* bool: export private constants *) + | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe +type exported_private_constant = + constant * private_constants 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) *) val add_constant : - DirPath.t -> Label.t -> global_declaration -> constant safe_transformer + DirPath.t -> Label.t -> global_declaration -> + (constant * exported_private_constant list) safe_transformer (** Adding an inductive type *) @@ -90,10 +121,10 @@ val add_modtype : (** Adding universe constraints *) val push_context_set : - Univ.universe_context_set -> safe_transformer0 + bool -> Univ.universe_context_set -> safe_transformer0 val push_context : - Univ.universe_context -> safe_transformer0 + bool -> Univ.universe_context -> safe_transformer0 val add_constraints : Univ.constraints -> safe_transformer0 @@ -101,12 +132,9 @@ val add_constraints : (* (\** Generator of universes *\) *) (* val next_universe : int safe_transformer *) -(** Setting the strongly constructive or classical logical engagement *) +(** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 -(** Collapsing the type hierarchy *) -val set_type_in_type : safe_transformer0 - (** {6 Interactive module functions } *) val start_module : Label.t -> module_path safe_transformer @@ -139,6 +167,8 @@ type compiled_library type native_library = Nativecode.global list +val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols + val start_library : DirPath.t -> module_path safe_transformer val export : @@ -148,7 +178,7 @@ val export : (* Constraints are non empty iff the file is a vi2vo *) val import : compiled_library -> Univ.universe_context_set -> vodigest -> - (module_path * Nativecode.symbol array) safe_transformer + module_path safe_transformer (** {6 Safe typing judgments } *) |