src/Pure/General/name_space.ML
changeset 25072 03f57b516e12
parent 24361 52a14669f9e9
child 25225 e638164593bf
     1.1 --- a/src/Pure/General/name_space.ML	Wed Oct 17 23:16:30 2007 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Oct 17 23:16:33 2007 +0200
     1.3 @@ -29,19 +29,15 @@
     1.4    val base: string -> string
     1.5    val qualifier: string -> string
     1.6    val map_base: (string -> string) -> string -> string
     1.7 -  val suffixes_prefixes: 'a list -> 'a list list
     1.8 -  val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
     1.9 -  val accesses: string -> string list
    1.10 -  val accesses': string -> string list
    1.11    type T
    1.12    val empty: T
    1.13 -  val valid_accesses: T -> string -> xstring list
    1.14    val intern: T -> xstring -> string
    1.15    val extern: T -> string -> xstring
    1.16    val hide: bool -> string -> T -> T
    1.17    val merge: T * T -> T
    1.18    type naming
    1.19    val path_of: naming -> string
    1.20 +  val external_names: naming -> string -> string list
    1.21    val full: naming -> bstring -> string
    1.22    val declare: naming -> string -> T -> T
    1.23    val default_naming: naming
    1.24 @@ -49,8 +45,6 @@
    1.25    val no_base_names: naming -> naming
    1.26    val qualified_names: naming -> naming
    1.27    val sticky_prefix: string -> naming -> naming
    1.28 -  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    1.29 -    naming -> naming
    1.30    type 'a table = T * 'a Symtab.table
    1.31    val empty_table: 'a table
    1.32    val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    1.33 @@ -93,7 +87,7 @@
    1.34        in implode_name (nth_map (length names - 1) f names) end;
    1.35  
    1.36  
    1.37 -(* accesses *)
    1.38 +(* standard accesses *)
    1.39  
    1.40  infixr 6 @@;
    1.41  fun ([] @@ yss) = []
    1.42 @@ -104,7 +98,7 @@
    1.43      val (xs, ws) = chop (length list - 1) list;
    1.44      val sfxs = suffixes xs @@ [ws];
    1.45      val pfxs = prefixes1 xs @@ [ws];
    1.46 -  in sfxs @ pfxs end;
    1.47 +  in (sfxs @ pfxs, sfxs) end;
    1.48  
    1.49  fun suffixes_prefixes_split i k list =
    1.50    let
    1.51 @@ -115,10 +109,7 @@
    1.52      val pfxs =
    1.53        prefixes1 xs @@ [ys @ ws] @
    1.54        [xs @ ys] @@ prefixes1 zs @@ [ws];
    1.55 -  in sfxs @ pfxs end;
    1.56 -
    1.57 -val accesses = map implode_name o suffixes_prefixes o explode_name;
    1.58 -val accesses' = map implode_name o Library.suffixes1 o explode_name;
    1.59 +  in (sfxs @ pfxs, sfxs) end;
    1.60  
    1.61  
    1.62  
    1.63 @@ -127,11 +118,13 @@
    1.64  (* datatype T *)
    1.65  
    1.66  datatype T =
    1.67 -  NameSpace of ((string list * string list) * stamp) Symtab.table;
    1.68 +  NameSpace of
    1.69 +    ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
    1.70 +    (string list * stamp) Symtab.table;                    (*externals*)
    1.71  
    1.72 -val empty = NameSpace Symtab.empty;
    1.73 +val empty = NameSpace (Symtab.empty, Symtab.empty);
    1.74  
    1.75 -fun lookup (NameSpace tab) xname =
    1.76 +fun lookup (NameSpace (tab, _)) xname =
    1.77    (case Symtab.lookup tab xname of
    1.78      NONE => (xname, true)
    1.79    | SOME (([], []), _) => (xname, true)
    1.80 @@ -139,7 +132,15 @@
    1.81    | SOME ((name :: _, _), _) => (name, false)
    1.82    | SOME (([], name' :: _), _) => (hidden name', true));
    1.83  
    1.84 -fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, ((names, _), _)) =>
    1.85 +fun get_accesses (NameSpace (_, tab)) name =
    1.86 +  (case Symtab.lookup tab name of
    1.87 +    NONE => [name]
    1.88 +  | SOME (xnames, _) => xnames);
    1.89 +
    1.90 +fun put_accesses name xnames (NameSpace (tab, xtab)) =
    1.91 +  NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
    1.92 +
    1.93 +fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
    1.94    if not (null names) andalso hd names = name then cons xname else I) tab [];
    1.95  
    1.96  
    1.97 @@ -162,23 +163,29 @@
    1.98    in
    1.99      if ! long_names then name
   1.100      else if ! short_names then base name
   1.101 -    else ex (accesses' name)
   1.102 +    else ex (get_accesses space name)
   1.103    end;
   1.104  
   1.105  
   1.106  (* basic operations *)
   1.107  
   1.108 -fun map_space f xname (NameSpace tab) =
   1.109 +local
   1.110 +
   1.111 +fun map_space f xname (NameSpace (tab, xtab)) =
   1.112    NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
   1.113 -    (fn (entry, _) => (f entry, stamp ())) tab);
   1.114 +    (fn (entry, _) => (f entry, stamp ())) tab, xtab);
   1.115  
   1.116  fun del (name: string) = remove (op =) name;
   1.117  fun add name names = name :: del name names;
   1.118  
   1.119 +in
   1.120 +
   1.121  val del_name = map_space o apfst o del;
   1.122  val add_name = map_space o apfst o add;
   1.123  val add_name' = map_space o apsnd o add;
   1.124  
   1.125 +end;
   1.126 +
   1.127  
   1.128  (* hide *)
   1.129  
   1.130 @@ -197,14 +204,21 @@
   1.131  
   1.132  (* merge *)
   1.133  
   1.134 -fun merge (NameSpace tab1, NameSpace tab2) =
   1.135 -  NameSpace ((tab1, tab2) |> Symtab.join
   1.136 -    (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
   1.137 -      if stamp1 = stamp2 then raise Symtab.SAME
   1.138 -      else
   1.139 -        ((Library.merge (op =) (names2, names1),
   1.140 -          Library.merge (op =) (names2', names1')), stamp ()))));
   1.141 +(* FIXME non-canonical merge order!? *)
   1.142  
   1.143 +fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   1.144 +  let
   1.145 +    val tab' = (tab1, tab2) |> Symtab.join
   1.146 +      (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
   1.147 +        if stamp1 = stamp2 then raise Symtab.SAME
   1.148 +        else
   1.149 +          ((Library.merge (op =) (names2, names1),
   1.150 +            Library.merge (op =) (names2', names1')), stamp ())));
   1.151 +    val xtab' = (xtab1, xtab2) |> Symtab.join
   1.152 +      (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
   1.153 +        if stamp1 = stamp2 then raise Symtab.SAME
   1.154 +        else (Library.merge (op =) (xnames2, xnames1), stamp ())));
   1.155 +  in NameSpace (tab', xtab') end;
   1.156  
   1.157  
   1.158  (** naming contexts **)
   1.159 @@ -212,16 +226,21 @@
   1.160  (* datatype naming *)
   1.161  
   1.162  datatype naming = Naming of
   1.163 -  string * ((string -> string -> string) * (string list -> string list list));
   1.164 +  string *                                                 (*path*)
   1.165 +  ((string -> string -> string) *                          (*qualify*)
   1.166 +   (string list -> string list list * string list list));  (*accesses*)
   1.167  
   1.168  fun path_of (Naming (path, _)) = path;
   1.169 +fun accesses (Naming (_, (_, accs))) = accs;
   1.170 +
   1.171 +fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
   1.172  
   1.173  
   1.174  (* declarations *)
   1.175  
   1.176  fun full (Naming (path, (qualify, _))) = qualify path;
   1.177  
   1.178 -fun declare (Naming (_, (_, accs))) name space =
   1.179 +fun declare naming name space =
   1.180    if is_hidden name then
   1.181      error ("Attempt to declare hidden name " ^ quote name)
   1.182    else
   1.183 @@ -230,7 +249,8 @@
   1.184        val _ = (null names orelse exists (fn s => s = "") names
   1.185            orelse exists_string (fn s => s = "\"") name) andalso
   1.186          error ("Bad name declaration " ^ quote name);
   1.187 -    in fold (add_name name) (map implode_name (accs names)) space end;
   1.188 +      val (accs, accs') = pairself (map implode_name) (accesses naming names);
   1.189 +    in space |> fold (add_name name) accs |> put_accesses name accs' end;
   1.190  
   1.191  
   1.192  (* manipulate namings *)
   1.193 @@ -250,7 +270,7 @@
   1.194    else Naming (append path elems, policy);
   1.195  
   1.196  fun no_base_names (Naming (path, (qualify, accs))) =
   1.197 -  Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
   1.198 +  Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
   1.199  
   1.200  fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   1.201  
   1.202 @@ -258,8 +278,6 @@
   1.203    Naming (append path prfx,
   1.204      (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
   1.205  
   1.206 -fun set_policy policy (Naming (path, _)) = Naming (path, policy);
   1.207 -
   1.208  
   1.209  
   1.210  (** name spaces coupled with symbol tables **)