Module `Nametab`Source

This module contains the tables for globalization.

These globalization tables associate internal object references to qualified names (qualid). There are three classes of names:

1a) internal kernel names: kernel_name, constant, inductive, module_path, DirPath.t

1b) other internal names: global_reference, abbreviation, extended_global_reference, global_dir_reference, ...

2) full, non ambiguous user names: full_path

3) non necessarily full, possibly ambiguous user names: reference and qualid

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.

Sourcetype 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 and obj_mp is the current "module" prefix.

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

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

Note that obj_dir is a "path" that is to say, as opposed to obj_mp which is a single module name.

Sourceval eq_op : object_prefix -> object_prefix -> bool

Sourcemodule GlobDirRef : sig ... end

to this type are mapped DirPath.t's in the nametab

Sourceexception GlobalizationError of Libnames.qualid

Sourceval error_global_not_found : info:Exninfo.info -> Libnames.qualid -> 'a

Raises a globalization error

Register visibility of things

The visibility can be registered either

for all suffixes not shorter then a given int -- when the object is loaded inside a module -- or
for a precise suffix, when the module containing (the module containing ...) the object is opened (imported)

Sourcetype visibility =

| Until of int
| Exactly of int

Sourceval map_visibility : (int -> int) -> visibility -> visibility

Sourceval push : visibility -> Libnames.full_path -> Names.GlobRef.t -> unit

Sourceval push_modtype : visibility -> Libnames.full_path -> Names.ModPath.t -> unit

Sourceval push_module : visibility -> Names.DirPath.t -> Names.ModPath.t -> unit

Sourceval push_dir : visibility -> Names.DirPath.t -> GlobDirRef.t -> unit

Source

val push_abbreviation : 
  visibility ->
  Libnames.full_path ->
  Globnames.abbreviation ->
  unit

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

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

The following functions perform globalization of qualified names

These functions globalize a (partially) qualified name or fail with Not_found

Sourceval locate : Libnames.qualid -> Names.GlobRef.t

Sourceval locate_extended : Libnames.qualid -> Globnames.extended_global_reference

Sourceval locate_constant : Libnames.qualid -> Names.Constant.t

Sourceval locate_abbreviation : Libnames.qualid -> Globnames.abbreviation

Sourceval locate_modtype : Libnames.qualid -> Names.ModPath.t

Sourceval locate_dir : Libnames.qualid -> GlobDirRef.t

Sourceval locate_module : Libnames.qualid -> Names.ModPath.t

Sourceval locate_section : Libnames.qualid -> Names.DirPath.t

Sourceval locate_universe : Libnames.qualid -> Univ.UGlobal.t

These functions globalize user-level references into global references, like locate and co, but raise a nice error message in case of failure

Sourceval global : Libnames.qualid -> Names.GlobRef.t

Sourceval global_inductive : Libnames.qualid -> Names.inductive

These functions locate all global references with a given suffix; if qualid is valid as such, it comes first in the list

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

Source

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

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

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

Sourceval locate_extended_all_module : Libnames.qualid -> Names.ModPath.t list

Source

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

Mapping a full path to a global reference

Sourceval global_of_path : Libnames.full_path -> Names.GlobRef.t

Source

val extended_global_of_path : 
  Libnames.full_path ->
  Globnames.extended_global_reference

These functions tell if the given absolute name is already taken

Sourceval exists_cci : Libnames.full_path -> bool

Sourceval exists_modtype : Libnames.full_path -> bool

Sourceval exists_module : Names.DirPath.t -> bool

Sourceval exists_dir : Names.DirPath.t -> bool

Sourceval exists_universe : Libnames.full_path -> bool

These functions locate qualids into full user names

Sourceval full_name_cci : Libnames.qualid -> Libnames.full_path

Sourceval full_name_modtype : Libnames.qualid -> Libnames.full_path

Sourceval full_name_module : Libnames.qualid -> Names.DirPath.t

Reverse lookup

Finding user names corresponding to the given internal name

Returns the full path bound to a global reference or syntactic definition, and the (full) dirpath associated to a module path

Sourceval path_of_abbreviation : Globnames.abbreviation -> Libnames.full_path

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

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

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

Sourceval path_of_universe : Univ.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.

Returns in particular the dirpath or the basename of the full path associated to global reference

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

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

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

The shortest_qualid functions given an object with user_name Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes the same object.

raises Not_found
for unknown objects.

Source

val shortest_qualid_of_global : 
  ?loc:Loc.t ->
  Names.Id.Set.t ->
  Names.GlobRef.t ->
  Libnames.qualid

Source

val shortest_qualid_of_abbreviation : 
  ?loc:Loc.t ->
  Names.Id.Set.t ->
  Globnames.abbreviation ->
  Libnames.qualid

Source

val shortest_qualid_of_modtype : 
  ?loc:Loc.t ->
  Names.ModPath.t ->
  Libnames.qualid

Source

val shortest_qualid_of_module : 
  ?loc:Loc.t ->
  Names.ModPath.t ->
  Libnames.qualid

Source

val shortest_qualid_of_universe : 
  ?loc:Loc.t ->
  'u Names.Id.Map.t ->
  Univ.UGlobal.t ->
  Libnames.qualid

In general we have a UnivNames.universe_binders around rather than a Id.Set.t

Generic name handling

NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API.

Sourcemodule type UserName = sig ... end

Sourcemodule type EqualityType = sig ... end

Sourcemodule type NAMETREE = sig ... end

Source

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

Sourcemodule Modules : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Nametab/index.html

Module `Nametab`Source

Register visibility of things

The following functions perform globalization of qualified names

These functions tell if the given absolute name is already taken

These functions locate qualids into full user names

Reverse lookup

Generic name handling

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.library/Nametab/index.html

Module NametabSource

Register visibility of things

The following functions perform globalization of qualified names

These functions tell if the given absolute name is already taken

These functions locate qualids into full user names

Reverse lookup

Generic name handling

Module `Nametab`Source