package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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, syndef_name, 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.

type 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, obj_mp is the current "module" prefix and obj_sec is the "section" prefix.

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

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

Note that both obj_dir and obj_sec are "paths" that is to say, as opposed to obj_mp which is a single module name.

val eq_op : object_prefix -> object_prefix -> bool
module GlobDirRef : sig ... end

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

exception GlobalizationError of Libnames.qualid
val 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)
type visibility =
  1. | Until of int
  2. | Exactly of int
val map_visibility : (int -> int) -> visibility -> visibility
val push_modtype : visibility -> Libnames.full_path -> Names.ModPath.t -> unit
val push_dir : visibility -> Names.DirPath.t -> GlobDirRef.t -> unit
val push_syndef : visibility -> Libnames.full_path -> Globnames.syndef_name -> unit
val push_universe : visibility -> Libnames.full_path -> Univ.Level.UGlobal.t -> unit
The following functions perform globalization of qualified names

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

val locate_constant : Libnames.qualid -> Names.Constant.t
val locate_syndef : Libnames.qualid -> Globnames.syndef_name
val locate_modtype : Libnames.qualid -> Names.ModPath.t
val locate_dir : Libnames.qualid -> GlobDirRef.t
val locate_module : Libnames.qualid -> Names.ModPath.t
val locate_section : Libnames.qualid -> Names.DirPath.t
val locate_universe : Libnames.qualid -> Univ.Level.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

val 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

val locate_all : Libnames.qualid -> Names.GlobRef.t list
val locate_extended_all : Libnames.qualid -> Globnames.extended_global_reference list
val locate_extended_all_dir : Libnames.qualid -> GlobDirRef.t list
val locate_extended_all_modtype : Libnames.qualid -> Names.ModPath.t list
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

val global_of_path : Libnames.full_path -> Names.GlobRef.t
These functions tell if the given absolute name is already taken
val exists_cci : Libnames.full_path -> bool
val exists_modtype : Libnames.full_path -> bool
val exists_dir : Names.DirPath.t -> bool
val exists_universe : Libnames.full_path -> bool
These functions locate qualids into full user names
val full_name_cci : Libnames.qualid -> Libnames.full_path
val full_name_modtype : Libnames.qualid -> Libnames.full_path
val 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

val path_of_global : Names.GlobRef.t -> Libnames.full_path
val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
val path_of_modtype : Names.ModPath.t -> Libnames.full_path
val path_of_universe : Univ.Level.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

val dirpath_of_global : Names.GlobRef.t -> Names.DirPath.t
val basename_of_global : Names.GlobRef.t -> Names.Id.t
val 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.

val shortest_qualid_of_global : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
val shortest_qualid_of_syndef : ?loc:Loc.t -> Names.Id.Set.t -> Globnames.syndef_name -> Libnames.qualid
val shortest_qualid_of_modtype : ?loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_module : ?loc:Loc.t -> Names.ModPath.t -> Libnames.qualid
val shortest_qualid_of_universe : ?loc:Loc.t -> 'u Names.Id.Map.t -> Univ.Level.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.

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