package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.kernel/Names/index.html

Module NamesSource

This file defines a lot of different notions of names used pervasively in the kernel as well as in other places. The essential datatypes exported by this API are:

  • Id.t is the type of identifiers, that is morally a subset of strings which only contains Unicode characters of the Letter kind (and a few more).
  • Name.t is an ad-hoc variant of Id.t option allowing to handle optionally named objects.
  • DirPath.t represents generic paths as sequences of identifiers.
  • ModPath.t are module paths.
  • KerName.t are absolute names of objects in Rocq.
Identifiers
Sourcemodule Id : sig ... end

Representation and operations on identifiers.

Sourcemodule Name : sig ... end

Representation and operations on identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax).

Type aliases
Sourcetype name = Name.t =
  1. | Anonymous
  2. | Name of Id.t
  • deprecated (8.8) Use Name.t
Sourcetype variable = Id.t
Directory paths = section names paths
Sourcemodule DirPath : sig ... end
Sourcemodule DPset = DirPath.Set
Sourcemodule DPmap = DirPath.Map
Unique names for bound modules
Sourcemodule MBId : sig ... end
Sourcemodule MBIset = MBId.Set
Sourcemodule MBImap = MBId.Map
The module part of the kernel name
Sourcemodule ModPath : sig ... end
Sourcemodule MPset = ModPath.Set
Sourcemodule MPmap = ModPath.Map
The absolute names of objects seen by kernel
Sourcemodule KerName : sig ... end
module KNset = KerName.Set
Sourcemodule KNpred = KerName.Pred
Sourcemodule KNmap = KerName.Map
Signature for quotiented names
Sourcemodule type EqType = sig ... end
Sourcemodule type QNameS = sig ... end
Constant Names
Sourcemodule Constant : sig ... end
module Cpred : Predicate.S with type elt = Constant.t

The *_env modules consider an order on user part of names the others consider an order on canonical part of names

module Cset : CSig.USetS with type elt = Constant.t
module Cset_env : CSig.USetS with type elt = Constant.t
Sourcemodule Cmap : Util.Map.UExtS with type key = Constant.t and module Set := Cset

A map whose keys are constants (values of the Constant.t type). Keys are ordered wrt. "canonical form" of the constant.

Sourcemodule Cmap_env : Util.Map.UExtS with type key = Constant.t and module Set := Cset_env

A map whose keys are constants (values of the Constant.t type). Keys are ordered wrt. "user form" of the constant.

Inductive names
Sourcemodule MutInd : sig ... end
module Mindset : CSig.USetS with type elt = MutInd.t
Sourcemodule Mindmap : Util.Map.UExtS with type key = MutInd.t and module Set := Mindset
module Mindmap_env : CMap.UExtS with type key = MutInd.t
Sourcemodule Ind : sig ... end
Sourcetype inductive = Ind.t
Sourcemodule Construct : sig ... end
Sourcetype constructor = Construct.t
module Indset : CSet.ExtS with type elt = inductive
module Constrset : CSet.ExtS with type elt = constructor
module Indset_env : CSet.ExtS with type elt = inductive
module Constrset_env : CSet.ExtS with type elt = constructor
module Indmap : CMap.ExtS with type key = inductive and module Set := Indset
module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset
module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env
module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env
Sourceval ith_mutual_inductive : inductive -> int -> inductive
Sourceval ith_constructor_of_inductive : inductive -> int -> constructor
Sourceval inductive_of_constructor : constructor -> inductive
Sourceval index_of_constructor : constructor -> int
Hash-consing
Sourceval hcons_mind : MutInd.t Hashcons.f
Sourceval hcons_ind : inductive Hashcons.f
Sourceval hcons_construct : constructor Hashcons.f
Sourcetype 'a tableKey =
  1. | ConstKey of 'a
  2. | VarKey of Id.t
  3. | RelKey of Int.t
Sourcetype inv_rel_key = int

index in the rel_context part of environment starting by the end, inverse of de Bruijn indice

Sourceval eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
Sourceval hash_table_key : ('a -> int) -> 'a tableKey -> int
Sourceval eq_constant_key : Constant.t -> Constant.t -> bool
Module paths
Sourcetype module_path = ModPath.t =
  1. | MPfile of DirPath.t
  2. | MPbound of MBId.t
  3. | MPdot of ModPath.t * Id.t
  • deprecated (8.8) Alias type
Sourcemodule Projection : sig ... end
module PRset : CSig.USetS with type elt = Projection.Repr.t
Sourcemodule PRmap : Util.Map.UExtS with type key = Projection.Repr.t and module Set := PRset

Predicate on projection representation (ignoring unfolding state)

Global reference is a kernel side type for all references together
Sourcemodule GlobRef : sig ... end

Located identifiers and objects with syntax.

Sourcetype lident = Id.t CAst.t
Sourcetype lname = Name.t CAst.t
Sourcetype lstring = string CAst.t
Sourceval lident_eq : lident -> lident -> bool
Sourcemodule Label : sig ... end

Deprecated