src/Pure/name_space.ML

Hierarchically structured name spaces.

(*  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;