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
|
(* $Id$ *)
open Util
open Pp
open Names
open Libobject
open Declarations
open Term
type cci_table = global_reference Stringmap.t
type obj_table = (section_path * obj) Stringmap.t
type mod_table = (section_path * module_contents) Stringmap.t
and module_contents = Closed of cci_table * obj_table * mod_table
let empty =
Closed (Stringmap.empty, Stringmap.empty, Stringmap.empty)
let nametabs = ref (empty : module_contents)
let push_cci (Closed (ccitab, objtab, modtab)) s ref =
Closed (Stringmap.add s ref ccitab, objtab, modtab)
let push_obj (Closed (ccitab, objtab, modtab)) s obj =
Closed (ccitab, Stringmap.add s obj objtab, modtab)
let push_mod (Closed (ccitab, objtab, modtab)) s mc =
(* devrait pas mais ca plante en d�commentant la ligne ci-dessous *)
(* assert (not (Stringmap.mem s modtab)); *)
Closed (ccitab, objtab, Stringmap.add s mc modtab)
let push_tree push dir id o =
let rec search (Closed (ccitab, objtab, modtab) as tabs) pref = function
| id :: dir' ->
let sp, mc =
try Stringmap.find id modtab
with Not_found ->
let pref = List.rev pref in
let dir = if pref@[id] = coq_root then [] else pref in
(make_path dir (id_of_string id) CCI, empty)
in
Closed (ccitab, objtab,
Stringmap.add id (sp,search mc (id::pref) dir') modtab)
| [] ->
push tabs id o
in nametabs := search !nametabs [] dir
(* This pushes a name at the current level (for relative qualified use) *)
let push_cci_current = push_tree push_cci []
let push_obj_current = push_tree push_obj []
let push_mod_current = push_tree push_mod []
(* This pushes a name at the root level (for absolute access) *)
let push_cci_absolute = push_tree push_cci
let push_obj_absolute = push_tree push_obj
let push_mod_absolute = push_tree push_mod
(* These are entry points for new declarations at toplevel *)
(* Do not use with "open" since it pushes an absolute name too *)
let push sp ref =
let dir, s = repr_qualid (qualid_of_sp sp) in
push_cci_absolute dir s ref;
push_cci_current s ref
let push_object sp obj =
let dir, s = repr_qualid (qualid_of_sp sp) in
push_obj_absolute dir s (sp,obj);
push_obj_current s (sp,obj)
let push_module sp mc =
let dir, s = repr_qualid (qualid_of_sp sp) in
push_mod_absolute dir s (sp,mc);
if s = List.hd coq_root then
warning ("Cannot allow access to "^s^" by relative paths: it conflicts with the \nroot of Coq library")
else push_mod_current s (sp,mc)
(* These are entry points to locate names *)
(* If the name starts with the coq_root name, then it is an absolute name *)
let locate qid =
let (dir,id) = repr_qualid qid in
let rec search (Closed (ccitab,_,modtab)) = function
| id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
| [] -> Stringmap.find id ccitab
in search !nametabs dir
let locate_obj qid =
let (dir,id) = repr_qualid qid in
let rec search (Closed (_,objtab,modtab)) = function
| id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
| [] -> Stringmap.find id objtab
in search !nametabs dir
let locate_module qid =
let (dir,id) = repr_qualid qid in
let rec search (Closed (_,_,modtab)) = function
| id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
| [] -> Stringmap.find id modtab
in search !nametabs dir
let locate_constant qid =
match locate qid with
| ConstRef sp -> sp
| _ -> raise Not_found
let sp_of_id _ id = locate (make_qualid [] (string_of_id id))
let constant_sp_of_id id =
match locate (make_qualid [] (string_of_id id)) with
| ConstRef sp -> sp
| _ -> raise Not_found
(* These are entry points to make the contents of a module/section visible *)
(* in the current env (does not affect the absolute name space `coq_root') *)
let open_module_contents qid =
let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
Stringmap.iter push_cci_current ccitab;
(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
Stringmap.iter push_mod_current modtab
let rec rec_open_module_contents qid =
let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
Stringmap.iter push_cci_current ccitab;
(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
Stringmap.iter
(fun m (sp,_ as mt) ->
push_mod_current m mt;
rec_open_module_contents (qualid_of_sp sp))
modtab
let exists_cci sp =
try let _ = locate (qualid_of_sp sp) in true with Not_found -> false
(***********************************************)
(* Registration as a global table and rollback *)
let init () = nametabs := empty
type frozen = module_contents
let freeze () = !nametabs
let unfreeze mc = nametabs := mc
let _ =
Summary.declare_summary "names"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
Summary.survive_section = false }
let rollback f x =
let fs = freeze () in
try f x with e -> begin unfreeze fs; raise e end
|
