src/Pure/General/name_space.ML
changeset 5012 086b055c4d73
child 5175 2dbef0104bcf
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/name_space.ML	Wed Jun 10 11:51:58 1998 +0200
@@ -0,0 +1,107 @@
+(*  Title:      Pure/name_space.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Hierarchically structured name spaces.
+
+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 NAME_SPACE =
+sig
+  val separator: string                 (*single char!*)
+  val append: string -> string -> string
+  val unpack: string -> string list
+  val pack: string list -> string
+  val base: string -> string
+  val qualified: string -> bool
+  val accesses: string -> string list
+  type T
+  val empty: T
+  val extend: T * string list -> T
+  val merge: T * T -> T
+  val intern: T -> string -> string
+  val extern: T -> string -> string
+  val dest: T -> (string * string list) list
+end;
+
+structure NameSpace: NAME_SPACE =
+struct
+
+
+(** utils **)
+
+fun prefixes1 [] = []
+  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
+
+fun suffixes1 xs = map rev (prefixes1 (rev xs));
+
+
+
+(** long identifiers **)
+
+val separator = ".";
+
+fun append name1 name2 = name1 ^ separator ^ name2;
+
+val unpack = space_explode separator;
+val pack = space_implode separator;
+
+val base = last_elem o unpack;
+fun qualified name = length (unpack name) > 1;
+
+fun accesses name =
+  let
+    val uname = unpack name;
+    val (q, b) = split_last uname;
+    val sfxs = suffixes1 uname;
+    val pfxs = map (fn x => x @ [b]) (prefixes1 q);
+  in map pack (sfxs @ pfxs) end;
+
+
+
+(** name spaces **)
+
+(* datatype T *)
+
+datatype T =
+  NameSpace of string Symtab.table;
+
+val empty = NameSpace Symtab.empty;
+
+
+(* extend, merge operations *)
+
+fun add (tab, entry) = Symtab.update (entry, tab);
+
+fun extend (NameSpace tab, names) =
+  NameSpace (foldl add (tab, flat (map (fn name => map (rpair name) (accesses name)) names)));
+
+fun merge (NameSpace tab1, NameSpace tab2) =    (*2nd overrides 1st*)
+  NameSpace (foldl add (tab1, Symtab.dest tab2));
+
+
+(* intern / extern names *)
+
+fun intern (NameSpace tab) name =
+  if_none (Symtab.lookup (tab, name)) name;
+
+fun extern space name =
+  let
+    fun try [] = "??" ^ separator ^ name      (*hidden name*)
+      | try (nm :: nms) =
+          if intern space nm = name then nm
+          else try nms;
+  in try (map pack (suffixes1 (unpack name))) end;
+
+
+(* dest *)
+
+fun dest (NameSpace tab) =
+  map (apsnd (sort (int_ord o pairself size)))
+    (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab))));
+
+
+end;