Safe_typing (p.coq.8.14.0.doc.coq-core.kernel.Safe

Sourcetype vodigest =

| Dvo_or_vi of Digest.t
| Dvivo of Digest.t * Digest.t

Sourceval 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.

Sourcetype safe_environment

Sourcetype section_data

Sourceval empty_environment : safe_environment

Sourceval is_initial : safe_environment -> bool

Sourceval env_of_safe_env : safe_environment -> Environ.env

Sourceval sections_of_safe_env : safe_environment -> section_data Section.t option

Source

val structure_body_of_safe_env : 
  safe_environment ->
  Declarations.structure_body

The safe_environment state monad

Sourcetype safe_transformer0 = safe_environment -> safe_environment

Sourcetype 'a safe_transformer = safe_environment -> 'a * safe_environment

Stm machinery

Sourcetype private_constants

Sourceval empty_private_constants : private_constants

Sourceval is_empty_private_constants : private_constants -> bool

Source

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.

Sourceval mk_pure_proof : Constr.constr -> private_constants Entries.proof_output

Source

val inline_private_constants : 
  Environ.env ->
  private_constants Entries.proof_output ->
  Constr.constr Univ.in_universe_context_set

Sourceval push_private_constants : Environ.env -> private_constants -> Environ.env

Push the constants in the environment if not already there.

Sourceval universes_of_private : private_constants -> Univ.ContextSet.t

Sourceval is_curmod_library : safe_environment -> bool

Source

val join_safe_environment : 
  ?except:Future.UUIDSet.t ->
  safe_environment ->
  safe_environment

Sourceval is_joined_environment : safe_environment -> bool

Enriching a safe environment

Insertion of global axioms or definitions

Sourcetype global_declaration =

| ConstantEntry : Entries.constant_entry -> global_declaration
| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration

Sourcetype side_effect_declaration =

| DefinitionEff : Entries.definition_entry -> side_effect_declaration
| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration

Sourcetype exported_private_constant = Names.Constant.t

Source

val export_private_constants : 
  private_constants ->
  exported_private_constant list safe_transformer

Source

val add_constant : 
  ?typing_flags:Declarations.typing_flags ->
  Names.Label.t ->
  global_declaration ->
  Names.Constant.t safe_transformer

returns the main constant

Source

val add_private_constant : 
  Names.Label.t ->
  side_effect_declaration ->
  (Names.Constant.t * private_constants) safe_transformer

Similar to add_constant but also returns a certificate

Adding an inductive type

Source

val add_mind : 
  ?typing_flags:Declarations.typing_flags ->
  Names.Label.t ->
  Entries.mutual_inductive_entry ->
  Names.MutInd.t safe_transformer

Adding a module or a module type

Source

val add_module : 
  Names.Label.t ->
  Entries.module_entry ->
  Declarations.inline ->
  (Names.ModPath.t * Mod_subst.delta_resolver) safe_transformer

Source

val add_modtype : 
  Names.Label.t ->
  Entries.module_type_entry ->
  Declarations.inline ->
  Names.ModPath.t safe_transformer

Adding universe constraints

Sourceval push_context_set : strict:bool -> Univ.ContextSet.t -> safe_transformer0

Sourceval add_constraints : Univ.Constraint.t -> safe_transformer0

Sourceval set_engagement : Declarations.engagement -> safe_transformer0

Setting the type theory flavor

Sourceval set_indices_matter : bool -> safe_transformer0

Sourceval set_typing_flags : Declarations.typing_flags -> safe_transformer0

Sourceval set_share_reduction : bool -> safe_transformer0

Sourceval set_check_guarded : bool -> safe_transformer0

Sourceval set_check_positive : bool -> safe_transformer0

Sourceval set_check_universes : bool -> safe_transformer0

Sourceval set_VM : bool -> safe_transformer0

Sourceval set_native_compiler : bool -> safe_transformer0

Sourceval set_allow_sprop : bool -> safe_transformer0

Sourceval check_engagement : Environ.env -> Declarations.set_predicativity -> unit

Interactive section functions

Sourceval open_section : safe_transformer0

Sourceval close_section : safe_transformer0

Sourceval sections_are_opened : safe_environment -> bool

Insertion of local declarations (Local or Variables)

Sourceval push_named_assum : (Names.Id.t * Constr.types) -> safe_transformer0

Source

val push_named_def : 
  (Names.Id.t * Entries.section_def_entry) ->
  safe_transformer0

Source

val push_section_context : 
  (Names.Name.t array * Univ.UContext.t) ->
  safe_transformer0

Add local universes to a polymorphic section

Interactive module functions

Sourceval start_module : Names.Label.t -> Names.ModPath.t safe_transformer

Sourceval start_modtype : Names.Label.t -> Names.ModPath.t safe_transformer

Source

val add_module_parameter : 
  Names.MBId.t ->
  Entries.module_struct_entry ->
  Declarations.inline ->
  Mod_subst.delta_resolver safe_transformer

Sourceval allow_delayed_constants : bool ref

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

The optional result type is given without its functorial part

Source

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

Source

val end_modtype : 
  Names.Label.t ->
  (Names.ModPath.t * Names.MBId.t list) safe_transformer

Source

val add_include : 
  Entries.module_struct_entry ->
  bool ->
  Declarations.inline ->
  Mod_subst.delta_resolver safe_transformer

Sourceval current_modpath : safe_environment -> Names.ModPath.t

Sourceval current_dirpath : safe_environment -> Names.DirPath.t

Libraries : loading and saving compilation units

Sourcetype compiled_library

Sourceval module_of_library : compiled_library -> Declarations.module_body

Sourceval univs_of_library : compiled_library -> Univ.ContextSet.t

Sourceval start_library : Names.DirPath.t -> Names.ModPath.t safe_transformer

Source

val export : 
  ?except:Future.UUIDSet.t ->
  output_native_objects:bool ->
  safe_environment ->
  Names.DirPath.t ->
  Names.ModPath.t * compiled_library * Nativelib.native_library

Source

val import : 
  compiled_library ->
  Univ.ContextSet.t ->
  vodigest ->
  Names.ModPath.t safe_transformer

Safe typing judgments

Sourcetype judgment

Sourceval j_val : judgment -> Constr.constr

Sourceval j_type : judgment -> Constr.constr

Sourceval typing : safe_environment -> Constr.constr -> judgment

The safe typing of a term returns a typing judgment.

Queries

Sourceval exists_objlabel : Names.Label.t -> safe_environment -> bool

Source

val delta_of_senv : 
  safe_environment ->
  Mod_subst.delta_resolver * Mod_subst.delta_resolver

Source

val constant_of_delta_kn_senv : 
  safe_environment ->
  Names.KerName.t ->
  Names.Constant.t

Source

val mind_of_delta_kn_senv : 
  safe_environment ->
  Names.KerName.t ->
  Names.MutInd.t

Retroknowledge / Native compiler

Sourceval register_inline : Names.Constant.t -> safe_transformer0

Source

val register_inductive : 
  Names.inductive ->
  'a CPrimitives.prim_ind ->
  safe_transformer0

Source

val set_strategy : 
  Names.Constant.t Names.tableKey ->
  Conv_oracle.level ->
  safe_transformer0