1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Libnames
(** 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:
{ul {- [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.}}
*)
(** 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.
*)
type object_prefix = {
obj_dir : DirPath.t;
obj_mp : ModPath.t;
}
val eq_op : object_prefix -> object_prefix -> bool
(** to this type are mapped [DirPath.t]'s in the nametab *)
module GlobDirRef : sig
type t =
| DirOpenModule of ModPath.t
| DirOpenModtype of ModPath.t
| DirOpenSection of DirPath.t
val equal : t -> t -> bool
end
exception GlobalizationError of qualid
(** Raises a globalization error *)
val error_global_not_found : info:Exninfo.info -> qualid -> 'a
(** {6 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 = Until of int | Exactly of int
val map_visibility : (int -> int) -> visibility -> visibility
val push : ?user_warns:UserWarn.t -> visibility -> full_path -> GlobRef.t -> unit
val push_modtype : visibility -> full_path -> ModPath.t -> unit
val push_module : visibility -> DirPath.t -> ModPath.t -> unit
val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
val push_abbreviation : ?user_warns:UserWarn.t -> visibility -> full_path -> Globnames.abbreviation -> unit
val push_universe : visibility -> full_path -> Univ.UGlobal.t -> unit
(** Deprecation and user warn info *)
val is_warned_xref : Globnames.extended_global_reference -> UserWarn.t option
val warn_user_warn_xref : ?loc:Loc.t -> UserWarn.t -> Globnames.extended_global_reference -> unit
(** {6 The following functions perform globalization of qualified names } *)
(** These functions globalize a (partially) qualified name or fail with
[Not_found] *)
val locate : qualid -> GlobRef.t
val locate_extended : qualid -> Globnames.extended_global_reference
val locate_constant : qualid -> Constant.t
val locate_abbreviation : qualid -> Globnames.abbreviation
val locate_modtype : qualid -> ModPath.t
val locate_dir : qualid -> GlobDirRef.t
val locate_module : qualid -> ModPath.t
val locate_section : qualid -> DirPath.t
val locate_universe : qualid -> Univ.UGlobal.t
val locate_extended_nowarn : qualid -> Globnames.extended_global_reference
(** Remove the binding to an abbreviation *)
val remove_abbreviation : 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 *)
val global : qualid -> GlobRef.t
val global_inductive : qualid -> 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 : qualid -> GlobRef.t list
val locate_extended_all : qualid -> Globnames.extended_global_reference list
val locate_extended_all_dir : qualid -> GlobDirRef.t list
val locate_extended_all_modtype : qualid -> ModPath.t list
val locate_extended_all_module : qualid -> ModPath.t list
(** Experimental completion support, API is _unstable_ *)
val completion_canditates : qualid -> Globnames.extended_global_reference list
(** [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 : full_path -> GlobRef.t
val extended_global_of_path : full_path -> Globnames.extended_global_reference
(** {6 These functions tell if the given absolute name is already taken } *)
val exists_cci : full_path -> bool
val exists_modtype : full_path -> bool
val exists_module : DirPath.t -> bool
val exists_dir : DirPath.t -> bool
val exists_universe : full_path -> bool
(** {6 These functions locate qualids into full user names } *)
val full_name_modtype : qualid -> full_path
val full_name_module : qualid -> DirPath.t
(** {6 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_abbreviation : Globnames.abbreviation -> full_path
val path_of_global : GlobRef.t -> full_path
val dirpath_of_module : ModPath.t -> DirPath.t
val path_of_modtype : ModPath.t -> full_path
(** A universe_id might not be registered with a corresponding user name.
@raise Not_found if the universe was not introduced by the user. *)
val path_of_universe : Univ.UGlobal.t -> full_path
(** Returns in particular the dirpath or the basename of the full path
associated to global reference *)
val dirpath_of_global : GlobRef.t -> DirPath.t
val basename_of_global : GlobRef.t -> Id.t
(** Printing of global references using names as short as possible.
@raise Not_found when the reference is not in the global tables. *)
val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
(** 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.
@raise Not_found for unknown objects. *)
val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
val shortest_qualid_of_abbreviation : ?loc:Loc.t -> Id.Set.t -> Globnames.abbreviation -> qualid
val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
(** In general we have a [UnivNames.universe_binders] around rather than a [Id.Set.t] *)
val shortest_qualid_of_universe : ?loc:Loc.t -> 'u Id.Map.t -> Univ.UGlobal.t -> qualid
(** {5 Generic name handling} *)
(** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
module type UserName = sig
type t
val equal : t -> t -> bool
val to_string : t -> string
val repr : t -> Id.t * module_ident list
end
module type EqualityType =
sig
type t
val equal : t -> t -> bool
end
module type NAMETREE = sig
type elt
type t
type user_name
val empty : t
val push : visibility -> user_name -> elt -> t -> t
val locate : qualid -> t -> elt
val find : user_name -> t -> elt
val remove : user_name -> t -> t
val exists : user_name -> t -> bool
val user_name : qualid -> t -> user_name
val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid
val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
val find_prefixes : qualid -> t -> elt list
val match_prefixes : qualid -> t -> elt list
end
module Make (U : UserName) (E : EqualityType) :
NAMETREE with type user_name = U.t and type elt = E.t
module Modules : sig
type t
val freeze : unit -> t
val unfreeze : t -> unit
val summary_tag : t Summary.Dyn.tag
end
|