Nametab (p.rocq-runtime.9.2.0.doc.rocq-runtime.library.Nametab)

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.

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

Nametab generic APIs

Sourcemodule type NAMETAB = sig ... end

Common APIs on name tables.

Sourcemodule type WarnedTab = sig ... end

NAMETAB extended with warnings associated to some of the elements.

Core nametabs

Source

module XRefs : 
  WarnedTab
    with type elt = Globnames.extended_global_reference
     and type warning_data :=
           Globnames.extended_global_reference UserWarn.with_qf

NAMETAB extended with warnings associated to some of the elements.

Sourcemodule Univs : NAMETAB with type elt = Univ.UGlobal.t

Common APIs on name tables.

Sourcemodule Quality : NAMETAB with type elt = Sorts.QGlobal.t

Common APIs on name tables.

Sourcemodule ModTypes : NAMETAB with type elt = Names.ModPath.t

Module types, modules and open modules/modtypes/sections form three separate name spaces (maybe this will change someday)

Sourcemodule Modules : NAMETAB with type elt = Names.ModPath.t

Common APIs on name tables.

Sourcemodule OpenMods : NAMETAB with type elt = GlobDirRef.t

Common APIs on name tables.

Sourcemodule CustomEntries : NAMETAB with type elt = Globnames.CustomName.t

Do not directly use locate with this, instead use the compat layer Metasyntax.intern_custom_name.

Specializations for extended references

These functions operate on XRefs but are about a subset of extended_global_reference for convenience.

Source

val push : 
  ?user_warns:Globnames.extended_global_reference UserWarn.with_qf ->
  visibility ->
  Libnames.full_path ->
  Names.GlobRef.t ->
  unit

Source

val push_abbreviation : 
  ?user_warns:Globnames.extended_global_reference UserWarn.with_qf ->
  visibility ->
  Libnames.full_path ->
  Globnames.abbreviation ->
  unit

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

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

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

Sourceval locate_abbreviation : Libnames.qualid -> Globnames.abbreviation

Sourceval remove_abbreviation : Libnames.full_path -> Globnames.abbreviation -> unit

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

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

Sourceval path_of_abbreviation : Globnames.abbreviation -> Libnames.full_path

Source

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

Returns a qualid for the given global reference. If ~force_short:true is passed, always returns the shortest qualid. Otherwise (default), respects the "Printing Fully Qualified" flag: when the flag is set, returns the fully qualified name; when unset, returns the shortest qualid.

Source

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

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.

Sourceval print_fully_qualified : unit -> bool

Fully qualified printing control. When enabled, pr_global_env uses fully qualified names instead of shortest names. The flag is controlled by the "Printing Fully Qualified" option declared in printer.ml.

Sourceval set_print_fully_qualified : bool -> unit

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

These functions globalize user-level references into global references, like locate and co, but raise GlobalizationError for unbound qualid and UserError for type mismatches (eg global_inductive when the qualid is bound to a constructor)

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

Sourceval global_inductive : Libnames.qualid -> Names.inductive

These functions declare (resp. return) the source location of the object if known

Sourceval set_cci_src_loc : Globnames.extended_global_reference -> Loc.t -> unit

Sourceval cci_src_loc : Globnames.extended_global_reference -> Loc.t option

Nametab generators

Sourcemodule type ValueType = sig ... end

Sourcemodule type StateInfo = sig ... end

Necessary data to declare the imperative state for a nametab.

Sourcemodule EasyNoWarn (M : sig ... end) () : NAMETAB with type elt = M.t

Generate a nametab, without warning support.

Sourcemodule type WarnInfo = sig ... end

Source

module MakeWarned
  (M : NAMETAB)
  (W : WarnInfo with type elt = M.elt)
  () : 
  WarnedTab with type elt = M.elt and type warning_data := W.data

Add warning support to an existing nametab.

Sourcemodule type SimpleWarnS = sig ... end

Source

module Easy
  (M : sig ... end)
  () : 
  WarnedTab with type elt = M.t and type warning_data := M.t UserWarn.with_qf

Generate a nametab with simple warning support (UserWarn.create_depr_and_user_warnings_qf).

legacy APIs

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

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

Sourceval push_dir : visibility -> Libnames.full_path -> GlobDirRef.t -> unit

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

Deprecation and user warn info

Source

val is_warned_xref : 
  Globnames.extended_global_reference ->
  Globnames.extended_global_reference UserWarn.with_qf option

Source

val warn_user_warn_xref : 
  ?loc:Loc.t ->
  Globnames.extended_global_reference UserWarn.with_qf ->
  Globnames.extended_global_reference ->
  unit

The following functions perform globalization of qualified names

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

Sourceval locate_extended : Libnames.qualid -> Globnames.extended_global_reference

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 -> Libnames.full_path

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

Source

val locate_extended_nowarn : 
  Libnames.qualid ->
  Globnames.extended_global_reference

These functions locate all global references with a given suffix; if qualid is valid as such, it comes first in the 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

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 : Libnames.full_path -> bool

Sourceval exists_dir : Libnames.full_path -> bool

Sourceval exists_universe : Libnames.full_path -> bool

These functions locate qualids into full user names

Sourceval full_name_modtype : Libnames.qualid -> Libnames.full_path

Sourceval full_name_module : Libnames.qualid -> Libnames.full_path

Sourceval full_name_open_mod : Libnames.qualid -> Libnames.full_path

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_module : Names.ModPath.t -> Libnames.full_path

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.

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

raises Not_found
for unknown objects.

Source

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

Source

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

Source

val shortest_qualid_of_dir : 
  ?loc:Loc.t ->
  ?force_short:bool ->
  GlobDirRef.t ->
  Libnames.qualid

Source

val shortest_qualid_of_universe : 
  ?loc:Loc.t ->
  ?force_short:bool ->
  '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