package coq-core

  1. Overview
  2. Docs
package coq-core
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.

Sourcetype object_prefix = {
  1. obj_dir : Names.DirPath.t;
  2. 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 =
  1. | Until of int
  2. | Exactly of int
Sourceval map_visibility : (int -> int) -> visibility -> visibility
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
Sourceval push_abbreviation : visibility -> Libnames.full_path -> Globnames.abbreviation -> unit
module 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_constant : Libnames.qualid -> Names.Constant.t
Sourceval locate_abbreviation : Libnames.qualid -> Globnames.abbreviation
Sourceval locate_modtype : Libnames.qualid -> Names.ModPath.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

Remove the binding to an abbreviation

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

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

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 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_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
Sourcemodule Make (U : UserName) (E : EqualityType) : NAMETREE with type user_name = U.t and type elt = E.t
Sourcemodule Modules : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct