src/Pure/General/name_space.ML
changeset 30233 6eb726e43ed1
parent 30222 4102bbf2af21
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 03 21:49:34 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 03 21:53:52 2009 +0100
     1.3 @@ -3,7 +3,6 @@
     1.4  
     1.5  Generic name spaces with declared and hidden entries.  Unknown names
     1.6  are considered global; no support for absolute addressing.
     1.7 -Cf. Pure/General/binding.ML
     1.8  *)
     1.9  
    1.10  type xstring = string;    (*external names*)
    1.11 @@ -48,12 +47,11 @@
    1.12    val qualified_names: naming -> naming
    1.13    val sticky_prefix: string -> naming -> naming
    1.14    type 'a table = T * 'a Symtab.table
    1.15 +  val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
    1.16    val empty_table: 'a table
    1.17 -  val bind: naming -> binding * 'a
    1.18 -    -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.19 -  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.20 -  val join_tables: (string -> 'a * 'a -> 'a)
    1.21 -    -> 'a table * 'a table -> 'a table
    1.22 +  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table  (*exception Symtab.DUP*)
    1.23 +  val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
    1.24 +    'a table * 'a table -> 'a table                                       (*exception Symtab.DUP*)
    1.25    val dest_table: 'a table -> (string * 'a) list
    1.26    val extern_table: 'a table -> (xstring * 'a) list
    1.27  end;
    1.28 @@ -124,28 +122,28 @@
    1.29  
    1.30  datatype T =
    1.31    NameSpace of
    1.32 -    ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
    1.33 -    (string list * stamp) Symtab.table;                    (*externals*)
    1.34 +    (string list * string list) Symtab.table *   (*internals, hidden internals*)
    1.35 +    string list Symtab.table;                    (*externals*)
    1.36  
    1.37  val empty = NameSpace (Symtab.empty, Symtab.empty);
    1.38  
    1.39  fun lookup (NameSpace (tab, _)) xname =
    1.40    (case Symtab.lookup tab xname of
    1.41      NONE => (xname, true)
    1.42 -  | SOME (([], []), _) => (xname, true)
    1.43 -  | SOME (([name], _), _) => (name, true)
    1.44 -  | SOME ((name :: _, _), _) => (name, false)
    1.45 -  | SOME (([], name' :: _), _) => (hidden name', true));
    1.46 +  | SOME ([], []) => (xname, true)
    1.47 +  | SOME ([name], _) => (name, true)
    1.48 +  | SOME (name :: _, _) => (name, false)
    1.49 +  | SOME ([], name' :: _) => (hidden name', true));
    1.50  
    1.51 -fun get_accesses (NameSpace (_, tab)) name =
    1.52 -  (case Symtab.lookup tab name of
    1.53 +fun get_accesses (NameSpace (_, xtab)) name =
    1.54 +  (case Symtab.lookup xtab name of
    1.55      NONE => [name]
    1.56 -  | SOME (xnames, _) => xnames);
    1.57 +  | SOME xnames => xnames);
    1.58  
    1.59  fun put_accesses name xnames (NameSpace (tab, xtab)) =
    1.60 -  NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
    1.61 +  NameSpace (tab, Symtab.update (name, xnames) xtab);
    1.62  
    1.63 -fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
    1.64 +fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
    1.65    if not (null names) andalso hd names = name then cons xname else I) tab [];
    1.66  
    1.67  
    1.68 @@ -183,8 +181,7 @@
    1.69  local
    1.70  
    1.71  fun map_space f xname (NameSpace (tab, xtab)) =
    1.72 -  NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
    1.73 -    (fn (entry, _) => (f entry, stamp ())) tab, xtab);
    1.74 +  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
    1.75  
    1.76  in
    1.77  
    1.78 @@ -217,15 +214,13 @@
    1.79  fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
    1.80    let
    1.81      val tab' = (tab1, tab2) |> Symtab.join
    1.82 -      (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
    1.83 -        if stamp1 = stamp2 then raise Symtab.SAME
    1.84 -        else
    1.85 -          ((Library.merge (op =) (names1, names2),
    1.86 -            Library.merge (op =) (names1', names2')), stamp ())));
    1.87 +      (K (fn names as ((names1, names1'), (names2, names2')) =>
    1.88 +        if pointer_eq names then raise Symtab.SAME
    1.89 +        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
    1.90      val xtab' = (xtab1, xtab2) |> Symtab.join
    1.91 -      (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
    1.92 -        if stamp1 = stamp2 then raise Symtab.SAME
    1.93 -        else (Library.merge (op =) (xnames1, xnames2), stamp ())));
    1.94 +      (K (fn xnames =>
    1.95 +        if pointer_eq xnames then raise Symtab.SAME
    1.96 +        else (Library.merge (op =) xnames)));
    1.97    in NameSpace (tab', xtab') end;
    1.98  
    1.99  
   1.100 @@ -277,32 +272,33 @@
   1.101    in fold mk_prefix end;
   1.102  
   1.103  
   1.104 -(* declarations *)
   1.105 +(* full name *)
   1.106 +
   1.107 +fun full (Naming (path, (qualify, _))) = qualify path;
   1.108  
   1.109 -fun full_internal (Naming (path, (qualify, _))) = qualify path;
   1.110 +fun full_name naming binding =
   1.111 +  let
   1.112 +    val (prefix, qualifier, bname) = Binding.dest binding;
   1.113 +    val naming' = apply_prefix (prefix @ qualifier) naming;
   1.114 +  in full naming' bname end;
   1.115 +
   1.116 +
   1.117 +(* declaration *)
   1.118  
   1.119 -fun declare_internal naming name space =
   1.120 -  if is_hidden name then
   1.121 -    error ("Attempt to declare hidden name " ^ quote name)
   1.122 -  else
   1.123 -    let
   1.124 -      val names = explode_name name;
   1.125 -      val _ = (null names orelse exists (fn s => s = "") names
   1.126 -          orelse exists_string (fn s => s = "\"") name) andalso
   1.127 -        error ("Bad name declaration " ^ quote name);
   1.128 -      val (accs, accs') = pairself (map implode_name) (accesses naming names);
   1.129 -    in space |> fold (add_name name) accs |> put_accesses name accs' end;
   1.130 +fun declare naming binding space =
   1.131 +  let
   1.132 +    val (prefix, qualifier, bname) = Binding.dest binding;
   1.133 +    val naming' = apply_prefix (prefix @ qualifier) naming;
   1.134 +    val name = full naming' bname;
   1.135 +    val names = explode_name name;
   1.136  
   1.137 -fun full_name naming b =
   1.138 -  let val (prefix, qualifier, bname) = Binding.dest b
   1.139 -  in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
   1.140 +    val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
   1.141 +        orelse exists_string (fn s => s = "\"") name) andalso
   1.142 +      error ("Bad name declaration " ^ quote (Binding.str_of binding));
   1.143  
   1.144 -fun declare bnaming b =
   1.145 -  let
   1.146 -    val (prefix, qualifier, bname) = Binding.dest b;
   1.147 -    val naming = apply_prefix (prefix @ qualifier) bnaming;
   1.148 -    val name = full_internal naming bname;
   1.149 -  in declare_internal naming name #> pair name end;
   1.150 +    val (accs, accs') = pairself (map implode_name) (accesses naming' names);
   1.151 +    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   1.152 +  in (name, space') end;
   1.153  
   1.154  
   1.155  
   1.156 @@ -310,12 +306,11 @@
   1.157  
   1.158  type 'a table = T * 'a Symtab.table;
   1.159  
   1.160 -val empty_table = (empty, Symtab.empty);
   1.161 +fun bind naming (binding, x) (space, tab) =
   1.162 +  let val (name, space') = declare naming binding space
   1.163 +  in (name, (space', Symtab.update_new (name, x) tab)) end;
   1.164  
   1.165 -fun bind naming (b, x) (space, tab) =
   1.166 -  let
   1.167 -    val (name, space') = declare naming b space;
   1.168 -  in (name, (space', Symtab.update_new (name, x) tab)) end;
   1.169 +val empty_table = (empty, Symtab.empty);
   1.170  
   1.171  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   1.172    (merge (space1, space2), Symtab.merge eq (tab1, tab2));