(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * 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
type vodigest =
| Dvo_or_vi of Digest.t (* The digest of the seg_lib part *)
val digest_match : actual:vodigest -> required:vodigest -> bool
(** {6 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 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 -> Mod_declarations.structure_body
val flatten_env : safe_environment -> ModPath.t * Mod_declarations.structure_body
(** The safe_environment state monad *)
type safe_transformer0 = safe_environment -> safe_environment type'a safe_transformer = safe_environment -> 'a * safe_environment
(** {6 Stm machinery } *)
type private_constants
val debug_print_private_constants : private_constants -> Pp.t
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 constants_of_private : private_constants -> Constant.t list
val is_curmod_library : safe_environment -> bool
val is_joined_environment : safe_environment -> bool (** {6 Enriching a safe environment } *)
type exported_opaque type exported_private_constant = 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
(** returns the main constant *) val add_constant :
?typing_flags:Declarations.typing_flags ->
Label.t -> Entries.constant_entry -> Constant.t safe_transformer
(** Similar to add_constant but also returns a certificate *) val add_private_constant :
Label.t -> Univ.ContextSet.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer
(** {5 Delayed proofs} *)
(** 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. *) type 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 check_opaque : safe_environment -> Opaqueproof.opaque_handle ->
private_constants Entries.proof_output -> opaque_certificate
(** 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 fill_opaque : opaque_certificate -> safe_transformer0
(** Check whether a handle was filled. It assumes that the handle was introduced
in the opaque table and throws an anomaly otherwise. *) val is_filled_opaque : Opaqueproof.opaque_handle -> safe_environment -> bool
(** Get the proof term that was checked by the kernel. *) val repr_certificate : opaque_certificate ->
Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes
(** {5 Rewrite rules} *)
(** Add a rewrite rule corresponding to the equality witnessed by the constant. *) val add_rewrite_rules : Label.t -> Declarations.rewrite_rules_body -> safe_environment -> safe_environment
(** returns the number of module (type) parameters following the nested module
structure. The inner module (type) comes first in the list. *) val module_num_parameters : safe_environment -> int 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 module_is_modtype : safe_environment -> boollist
(** Traditional mode: check at end of module that no future was
created. *) val allow_delayed_constants : boolref
(** The optional result type is given without its functorial part *)
val end_module :
Label.t -> (Entries.module_struct_entry * Declarations.inline) option ->
(ModPath.t * MBId.t list * Mod_subst.delta_resolver) safe_transformer
val end_modtype : Label.t -> (ModPath.t * MBId.t list) safe_transformer
(** The safe typing of a term returns a typing judgment. *) val typing : safe_environment -> Constr.constr -> judgment
(** {6 Queries } *)
val exists_objlabel : Label.t -> safe_environment -> bool
val delta_of_senv : safe_environment -> Mod_subst.delta_resolver
val constant_of_delta_kn_senv : safe_environment -> KerName.t -> Constant.t val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t
(** {6 Retroknowledge / Native compiler } *)
val register_inline : Constant.t -> safe_transformer0 val register_inductive : inductive -> 'a CPrimitives.prim_ind -> safe_transformer0
val set_strategy : Conv_oracle.evaluable -> Conv_oracle.level -> safe_transformer0
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
