Source file nametab.ml
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
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
open Names
open Libnames
open Globnames
module GlobDirRef = struct
type t =
| DirOpenModule of ModPath.t
| DirOpenModtype of ModPath.t
| DirOpenSection of full_path
let equal r1 r2 = match r1, r2 with
| DirOpenModule op1, DirOpenModule op2 -> ModPath.equal op1 op2
| DirOpenModtype op1, DirOpenModtype op2 -> ModPath.equal op1 op2
| DirOpenSection op1, DirOpenSection op2 -> eq_full_path op1 op2
| (DirOpenModule _ | DirOpenModtype _ | DirOpenSection _), _ -> false
let compare r1 r2 = match r1, r2 with
| DirOpenModule op1, DirOpenModule op2 -> ModPath.compare op1 op2
| DirOpenModule _, _ -> -1
| _, DirOpenModule _ -> 1
| DirOpenModtype op1, DirOpenModtype op2 -> ModPath.compare op1 op2
| DirOpenModtype _, _ -> -1
| _, DirOpenModtype _ -> 1
| DirOpenSection op1, DirOpenSection op2 -> compare_full_path op1 op2
end
exception GlobalizationError of qualid
let error_global_not_found ~info qid =
let info = Option.cata (Loc.add_loc info) info qid.CAst.loc in
Exninfo.iraise (GlobalizationError qid, info)
type visibility = Until of int | Exactly of int
let map_visibility f = function
| Until i -> Until (f i)
| Exactly i -> Exactly (f i)
module type EqualityType =
sig
type t
val equal : t -> t -> bool
end
module type NAMETREE = sig
type elt
type t
val empty : t
val push : visibility -> full_path -> elt -> t -> t
val locate : qualid -> t -> elt
val find : full_path -> t -> elt
val remove : full_path -> t -> t
val exists : full_path -> t -> bool
val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> full_path -> t -> qualid
val find_prefixes : qualid -> t -> elt list
(** Matches a prefix of [qualid], useful for completion *)
val match_prefixes : qualid -> t -> elt list
end
let masking_absolute = CWarnings.create_warning
~from:[Deprecation.Version.v8_8] ~name:"masking-absolute-name" ()
let coq_id = Id.of_string "Coq"
let stdlib_id = Id.of_string "Stdlib"
let corelib_id = Id.of_string "Corelib"
let warn_deprecated_dirpath_Coq =
CWarnings.create_with_quickfix ~name:"deprecated-dirpath-Coq"
~category:Deprecation.Version.v9_0
(fun (old_id, new_id) ->
Pp.(old_id ++ spc () ++ str "has been replaced by" ++ spc () ++ new_id ++ str "."))
let fix_coq_id coq_repl l =
(match l with
| _coq_id :: l -> coq_repl :: l
| _ -> l)
let warn_deprecated_dirpath_Coq ?loc (coq_repl, l, id) =
let dp l = DirPath.make (List.rev l) in
let old_id = pr_qualid @@ Libnames.make_qualid (DirPath.make l) id in
let new_id = pr_qualid @@ Libnames.make_qualid (dp @@ fix_coq_id coq_repl (List.rev l)) id in
let quickfix = Option.map (fun loc -> [ Quickfix.make ~loc new_id ]) loc in
warn_deprecated_dirpath_Coq ?loc ?quickfix (old_id, new_id)
module Make (E : EqualityType) : NAMETREE
with type elt = E.t =
struct
type elt = E.t
let warn_masking_absolute =
CWarnings.create_in masking_absolute
Pp.(fun n -> str "Trying to mask the absolute name \"" ++ pr_path n ++ str "\"!")
type path_status =
| Relative of full_path * elt
| Absolute of full_path * elt
let eq_path_status p q = match p, q with
| Relative (u1, o1), Relative (u2, o2) -> eq_full_path u1 u2 && E.equal o1 o2
| Absolute (u1, o1), Absolute (u2, o2) -> eq_full_path u1 u2 && E.equal o1 o2
| (Absolute _ | Relative _), _ -> false
type nametree =
{ path : path_status list;
map : nametree Id.Map.t }
let push_path arg path = match path with
| [] -> [arg]
| arg' :: _ -> if eq_path_status arg arg' then path else arg :: path
let mktree p m = { path=p; map=m }
let empty_tree = mktree [] Id.Map.empty
let is_empty_tree tree = tree.path = [] && Id.Map.is_empty tree.map
type t = nametree Id.Map.t
let empty = Id.Map.empty
let rec push_until uname o level tree = function
| modid :: path ->
let modify _ mc = push_until uname o (level-1) mc path in
let map =
try Id.Map.modify modid modify tree.map
with Not_found ->
let ptab = modify () empty_tree in
Id.Map.add modid ptab tree.map
in
let this =
if level <= 0 then
match tree.path with
| Absolute (n,_)::_ ->
warn_masking_absolute n; tree.path
| current -> push_path (Relative (uname, o)) current
else tree.path
in
if this == tree.path && map == tree.map then tree
else mktree this map
| [] ->
match tree.path with
| Absolute (uname',o') :: _ ->
if E.equal o' o then begin
assert (eq_full_path uname uname');
tree
end
else
CErrors.user_err
Pp.(str "Cannot mask the absolute name \"" ++ pr_path uname' ++ str "\"!")
| current ->
let this = push_path (Absolute (uname, o)) current in
if this == tree.path then tree
else mktree this tree.map
let rec push_exactly uname o level tree = function
| [] ->
CErrors.anomaly (Pp.str "Prefix longer than path! Impossible!")
| modid :: path ->
if Int.equal level 0 then
let this =
match tree.path with
| Absolute (n,_) :: _ ->
warn_masking_absolute n; tree.path
| current -> push_path (Relative (uname, o)) current
in
if this == tree.path then tree
else mktree this tree.map
else
let modify _ mc = push_exactly uname o (level-1) mc path in
let map =
try Id.Map.modify modid modify tree.map
with Not_found ->
let ptab = modify () empty_tree in
Id.Map.add modid ptab tree.map
in
if map == tree.map then tree
else mktree tree.path map
let push visibility uname o tab =
let dir,id = repr_path uname in
let dir = DirPath.repr dir in
let modify _ 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
try Id.Map.modify id modify tab
with Not_found ->
let ptab = modify () empty_tree in
Id.Map.add id ptab tab
(** [remove_path uname tree dir] removes all bindings pointing to
[uname] along the path [dir] in [tree] (i.e. all such bindings are
assumed to be on this path) *)
let rec remove_path uname tree = function
| modid :: path ->
let update = function
| None -> None
| Some mc ->
let mc = remove_path uname mc path in
if is_empty_tree mc then None else Some mc
in
let map = Id.Map.update modid update tree.map in
let this =
let test = function Relative (uname',_) -> not (eq_full_path uname uname') | _ -> true in
List.filter test tree.path
in
mktree this map
| [] ->
let this =
let test = function Absolute (uname',_) -> not (eq_full_path uname uname') | _ -> true in
List.filter test tree.path
in
mktree this tree.map
(** Remove all bindings pointing to [uname] in [tab] *)
let remove uname tab =
let dir,id = repr_path uname in
let dir = DirPath.repr dir in
let modify _ ptab = remove_path uname ptab dir in
try Id.Map.modify id modify tab
with Not_found -> tab
let rec search tree = function
| modid :: path ->
begin match Id.Map.find_opt modid tree.map with
| None -> None
| Some modid -> search modid path
end
| [] -> Some tree.path
let search ?loc id tree dir =
let dirs = match List.rev dir with
| last :: l when Id.equal last coq_id ->
[ (Some stdlib_id, List.rev (stdlib_id :: l));
(Some corelib_id, List.rev (corelib_id :: l)) ]
| _ -> [ None, dir ]
in
let search_one (warn, dir) =
match search tree dir with
| Some v -> Some (warn, v)
| None -> None
in
match List.find_map search_one dirs with
| Some (coq_repl, p) ->
Option.iter (fun coq_repl -> warn_deprecated_dirpath_Coq ?loc (coq_repl, dir, id)) coq_repl;
p
| None -> raise Not_found
let find_node qid tab =
let loc = qid.CAst.loc in
let (dir,id) = repr_qualid qid in
search ?loc id (Id.Map.find id tab) (DirPath.repr dir)
let locate qid tab =
let o = match find_node qid tab with
| (Absolute (uname,o) | Relative (uname,o)) :: _ -> o
| [] -> raise Not_found
in
o
let find uname tab =
let l,id = repr_path uname in
let l = DirPath.repr l in
match search id (Id.Map.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_gen ?loc hidden uname tab =
let dir,id = repr_path uname in
let dir = DirPath.repr dir in
let hidden = hidden id in
let rec find_uname pos dir tree =
let is_empty = match pos with [] -> true | _ -> false in
match tree.path with
| (Absolute (u,_) | Relative (u,_)) :: _
when eq_full_path u uname && not (is_empty && hidden) -> List.rev pos
| _ ->
match dir with
[] -> raise Not_found
| id::dir -> find_uname (id::pos) dir (Id.Map.find id tree.map)
in
let ptab = Id.Map.find id tab in
let found_dir = find_uname [] dir ptab in
make_qualid ?loc (DirPath.make found_dir) id
let push_node node l =
match node with
| (Absolute (_,o) | Relative (_,o)) :: _
when not (Util.List.mem_f E.equal o l) -> o::l
| _ -> l
let rec flatten_tree tree l =
let f _ tree l = flatten_tree tree l in
Id.Map.fold f tree.map (push_node tree.path l)
let rec search_prefixes tree = function
| modid :: path -> search_prefixes (Id.Map.find modid tree.map) path
| [] -> List.rev (flatten_tree tree [])
let find_prefixes qid tab =
try
let (dir,id) = repr_qualid qid in
search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
with Not_found -> []
let match_prefixes =
let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in
fun qid tab ->
try
let (dir,id) = repr_qualid qid in
let id_prefix = cprefix Id.(to_string id) in
let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in
let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in
CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches [])
with Not_found -> []
end
module type NAMETAB_gen = sig
type 'a read_tab
type write_tab
type elt
val push : visibility -> full_path -> elt -> write_tab
val remove : full_path -> elt -> write_tab
val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> elt -> qualid read_tab
val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> elt -> qualid read_tab
val pr : elt -> Pp.t read_tab
val locate : qualid -> elt read_tab
val locate_all : qualid -> elt list read_tab
val completion_candidates : qualid -> elt list read_tab
val to_path : elt -> full_path read_tab
val of_path : full_path -> elt read_tab
val exists : full_path -> bool read_tab
end
module type ValueType = sig
include EqualityType
val is_var : t -> Id.t option
module Map : CSig.UMapS with type key = t
end
module type WarnInfo = sig
type elt
type data
module Map : CSig.UMapS with type key = elt
val stage : Summary.Stage.t
val summary_name : string
val warn : ?loc:Loc.t -> elt -> data -> unit
end
module type Functional_NAMETAB = sig
type t
val empty : t
include NAMETAB_gen with type 'a read_tab := t -> 'a and type write_tab := t -> t
end
module MakeTab (E:ValueType) : Functional_NAMETAB with type elt = E.t = struct
type elt = E.t
module Tab = Make(E)
type t = {
tab : Tab.t;
revtab : full_path E.Map.t;
}
let empty = {
tab = Tab.empty;
revtab = E.Map.empty;
}
let push vis sp v { tab; revtab } =
match vis with
| Until _ ->
{
tab = Tab.push vis sp v tab;
revtab = E.Map.add v sp revtab;
}
| Exactly _ ->
{
tab = Tab.push vis sp v tab;
revtab;
}
let remove sp v { tab; revtab } =
{
tab = Tab.remove sp tab;
revtab = E.Map.remove v revtab;
}
let shortest_qualid_gen ?loc avoid v { tab; revtab } =
match E.is_var v with
| Some id -> make_qualid ?loc DirPath.empty id
| None ->
let sp = E.Map.find v revtab in
Tab.shortest_qualid_gen ?loc avoid sp tab
let shortest_qualid ?loc avoid v tabs =
shortest_qualid_gen ?loc (fun id -> Id.Set.mem id avoid) v tabs
let pr v tab = pr_qualid (shortest_qualid Id.Set.empty v tab)
let locate qid { tab } = Tab.locate qid tab
let locate_all qid { tab } = Tab.find_prefixes qid tab
let completion_candidates qid { tab } = Tab.match_prefixes qid tab
let to_path v { revtab } = match E.is_var v with
| Some id -> make_path DirPath.empty id
| None -> E.Map.find v revtab
let of_path sp { tab } = Tab.find sp tab
let exists sp { tab } = Tab.exists sp tab
end
module type NAMETAB = NAMETAB_gen with type 'a read_tab := 'a and type write_tab := unit
module type StateInfo = sig
val stage : Summary.Stage.t
val summary_name : string
end
module MakeImperative (Tab:Functional_NAMETAB) (SI:StateInfo) ()
: NAMETAB with type elt = Tab.elt
= struct
type elt = Tab.elt
let the_tab = Summary.ref ~stage:SI.stage ~name:SI.summary_name Tab.empty
let push vis sp v = the_tab := Tab.push vis sp v !the_tab
let remove sp v = the_tab := Tab.remove sp v !the_tab
let shortest_qualid_gen ?loc f v = Tab.shortest_qualid_gen ?loc f v !the_tab
let shortest_qualid ?loc avoid v = Tab.shortest_qualid ?loc avoid v !the_tab
let pr v = Tab.pr v !the_tab
let locate qid = Tab.locate qid !the_tab
let locate_all qid = Tab.locate_all qid !the_tab
let completion_candidates qid = Tab.completion_candidates qid !the_tab
let to_path v = Tab.to_path v !the_tab
let of_path v = Tab.of_path v !the_tab
let exists v = Tab.exists v !the_tab
end
module type WarnedTab = sig
include NAMETAB
type warning_data
val push : ?wdata:warning_data -> visibility -> full_path -> elt -> unit
val is_warned : elt -> warning_data option
val warn : ?loc:Loc.t -> elt -> warning_data -> unit
val locate : ?nowarn:bool -> qualid -> elt
end
module MakeWarned (M:NAMETAB)
(W:WarnInfo with type elt = M.elt)
()
: WarnedTab with type elt = M.elt and type warning_data := W.data
= struct
include M
let warntab = Summary.ref ~stage:W.stage ~name:W.summary_name W.Map.empty
let push ?wdata vis sp elt =
M.push vis sp elt;
match wdata with
| None -> ()
| Some wdata ->
let () = match vis with
| Until _ -> ()
| Exactly _ -> assert false
in
warntab := W.Map.add elt wdata !warntab
let remove sp elt =
M.remove sp elt;
warntab := W.Map.remove elt !warntab
let is_warned elt = W.Map.find_opt elt !warntab
let warn = W.warn
let locate ?(nowarn=false) qid =
let elt = M.locate qid in
let () = if nowarn then ()
else match is_warned elt with
| None -> ()
| Some wdata -> warn ?loc:qid.loc elt wdata
in
elt
end
module EasyNoWarn (M:sig include ValueType include StateInfo end) () =
MakeImperative(MakeTab(M))(M)()
module type SimpleWarnS = sig
val object_name : string
val warning_name_base : string
end
module Easy (M:sig include ValueType include StateInfo include SimpleWarnS end) () = struct
module I = EasyNoWarn(M)()
module WInfo = struct
type elt = M.t
type data = elt UserWarn.with_qf
module Map = M.Map
let stage = M.stage
let summary_name = M.summary_name ^ "-warnings"
let warn = UserWarn.create_depr_and_user_warnings_qf
~object_name:M.object_name ~warning_name_base:M.warning_name_base
~pp_qf:I.pr I.pr
()
end
include MakeWarned(I)(WInfo)()
end
module XRefV = struct
include ExtRefOrdered
let is_var = function
| TrueGlobal (VarRef id) -> Some id
| _ -> None
module Map = ExtRefMap
let stage = Summary.Stage.Interp
let summary_name = "xreftab"
end
module XRefNoWarn = EasyNoWarn(XRefV)()
module XRefWarn = struct
type elt = extended_global_reference
type data = elt UserWarn.with_qf
module Map = ExtRefMap
let pp = XRefNoWarn.pr
let depr_ref = Deprecation.create_warning_with_qf ~object_name:"Reference" ~warning_name_if_no_since:"deprecated-reference" ~pp_qf:pp pp
let depr_abbrev = Deprecation.create_warning_with_qf ~object_name:"Notation" ~warning_name_if_no_since:"deprecated-syntactic-definition" ~pp_qf:pp pp
let user_warn = UserWarn.create_warning ~warning_name_if_no_cats:"warn-reference" ()
let depr_xref ?loc depr xref =
match xref with
| TrueGlobal _ -> depr_ref ?loc (xref,depr)
| Abbrev _ -> depr_abbrev ?loc (xref,depr)
let warn ?loc xref uwarns =
uwarns.UserWarn.depr_qf |> Option.iter (fun depr -> depr_xref ?loc depr xref);
uwarns.UserWarn.warn_qf |> List.iter (user_warn ?loc)
let stage = Summary.Stage.Interp
let summary_name = "xrefwarntab"
end
module XRefs = MakeWarned(XRefNoWarn)(XRefWarn)()
module UnivsV = struct
include Univ.UGlobal
let is_var _ = None
module Map = HMap.Make(Univ.UGlobal)
let stage = Summary.Stage.Interp
let summary_name = "univtab"
end
module Univs = EasyNoWarn(UnivsV)()
module QualityV = struct
include Sorts.QGlobal
let is_var _ = None
module Map = HMap.Make(Sorts.QGlobal)
let stage = Summary.Stage.Interp
let summary_name = "sorttab"
end
module Quality = EasyNoWarn(QualityV)()
module ModTypeV = struct
include ModPath
let is_var _ = None
module Map = MPmap
let stage = Summary.Stage.Synterp
let summary_name = "modtypetab"
end
module ModTypes = EasyNoWarn(ModTypeV)()
module ModuleV = struct
include ModPath
let is_var _ = None
module Map = MPmap
let stage = Summary.Stage.Synterp
let summary_name = "moduletab"
end
module Modules = EasyNoWarn(ModuleV)()
module OpenModV = struct
include GlobDirRef
let is_var _ = None
module Map = Map.Make(GlobDirRef)
let stage = Summary.Stage.Synterp
let summary_name = "openmodtab"
end
module OpenMods = EasyNoWarn(OpenModV)()
let push_abbreviation ?user_warns visibility sp kn =
XRefs.push ?wdata:user_warns visibility sp (Abbrev kn)
let remove_abbreviation sp kn =
XRefs.remove sp (Abbrev kn)
let push ?user_warns vis sp kn = XRefs.push ?wdata:user_warns vis sp (TrueGlobal kn)
let push_modtype vis sp kn = ModTypes.push vis sp kn
let push_module vis dir mp = Modules.push vis dir mp
let push_dir vis dir dir_ref = OpenMods.push vis dir dir_ref
let push_universe vis sp univ = Univs.push vis sp univ
let path_of_global ref = XRefs.to_path (TrueGlobal ref)
let dirpath_of_global ref =
fst (repr_path (path_of_global ref))
let basename_of_global ref =
snd (repr_path (path_of_global ref))
let path_of_abbreviation kn = XRefs.to_path (Abbrev kn)
let path_of_module mp = Modules.to_path mp
let path_of_modtype mp = ModTypes.to_path mp
let path_of_universe mp = Univs.to_path mp
let shortest_qualid_of_global ?loc ctx ref = XRefs.shortest_qualid ?loc ctx (TrueGlobal ref)
let shortest_qualid_of_abbreviation ?loc ctx kn = XRefs.shortest_qualid ?loc ctx (Abbrev kn)
let shortest_qualid_of_module ?loc mp = Modules.shortest_qualid ?loc Id.Set.empty mp
let shortest_qualid_of_modtype ?loc kn = ModTypes.shortest_qualid ?loc Id.Set.empty kn
let shortest_qualid_of_dir ?loc sp = OpenMods.shortest_qualid ?loc Id.Set.empty sp
let shortest_qualid_of_universe ?loc avoid u =
Univs.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id avoid) u
let pr_global_env env ref =
try pr_qualid (shortest_qualid_of_global env ref)
with Not_found as exn ->
let exn, info = Exninfo.capture exn in
if !Flags.in_debugger then GlobRef.print ref
else begin
let () = if CDebug.(get_flag misc)
then Feedback.msg_debug (Pp.str "pr_global_env not found")
in
Exninfo.iraise (exn, info)
end
let is_warned_xref = XRefs.is_warned
let warn_user_warn_xref ?loc wdata x = XRefs.warn ?loc x wdata
let locate_extended_nowarn qid = XRefs.locate ~nowarn:true qid
let locate_extended qid = XRefs.locate qid
let locate qid = match locate_extended qid with
| TrueGlobal ref -> ref
| Abbrev _ -> raise Not_found
let locate_abbreviation qid = match locate_extended qid with
| TrueGlobal _ -> raise Not_found
| Abbrev kn -> kn
let locate_modtype qid = ModTypes.locate qid
let full_name_modtype qid = ModTypes.to_path (locate_modtype qid)
let locate_universe qid = Univs.locate qid
let locate_dir qid = OpenMods.locate qid
let locate_module qid = Modules.locate qid
let full_name_module qid = Modules.to_path (locate_module qid)
let full_name_open_mod qid = OpenMods.to_path (locate_dir qid)
let locate_section qid =
match locate_dir qid with
| GlobDirRef.DirOpenSection dir -> dir
| _ -> raise Not_found
let locate_extended_all qid = XRefs.locate_all qid
let locate_all qid =
let l = locate_extended_all qid in
CList.filter_map (function TrueGlobal a -> Some a | Abbrev _ -> None) l
let locate_extended_all_dir qid = OpenMods.locate_all qid
let locate_extended_all_modtype qid = ModTypes.locate_all qid
let locate_extended_all_module qid = Modules.locate_all qid
let completion_canditates qualid = XRefs.completion_candidates qualid
let locate_constant qid =
let open GlobRef in
match locate_extended qid with
| TrueGlobal (ConstRef kn) -> kn
| _ -> raise Not_found
let global_of_path sp =
match XRefs.of_path sp with
| TrueGlobal ref -> ref
| _ -> raise Not_found
let extended_global_of_path = XRefs.of_path
let global qid =
try match locate_extended qid with
| TrueGlobal ref -> ref
| Abbrev _ ->
CErrors.user_err ?loc:qid.CAst.loc
Pp.(str "Unexpected reference to a notation: " ++
pr_qualid qid ++ str ".")
with Not_found as exn ->
let _, info = Exninfo.capture exn in
error_global_not_found ~info qid
let global_inductive qid =
let open GlobRef in
match global qid with
| IndRef ind -> ind
| ref ->
CErrors.user_err ?loc:qid.CAst.loc
Pp.(pr_qualid qid ++ spc () ++ str "is not an inductive type.")
let exists_cci = XRefs.exists
let exists_dir = OpenMods.exists
let exists_module = Modules.exists
let exists_modtype = ModTypes.exists
let exists_universe = Univs.exists
open Globnames
let cci_loc_table : Loc.t ExtRefMap.t ref = Summary.ref ~name:"constant-loc-table" ExtRefMap.empty
let set_cci_src_loc kn loc = cci_loc_table := ExtRefMap.add kn loc !cci_loc_table
let cci_src_loc kn = ExtRefMap.find_opt kn !cci_loc_table