package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Register visibility of things
Nametab generic APIs
Core nametabs
Specializations for extended references
These functions declare (resp. return) the source location of the object if known
Nametab generators
legacy APIs
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

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz

sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.library/Nametab/index.html

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.

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.

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

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

Source

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

Sourceval shortest_qualid_of_dir : ?loc:Loc.t -> GlobDirRef.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

On This Page

Register visibility of things
Nametab generic APIs
Core nametabs
Specializations for extended references
These functions declare (resp. return) the source location of the object if known
Nametab generators
legacy APIs
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

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.library/Nametab/index.html

Module NametabSource

Register visibility of things

Nametab generic APIs

Core nametabs

Specializations for extended references

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

Nametab generators

legacy APIs

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

dune-project
Dependency

Module `Nametab`Source