# HG changeset patch
# User wenzelm
# Date 875709038 -7200
# Node ID d99d93d46ca530d277e2a8ad072afea4dfe80c08
# Parent  77f71f650433a9cc38574ce08df096a53273d409
Hierarchically structured name spaces.

diff -r 77f71f650433 -r d99d93d46ca5 src/Pure/name_space.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/name_space.ML	Wed Oct 01 14:30:38 1997 +0200
@@ -0,0 +1,113 @@
+(*  Title:      Pure/name_space.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Hierarchically structured name spaces.
+
+More general than ML-like nested structures, but slightly more ad-hoc.
+Does not support absolute addressing.  Unknown short (FIXME?) names
+are implicitely considered to be declared outermost.
+*)
+
+signature NAME_SPACE =
+sig
+  val unpack: string -> string list
+  val pack: string list -> string
+  val qualified: string -> bool
+  type T
+  val dest: T -> string list
+  val empty: T
+  val extend: string list -> string list * T -> T
+  val merge: T * T -> T
+  val lookup: T -> string -> string
+  val prune: T -> string -> string
+end;
+
+structure NameSpace: NAME_SPACE =
+struct
+
+
+(** long identifiers **)
+
+val separator = "'";
+
+fun unpack_aux name =
+  let
+    (*handle trailing separators gracefully*)
+    val (chars, seps) = take_suffix (equal separator) name;
+    fun expl chs =
+      (case take_prefix (not_equal separator) chs of
+        (cs, []) => [implode (cs @ seps)]
+      | (cs, _ :: cs') => implode cs :: expl cs');
+  in expl chars end;
+
+val unpack = unpack_aux o explode;
+val pack = space_implode separator;
+
+fun qualified name =
+  let val chs = explode name in
+    exists (equal separator) chs andalso (length (unpack_aux chs) > 1)
+  end;
+
+
+
+(** name spaces **)
+
+(* utils *)
+
+fun prefixes1 [] = []
+  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
+
+fun suffixes1 xs = map rev (prefixes1 (rev xs));
+
+
+(* datatype T *)
+
+datatype T =
+  NameSpace of string list list * string Symtab.table;
+
+fun entries_of (NameSpace (entries, _)) = entries;
+fun tab_of (NameSpace (_, tab)) = tab;
+
+fun make entries =
+  let
+    fun accesses entry =
+      let val packed = pack entry in
+        map (rpair packed o pack) (suffixes1 entry)
+      end;
+    val mapping = gen_distinct eq_fst (flat (map accesses entries));
+  in
+    NameSpace (entries, Symtab.make mapping)
+  end;
+
+fun dest space = rev (map pack (entries_of space));
+
+
+
+(* empty, extend, merge operations *)
+
+val empty = make [];
+
+fun extend path (entries, space) =
+  make (map (fn e => path @ unpack e) (rev entries) @ entries_of space);
+
+fun merge (space1, space2) =
+  make (merge_lists (entries_of space1) (entries_of space2));
+
+
+(* lookup / prune names *)
+
+(* FIXME improve handling of undeclared qualified names (?) *)
+fun lookup space name =
+  if_none (Symtab.lookup (tab_of space, name)) name;
+
+fun prune space name =
+  let
+    fun try [] = name
+      | try (nm :: nms) =
+          if lookup space nm = name then nm
+          else try nms;
+  in try (map pack (suffixes1 (unpack name))) end;
+
+
+end;