renamed cond_extern to extern;
authorwenzelm
Tue May 31 11:53:28 2005 +0200 (2005-05-31)
changeset 1613700e9ca1e7261
parent 16136 1cb99d74eebb
child 16138 727c5e32930e
renamed cond_extern to extern;
append, base, drop_base, map_base: made robust against empty names;
added qualified;
extern: improved output for non-unique non-hidden names;
name entry path superceded by general naming context;
added reject_qualified, default_naming, add_path, no_base_names, custom_accesses, set_policy;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue May 31 11:53:27 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Tue May 31 11:53:28 2005 +0200
     1.3 @@ -2,39 +2,56 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Hierarchically structured name spaces.
     1.8 +Generic name spaces with declared and hidden entries.  Unknown names
     1.9 +are considered as global; no support for absolute addressing.
    1.10 +*)
    1.11 +
    1.12 +type bstring = string;    (*names to be bound / internalized*)
    1.13 +type xstring = string;    (*externalized names / to be printed*)
    1.14  
    1.15 -More general than ML-like nested structures, but also slightly more
    1.16 -ad-hoc.  Does not support absolute addressing.  Unknown names are
    1.17 -implicitely considered to be declared outermost.
    1.18 -*)
    1.19 +signature BASIC_NAME_SPACE =
    1.20 +sig
    1.21 +  val long_names: bool ref
    1.22 +  val short_names: bool ref
    1.23 +  val unique_names: bool ref
    1.24 +end;
    1.25  
    1.26  signature NAME_SPACE =
    1.27  sig
    1.28 -  val separator: string                 (*single char*)
    1.29 +  include BASIC_NAME_SPACE
    1.30    val hidden: string -> string
    1.31 -  val append: string -> string -> string
    1.32 +  val separator: string                 (*single char*)
    1.33 +  val is_qualified: string -> bool
    1.34 +  val pack: string list -> string
    1.35    val unpack: string -> string list
    1.36 -  val pack: string list -> string
    1.37 +  val append: string -> string -> string
    1.38 +  val qualified: string -> string -> string
    1.39    val base: string -> string
    1.40 +  val drop_base: string -> string
    1.41    val map_base: (string -> string) -> string -> string
    1.42 -  val is_qualified: string -> bool
    1.43 +  val suffixes_prefixes: 'a list -> 'a list list
    1.44    val accesses: string -> string list
    1.45    val accesses': string -> string list
    1.46    type T
    1.47    val empty: T
    1.48 -  val extend: T * string list -> T
    1.49 -  val extend': (string -> string list) -> T * string list -> T
    1.50 +  val valid_accesses: T -> string -> xstring list
    1.51 +  val intern: T -> xstring -> string
    1.52 +  val extern: T -> string -> xstring
    1.53 +  val extern_table: T -> 'a Symtab.table -> (xstring * 'a) list
    1.54 +  val hide: bool -> string -> T -> T
    1.55    val merge: T * T -> T
    1.56 -  val hide: bool -> T * string list -> T
    1.57 -  val intern: T -> string -> string
    1.58 -  val extern: T -> string -> string
    1.59 -  val long_names: bool ref
    1.60 -  val short_names: bool ref
    1.61 -  val unique_names: bool ref
    1.62 -  val cond_extern: T -> string -> string
    1.63 -  val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
    1.64 -  val dest: T -> (string * string list) list
    1.65 +  val dest: T -> (string * xstring list) list
    1.66 +  type naming
    1.67 +  val path_of: naming -> string
    1.68 +  val full: naming -> bstring -> string
    1.69 +  val declare: naming -> string -> T -> T
    1.70 +  val default_naming: naming
    1.71 +  val add_path: string -> naming -> naming
    1.72 +  val qualified_names: naming -> naming
    1.73 +  val no_base_names: naming -> naming
    1.74 +  val custom_accesses: (string list -> string list list) -> naming -> naming
    1.75 +  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    1.76 +    naming -> naming
    1.77  end;
    1.78  
    1.79  structure NameSpace: NAME_SPACE =
    1.80 @@ -42,52 +59,48 @@
    1.81  
    1.82  (** long identifiers **)
    1.83  
    1.84 +fun hidden name = "??." ^ name;
    1.85 +val is_hidden = String.isPrefix "??."
    1.86 +
    1.87  val separator = ".";
    1.88 -fun hidden name = "??." ^ name;
    1.89 -fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false);
    1.90 +val is_qualified = exists_string (equal separator);
    1.91  
    1.92 -fun append name1 name2 = name1 ^ separator ^ name2;
    1.93 -
    1.94 +val pack = space_implode separator;
    1.95  val unpack = space_explode separator;
    1.96 -val pack = space_implode separator;
    1.97  
    1.98 -val base = List.last o unpack;
    1.99 +fun append name1 "" = name1
   1.100 +  | append "" name2 = name2
   1.101 +  | append name1 name2 = name1 ^ separator ^ name2;
   1.102 +
   1.103 +fun qualified path name =
   1.104 +  if path = "" orelse name = "" then name
   1.105 +  else path ^ separator ^ name;
   1.106  
   1.107 -fun map_base f name =
   1.108 -  let val uname = unpack name
   1.109 -  in pack (map_nth_elem (length uname - 1) f uname) end;
   1.110 +fun base "" = ""
   1.111 +  | base name = List.last (unpack name);
   1.112  
   1.113 -fun is_qualified name = length (unpack name) > 1;
   1.114 +fun drop_base "" = ""
   1.115 +  | drop_base name = pack (#1 (split_last (unpack name)));
   1.116  
   1.117 -fun accesses name =
   1.118 +fun map_base _ "" = ""
   1.119 +  | map_base f name =
   1.120 +      let val names = unpack name
   1.121 +      in pack (map_nth_elem (length names - 1) f names) end;
   1.122 +
   1.123 +fun suffixes_prefixes xs =
   1.124    let
   1.125 -    val uname = unpack name;
   1.126 -    val (q, b) = split_last uname;
   1.127 -    val sfxs = Library.suffixes1 uname;
   1.128 -    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
   1.129 -  in map pack (sfxs @ pfxs) end;
   1.130 +    val (qs, b) = split_last xs;
   1.131 +    val sfxs = Library.suffixes1 xs;
   1.132 +    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 qs);
   1.133 +  in sfxs @ pfxs end;
   1.134  
   1.135 +val accesses = map pack o suffixes_prefixes o unpack;
   1.136  val accesses' = map pack o Library.suffixes1 o unpack;
   1.137  
   1.138  
   1.139  
   1.140  (** name spaces **)
   1.141  
   1.142 -(* basic operations *)
   1.143 -
   1.144 -fun map_space f xname tab =
   1.145 -  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
   1.146 -
   1.147 -fun change f xname (name, tab) =
   1.148 -  map_space (fn (names, names') => (f names name, names')) xname tab;
   1.149 -
   1.150 -fun change' f xname (name', tab) =
   1.151 -  map_space (fn (names, names') => (names, f names' name')) xname tab;
   1.152 -
   1.153 -fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names;
   1.154 -fun add names nm = nm :: del names nm;
   1.155 -
   1.156 -
   1.157  (* datatype T *)
   1.158  
   1.159  datatype T =
   1.160 @@ -95,81 +108,79 @@
   1.161  
   1.162  val empty = NameSpace Symtab.empty;
   1.163  
   1.164 -
   1.165 -(* extend *)            (*later entries preferred*)
   1.166 +fun lookup (NameSpace tab) xname =
   1.167 +  (case Symtab.lookup (tab, xname) of
   1.168 +    NONE => (xname, true)
   1.169 +  | SOME ([], []) => (xname, true)
   1.170 +  | SOME ([name], _) => (name, true)
   1.171 +  | SOME (name :: _, _) => (name, false)
   1.172 +  | SOME ([], name' :: _) => (hidden name', true));
   1.173  
   1.174 -fun gen_extend_aux acc (name, tab) =
   1.175 -  if is_hidden name then
   1.176 -    error ("Attempt to declare hidden name " ^ quote name)
   1.177 -  else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name);
   1.178 -
   1.179 -fun extend' acc (NameSpace tab, names) =
   1.180 -  NameSpace (foldr (gen_extend_aux acc) tab names);
   1.181 -fun extend (NameSpace tab, names) =
   1.182 -  NameSpace (foldr (gen_extend_aux accesses) tab names);
   1.183 +fun valid_accesses (NameSpace tab) name =
   1.184 +  ([], tab) |> Symtab.foldl (fn (accs, (xname, (names, _))) =>
   1.185 +    if null names orelse hd names <> name then accs else xname :: accs);
   1.186  
   1.187  
   1.188 -(* merge *)             (*1st preferred over 2nd*)
   1.189 +(* intern and extern *)
   1.190 +
   1.191 +fun intern space xname = #1 (lookup space xname);
   1.192 +
   1.193 +val long_names = ref false;
   1.194 +val short_names = ref false;
   1.195 +val unique_names = ref true;
   1.196 +
   1.197 +fun extern space name =
   1.198 +  let
   1.199 +    fun valid unique xname =
   1.200 +      let val (name', uniq) = lookup space xname
   1.201 +      in name = name' andalso (uniq orelse (not unique)) end;
   1.202  
   1.203 -fun merge_aux (tab, (xname, (names1, names1'))) =
   1.204 -  map_space (fn (names2, names2') =>
   1.205 -    (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab;
   1.206 +    fun ex [] = if valid false name then name else hidden name
   1.207 +      | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
   1.208 +  in
   1.209 +    if ! long_names then name
   1.210 +    else if ! short_names then base name
   1.211 +    else ex (accesses' name)
   1.212 +  end;
   1.213 +
   1.214 +fun extern_table space tab =
   1.215 +  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
   1.216 +
   1.217  
   1.218 -fun merge (NameSpace tab1, NameSpace tab2) =
   1.219 -  NameSpace (Symtab.foldl merge_aux (tab2, tab1));
   1.220 +(* basic operations *)
   1.221 +
   1.222 +fun map_space f xname (NameSpace tab) =
   1.223 +  NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
   1.224 +
   1.225 +fun del (name: string) = remove (op =) name;
   1.226 +fun add name names = name :: del name names;
   1.227 +
   1.228 +val del_name = map_space o apfst o del;
   1.229 +val add_name = map_space o apfst o add;
   1.230 +val add_name' = map_space o apsnd o add;
   1.231  
   1.232  
   1.233  (* hide *)
   1.234  
   1.235 -fun hide_aux fully (name, tab) =
   1.236 +fun hide fully name space =
   1.237    if not (is_qualified name) then
   1.238      error ("Attempt to hide global name " ^ quote name)
   1.239    else if is_hidden name then
   1.240      error ("Attempt to hide hidden name " ^ quote name)
   1.241 -  else (change' add name (name,
   1.242 -    Library.foldl (fn (tb, xname) => change del xname (name, tb))
   1.243 -      (tab, if fully then accesses name else [base name])));
   1.244 -
   1.245 -fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
   1.246 +  else
   1.247 +    let val names = valid_accesses space name in
   1.248 +      space
   1.249 +      |> add_name' name name
   1.250 +      |> fold (del_name name) (if fully then names else names inter_string [base name])
   1.251 +    end;
   1.252  
   1.253  
   1.254 -(* intern / extern names *)
   1.255 -
   1.256 -fun lookup (NameSpace tab) xname =
   1.257 -  (case Symtab.lookup (tab, xname) of
   1.258 -    NONE => (xname, true)
   1.259 -  | SOME ([name], _) => (name, true)
   1.260 -  | SOME (name :: _, _) => (name, false)
   1.261 -  | SOME ([], []) => (xname, true)
   1.262 -  | SOME ([], name' :: _) => (hidden name', true));
   1.263 -
   1.264 -fun intern spc xname = #1 (lookup spc xname);
   1.265 +(* merge *)
   1.266  
   1.267 -fun unique_extern mkunique space name =
   1.268 -  let
   1.269 -    fun try [] = hidden name
   1.270 -      | try (nm :: nms) =
   1.271 -          let val (full_nm, uniq) = lookup space nm
   1.272 -          in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end
   1.273 -  in try (accesses' name) end;
   1.274 -
   1.275 -(*output unique names by default*)
   1.276 -val unique_names = ref true;
   1.277 -
   1.278 -(*prune names on output by default*)
   1.279 -val long_names = ref false;
   1.280 -
   1.281 -(*output only base name*)
   1.282 -val short_names = ref false;
   1.283 -
   1.284 -fun extern space name = unique_extern (!unique_names) space name; 
   1.285 -
   1.286 -fun cond_extern space =
   1.287 -  if ! long_names then I
   1.288 -  else if ! short_names then base else extern space;
   1.289 -
   1.290 -fun cond_extern_table space tab =
   1.291 -  Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
   1.292 +fun merge (NameSpace tab1, space2) = (space2, tab1) |> Symtab.foldl
   1.293 +  (fn (space, (xname, (names1, names1'))) =>
   1.294 +    map_space (fn (names2, names2') =>
   1.295 +      (merge_lists' names2 names1, merge_lists' names2' names1')) xname space);
   1.296  
   1.297  
   1.298  (* dest *)
   1.299 @@ -182,7 +193,60 @@
   1.300      (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
   1.301  
   1.302  
   1.303 +
   1.304 +(** naming contexts **)
   1.305 +
   1.306 +(* datatype naming *)
   1.307 +
   1.308 +datatype naming = Naming of
   1.309 +  string * ((string -> string -> string) * (string list -> string list list));
   1.310 +
   1.311 +fun path_of (Naming (path, _)) = path;
   1.312 +
   1.313 +
   1.314 +(* declarations *)
   1.315 +
   1.316 +fun full (Naming (path, (qualify, _))) = qualify path;
   1.317 +
   1.318 +fun declare (Naming (_, (_, accs))) name space =
   1.319 +  if is_hidden name then
   1.320 +    error ("Attempt to declare hidden name " ^ quote name)
   1.321 +  else
   1.322 +    let val names = unpack name in
   1.323 +      conditional (null names orelse exists (equal "") names) (fn () =>
   1.324 +        error ("Bad name declaration " ^ quote name));
   1.325 +      conditional (exists (not o Symbol.is_ident o Symbol.explode) names) (fn () =>
   1.326 +        warning ("Declared non-identifier " ^ quote name));
   1.327 +      fold (add_name name) (map pack (accs names)) space
   1.328 +    end;
   1.329 +
   1.330 +
   1.331 +(* manipulate namings *)
   1.332 +
   1.333 +fun reject_qualified name =
   1.334 +  if is_qualified name then
   1.335 +    error ("Attempt to declare qualified name " ^ quote name)
   1.336 +  else name;
   1.337 +
   1.338 +val default_naming =
   1.339 +  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
   1.340 +
   1.341 +fun add_path elems (Naming (path, policy)) =
   1.342 +  if elems = "//" then Naming ("", (qualified, #2 policy))
   1.343 +  else if elems = "/" then Naming ("", policy)
   1.344 +  else if elems = ".." then Naming (drop_base path, policy)
   1.345 +  else Naming (append path elems, policy);
   1.346 +
   1.347 +fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
   1.348 +
   1.349 +fun no_base_names (Naming (path, (qualify, accs))) =
   1.350 +  Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
   1.351 +
   1.352 +fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
   1.353 +fun set_policy policy (Naming (path, _)) = Naming (path, policy);
   1.354 +
   1.355 +
   1.356  end;
   1.357  
   1.358 -
   1.359 -val long_names = NameSpace.long_names;
   1.360 +structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
   1.361 +open BasicNameSpace;