Module `Names`

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.
Label.t is an equivalent of Id.t made distinct for semantical purposes.
ModPath.t are module paths.
KerName.t are absolute names of objects in Coq.

Identifiers

module Id : sig ... end: Representation and operations on identifiers.

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

Type aliases

type name = Name.t = | Anonymous | Name of Id.t
type variable = Id.t
type module_ident = Id.t

module ModIdset : Util.Set.S with type S.elt = module_ident

module ModIdmap : Util.Map.ExtS with type key = module_ident and module Set := ModIdset

Directory paths = section names paths

module DirPath : sig ... end

Names of structure elements

module Label : sig ... end

Unique names for bound modules

module MBId : sig ... end

module MBIset : Util.Set.S with type S.elt = MBId.t

module MBImap : Util.Map.ExtS with type key = MBId.t and module Set := MBIset

The module part of the kernel name

module ModPath : sig ... end

module MPset : Util.Set.S with type S.elt = ModPath.t

module MPmap : Util.Map.ExtS with type key = ModPath.t and module Set := MPset

The absolute names of objects seen by kernel

module KerName : sig ... end

module KNset : CSig.SetS with type elt = KerName.t

module KNpred : Predicate.S with type elt = KerName.t

module KNmap : Util.Map.ExtS with type key = KerName.t and module Set := KNset

Constant Names

module 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.SetS with type elt = Constant.t

module Cset_env : CSig.SetS with type elt = Constant.t

module Cmap : Util.Map.ExtS 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.

module Cmap_env : Util.Map.ExtS 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

module MutInd : sig ... end

module Mindset : CSig.SetS with type elt = MutInd.t

module Mindmap : Util.Map.ExtS with type key = MutInd.t and module Set := Mindset

module Mindmap_env : CSig.MapS with type key = MutInd.t

type inductive = MutInd.t * int: Designation of a (particular) inductive type.

type constructor = inductive * int: Designation of a (particular) constructor of a (particular) inductive type.

module Indmap : CSig.MapS with type key = inductive

module Constrmap : CSig.MapS with type key = constructor

module Indmap_env : CSig.MapS with type key = inductive

module Constrmap_env : CSig.MapS with type key = constructor

val ind_modpath : inductive -> ModPath.t
val constr_modpath : constructor -> ModPath.t
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
val eq_ind : inductive -> inductive -> bool
val eq_user_ind : inductive -> inductive -> bool
val eq_syntactic_ind : inductive -> inductive -> bool
val ind_ord : inductive -> inductive -> int
val ind_hash : inductive -> int
val ind_user_ord : inductive -> inductive -> int
val ind_user_hash : inductive -> int
val ind_syntactic_ord : inductive -> inductive -> int
val ind_syntactic_hash : inductive -> int
val eq_constructor : constructor -> constructor -> bool
val eq_user_constructor : constructor -> constructor -> bool
val eq_syntactic_constructor : constructor -> constructor -> bool
val constructor_ord : constructor -> constructor -> int
val constructor_hash : constructor -> int
val constructor_user_ord : constructor -> constructor -> int
val constructor_user_hash : constructor -> int
val constructor_syntactic_ord : constructor -> constructor -> int
val constructor_syntactic_hash : constructor -> int

Hash-consing

val hcons_con : Constant.t -> Constant.t
val hcons_mind : MutInd.t -> MutInd.t
val hcons_ind : inductive -> inductive
val hcons_construct : constructor -> constructor

type 'a tableKey = | ConstKey of 'a | VarKey of Id.t | RelKey of Int.t
type inv_rel_key = int: index in the rel_context part of environment starting by the end, inverse of de Bruijn indice

val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
val eq_constant_key : Constant.t -> Constant.t -> bool

val eq_ind_chk : inductive -> inductive -> bool

Module paths

type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of ModPath.t * Label.t

module Projection : sig ... end

Global reference is a kernel side type for all references together

module GlobRef : sig ... end

type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t: Better to have it here that in Closure, since required in grammar.cma

val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool

type lident = Id.t CAst.t
type lname = Name.t CAst.t
type lstring = string CAst.t