package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module NametabSource

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.

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 =
  1. | Until of int
  2. | 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

NAMETAB extended with warnings associated to some of the elements.

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

Common APIs on name tables.

Common APIs on name tables.

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

Common APIs on name tables.

Sourcemodule OpenMods : NAMETAB with type elt = GlobDirRef.t

Common APIs on name tables.

Specializations for extended references

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

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 path_of_abbreviation : Globnames.abbreviation -> Libnames.full_path
Sourceval shortest_qualid_of_global : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
Sourceval shortest_qualid_of_abbreviation : ?loc:Loc.t -> 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.

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_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
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
Sourcemodule 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
Sourcemodule 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

The following functions perform globalization of qualified names

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

Sourceval locate_modtype : Libnames.qualid -> Names.ModPath.t
Sourceval locate_module : Libnames.qualid -> Names.ModPath.t
Sourceval locate_universe : Libnames.qualid -> Univ.UGlobal.t

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

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

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

Sourceval shortest_qualid_of_modtype : ?loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
Sourceval shortest_qualid_of_module : ?loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
Sourceval shortest_qualid_of_dir : ?loc:Loc.t -> GlobDirRef.t -> Libnames.qualid
Sourceval 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