Module `Nametab`

Most functions in this module fall into one of the following categories:

push : visibility -> full_user_name -> object_reference -> unit
Registers the object_reference to be referred to by the full_user_name (and its suffixes according to visibility). full_user_name can either be a full_path or a DirPath.t.
exists : full_user_name -> bool
Is the full_user_name already attributed as an absolute user name of some object?
locate : qualid -> object_reference
Finds the object referred to by qualid or raises Not_found
full_name : qualid -> full_user_name
Finds the full user name referred to by qualid or raises Not_found
shortest_qualid_of : object_reference -> user_name
The user_name can be for example the shortest non ambiguous qualid or the full_user_name or Id.t. Such a function can also have a local context argument.

type object_prefix = { obj_dir : Names.DirPath.t; obj_mp : Names.ModPath.t; }

Object prefix morally contains the "prefix" naming of an object to be stored by library, where obj_dir is the "absolute" path, obj_mp is the current "module" prefix and obj_sec is the "section" prefix.

Thus, for an object living inside Module A. Section B. the prefix would be:

{ obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" }

Note that both obj_dir and obj_sec are "paths" that is to say, as opposed to obj_mp which is a single module name.

val eq_op : object_prefix -> object_prefix -> bool

module GlobDirRef : sig ... end: to this type are mapped DirPath.t's in the nametab

exception GlobalizationError of Libnames.qualid

val error_global_not_found : info:Exninfo.info -> Libnames.qualid -> 'a: Raises a globalization error

Register visibility of things

type visibility = | Until of int | Exactly of int

val map_visibility : (int -> int) -> visibility -> visibility
val push : visibility -> Libnames.full_path -> Names.GlobRef.t -> unit
val push_modtype : visibility -> Libnames.full_path -> Names.ModPath.t -> unit
val push_dir : visibility -> Names.DirPath.t -> GlobDirRef.t -> unit
val push_syndef : visibility -> Libnames.full_path -> Globnames.syndef_name -> unit

module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t

val push_universe : visibility -> Libnames.full_path -> Univ.Level.UGlobal.t -> unit

The following functions perform globalization of qualified names

val locate : Libnames.qualid -> Names.GlobRef.t
val locate_extended : Libnames.qualid -> Globnames.extended_global_reference
val locate_constant : Libnames.qualid -> Names.Constant.t
val locate_syndef : Libnames.qualid -> Globnames.syndef_name
val locate_modtype : Libnames.qualid -> Names.ModPath.t
val locate_dir : Libnames.qualid -> GlobDirRef.t
val locate_module : Libnames.qualid -> Names.ModPath.t
val locate_section : Libnames.qualid -> Names.DirPath.t
val locate_universe : Libnames.qualid -> Univ.Level.UGlobal.t

val global : Libnames.qualid -> Names.GlobRef.t
val global_inductive : Libnames.qualid -> Names.inductive

val locate_all : Libnames.qualid -> Names.GlobRef.t list

val locate_extended_all : Libnames.qualid -> Globnames.extended_global_reference list

val locate_extended_all_dir : Libnames.qualid -> GlobDirRef.t list

val locate_extended_all_modtype : Libnames.qualid -> Names.ModPath.t list

val completion_canditates : Libnames.qualid -> Globnames.extended_global_reference list

Experimental completion support, API is _unstable_

completion_canditates qualid will return the list of global references that have qualid as a prefix. UI usually will want to compose this with shortest_qualid_of_global

val global_of_path : Libnames.full_path -> Names.GlobRef.t
val extended_global_of_path : Libnames.full_path -> Globnames.extended_global_reference

These functions tell if the given absolute name is already taken

val exists_cci : Libnames.full_path -> bool
val exists_modtype : Libnames.full_path -> bool
val exists_dir : Names.DirPath.t -> bool
val exists_universe : Libnames.full_path -> bool

These functions locate qualids into full user names

val full_name_cci : Libnames.qualid -> Libnames.full_path
val full_name_modtype : Libnames.qualid -> Libnames.full_path
val full_name_module : Libnames.qualid -> Names.DirPath.t

Reverse lookup

Finding user names corresponding to the given internal name

val path_of_syndef : Globnames.syndef_name -> Libnames.full_path

val path_of_global : Names.GlobRef.t -> Libnames.full_path

val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t

val path_of_modtype : Names.ModPath.t -> Libnames.full_path

val path_of_universe : Univ.Level.UGlobal.t -> Libnames.full_path

A universe_id might not be registered with a corresponding user name.

raises Not_found: if the universe was not introduced by the user.

val dirpath_of_global : Names.GlobRef.t -> Names.DirPath.t

val basename_of_global : Names.GlobRef.t -> Names.Id.t

val pr_global_env : Names.Id.Set.t -> Names.GlobRef.t -> Pp.t

Printing of global references using names as short as possible.

raises Not_found: when the reference is not in the global tables.

val shortest_qualid_of_global : ?⁠loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
val shortest_qualid_of_syndef : ?⁠loc:Loc.t -> Names.Id.Set.t -> Globnames.syndef_name -> Libnames.qualid
val shortest_qualid_of_modtype : ?⁠loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_module : ?⁠loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_universe : ?⁠loc:Loc.t -> 'u Names.Id.Map.t -> Univ.Level.UGlobal.t -> Libnames.qualid: In general we have a UnivNames.universe_binders around rather than a Id.Set.t

Generic name handling

module type UserName = sig ... end

module type EqualityType = sig ... end

module type NAMETREE = sig ... end

module Make : functor (U : UserName) -> functor (E : EqualityType) -> NAMETREE with type user_name = U.t and type elt = E.t