Safe_typing
Since we are now able to type terms, we can define an abstract type of safe environments, where objects are typed before being added.
We also provide functionality for modules : start_module
, end_module
, etc.
val empty_environment : safe_environment
val env_of_safe_env : safe_environment -> Environ.env
val sections_of_safe_env : safe_environment -> section_data Section.t option
val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
val flatten_env : safe_environment -> Names.ModPath.t * Declarations.structure_body
The safe_environment state monad
type safe_transformer0 = safe_environment -> safe_environment
type 'a safe_transformer = safe_environment -> 'a * safe_environment
val empty_private_constants : private_constants
val is_empty_private_constants : private_constants -> bool
val concat_private : private_constants -> private_constants -> private_constants
concat_private e1 e2
adds the constants of e1
to e2
, i.e. constants in e1
must be more recent than those of e2
.
val inline_private_constants : Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set
Abstract the private constants of a proof over the proof output
val push_private_constants : Environ.env -> private_constants -> Environ.env
Push the constants in the environment if not already there.
val universes_of_private : private_constants -> Univ.ContextSet.t
val is_curmod_library : safe_environment -> bool
val is_joined_environment : safe_environment -> bool
Enriching a safe environment
Insertion of global axioms or definitions
type side_effect_declaration =
| DefinitionEff : Entries.definition_entry -> side_effect_declaration |
| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration |
type exported_private_constant = Names.Constant.t * exported_opaque option
val repr_exported_opaque : exported_opaque -> Opaqueproof.opaque_handle * Opaqueproof.opaque_proofterm
val export_private_constants : private_constants -> exported_private_constant list safe_transformer
val add_constant : ?typing_flags:Declarations.typing_flags -> Names.Label.t -> Entries.constant_entry -> Names.Constant.t safe_transformer
returns the main constant
val add_private_constant : Names.Label.t -> Univ.ContextSet.t -> side_effect_declaration -> (Names.Constant.t * private_constants) safe_transformer
Similar to add_constant but also returns a certificate
Witness that a delayed Qed hole has a proof. This datatype is marshallable but care must be taken to marshal it at the same time as the environment it is referring to, since fill_opaque
relies on a shared pointer between the environment and the certificate.
val check_opaque : safe_environment -> Opaqueproof.opaque_handle -> private_constants Entries.proof_output -> opaque_certificate
Check that the provided proof is correct for the corresponding handle. This does not modify the environment. Call fill_opaque
below for that.
val fill_opaque : opaque_certificate -> safe_transformer0
Given an already checked proof for an opaque hole, actually fill it with the proof. This might fail if the current set of global universes is inconsistent with the one at the time of the call to check_opaque
. Precondition: the underlying handle must exist and must not have been filled.
val is_filled_opaque : Opaqueproof.opaque_handle -> safe_environment -> bool
Check whether a handle was filled. It assumes that the handle was introduced in the opaque table and throws an anomaly otherwise.
val repr_certificate : opaque_certificate -> Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes
Get the proof term that was checked by the kernel.
val add_rewrite_rules : Names.Label.t -> Declarations.rewrite_rules_body -> safe_environment -> safe_environment
Add a rewrite rule corresponding to the equality witnessed by the constant.
Adding an inductive type
val add_mind : ?typing_flags:Declarations.typing_flags -> Names.Label.t -> Entries.mutual_inductive_entry -> (Names.MutInd.t * IndTyping.NotPrimRecordReason.t option) safe_transformer
Adding a module or a module type
val add_module : Names.Label.t -> Entries.module_entry -> Declarations.inline -> (Names.ModPath.t * Mod_subst.delta_resolver) safe_transformer
val add_modtype : Names.Label.t -> Entries.module_type_entry -> Declarations.inline -> Names.ModPath.t safe_transformer
Adding universe constraints
val push_context_set : strict:bool -> Univ.ContextSet.t -> safe_transformer0
val add_constraints : Univ.Constraints.t -> safe_transformer0
val set_rewrite_rules_allowed : bool -> safe_transformer0
Setting the type theory flavor
val set_impredicative_set : bool -> safe_transformer0
val set_indices_matter : bool -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
val set_check_guarded : bool -> safe_transformer0
val set_check_positive : bool -> safe_transformer0
val set_check_universes : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
val set_allow_sprop : bool -> safe_transformer0
val open_section : safe_transformer0
val close_section : safe_transformer0
val sections_are_opened : safe_environment -> bool
Insertion of local declarations (Local or Variables)
val push_named_assum : (Names.Id.t * Constr.types) -> safe_transformer0
val push_named_def : (Names.Id.t * Entries.section_def_entry) -> safe_transformer0
val push_section_context : UVars.UContext.t -> safe_transformer0
Add local universes to a polymorphic section
val start_module : Names.Label.t -> Names.ModPath.t safe_transformer
val start_modtype : Names.Label.t -> Names.ModPath.t safe_transformer
val add_module_parameter : Names.MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer
val module_num_parameters : safe_environment -> int list
returns the number of module (type) parameters following the nested module structure. The inner module (type) comes first in the list.
val module_is_modtype : safe_environment -> bool list
returns true if the module is a module type following the nested module structure. The inner module (type) comes first in the list. true means a module type, false a regular module
Traditional mode: check at end of module that no future was created.
The optional result type is given without its functorial part
val end_module : Names.Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> (Names.ModPath.t * Names.MBId.t list * Mod_subst.delta_resolver) safe_transformer
val end_modtype : Names.Label.t -> (Names.ModPath.t * Names.MBId.t list) safe_transformer
val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer
val current_modpath : safe_environment -> Names.ModPath.t
val current_dirpath : safe_environment -> Names.DirPath.t
val module_of_library : compiled_library -> Declarations.module_body
val univs_of_library : compiled_library -> Univ.ContextSet.t
val check_flags_for_library : compiled_library -> safe_transformer0
val start_library : Names.DirPath.t -> Names.ModPath.t safe_transformer
val export : output_native_objects:bool -> safe_environment -> Names.DirPath.t -> Names.ModPath.t * compiled_library * Vmlibrary.compiled_library * Nativelib.native_library
val import : compiled_library -> Vmlibrary.on_disk -> vodigest -> Names.ModPath.t safe_transformer
type judgment = private {
jdg_env : safe_environment; |
jdg_val : Constr.constr; |
jdg_type : Constr.types; |
}
val typing : safe_environment -> Constr.constr -> judgment
The safe typing of a term returns a typing judgment.
val exists_objlabel : Names.Label.t -> safe_environment -> bool
val delta_of_senv : safe_environment -> Mod_subst.delta_resolver * Mod_subst.delta_resolver
val constant_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.Constant.t
val mind_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.MutInd.t
val register_inline : Names.Constant.t -> safe_transformer0
val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> safe_transformer0
val set_strategy : Conv_oracle.evaluable -> Conv_oracle.level -> safe_transformer0