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:

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