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
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Pp
open Names
open Libnames
open Nameops
open Declarations
exception GlobalizationError of qualid
exception GlobalizationConstantError of qualid
let error_global_not_found_loc loc q =
Stdpp.raise_with_loc loc (GlobalizationError q)
let error_global_constant_not_found_loc loc q =
Stdpp.raise_with_loc loc (GlobalizationConstantError q)
let error_global_not_found q = raise (GlobalizationError q)
(* 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 open (imported)
*)
type visibility = Until of int | Exactly of int
(* Data structure for nametabs *******************************************)
(* This module type will be instantiated by [section_path] of [dir_path] *)
(* The [repr] function is assumed to return the reversed list of idents. *)
module type UserName = sig
type t
val to_string : t -> string
val repr : t -> identifier * module_ident list
end
(* A ['a t] is a map from [user_name] to ['a], with possible lookup by
partially qualified names of type [qualid]. The mapping of
partially qualified names to ['a] is determined by the [visibility]
parameter of [push].
The [shortest_qualid] function given a user_name Coq.A.B.x, tries
to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes
the same object.
*)
module type NAMETREE = sig
type 'a t
type user_name
val empty : 'a t
val push : visibility -> user_name -> 'a -> 'a t -> 'a t
val locate : qualid -> 'a t -> 'a
val find : user_name -> 'a t -> 'a
val exists : user_name -> 'a t -> bool
val user_name : qualid -> 'a t -> user_name
val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid
end
module Make(U:UserName) : NAMETREE with type user_name = U.t
=
struct
type user_name = U.t
type 'a path_status =
Nothing
| Relative of user_name * 'a
| Absolute of user_name * 'a
(* Dictionaries of short names *)
type 'a nametree = ('a path_status * 'a nametree ModIdmap.t)
type 'a t = 'a nametree Idmap.t
let empty = Idmap.empty
(* [push_until] is used to register [Until vis] visibility and
[push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
let rec push_until uname o level (current,dirmap) = function
| modid :: path as dir ->
let mc =
try ModIdmap.find modid dirmap
with Not_found -> (Nothing, ModIdmap.empty)
in
let this =
if level <= 0 then
match current with
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
warning ("Trying to mask the absolute name \""
^ U.to_string n ^ "\"!");
current
| Nothing
| Relative _ -> Relative (uname,o)
else current
in
let ptab' = push_until uname o (level-1) mc path in
(this, ModIdmap.add modid ptab' dirmap)
| [] ->
match current with
| Absolute (uname',o') ->
if o'=o then begin
assert (uname=uname');
current, dirmap
(* we are putting the same thing for the second time :) *)
end
else
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
(* But ours is also absolute! This is an error! *)
error ("Cannot mask the absolute name \""
^ U.to_string uname' ^ "\"!")
| Nothing
| Relative _ -> Absolute (uname,o), dirmap
let rec push_exactly uname o level (current,dirmap) = function
| modid :: path as dir ->
let mc =
try ModIdmap.find modid dirmap
with Not_found -> (Nothing, ModIdmap.empty)
in
if level = 0 then
let this =
match current with
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
warning ("Trying to mask the absolute name \""
^ U.to_string n ^ "\"!");
current
| Nothing
| Relative _ -> Relative (uname,o)
in
(this, dirmap)
else (* not right level *)
let ptab' = push_exactly uname o (level-1) mc path in
(current, ModIdmap.add modid ptab' dirmap)
| [] ->
anomaly "Prefix longer than path! Impossible!"
let push visibility uname o tab =
let id,dir = U.repr uname in
let ptab =
try Idmap.find id tab
with Not_found -> (Nothing, ModIdmap.empty)
in
let ptab' = match visibility with
| Until i -> push_until uname o (i-1) ptab dir
| Exactly i -> push_exactly uname o (i-1) ptab dir
in
Idmap.add id ptab' tab
let rec search (current,modidtab) = function
| modid :: path -> search (ModIdmap.find modid modidtab) path
| [] -> current
let find_node qid tab =
let (dir,id) = repr_qualid qid in
search (Idmap.find id tab) (repr_dirpath dir)
let locate qid tab =
let o = match find_node qid tab with
| Absolute (uname,o) | Relative (uname,o) -> o
| Nothing -> raise Not_found
in
o
let user_name qid tab =
let uname = match find_node qid tab with
| Absolute (uname,o) | Relative (uname,o) -> uname
| Nothing -> raise Not_found
in
uname
let find uname tab =
let id,l = U.repr uname in
match search (Idmap.find id tab) l with
Absolute (_,o) -> o
| _ -> raise Not_found
let exists uname tab =
try
let _ = find uname tab in
true
with
Not_found -> false
let shortest_qualid ctx uname tab =
let id,dir = U.repr uname in
let hidden = Idset.mem id ctx in
let rec find_uname pos dir (path,tab) = match path with
| Absolute (u,_) | Relative (u,_)
when u=uname && not(pos=[] && hidden) -> List.rev pos
| _ ->
match dir with
[] -> raise Not_found
| id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab)
in
let ptab = Idmap.find id tab in
let found_dir = find_uname [] dir ptab in
make_qualid (make_dirpath found_dir) id
end
(* Global name tables *************************************************)
module SpTab = Make (struct
type t = section_path
let to_string = string_of_path
let repr sp =
let dir,id = repr_path sp in
id, (repr_dirpath dir)
end)
type ccitab = extended_global_reference SpTab.t
let the_ccitab = ref (SpTab.empty : ccitab)
type kntab = kernel_name SpTab.t
let the_modtypetab = ref (SpTab.empty : kntab)
type objtab = unit SpTab.t
let the_objtab = ref (SpTab.empty : objtab)
module DirTab = Make(struct
type t = dir_path
let to_string = string_of_dirpath
let repr dir = match repr_dirpath dir with
| [] -> anomaly "Empty dirpath"
| id::l -> (id,l)
end)
(* If we have a (closed) module M having a submodule N, than N does not
have the entry in [the_dirtab]. *)
type dirtab = global_dir_reference DirTab.t
let the_dirtab = ref (DirTab.empty : dirtab)
(* Reversed name tables ***************************************************)
(* This table translates extended_global_references back to section paths *)
module Globrevtab = Map.Make(struct
type t=extended_global_reference
let compare = compare
end)
type globrevtab = section_path Globrevtab.t
let the_globrevtab = ref (Globrevtab.empty : globrevtab)
type mprevtab = dir_path MPmap.t
let the_modrevtab = ref (MPmap.empty : mprevtab)
type knrevtab = section_path KNmap.t
let the_modtyperevtab = ref (KNmap.empty : knrevtab)
(* Push functions *********************************************************)
(* This is for permanent constructions (never discharged -- but with
possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
Parameter but also Remark and Fact) *)
let push_xref visibility sp xref =
the_ccitab := SpTab.push visibility sp xref !the_ccitab;
match visibility with
| Until _ ->
the_globrevtab := Globrevtab.add xref sp !the_globrevtab
| _ -> ()
let push_cci visibility sp ref =
push_xref visibility sp (TrueGlobal ref)
(* This is for Syntactic Definitions *)
let push_syntactic_definition visibility sp kn =
push_xref visibility sp (SyntacticDef kn)
let push = push_cci
let push_modtype vis sp kn =
the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab
(* This is for dischargeable non-cci objects (removed at the end of the
section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
let push_object visibility sp =
the_objtab := SpTab.push visibility sp () !the_objtab
(* This is for tactic definition names *)
let push_tactic = push_object
(* This is to remember absolute Section/Module names and to avoid redundancy *)
let push_dir vis dir dir_ref =
the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
match dir_ref with
DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab
| _ -> ()
(* Locate functions *******************************************************)
(* This should be used when syntactic definitions are allowed *)
let extended_locate qid = SpTab.locate qid !the_ccitab
(* This should be used when no syntactic definitions is expected *)
let locate qid = match extended_locate qid with
| TrueGlobal ref -> ref
| SyntacticDef _ -> raise Not_found
let full_name_cci qid = SpTab.user_name qid !the_ccitab
let locate_syntactic_definition qid = match extended_locate qid with
| TrueGlobal _ -> raise Not_found
| SyntacticDef kn -> kn
let locate_modtype qid = SpTab.locate qid !the_modtypetab
let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
let locate_obj qid = SpTab.user_name qid !the_objtab
type ltac_constant = section_path
let locate_tactic = locate_obj
let shortest_qualid_of_tactic sp =
SpTab.shortest_qualid Idset.empty sp !the_objtab
let locate_dir qid = DirTab.locate qid !the_dirtab
let locate_module qid =
match locate_dir qid with
| DirModule (_,(mp,_)) -> mp
| _ -> raise Not_found
let full_name_module qid =
match locate_dir qid with
| DirModule (dir,_) -> dir
| _ -> raise Not_found
let locate_section qid =
match locate_dir qid with
| DirOpenSection (dir, _)
| DirClosedSection dir -> dir
| _ -> raise Not_found
(* Derived functions *)
let locate_constant qid =
match extended_locate qid with
| TrueGlobal (ConstRef kn) -> kn
| _ -> raise Not_found
let locate_mind qid =
match extended_locate qid with
| TrueGlobal (IndRef (kn,0)) -> kn
| _ -> raise Not_found
let absolute_reference sp =
match SpTab.find sp !the_ccitab with
| TrueGlobal ref -> ref
| _ -> raise Not_found
let locate_in_absolute_module dir id =
absolute_reference (make_path dir id)
let global r =
let (loc,qid) = qualid_of_reference r in
try match extended_locate qid with
| TrueGlobal ref -> ref
| SyntacticDef _ ->
user_err_loc (loc,"global",
str "Unexpected reference to a syntactic definition: " ++
pr_qualid qid)
with Not_found ->
error_global_not_found_loc loc qid
(* Exists functions ********************************************************)
let exists_cci sp = SpTab.exists sp !the_ccitab
let exists_dir dir = DirTab.exists dir !the_dirtab
let exists_section = exists_dir
let exists_module = exists_dir
let exists_modtype sp = SpTab.exists sp !the_modtypetab
(* Reverse locate functions ***********************************************)
let sp_of_global ref =
match ref with
| VarRef id -> make_path empty_dirpath id
| _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
let id_of_global ref =
let (_,id) = repr_path (sp_of_global ref) in
id
let sp_of_syntactic_definition kn =
Globrevtab.find (SyntacticDef kn) !the_globrevtab
let dir_of_mp mp =
MPmap.find mp !the_modrevtab
(* Shortest qualid functions **********************************************)
let shortest_qualid_of_global ctx ref =
match ref with
| VarRef id -> make_qualid empty_dirpath id
| _ ->
let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
SpTab.shortest_qualid ctx sp !the_ccitab
let shortest_qualid_of_syndef kn =
let sp = sp_of_syntactic_definition kn in
SpTab.shortest_qualid Idset.empty sp !the_ccitab
let shortest_qualid_of_module mp =
let dir = MPmap.find mp !the_modrevtab in
DirTab.shortest_qualid Idset.empty dir !the_dirtab
let shortest_qualid_of_modtype kn =
let sp = KNmap.find kn !the_modtyperevtab in
SpTab.shortest_qualid Idset.empty sp !the_modtypetab
let pr_global_env env ref =
(* Il est important de laisser le let-in, car les streams s'évaluent
paresseusement : il faut forcer l'évaluation pour capturer
l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
let s = string_of_qualid (shortest_qualid_of_global env ref) in
(str s)
let global_inductive r =
match global r with
| IndRef ind -> ind
| ref ->
user_err_loc (loc_of_reference r,"global_inductive",
pr_reference r ++ spc () ++ str "is not an inductive type")
(********************************************************************)
(********************************************************************)
(* Registration of tables as a global table and rollback *)
type frozen = ccitab * dirtab * objtab * kntab
* globrevtab * mprevtab * knrevtab
let init () =
the_ccitab := SpTab.empty;
the_dirtab := DirTab.empty;
the_objtab := SpTab.empty;
the_modtypetab := SpTab.empty;
the_globrevtab := Globrevtab.empty;
the_modrevtab := MPmap.empty;
the_modtyperevtab := KNmap.empty
let freeze () =
!the_ccitab,
!the_dirtab,
!the_objtab,
!the_modtypetab,
!the_globrevtab,
!the_modrevtab,
!the_modtyperevtab
let unfreeze (mc,md,mo,mt,gt,mrt,mtrt) =
the_ccitab := mc;
the_dirtab := md;
the_objtab := mo;
the_modtypetab := mt;
the_globrevtab := gt;
the_modrevtab := mrt;
the_modtyperevtab := mtrt
let _ =
Summary.declare_summary "names"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
Summary.survive_section = false }
|