1(* Title: Pure/General/name_space.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Generic name spaces with declared and hidden entries; no support for 5absolute addressing. 6*) 7 8type xstring = string; (*external names*) 9 10signature NAME_SPACE = 11sig 12 type T 13 val empty: string -> T 14 val kind_of: T -> string 15 val markup: T -> string -> Markup.T 16 val markup_def: T -> string -> Markup.T 17 val the_entry: T -> string -> 18 {concealed: bool, 19 group: serial option, 20 theory_long_name: string, 21 pos: Position.T, 22 serial: serial} 23 val the_entry_theory_name: T -> string -> string 24 val entry_ord: T -> string ord 25 val is_concealed: T -> string -> bool 26 val intern: T -> xstring -> string 27 val names_long: bool Config.T 28 val names_short: bool Config.T 29 val names_unique: bool Config.T 30 val extern: Proof.context -> T -> string -> xstring 31 val extern_ord: Proof.context -> T -> string ord 32 val extern_shortest: Proof.context -> T -> string -> xstring 33 val markup_extern: Proof.context -> T -> string -> Markup.T * xstring 34 val pretty: Proof.context -> T -> string -> Pretty.T 35 val completion: Context.generic -> T -> (string -> bool) -> xstring * Position.T -> Completion.T 36 val merge: T * T -> T 37 type naming 38 val get_scopes: naming -> Binding.scope list 39 val get_scope: naming -> Binding.scope option 40 val new_scope: naming -> Binding.scope * naming 41 val restricted: bool -> Position.T -> naming -> naming 42 val private_scope: Binding.scope -> naming -> naming 43 val private: Position.T -> naming -> naming 44 val qualified_scope: Binding.scope -> naming -> naming 45 val qualified: Position.T -> naming -> naming 46 val concealed: naming -> naming 47 val get_group: naming -> serial option 48 val set_group: serial option -> naming -> naming 49 val set_theory_long_name: string -> naming -> naming 50 val new_group: naming -> naming 51 val reset_group: naming -> naming 52 val add_path: string -> naming -> naming 53 val root_path: naming -> naming 54 val parent_path: naming -> naming 55 val mandatory_path: string -> naming -> naming 56 val qualified_path: bool -> binding -> naming -> naming 57 val global_naming: naming 58 val local_naming: naming 59 val transform_naming: naming -> naming -> naming 60 val transform_binding: naming -> binding -> binding 61 val full_name: naming -> binding -> string 62 val base_name: binding -> string 63 val hide: bool -> string -> T -> T 64 val alias: naming -> binding -> string -> T -> T 65 val naming_of: Context.generic -> naming 66 val map_naming: (naming -> naming) -> Context.generic -> Context.generic 67 val declared: T -> string -> bool 68 val declare: Context.generic -> bool -> binding -> T -> string * T 69 type 'a table 70 val change_base: bool -> 'a table -> 'a table 71 val change_ignore: 'a table -> 'a table 72 val space_of_table: 'a table -> T 73 val check_reports: Context.generic -> 'a table -> 74 xstring * Position.T list -> (string * Position.report list) * 'a 75 val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a 76 val defined: 'a table -> string -> bool 77 val lookup: 'a table -> string -> 'a option 78 val lookup_key: 'a table -> string -> (string * 'a) option 79 val get: 'a table -> string -> 'a 80 val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table 81 val alias_table: naming -> binding -> string -> 'a table -> 'a table 82 val hide_table: bool -> string -> 'a table -> 'a table 83 val del_table: string -> 'a table -> 'a table 84 val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table 85 val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b 86 val dest_table: 'a table -> (string * 'a) list 87 val empty_table: string -> 'a table 88 val merge_tables: 'a table * 'a table -> 'a table 89 val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) -> 90 'a table * 'a table -> 'a table 91 val extern_entries: bool -> Proof.context -> T -> (string * 'a) list -> 92 ((string * xstring) * 'a) list 93 val markup_entries: bool -> Proof.context -> T -> (string * 'a) list -> 94 ((Markup.T * xstring) * 'a) list 95 val extern_table: bool -> Proof.context -> 'a table -> ((string * xstring) * 'a) list 96 val markup_table: bool -> Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list 97end; 98 99structure Name_Space: NAME_SPACE = 100struct 101 102 103(** name spaces **) 104 105(* datatype entry *) 106 107type entry = 108 {concealed: bool, 109 group: serial option, 110 theory_long_name: string, 111 pos: Position.T, 112 serial: serial}; 113 114fun entry_markup def kind (name, {pos, serial, ...}: entry) = 115 Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name); 116 117fun print_entry_ref kind (name, entry) = 118 quote (Markup.markup (entry_markup false kind (name, entry)) name); 119 120fun err_dup kind entry1 entry2 pos = 121 error ("Duplicate " ^ plain_words kind ^ " declaration " ^ 122 print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos); 123 124 125(* internal names *) 126 127type internals = (string list * string list) Change_Table.T; (*xname -> visible, hidden*) 128 129fun map_internals f xname : internals -> internals = 130 Change_Table.map_default (xname, ([], [])) f; 131 132val del_name = map_internals o apfst o remove (op =); 133fun del_name_extra name = 134 map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs)); 135val add_name = map_internals o apfst o update (op =); 136fun hide_name name = map_internals (apsnd (update (op =) name)) name; 137 138 139(* external accesses *) 140 141type accesses = (xstring list * xstring list); (*input / output fragments*) 142type entries = (accesses * entry) Change_Table.T; (*name -> accesses, entry*) 143 144 145(* datatype T *) 146 147datatype T = Name_Space of {kind: string, internals: internals, entries: entries}; 148 149fun make_name_space (kind, internals, entries) = 150 Name_Space {kind = kind, internals = internals, entries = entries}; 151 152fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) = 153 make_name_space (f (kind, internals, entries)); 154 155fun change_base_space begin = map_name_space (fn (kind, internals, entries) => 156 (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries)); 157 158val change_ignore_space = map_name_space (fn (kind, internals, entries) => 159 (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries)); 160 161 162fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty); 163 164fun kind_of (Name_Space {kind, ...}) = kind; 165 166fun gen_markup def (Name_Space {kind, entries, ...}) name = 167 (case Change_Table.lookup entries name of 168 NONE => Markup.intensify 169 | SOME (_, entry) => entry_markup def kind (name, entry)); 170 171val markup = gen_markup false; 172val markup_def = gen_markup true; 173 174fun undefined (space as Name_Space {kind, entries, ...}) bad = 175 let 176 val (prfx, sfx) = 177 (case Long_Name.dest_hidden bad of 178 SOME name => 179 if Change_Table.defined entries name 180 then ("Inaccessible", Markup.markup (markup space name) (quote name)) 181 else ("Undefined", quote name) 182 | NONE => ("Undefined", quote bad)); 183 in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end; 184 185fun the_entry (space as Name_Space {entries, ...}) name = 186 (case Change_Table.lookup entries name of 187 NONE => error (undefined space name) 188 | SOME (_, entry) => entry); 189 190fun the_entry_theory_name space name = 191 Long_Name.base_name (#theory_long_name (the_entry space name)); 192 193fun entry_ord space = int_ord o apply2 (#serial o the_entry space); 194 195fun is_concealed space name = 196 #concealed (the_entry space name) handle ERROR _ => false; 197 198 199(* intern *) 200 201fun intern' (Name_Space {internals, ...}) xname = 202 (case the_default ([], []) (Change_Table.lookup internals xname) of 203 ([name], _) => (name, true) 204 | (name :: _, _) => (name, false) 205 | ([], []) => (Long_Name.hidden xname, true) 206 | ([], name' :: _) => (Long_Name.hidden name', true)); 207 208val intern = #1 oo intern'; 209 210fun get_accesses (Name_Space {entries, ...}) name = 211 (case Change_Table.lookup entries name of 212 NONE => ([], []) 213 | SOME (accesses, _) => accesses); 214 215fun is_valid_access (Name_Space {internals, ...}) name xname = 216 (case Change_Table.lookup internals xname of 217 SOME (name' :: _, _) => name = name' 218 | _ => false); 219 220 221(* extern *) 222 223val names_long = Config.declare_option_bool ("names_long", \<^here>); 224val names_short = Config.declare_option_bool ("names_short", \<^here>); 225val names_unique = Config.declare_option_bool ("names_unique", \<^here>); 226 227fun extern ctxt space name = 228 let 229 val names_long = Config.get ctxt names_long; 230 val names_short = Config.get ctxt names_short; 231 val names_unique = Config.get ctxt names_unique; 232 233 fun valid require_unique xname = 234 let val (name', is_unique) = intern' space xname 235 in name = name' andalso (not require_unique orelse is_unique) end; 236 237 fun ext [] = if valid false name then name else Long_Name.hidden name 238 | ext (nm :: nms) = if valid names_unique nm then nm else ext nms; 239 in 240 if names_long then name 241 else if names_short then Long_Name.base_name name 242 else ext (#2 (get_accesses space name)) 243 end; 244 245fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space); 246 247fun extern_shortest ctxt = 248 extern 249 (ctxt 250 |> Config.put names_long false 251 |> Config.put names_short false 252 |> Config.put names_unique false); 253 254fun markup_extern ctxt space name = (markup space name, extern ctxt space name); 255fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name); 256 257 258(* completion *) 259 260fun completion context space pred (xname, pos) = 261 Completion.make (xname, pos) (fn completed => 262 let 263 fun result_ord ((pri1, (xname1, (_, name1))), (pri2, (xname2, (_, name2)))) = 264 (case int_ord (pri2, pri1) of 265 EQUAL => 266 (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of 267 EQUAL => 268 (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of 269 EQUAL => string_ord (xname1, xname2) 270 | ord => ord) 271 | ord => ord) 272 | ord => ord); 273 val Name_Space {kind, internals, ...} = space; 274 val ext = extern_shortest (Context.proof_of context) space; 275 val full = Name.clean xname = ""; 276 277 fun complete xname' name = 278 if (completed xname' orelse exists completed (Long_Name.explode xname')) andalso 279 not (is_concealed space name) andalso pred name 280 then 281 let 282 val xname'' = ext name; 283 val pri = (if xname' = xname'' then 1 else 0) + (if completed xname' then 1 else 0); 284 in 285 if xname' <> xname'' andalso full then I 286 else cons (pri, (xname', (kind, name))) 287 end 288 else I; 289 in 290 Change_Table.fold (fn (xname', (name :: _, _)) => complete xname' name | _ => I) internals [] 291 |> sort_distinct result_ord 292 |> map #2 293 end); 294 295 296(* merge *) 297 298fun merge 299 (Name_Space {kind = kind1, internals = internals1, entries = entries1}, 300 Name_Space {kind = kind2, internals = internals2, entries = entries2}) = 301 let 302 val kind' = 303 if kind1 = kind2 then kind1 304 else error ("Attempt to merge different kinds of name spaces " ^ 305 quote kind1 ^ " vs. " ^ quote kind2); 306 val internals' = (internals1, internals2) |> Change_Table.join 307 (K (fn ((names1, names1'), (names2, names2')) => 308 if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') 309 then raise Change_Table.SAME 310 else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2')))); 311 val entries' = (entries1, entries2) |> Change_Table.join 312 (fn name => fn ((_, entry1), (_, entry2)) => 313 if #serial entry1 = #serial entry2 then raise Change_Table.SAME 314 else err_dup kind' (name, entry1) (name, entry2) Position.none); 315 in make_name_space (kind', internals', entries') end; 316 317 318 319(** naming context **) 320 321(* datatype naming *) 322 323datatype naming = Naming of 324 {scopes: Binding.scope list, 325 restricted: (bool * Binding.scope) option, 326 concealed: bool, 327 group: serial option, 328 theory_long_name: string, 329 path: (string * bool) list}; 330 331fun make_naming (scopes, restricted, concealed, group, theory_long_name, path) = 332 Naming {scopes = scopes, restricted = restricted, concealed = concealed, 333 group = group, theory_long_name = theory_long_name, path = path}; 334 335fun map_naming f (Naming {scopes, restricted, concealed, group, theory_long_name, path}) = 336 make_naming (f (scopes, restricted, concealed, group, theory_long_name, path)); 337 338 339(* scope and access restriction *) 340 341fun get_scopes (Naming {scopes, ...}) = scopes; 342val get_scope = try hd o get_scopes; 343 344fun new_scope naming = 345 let 346 val scope = Binding.new_scope (); 347 val naming' = 348 naming |> map_naming (fn (scopes, restricted, concealed, group, theory_long_name, path) => 349 (scope :: scopes, restricted, concealed, group, theory_long_name, path)); 350 in (scope, naming') end; 351 352fun restricted_scope strict scope = 353 map_naming (fn (scopes, _, concealed, group, theory_long_name, path) => 354 (scopes, SOME (strict, scope), concealed, group, theory_long_name, path)); 355 356fun restricted strict pos naming = 357 (case get_scope naming of 358 SOME scope => restricted_scope strict scope naming 359 | NONE => error ("Missing local scope -- cannot restrict name space accesses" ^ Position.here pos)); 360 361val private_scope = restricted_scope true; 362val private = restricted true; 363 364val qualified_scope = restricted_scope false; 365val qualified = restricted false; 366 367val concealed = map_naming (fn (scopes, restricted, _, group, theory_long_name, path) => 368 (scopes, restricted, true, group, theory_long_name, path)); 369 370 371(* additional structural info *) 372 373fun set_theory_long_name theory_long_name = 374 map_naming (fn (scopes, restricted, concealed, group, _, path) => 375 (scopes, restricted, concealed, group, theory_long_name, path)); 376 377fun get_group (Naming {group, ...}) = group; 378 379fun set_group group = 380 map_naming (fn (scopes, restricted, concealed, _, theory_long_name, path) => 381 (scopes, restricted, concealed, group, theory_long_name, path)); 382 383fun new_group naming = set_group (SOME (serial ())) naming; 384val reset_group = set_group NONE; 385 386 387(* name entry path *) 388 389fun get_path (Naming {path, ...}) = path; 390 391fun map_path f = 392 map_naming (fn (scopes, restricted, concealed, group, theory_long_name, path) => 393 (scopes, restricted, concealed, group, theory_long_name, f path)); 394 395fun add_path elems = map_path (fn path => path @ [(elems, false)]); 396val root_path = map_path (fn _ => []); 397val parent_path = map_path (perhaps (try (#1 o split_last))); 398fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]); 399 400fun qualified_path mandatory binding = map_path (fn path => 401 path @ Binding.path_of (Binding.qualify_name mandatory binding "")); 402 403val global_naming = make_naming ([], NONE, false, NONE, "", []); 404val local_naming = global_naming |> add_path Long_Name.localN; 405 406 407(* transform *) 408 409fun transform_naming (Naming {restricted = restricted', concealed = concealed', ...}) = 410 (case restricted' of 411 SOME (strict, scope) => restricted_scope strict scope 412 | NONE => I) #> 413 concealed' ? concealed; 414 415fun transform_binding (Naming {restricted, concealed, ...}) = 416 Binding.restricted restricted #> 417 concealed ? Binding.concealed; 418 419 420(* full name *) 421 422fun name_spec naming binding = 423 Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding); 424 425fun full_name naming = 426 name_spec naming #> #spec #> map #1 #> Long_Name.implode; 427 428val base_name = full_name global_naming #> Long_Name.base_name; 429 430 431(* accesses *) 432 433fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs; 434 435fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs 436and mandatory_prefixes1 [] = [] 437 | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs) 438 | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs); 439 440fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs)); 441 442fun make_accesses naming binding = 443 (case name_spec naming binding of 444 {restriction = SOME true, ...} => ([], []) 445 | {restriction, spec, ...} => 446 let 447 val restrict = is_some restriction ? filter (fn [_] => false | _ => true); 448 val sfxs = restrict (mandatory_suffixes spec); 449 val pfxs = restrict (mandatory_prefixes spec); 450 in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end); 451 452 453(* hide *) 454 455fun hide fully name space = 456 space |> map_name_space (fn (kind, internals, entries) => 457 let 458 val _ = the_entry space name; 459 val (accs, accs') = get_accesses space name; 460 val xnames = filter (is_valid_access space name) accs; 461 val internals' = internals 462 |> hide_name name 463 |> fold (del_name name) 464 (if fully then xnames else inter (op =) [Long_Name.base_name name] xnames) 465 |> fold (del_name_extra name) accs'; 466 in (kind, internals', entries) end); 467 468 469(* alias *) 470 471fun alias naming binding name space = 472 space |> map_name_space (fn (kind, internals, entries) => 473 let 474 val _ = the_entry space name; 475 val (more_accs, more_accs') = make_accesses naming binding; 476 val internals' = internals |> fold (add_name name) more_accs; 477 val entries' = entries 478 |> Change_Table.map_entry name (apfst (fn (accs, accs') => 479 (fold_rev (update op =) more_accs accs, 480 fold_rev (update op =) more_accs' accs'))) 481 in (kind, internals', entries') end); 482 483 484 485(** context naming **) 486 487structure Data_Args = 488struct 489 type T = naming; 490 val empty = global_naming; 491 fun extend _ = global_naming; 492 fun merge _ = global_naming; 493 fun init _ = local_naming; 494end; 495 496structure Global_Naming = Theory_Data(Data_Args); 497structure Local_Naming = Proof_Data(Data_Args); 498 499fun naming_of (Context.Theory thy) = Global_Naming.get thy 500 | naming_of (Context.Proof ctxt) = Local_Naming.get ctxt; 501 502fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy) 503 | map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt); 504 505 506 507(** entry definition **) 508 509(* declaration *) 510 511fun declared (Name_Space {entries, ...}) = Change_Table.defined entries; 512 513fun declare context strict binding space = 514 let 515 val naming = naming_of context; 516 val Naming {group, theory_long_name, ...} = naming; 517 val {concealed, spec, ...} = name_spec naming binding; 518 val accesses = make_accesses naming binding; 519 520 val name = Long_Name.implode (map fst spec); 521 val _ = name = "" andalso error (Binding.bad binding); 522 523 val (proper_pos, pos) = Position.default (Binding.pos_of binding); 524 val entry = 525 {concealed = concealed, 526 group = group, 527 theory_long_name = theory_long_name, 528 pos = pos, 529 serial = serial ()}; 530 val space' = 531 space |> map_name_space (fn (kind, internals, entries) => 532 let 533 val internals' = internals |> fold (add_name name) (#1 accesses); 534 val entries' = 535 (if strict then Change_Table.update_new else Change_Table.update) 536 (name, (accesses, entry)) entries 537 handle Change_Table.DUP dup => 538 err_dup kind (dup, #2 (the (Change_Table.lookup entries dup))) 539 (name, entry) (#pos entry); 540 in (kind, internals', entries') end); 541 val _ = 542 if proper_pos andalso Context_Position.is_reported_generic context pos then 543 Position.report pos (entry_markup true (kind_of space) (name, entry)) 544 else (); 545 in (name, space') end; 546 547 548(* definition in symbol table *) 549 550datatype 'a table = Table of T * 'a Change_Table.T; 551 552fun change_base begin (Table (space, tab)) = 553 Table (change_base_space begin space, Change_Table.change_base begin tab); 554 555fun change_ignore (Table (space, tab)) = 556 Table (change_ignore_space space, Change_Table.change_ignore tab); 557 558fun space_of_table (Table (space, _)) = space; 559 560fun check_reports context (Table (space, tab)) (xname, ps) = 561 let val name = intern space xname in 562 (case Change_Table.lookup tab name of 563 SOME x => 564 let 565 val reports = 566 filter (Context_Position.is_reported_generic context) ps 567 |> map (fn pos => (pos, markup space name)); 568 in ((name, reports), x) end 569 | NONE => 570 error (undefined space name ^ Position.here_list ps ^ 571 Completion.markup_report 572 (map (fn pos => completion context space (K true) (xname, pos)) ps))) 573 end; 574 575fun check context table (xname, pos) = 576 let 577 val ((name, reports), x) = check_reports context table (xname, [pos]); 578 val _ = Position.reports reports; 579 in (name, x) end; 580 581fun defined (Table (_, tab)) name = Change_Table.defined tab name; 582fun lookup (Table (_, tab)) name = Change_Table.lookup tab name; 583fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name; 584 585fun get table name = 586 (case lookup_key table name of 587 SOME (_, x) => x 588 | NONE => error (undefined (space_of_table table) name)); 589 590fun define context strict (binding, x) (Table (space, tab)) = 591 let 592 val (name, space') = declare context strict binding space; 593 val tab' = Change_Table.update (name, x) tab; 594 in (name, Table (space', tab')) end; 595 596 597(* derived table operations *) 598 599fun alias_table naming binding name (Table (space, tab)) = 600 Table (alias naming binding name space, tab); 601 602fun hide_table fully name (Table (space, tab)) = 603 Table (hide fully name space, tab); 604 605fun del_table name (Table (space, tab)) = 606 let 607 val space' = hide true name space handle ERROR _ => space; 608 val tab' = Change_Table.delete_safe name tab; 609 in Table (space', tab') end; 610 611fun map_table_entry name f (Table (space, tab)) = 612 Table (space, Change_Table.map_entry name f tab); 613 614fun fold_table f (Table (_, tab)) = Change_Table.fold f tab; 615fun dest_table (Table (_, tab)) = Change_Table.dest tab; 616 617fun empty_table kind = Table (empty kind, Change_Table.empty); 618 619fun merge_tables (Table (space1, tab1), Table (space2, tab2)) = 620 Table (merge (space1, space2), Change_Table.merge (K true) (tab1, tab2)); 621 622fun join_tables f (Table (space1, tab1), Table (space2, tab2)) = 623 Table (merge (space1, space2), Change_Table.join f (tab1, tab2)); 624 625 626(* present table content *) 627 628fun extern_entries verbose ctxt space entries = 629 fold (fn (name, x) => 630 (verbose orelse not (is_concealed space name)) ? 631 cons ((name, extern ctxt space name), x)) entries [] 632 |> sort_by (#2 o #1); 633 634fun markup_entries verbose ctxt space entries = 635 extern_entries verbose ctxt space entries 636 |> map (fn ((name, xname), x) => ((markup space name, xname), x)); 637 638fun extern_table verbose ctxt (Table (space, tab)) = 639 extern_entries verbose ctxt space (Change_Table.dest tab); 640 641fun markup_table verbose ctxt (Table (space, tab)) = 642 markup_entries verbose ctxt space (Change_Table.dest tab); 643 644end; 645