blob: f1af6c171373ceb5e77d8b276d19add743c0e6f1 (
plain)
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Pp
open Names
open Libnames
(*i*)
(*s This module contains the tables for globalization, which
associates internal object references to qualified names (qualid). *)
(* Most functions in this module fall into one of the following categories:
\begin{itemize}
\item [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 [section_path] or a [dir_path].
\item [exists : full_user_name -> bool]
Is the [full_user_name] already atributed as an absolute user name
of some object?
\item [locate : qualid -> object_reference]
Finds the object referred to by [qualid] or raises Not_found
\item [name_of] : object_reference -> user_name
The [user_name] can be for example the shortest non ambiguous [qualid] or
the [full_user_name] or [identifier]. Such a function can also have a
local context argument.
*)
exception GlobalizationError of qualid
exception GlobalizationConstantError of qualid
(* Raises a globalization error *)
val error_global_not_found_loc : loc -> qualid -> 'a
val error_global_not_found : qualid -> 'a
val error_global_constant_not_found_loc : loc -> qualid -> 'a
(*s Register visibility of things *)
(* The visibility can be registered either
\begin{itemize}
\item for all suffixes not shorter then a given int -- when the
object is loaded inside a module -- or
\item for a precise suffix, when the module containing (the module
containing ...) the object is opened (imported)
\end{itemize}
*)
type visibility = Until of int | Exactly of int
val push : visibility -> section_path -> global_reference -> unit
val push_syntactic_definition :
visibility -> section_path -> kernel_name -> unit
val push_modtype : visibility -> section_path -> kernel_name -> unit
val push_dir : visibility -> dir_path -> global_dir_reference -> unit
val push_object : visibility -> section_path -> unit
val push_tactic : visibility -> section_path -> kernel_name -> unit
(*s The following functions perform globalization of qualified names *)
(* This returns the section path of a constant or fails with [Not_found] *)
val locate : qualid -> global_reference
(* This function is used to transform a qualified identifier into a
global reference, with a nice error message in case of failure *)
val global : reference -> global_reference
(* The same for inductive types *)
val global_inductive : reference -> inductive
(* This locates also syntactic definitions *)
val extended_locate : qualid -> extended_global_reference
val locate_obj : qualid -> section_path
val locate_constant : qualid -> constant
val locate_mind : qualid -> mutual_inductive
val locate_section : qualid -> dir_path
val locate_modtype : qualid -> kernel_name
val locate_syntactic_definition : qualid -> kernel_name
type ltac_constant = kernel_name
val locate_tactic : qualid -> ltac_constant
val locate_dir : qualid -> global_dir_reference
val locate_module : qualid -> module_path
(* A variant looking up a [section_path] *)
val absolute_reference : section_path -> global_reference
(*s These function tell if the given absolute name is already taken *)
val exists_cci : section_path -> bool
val exists_modtype : section_path -> bool
(* Those three functions are the same *)
val exists_dir : dir_path -> bool
val exists_section : dir_path -> bool (* deprecated *)
val exists_module : dir_path -> bool (* deprecated *)
(*s These functions turn qualids into full user names: [section_path]s
or [dir_path]s *)
val full_name_modtype : qualid -> section_path
val full_name_cci : qualid -> section_path
(* As above but checks that the path found is indeed a module *)
val full_name_module : qualid -> dir_path
(*s Reverse lookup -- finding user names corresponding to the given
internal name *)
val sp_of_syntactic_definition : kernel_name -> section_path
val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
val shortest_qualid_of_syndef : kernel_name -> qualid
val shortest_qualid_of_tactic : ltac_constant -> qualid
val dir_of_mp : module_path -> dir_path
val sp_of_global : global_reference -> section_path
val id_of_global : global_reference -> identifier
(* Printing of global references using names as short as possible *)
val pr_global_env : Idset.t -> global_reference -> std_ppcmds
(* 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_module : module_path -> qualid
val shortest_qualid_of_modtype : kernel_name -> qualid
(*
type frozen
val freeze : unit -> frozen
val unfreeze : frozen -> unit
*)
|
