18 sig |
18 sig |
19 include BASIC_NAME_SPACE |
19 include BASIC_NAME_SPACE |
20 val hidden: string -> string |
20 val hidden: string -> string |
21 val is_hidden: string -> bool |
21 val is_hidden: string -> bool |
22 type T |
22 type T |
23 val empty: T |
23 val empty: string -> T |
|
24 val kind_of: T -> string |
|
25 val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial} |
24 val intern: T -> xstring -> string |
26 val intern: T -> xstring -> string |
25 val extern: T -> string -> xstring |
27 val extern: T -> string -> xstring |
26 val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} -> |
28 val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} -> |
27 T -> string -> xstring |
29 T -> string -> xstring |
28 val hide: bool -> string -> T -> T |
30 val hide: bool -> string -> T -> T |
36 val root_path: naming -> naming |
38 val root_path: naming -> naming |
37 val parent_path: naming -> naming |
39 val parent_path: naming -> naming |
38 val mandatory_path: string -> naming -> naming |
40 val mandatory_path: string -> naming -> naming |
39 type 'a table = T * 'a Symtab.table |
41 type 'a table = T * 'a Symtab.table |
40 val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table |
42 val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table |
41 val empty_table: 'a table |
43 val empty_table: string -> 'a table |
42 val merge_tables: 'a table * 'a table -> 'a table |
44 val merge_tables: 'a table * 'a table -> 'a table |
43 val join_tables: |
45 val join_tables: |
44 (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table |
46 (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table |
45 val dest_table: 'a table -> (string * 'a) list |
47 val dest_table: 'a table -> (string * 'a) list |
46 val extern_table: 'a table -> (xstring * 'a) list |
48 val extern_table: 'a table -> (xstring * 'a) list |
64 {externals: xstring list, |
66 {externals: xstring list, |
65 is_system: bool, |
67 is_system: bool, |
66 pos: Position.T, |
68 pos: Position.T, |
67 id: serial}; |
69 id: serial}; |
68 |
70 |
69 fun make_entry (externals, is_system, pos, id) : entry = |
|
70 {externals = externals, is_system = is_system, pos = pos, id = id}; |
|
71 |
|
72 fun str_of_entry def (name, {pos, id, ...}: entry) = |
71 fun str_of_entry def (name, {pos, id, ...}: entry) = |
73 let |
72 let |
74 val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id); |
73 val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id); |
75 val props = occurrence :: Position.properties_of pos; |
74 val props = occurrence :: Position.properties_of pos; |
76 in Markup.markup (Markup.properties props (Markup.entity name)) name end; |
75 in Markup.markup (Markup.properties props (Markup.entity name)) name end; |
77 |
76 |
|
77 fun err_dup kind entry1 entry2 = |
|
78 error ("Duplicate " ^ kind ^ " declaration " ^ |
|
79 quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2)); |
|
80 |
78 |
81 |
79 (* datatype T *) |
82 (* datatype T *) |
80 |
83 |
81 datatype T = |
84 datatype T = |
82 Name_Space of |
85 Name_Space of |
83 (string list * string list) Symtab.table * (*internals, hidden internals*) |
86 {kind: string, |
84 entry Symtab.table; |
87 internals: (string list * string list) Symtab.table, (*visible, hidden*) |
85 |
88 entries: entry Symtab.table}; |
86 val empty = Name_Space (Symtab.empty, Symtab.empty); |
89 |
87 |
90 fun make_name_space (kind, internals, entries) = |
88 fun lookup (Name_Space (tab, _)) xname = |
91 Name_Space {kind = kind, internals = internals, entries = entries}; |
89 (case Symtab.lookup tab xname of |
92 |
|
93 fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) = |
|
94 make_name_space (f (kind, internals, entries)); |
|
95 |
|
96 fun map_internals f xname = map_name_space (fn (kind, internals, entries) => |
|
97 (kind, Symtab.map_default (xname, ([], [])) f internals, entries)); |
|
98 |
|
99 |
|
100 fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty); |
|
101 |
|
102 fun kind_of (Name_Space {kind, ...}) = kind; |
|
103 |
|
104 fun the_entry (Name_Space {kind, entries, ...}) name = |
|
105 (case Symtab.lookup entries name of |
|
106 NONE => error ("Unknown " ^ kind ^ " " ^ quote name) |
|
107 | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id}); |
|
108 |
|
109 |
|
110 (* name accesses *) |
|
111 |
|
112 fun lookup (Name_Space {internals, ...}) xname = |
|
113 (case Symtab.lookup internals xname of |
90 NONE => (xname, true) |
114 NONE => (xname, true) |
91 | SOME ([], []) => (xname, true) |
115 | SOME ([], []) => (xname, true) |
92 | SOME ([name], _) => (name, true) |
116 | SOME ([name], _) => (name, true) |
93 | SOME (name :: _, _) => (name, false) |
117 | SOME (name :: _, _) => (name, false) |
94 | SOME ([], name' :: _) => (hidden name', true)); |
118 | SOME ([], name' :: _) => (hidden name', true)); |
95 |
119 |
96 fun get_accesses (Name_Space (_, entries)) name = |
120 fun get_accesses (Name_Space {entries, ...}) name = |
97 (case Symtab.lookup entries name of |
121 (case Symtab.lookup entries name of |
98 NONE => [name] |
122 NONE => [name] |
99 | SOME {externals, ...} => externals); |
123 | SOME {externals, ...} => externals); |
100 |
124 |
101 fun valid_accesses (Name_Space (tab, _)) name = |
125 fun valid_accesses (Name_Space {internals, ...}) name = |
102 Symtab.fold (fn (xname, (names, _)) => |
126 Symtab.fold (fn (xname, (names, _)) => |
103 if not (null names) andalso hd names = name then cons xname else I) tab []; |
127 if not (null names) andalso hd names = name then cons xname else I) internals []; |
104 |
128 |
105 |
129 |
106 (* intern and extern *) |
130 (* intern and extern *) |
107 |
131 |
108 fun intern space xname = #1 (lookup space xname); |
132 fun intern space xname = #1 (lookup space xname); |
130 {long_names = ! long_names, |
154 {long_names = ! long_names, |
131 short_names = ! short_names, |
155 short_names = ! short_names, |
132 unique_names = ! unique_names} space name; |
156 unique_names = ! unique_names} space name; |
133 |
157 |
134 |
158 |
135 (* basic operations *) |
159 (* modify internals *) |
136 |
160 |
137 local |
161 val del_name = map_internals o apfst o remove (op =); |
138 |
162 fun del_name_extra name = |
139 fun map_space f xname (Name_Space (tab, entries)) = |
163 map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs)); |
140 Name_Space (Symtab.map_default (xname, ([], [])) f tab, entries); |
164 val add_name = map_internals o apfst o update (op =); |
141 |
165 val add_name' = map_internals o apsnd o update (op =); |
142 in |
|
143 |
|
144 val del_name = map_space o apfst o remove (op =); |
|
145 fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs)); |
|
146 val add_name = map_space o apfst o update (op =); |
|
147 val add_name' = map_space o apsnd o update (op =); |
|
148 |
|
149 end; |
|
150 |
166 |
151 |
167 |
152 (* hide *) |
168 (* hide *) |
153 |
169 |
154 fun hide fully name space = |
170 fun hide fully name space = |
166 end; |
182 end; |
167 |
183 |
168 |
184 |
169 (* merge *) |
185 (* merge *) |
170 |
186 |
171 fun merge (Name_Space (tab1, entries1), Name_Space (tab2, entries2)) = |
187 fun merge |
172 let |
188 (Name_Space {kind = kind1, internals = internals1, entries = entries1}, |
173 val tab' = (tab1, tab2) |> Symtab.join |
189 Name_Space {kind = kind2, internals = internals2, entries = entries2}) = |
|
190 let |
|
191 val kind' = |
|
192 if kind1 = kind2 then kind1 |
|
193 else error ("Attempt to merge different kinds of name spaces " ^ |
|
194 quote kind1 ^ " vs. " ^ quote kind2); |
|
195 val internals' = (internals1, internals2) |> Symtab.join |
174 (K (fn ((names1, names1'), (names2, names2')) => |
196 (K (fn ((names1, names1'), (names2, names2')) => |
175 if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') |
197 if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') |
176 then raise Symtab.SAME |
198 then raise Symtab.SAME |
177 else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2')))); |
199 else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2')))); |
178 val entries' = (entries1, entries2) |> Symtab.join |
200 val entries' = (entries1, entries2) |> Symtab.join |
179 (fn name => fn (entry1, entry2) => |
201 (fn name => fn (entry1, entry2) => |
180 if #id entry1 = #id entry2 then raise Symtab.SAME |
202 if #id entry1 = #id entry2 then raise Symtab.SAME |
181 else |
203 else err_dup kind' (name, entry1) (name, entry2)); |
182 error ("Duplicate declaration " ^ |
204 in make_name_space (kind', internals', entries') end; |
183 quote (str_of_entry true (name, entry1)) ^ " vs. " ^ |
|
184 quote (str_of_entry true (name, entry2)))); |
|
185 in Name_Space (tab', entries') end; |
|
186 |
205 |
187 |
206 |
188 |
207 |
189 (** naming contexts **) |
208 (** naming contexts **) |
190 |
209 |
243 fun external_names naming = #2 o accesses naming o Binding.qualified_name; |
262 fun external_names naming = #2 o accesses naming o Binding.qualified_name; |
244 |
263 |
245 |
264 |
246 (* declaration *) |
265 (* declaration *) |
247 |
266 |
248 fun new_entry strict entry (Name_Space (tab, entries)) = |
267 fun new_entry strict entry = |
249 let |
268 map_name_space (fn (kind, internals, entries) => |
250 val entries' = |
269 let |
251 (if strict then Symtab.update_new else Symtab.update) entry entries |
270 val entries' = |
252 handle Symtab.DUP _ => |
271 (if strict then Symtab.update_new else Symtab.update) entry entries |
253 error ("Duplicate declaration " ^ quote (str_of_entry true entry)); |
272 handle Symtab.DUP dup => |
254 in Name_Space (tab, entries') end; |
273 err_dup kind (dup, the (Symtab.lookup entries dup)) entry; |
|
274 in (kind, internals, entries') end); |
255 |
275 |
256 fun declare strict naming binding space = |
276 fun declare strict naming binding space = |
257 let |
277 let |
258 val names = full naming binding; |
278 val names = full naming binding; |
259 val name = Long_Name.implode names; |
279 val name = Long_Name.implode names; |
260 val _ = name = "" andalso err_bad binding; |
280 val _ = name = "" andalso err_bad binding; |
261 val (accs, accs') = accesses naming binding; |
281 val (accs, accs') = accesses naming binding; |
262 |
282 val entry = |
263 val is_system = false; (* FIXME *) |
283 {externals = accs', |
264 val entry = make_entry (accs', is_system, Binding.pos_of binding, serial ()); |
284 is_system = false, |
265 val space' = space |
285 pos = Binding.pos_of binding, |
266 |> fold (add_name name) accs |
286 id = serial ()}; |
267 |> new_entry strict (name, entry); |
287 val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry); |
268 in (name, space') end; |
288 in (name, space') end; |
269 |
289 |
270 |
290 |
271 |
291 |
272 (** name spaces coupled with symbol tables **) |
292 (** name spaces coupled with symbol tables **) |
275 |
295 |
276 fun define strict naming (binding, x) (space, tab) = |
296 fun define strict naming (binding, x) (space, tab) = |
277 let val (name, space') = declare strict naming binding space |
297 let val (name, space') = declare strict naming binding space |
278 in (name, (space', Symtab.update (name, x) tab)) end; |
298 in (name, (space', Symtab.update (name, x) tab)) end; |
279 |
299 |
280 val empty_table = (empty, Symtab.empty); |
300 fun empty_table kind = (empty kind, Symtab.empty); |
281 |
301 |
282 fun merge_tables ((space1, tab1), (space2, tab2)) = |
302 fun merge_tables ((space1, tab1), (space2, tab2)) = |
283 (merge (space1, space2), Symtab.merge (K true) (tab1, tab2)); |
303 (merge (space1, space2), Symtab.merge (K true) (tab1, tab2)); |
284 |
304 |
285 fun join_tables f ((space1, tab1), (space2, tab2)) = |
305 fun join_tables f ((space1, tab1), (space2, tab2)) = |