package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/coq-core.library/Nametab/index.html

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

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

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

Sourceval locate_constant : Libnames.qualid -> Names.Constant.t
Sourceval locate_modtype : Libnames.qualid -> Names.ModPath.t
Sourceval locate_module : Libnames.qualid -> Names.ModPath.t
Sourceval locate_section : Libnames.qualid -> Names.DirPath.t

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 dirpath_of_module : Names.ModPath.t -> Names.DirPath.t
Sourceval path_of_modtype : Names.ModPath.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_syndef : ?loc:Loc.t -> Names.Id.Set.t -> Globnames.syndef_name -> 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.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.

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