# HG changeset patch # User wenzelm # Date 1236113632 -3600 # Node ID 6eb726e43ed1d15fccc14b036fc39442aa2f8db4 # Parent 8f551a13ee99d23bc4aa59138c3a66249c2b4c47 eliminated internal stamp equality, replaced by bare-metal pointer_eq; misc tuning and polishing; diff -r 8f551a13ee99 -r 6eb726e43ed1 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Mar 03 21:49:34 2009 +0100 +++ b/src/Pure/General/name_space.ML Tue Mar 03 21:53:52 2009 +0100 @@ -3,7 +3,6 @@ Generic name spaces with declared and hidden entries. Unknown names are considered global; no support for absolute addressing. -Cf. Pure/General/binding.ML *) type xstring = string; (*external names*) @@ -48,12 +47,11 @@ val qualified_names: naming -> naming val sticky_prefix: string -> naming -> naming type 'a table = T * 'a Symtab.table + val bind: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*) val empty_table: 'a table - val bind: naming -> binding * 'a - -> 'a table -> string * 'a table (*exception Symtab.DUP*) - val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table - val join_tables: (string -> 'a * 'a -> 'a) - -> 'a table * 'a table -> 'a table + val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*) + val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) -> + 'a table * 'a table -> 'a table (*exception Symtab.DUP*) val dest_table: 'a table -> (string * 'a) list val extern_table: 'a table -> (xstring * 'a) list end; @@ -124,28 +122,28 @@ datatype T = NameSpace of - ((string list * string list) * stamp) Symtab.table * (*internals, hidden internals*) - (string list * stamp) Symtab.table; (*externals*) + (string list * string list) Symtab.table * (*internals, hidden internals*) + string list Symtab.table; (*externals*) val empty = NameSpace (Symtab.empty, Symtab.empty); fun lookup (NameSpace (tab, _)) xname = (case Symtab.lookup tab xname of NONE => (xname, true) - | SOME (([], []), _) => (xname, true) - | SOME (([name], _), _) => (name, true) - | SOME ((name :: _, _), _) => (name, false) - | SOME (([], name' :: _), _) => (hidden name', true)); + | SOME ([], []) => (xname, true) + | SOME ([name], _) => (name, true) + | SOME (name :: _, _) => (name, false) + | SOME ([], name' :: _) => (hidden name', true)); -fun get_accesses (NameSpace (_, tab)) name = - (case Symtab.lookup tab name of +fun get_accesses (NameSpace (_, xtab)) name = + (case Symtab.lookup xtab name of NONE => [name] - | SOME (xnames, _) => xnames); + | SOME xnames => xnames); fun put_accesses name xnames (NameSpace (tab, xtab)) = - NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab); + NameSpace (tab, Symtab.update (name, xnames) xtab); -fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) => +fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) => if not (null names) andalso hd names = name then cons xname else I) tab []; @@ -183,8 +181,7 @@ local fun map_space f xname (NameSpace (tab, xtab)) = - NameSpace (Symtab.map_default (xname, (([], []), stamp ())) - (fn (entry, _) => (f entry, stamp ())) tab, xtab); + NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab); in @@ -217,15 +214,13 @@ fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) = let val tab' = (tab1, tab2) |> Symtab.join - (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) => - if stamp1 = stamp2 then raise Symtab.SAME - else - ((Library.merge (op =) (names1, names2), - Library.merge (op =) (names1', names2')), stamp ()))); + (K (fn names as ((names1, names1'), (names2, names2')) => + if pointer_eq names then raise Symtab.SAME + else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2')))); val xtab' = (xtab1, xtab2) |> Symtab.join - (K (fn ((xnames1, stamp1), (xnames2, stamp2)) => - if stamp1 = stamp2 then raise Symtab.SAME - else (Library.merge (op =) (xnames1, xnames2), stamp ()))); + (K (fn xnames => + if pointer_eq xnames then raise Symtab.SAME + else (Library.merge (op =) xnames))); in NameSpace (tab', xtab') end; @@ -277,32 +272,33 @@ in fold mk_prefix end; -(* declarations *) +(* full name *) + +fun full (Naming (path, (qualify, _))) = qualify path; -fun full_internal (Naming (path, (qualify, _))) = qualify path; +fun full_name naming binding = + let + val (prefix, qualifier, bname) = Binding.dest binding; + val naming' = apply_prefix (prefix @ qualifier) naming; + in full naming' bname end; + + +(* declaration *) -fun declare_internal naming name space = - if is_hidden name then - error ("Attempt to declare hidden name " ^ quote name) - else - let - val names = explode_name name; - val _ = (null names orelse exists (fn s => s = "") names - orelse exists_string (fn s => s = "\"") name) andalso - error ("Bad name declaration " ^ quote name); - val (accs, accs') = pairself (map implode_name) (accesses naming names); - in space |> fold (add_name name) accs |> put_accesses name accs' end; +fun declare naming binding space = + let + val (prefix, qualifier, bname) = Binding.dest binding; + val naming' = apply_prefix (prefix @ qualifier) naming; + val name = full naming' bname; + val names = explode_name name; -fun full_name naming b = - let val (prefix, qualifier, bname) = Binding.dest b - in full_internal (apply_prefix (prefix @ qualifier) naming) bname end; + val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names + orelse exists_string (fn s => s = "\"") name) andalso + error ("Bad name declaration " ^ quote (Binding.str_of binding)); -fun declare bnaming b = - let - val (prefix, qualifier, bname) = Binding.dest b; - val naming = apply_prefix (prefix @ qualifier) bnaming; - val name = full_internal naming bname; - in declare_internal naming name #> pair name end; + val (accs, accs') = pairself (map implode_name) (accesses naming' names); + val space' = space |> fold (add_name name) accs |> put_accesses name accs'; + in (name, space') end; @@ -310,12 +306,11 @@ type 'a table = T * 'a Symtab.table; -val empty_table = (empty, Symtab.empty); +fun bind naming (binding, x) (space, tab) = + let val (name, space') = declare naming binding space + in (name, (space', Symtab.update_new (name, x) tab)) end; -fun bind naming (b, x) (space, tab) = - let - val (name, space') = declare naming b space; - in (name, (space', Symtab.update_new (name, x) tab)) end; +val empty_table = (empty, Symtab.empty); fun merge_tables eq ((space1, tab1), (space2, tab2)) = (merge (space1, space2), Symtab.merge eq (tab1, tab2));