Module Safe_typing

type vodigest =
| Dvo_or_vi of Stdlib.Digest.t
| Dvivo of Stdlib.Digest.t * Stdlib.Digest.t
val digest_match : actual:vodigest -> required:vodigest -> bool
Safe environments

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.

type safe_environment
type section_data
val empty_environment : safe_environment
val is_initial : safe_environment -> bool
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

The safe_environment state monad

type safe_transformer0 = safe_environment -> safe_environment
type 'a safe_transformer = safe_environment -> 'a * safe_environment
Stm machinery
type private_constants
val empty_private_constants : private_constants
val is_empty_private_constants : private_constants -> bool

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 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 global_declaration =
| ConstantEntry : Entries.constant_entry -> global_declaration
| OpaqueEntry : unit Entries.opaque_entry -> global_declaration
type side_effect_declaration =
| DefinitionEff : Entries.definition_entry -> side_effect_declaration
| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
type exported_opaque
type exported_private_constant = Names.Constant.t * exported_opaque option
val export_private_constants : private_constants -> exported_private_constant list safe_transformer

returns the main constant

Similar to add_constant but also returns a certificate

Delayed proofs
type opaque_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.

Check that the provided proof is correct for the corresponding handle. This does not modify the environment. Call fill_opaque below for that.

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.

Get the proof term that was checked by the kernel.

Inductive blocks

Adding an inductive type

Adding a module or a module type

Adding universe constraints

val push_context_set : strict:bool -> Univ.ContextSet.t -> safe_transformer0
val add_constraints : Univ.Constraints.t -> safe_transformer0
val set_impredicative_set : bool -> safe_transformer0

Setting the type theory flavor

val set_indices_matter : bool -> safe_transformer0
val set_share_reduction : bool -> 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
Interactive section functions
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_section_context : Univ.UContext.t -> safe_transformer0

Add local universes to a polymorphic section

Interactive module functions
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

val allow_delayed_constants : bool Stdlib.ref

Traditional mode: check at end of module that no future was created.

The optional result type is given without its functorial part

val current_modpath : safe_environment -> Names.ModPath.t
val current_dirpath : safe_environment -> Names.DirPath.t
Libraries : loading and saving compilation units
type compiled_library
val module_of_library : compiled_library -> Declarations.module_body
val univs_of_library : compiled_library -> Univ.ContextSet.t
Safe typing judgments
type judgment
val j_val : judgment -> Constr.constr
val j_type : judgment -> Constr.constr

The safe typing of a term returns a typing judgment.

Queries
val exists_objlabel : Names.Label.t -> safe_environment -> bool
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
Retroknowledge / Native compiler
val register_inline : Names.Constant.t -> safe_transformer0
val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> safe_transformer0