# HG changeset patch
# User wenzelm
# Date 1117533208 -7200
# Node ID 00e9ca1e7261e5170bebacd3f5651f796a0d76a2
# Parent  1cb99d74eebb324d4cbd9e271a8a1ecf0f243f49
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;

diff -r 1cb99d74eebb -r 00e9ca1e7261 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue May 31 11:53:27 2005 +0200
+++ b/src/Pure/General/name_space.ML	Tue May 31 11:53:28 2005 +0200
@@ -2,39 +2,56 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Hierarchically structured name spaces.
+Generic name spaces with declared and hidden entries.  Unknown names
+are considered as global; no support for absolute addressing.
+*)
+
+type bstring = string;    (*names to be bound / internalized*)
+type xstring = string;    (*externalized names / to be printed*)
 
-More general than ML-like nested structures, but also slightly more
-ad-hoc.  Does not support absolute addressing.  Unknown names are
-implicitely considered to be declared outermost.
-*)
+signature BASIC_NAME_SPACE =
+sig
+  val long_names: bool ref
+  val short_names: bool ref
+  val unique_names: bool ref
+end;
 
 signature NAME_SPACE =
 sig
-  val separator: string                 (*single char*)
+  include BASIC_NAME_SPACE
   val hidden: string -> string
-  val append: string -> string -> string
+  val separator: string                 (*single char*)
+  val is_qualified: string -> bool
+  val pack: string list -> string
   val unpack: string -> string list
-  val pack: string list -> string
+  val append: string -> string -> string
+  val qualified: string -> string -> string
   val base: string -> string
+  val drop_base: string -> string
   val map_base: (string -> string) -> string -> string
-  val is_qualified: string -> bool
+  val suffixes_prefixes: 'a list -> 'a list list
   val accesses: string -> string list
   val accesses': string -> string list
   type T
   val empty: T
-  val extend: T * string list -> T
-  val extend': (string -> string list) -> T * string list -> T
+  val valid_accesses: T -> string -> xstring list
+  val intern: T -> xstring -> string
+  val extern: T -> string -> xstring
+  val extern_table: T -> 'a Symtab.table -> (xstring * 'a) list
+  val hide: bool -> string -> T -> T
   val merge: T * T -> T
-  val hide: bool -> T * string list -> T
-  val intern: T -> string -> string
-  val extern: T -> string -> string
-  val long_names: bool ref
-  val short_names: bool ref
-  val unique_names: bool ref
-  val cond_extern: T -> string -> string
-  val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
-  val dest: T -> (string * string list) list
+  val dest: T -> (string * xstring list) list
+  type naming
+  val path_of: naming -> string
+  val full: naming -> bstring -> string
+  val declare: naming -> string -> T -> T
+  val default_naming: naming
+  val add_path: string -> naming -> naming
+  val qualified_names: naming -> naming
+  val no_base_names: naming -> naming
+  val custom_accesses: (string list -> string list list) -> naming -> naming
+  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
+    naming -> naming
 end;
 
 structure NameSpace: NAME_SPACE =
@@ -42,52 +59,48 @@
 
 (** long identifiers **)
 
+fun hidden name = "??." ^ name;
+val is_hidden = String.isPrefix "??."
+
 val separator = ".";
-fun hidden name = "??." ^ name;
-fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false);
+val is_qualified = exists_string (equal separator);
 
-fun append name1 name2 = name1 ^ separator ^ name2;
-
+val pack = space_implode separator;
 val unpack = space_explode separator;
-val pack = space_implode separator;
 
-val base = List.last o unpack;
+fun append name1 "" = name1
+  | append "" name2 = name2
+  | append name1 name2 = name1 ^ separator ^ name2;
+
+fun qualified path name =
+  if path = "" orelse name = "" then name
+  else path ^ separator ^ name;
 
-fun map_base f name =
-  let val uname = unpack name
-  in pack (map_nth_elem (length uname - 1) f uname) end;
+fun base "" = ""
+  | base name = List.last (unpack name);
 
-fun is_qualified name = length (unpack name) > 1;
+fun drop_base "" = ""
+  | drop_base name = pack (#1 (split_last (unpack name)));
 
-fun accesses name =
+fun map_base _ "" = ""
+  | map_base f name =
+      let val names = unpack name
+      in pack (map_nth_elem (length names - 1) f names) end;
+
+fun suffixes_prefixes xs =
   let
-    val uname = unpack name;
-    val (q, b) = split_last uname;
-    val sfxs = Library.suffixes1 uname;
-    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
-  in map pack (sfxs @ pfxs) end;
+    val (qs, b) = split_last xs;
+    val sfxs = Library.suffixes1 xs;
+    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 qs);
+  in sfxs @ pfxs end;
 
+val accesses = map pack o suffixes_prefixes o unpack;
 val accesses' = map pack o Library.suffixes1 o unpack;
 
 
 
 (** name spaces **)
 
-(* basic operations *)
-
-fun map_space f xname tab =
-  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
-
-fun change f xname (name, tab) =
-  map_space (fn (names, names') => (f names name, names')) xname tab;
-
-fun change' f xname (name', tab) =
-  map_space (fn (names, names') => (names, f names' name')) xname tab;
-
-fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names;
-fun add names nm = nm :: del names nm;
-
-
 (* datatype T *)
 
 datatype T =
@@ -95,81 +108,79 @@
 
 val empty = NameSpace Symtab.empty;
 
-
-(* extend *)            (*later entries preferred*)
+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));
 
-fun gen_extend_aux acc (name, tab) =
-  if is_hidden name then
-    error ("Attempt to declare hidden name " ^ quote name)
-  else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name);
-
-fun extend' acc (NameSpace tab, names) =
-  NameSpace (foldr (gen_extend_aux acc) tab names);
-fun extend (NameSpace tab, names) =
-  NameSpace (foldr (gen_extend_aux accesses) tab names);
+fun valid_accesses (NameSpace tab) name =
+  ([], tab) |> Symtab.foldl (fn (accs, (xname, (names, _))) =>
+    if null names orelse hd names <> name then accs else xname :: accs);
 
 
-(* merge *)             (*1st preferred over 2nd*)
+(* intern and extern *)
+
+fun intern space xname = #1 (lookup space xname);
+
+val long_names = ref false;
+val short_names = ref false;
+val unique_names = ref true;
+
+fun extern space name =
+  let
+    fun valid unique xname =
+      let val (name', uniq) = lookup space xname
+      in name = name' andalso (uniq orelse (not unique)) end;
 
-fun merge_aux (tab, (xname, (names1, names1'))) =
-  map_space (fn (names2, names2') =>
-    (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab;
+    fun ex [] = if valid false name then name else hidden name
+      | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
+  in
+    if ! long_names then name
+    else if ! short_names then base name
+    else ex (accesses' name)
+  end;
+
+fun extern_table space tab =
+  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
+
 
-fun merge (NameSpace tab1, NameSpace tab2) =
-  NameSpace (Symtab.foldl merge_aux (tab2, tab1));
+(* basic operations *)
+
+fun map_space f xname (NameSpace tab) =
+  NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
+
+fun del (name: string) = remove (op =) name;
+fun add name names = name :: del name names;
+
+val del_name = map_space o apfst o del;
+val add_name = map_space o apfst o add;
+val add_name' = map_space o apsnd o add;
 
 
 (* hide *)
 
-fun hide_aux fully (name, tab) =
+fun hide fully name space =
   if not (is_qualified name) then
     error ("Attempt to hide global name " ^ quote name)
   else if is_hidden name then
     error ("Attempt to hide hidden name " ^ quote name)
-  else (change' add name (name,
-    Library.foldl (fn (tb, xname) => change del xname (name, tb))
-      (tab, if fully then accesses name else [base name])));
-
-fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
+  else
+    let val names = valid_accesses space name in
+      space
+      |> add_name' name name
+      |> fold (del_name name) (if fully then names else names inter_string [base name])
+    end;
 
 
-(* intern / extern names *)
-
-fun lookup (NameSpace tab) xname =
-  (case Symtab.lookup (tab, xname) of
-    NONE => (xname, true)
-  | SOME ([name], _) => (name, true)
-  | SOME (name :: _, _) => (name, false)
-  | SOME ([], []) => (xname, true)
-  | SOME ([], name' :: _) => (hidden name', true));
-
-fun intern spc xname = #1 (lookup spc xname);
+(* merge *)
 
-fun unique_extern mkunique space name =
-  let
-    fun try [] = hidden name
-      | try (nm :: nms) =
-          let val (full_nm, uniq) = lookup space nm
-          in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end
-  in try (accesses' name) end;
-
-(*output unique names by default*)
-val unique_names = ref true;
-
-(*prune names on output by default*)
-val long_names = ref false;
-
-(*output only base name*)
-val short_names = ref false;
-
-fun extern space name = unique_extern (!unique_names) space name; 
-
-fun cond_extern space =
-  if ! long_names then I
-  else if ! short_names then base else extern space;
-
-fun cond_extern_table space tab =
-  Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
+fun merge (NameSpace tab1, space2) = (space2, tab1) |> Symtab.foldl
+  (fn (space, (xname, (names1, names1'))) =>
+    map_space (fn (names2, names2') =>
+      (merge_lists' names2 names1, merge_lists' names2' names1')) xname space);
 
 
 (* dest *)
@@ -182,7 +193,60 @@
     (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
 
 
+
+(** naming contexts **)
+
+(* datatype naming *)
+
+datatype naming = Naming of
+  string * ((string -> string -> string) * (string list -> string list list));
+
+fun path_of (Naming (path, _)) = path;
+
+
+(* declarations *)
+
+fun full (Naming (path, (qualify, _))) = qualify path;
+
+fun declare (Naming (_, (_, accs))) name space =
+  if is_hidden name then
+    error ("Attempt to declare hidden name " ^ quote name)
+  else
+    let val names = unpack name in
+      conditional (null names orelse exists (equal "") names) (fn () =>
+        error ("Bad name declaration " ^ quote name));
+      conditional (exists (not o Symbol.is_ident o Symbol.explode) names) (fn () =>
+        warning ("Declared non-identifier " ^ quote name));
+      fold (add_name name) (map pack (accs names)) space
+    end;
+
+
+(* manipulate namings *)
+
+fun reject_qualified name =
+  if is_qualified name then
+    error ("Attempt to declare qualified name " ^ quote name)
+  else name;
+
+val default_naming =
+  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
+
+fun add_path elems (Naming (path, policy)) =
+  if elems = "//" then Naming ("", (qualified, #2 policy))
+  else if elems = "/" then Naming ("", policy)
+  else if elems = ".." then Naming (drop_base path, policy)
+  else Naming (append path elems, policy);
+
+fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
+
+fun no_base_names (Naming (path, (qualify, accs))) =
+  Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
+
+fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
+fun set_policy policy (Naming (path, _)) = Naming (path, policy);
+
+
 end;
 
-
-val long_names = NameSpace.long_names;
+structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
+open BasicNameSpace;