ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;
1 (* Title: Pure/General/name_space.ML
2 Author: Markus Wenzel, TU Muenchen
4 Generic name spaces with declared and hidden entries. Unknown names
5 are considered global; no support for absolute addressing.
8 type xstring = string; (*external names*)
10 signature NAME_SPACE =
12 val hidden: string -> string
13 val is_hidden: string -> bool
15 val empty: string -> T
16 val kind_of: T -> string
17 val the_entry: T -> string ->
18 {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
19 val entry_ord: T -> string * string -> order
20 val markup: T -> string -> Markup.T
21 val is_concealed: T -> string -> bool
22 val intern: T -> xstring -> string
23 val names_long_default: bool Unsynchronized.ref
24 val names_long_raw: Config.raw
25 val names_long: bool Config.T
26 val names_short_default: bool Unsynchronized.ref
27 val names_short_raw: Config.raw
28 val names_short: bool Config.T
29 val names_unique_default: bool Unsynchronized.ref
30 val names_unique_raw: Config.raw
31 val names_unique: bool Config.T
32 val extern: Proof.context -> T -> string -> xstring
33 val hide: bool -> string -> T -> T
36 val default_naming: naming
37 val conceal: naming -> naming
38 val get_group: naming -> serial option
39 val set_group: serial option -> naming -> naming
40 val set_theory_name: string -> naming -> naming
41 val new_group: naming -> naming
42 val reset_group: naming -> naming
43 val add_path: string -> naming -> naming
44 val root_path: naming -> naming
45 val parent_path: naming -> naming
46 val mandatory_path: string -> naming -> naming
47 val qualified_path: bool -> binding -> naming -> naming
48 val transform_binding: naming -> binding -> binding
49 val full_name: naming -> binding -> string
50 val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
51 val alias: naming -> binding -> string -> T -> T
52 type 'a table = T * 'a Symtab.table
53 val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
54 val get: 'a table -> string -> 'a
55 val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
56 val empty_table: string -> 'a table
57 val merge_tables: 'a table * 'a table -> 'a table
58 val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
59 'a table * 'a table -> 'a table
60 val dest_table: Proof.context -> 'a table -> (string * 'a) list
61 val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
64 structure Name_Space: NAME_SPACE =
72 fun hidden name = "??." ^ name;
73 val is_hidden = String.isPrefix "??.";
85 fun entry_markup def kind (name, {pos, id, ...}: entry) =
88 if def then (Markup.defN, string_of_int id) :: Position.properties_of pos
89 else (Markup.refN, string_of_int id) :: Position.def_properties_of pos;
90 in Markup.properties props (Markup.entity kind name) end;
92 fun print_entry def kind (name, entry) =
93 quote (Markup.markup (entry_markup def kind (name, entry)) name);
95 fun err_dup kind entry1 entry2 =
96 error ("Duplicate " ^ kind ^ " declaration " ^
97 print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
99 fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
107 internals: (string list * string list) Symtab.table, (*visible, hidden*)
108 entries: (xstring list * entry) Symtab.table}; (*externals, entry*)
110 fun make_name_space (kind, internals, entries) =
111 Name_Space {kind = kind, internals = internals, entries = entries};
113 fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
114 make_name_space (f (kind, internals, entries));
116 fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
117 (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
120 fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
122 fun kind_of (Name_Space {kind, ...}) = kind;
124 fun the_entry (Name_Space {kind, entries, ...}) name =
125 (case Symtab.lookup entries name of
126 NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
127 | SOME (_, entry) => entry);
129 fun entry_ord space = int_ord o pairself (#id o the_entry space);
131 fun markup (Name_Space {kind, entries, ...}) name =
132 (case Symtab.lookup entries name of
133 NONE => Markup.hilite
134 | SOME (_, entry) => entry_markup false kind (name, entry));
136 fun is_concealed space name = #concealed (the_entry space name);
141 fun lookup (Name_Space {internals, ...}) xname =
142 (case Symtab.lookup internals xname of
143 NONE => (xname, true)
144 | SOME ([], []) => (xname, true)
145 | SOME ([name], _) => (name, true)
146 | SOME (name :: _, _) => (name, false)
147 | SOME ([], name' :: _) => (hidden name', true));
149 fun get_accesses (Name_Space {entries, ...}) name =
150 (case Symtab.lookup entries name of
152 | SOME (externals, _) => externals);
154 fun valid_accesses (Name_Space {internals, ...}) name =
155 Symtab.fold (fn (xname, (names, _)) =>
156 if not (null names) andalso hd names = name then cons xname else I) internals [];
159 (* intern and extern *)
161 fun intern space xname = #1 (lookup space xname);
164 val names_long_default = Unsynchronized.ref false;
165 val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
166 val names_long = Config.bool names_long_raw;
168 val names_short_default = Unsynchronized.ref false;
169 val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
170 val names_short = Config.bool names_short_raw;
172 val names_unique_default = Unsynchronized.ref true;
173 val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
174 val names_unique = Config.bool names_unique_raw;
176 fun extern ctxt space name =
178 val names_long = Config.get ctxt names_long;
179 val names_short = Config.get ctxt names_short;
180 val names_unique = Config.get ctxt names_unique;
182 fun valid require_unique xname =
183 let val (name', is_unique) = lookup space xname
184 in name = name' andalso (not require_unique orelse is_unique) end;
186 fun ext [] = if valid false name then name else hidden name
187 | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
189 if names_long then name
190 else if names_short then Long_Name.base_name name
191 else ext (get_accesses space name)
195 (* modify internals *)
197 val del_name = map_internals o apfst o remove (op =);
198 fun del_name_extra name =
199 map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
200 val add_name = map_internals o apfst o update (op =);
201 val add_name' = map_internals o apsnd o update (op =);
206 fun hide fully name space =
207 if not (Long_Name.is_qualified name) then
208 error ("Attempt to hide global name " ^ quote name)
209 else if is_hidden name then
210 error ("Attempt to hide hidden name " ^ quote name)
212 let val names = valid_accesses space name in
214 |> add_name' name name
215 |> fold (del_name name)
216 (if fully then names else inter (op =) [Long_Name.base_name name] names)
217 |> fold (del_name_extra name) (get_accesses space name)
224 (Name_Space {kind = kind1, internals = internals1, entries = entries1},
225 Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
228 if kind1 = kind2 then kind1
229 else error ("Attempt to merge different kinds of name spaces " ^
230 quote kind1 ^ " vs. " ^ quote kind2);
231 val internals' = (internals1, internals2) |> Symtab.join
232 (K (fn ((names1, names1'), (names2, names2')) =>
233 if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
234 then raise Symtab.SAME
235 else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
236 val entries' = (entries1, entries2) |> Symtab.join
237 (fn name => fn ((_, entry1), (_, entry2)) =>
238 if #id entry1 = #id entry2 then raise Symtab.SAME
239 else err_dup kind' (name, entry1) (name, entry2));
240 in make_name_space (kind', internals', entries') end;
244 (** naming contexts **)
246 (* datatype naming *)
248 datatype naming = Naming of
250 group: serial option,
252 path: (string * bool) list};
254 fun make_naming (conceal, group, theory_name, path) =
255 Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
257 fun map_naming f (Naming {conceal, group, theory_name, path}) =
258 make_naming (f (conceal, group, theory_name, path));
260 fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
261 (conceal, group, theory_name, f path));
264 val default_naming = make_naming (false, NONE, "", []);
266 val conceal = map_naming (fn (_, group, theory_name, path) =>
267 (true, group, theory_name, path));
269 fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
270 (conceal, group, theory_name, path));
273 fun get_group (Naming {group, ...}) = group;
275 fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
276 (conceal, group, theory_name, path));
278 fun new_group naming = set_group (SOME (serial ())) naming;
279 val reset_group = set_group NONE;
281 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
282 val root_path = map_path (fn _ => []);
283 val parent_path = map_path (perhaps (try (#1 o split_last)));
284 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
286 fun qualified_path mandatory binding = map_path (fn path =>
287 path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
292 fun err_bad binding = error (Binding.bad binding);
294 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
295 | transform_binding _ = I;
297 fun name_spec (naming as Naming {path, ...}) raw_binding =
299 val binding = transform_binding naming raw_binding;
300 val (concealed, prefix, name) = Binding.dest binding;
301 val _ = Long_Name.is_qualified name andalso err_bad binding;
303 val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
304 val spec2 = if name = "" then [] else [(name, true)];
305 val spec = spec1 @ spec2;
307 exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
308 andalso err_bad binding;
309 in (concealed, if null spec2 then [] else spec) end;
311 fun full_name naming =
312 name_spec naming #> #2 #> map #1 #> Long_Name.implode;
317 fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
319 fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
320 and mandatory_prefixes1 [] = []
321 | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
322 | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
324 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
326 fun accesses naming binding =
328 val spec = #2 (name_spec naming binding);
329 val sfxs = mandatory_suffixes spec;
330 val pfxs = mandatory_prefixes spec;
331 in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
336 fun new_entry strict (name, (externals, entry)) =
337 map_name_space (fn (kind, internals, entries) =>
340 (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
341 handle Symtab.DUP dup =>
342 err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
343 in (kind, internals, entries') end);
345 fun declare ctxt strict naming binding space =
347 val Naming {group, theory_name, ...} = naming;
348 val (concealed, spec) = name_spec naming binding;
349 val (accs, accs') = accesses naming binding;
351 val name = Long_Name.implode (map fst spec);
352 val _ = name = "" andalso err_bad binding;
354 val pos = Position.default (Binding.pos_of binding);
356 {concealed = concealed,
358 theory_name = theory_name,
362 |> fold (add_name name) accs
363 |> new_entry strict (name, (accs', entry));
364 val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
365 in (name, space') end;
370 fun alias naming binding name space =
372 val (accs, accs') = accesses naming binding;
374 |> fold (add_name name) accs
375 |> map_name_space (fn (kind, internals, entries) =>
377 val _ = Symtab.defined entries name orelse error (undefined kind name);
378 val entries' = entries
379 |> Symtab.map_entry name (fn (externals, entry) =>
380 (Library.merge (op =) (externals, accs'), entry))
381 in (kind, internals, entries') end);
386 (** name space coupled with symbol table **)
388 type 'a table = T * 'a Symtab.table;
390 fun check ctxt (space, tab) (xname, pos) =
391 let val name = intern space xname in
392 (case Symtab.lookup tab name of
393 SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
394 | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
397 fun get (space, tab) name =
398 (case Symtab.lookup tab name of
400 | NONE => error (undefined (kind_of space) name));
402 fun define ctxt strict naming (binding, x) (space, tab) =
403 let val (name, space') = declare ctxt strict naming binding space
404 in (name, (space', Symtab.update (name, x) tab)) end;
406 fun empty_table kind = (empty kind, Symtab.empty);
408 fun merge_tables ((space1, tab1), (space2, tab2)) =
409 (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
411 fun join_tables f ((space1, tab1), (space2, tab2)) =
412 (merge (space1, space2), Symtab.join f (tab1, tab2));
414 fun ext_table ctxt (space, tab) =
415 Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
416 |> Library.sort_wrt (#2 o #1);
418 fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
419 fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);