src/Pure/name_space.ML
author wenzelm
Fri Oct 10 15:51:14 1997 +0200 (1997-10-10)
changeset 3833 370e845c391f
parent 3803 3e581526ae5e
child 3876 e6f918979f2d
permissions -rw-r--r--
tuned;
more accesses to long name;
wenzelm@3761
     1
(*  Title:      Pure/name_space.ML
wenzelm@3761
     2
    ID:         $Id$
wenzelm@3761
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@3761
     4
wenzelm@3761
     5
Hierarchically structured name spaces.
wenzelm@3761
     6
wenzelm@3786
     7
More general than ML-like nested structures, but also slightly more
wenzelm@3786
     8
ad-hoc.  Does not support absolute addressing.  Unknown names are
wenzelm@3786
     9
implicitely considered to be declared outermost.
wenzelm@3761
    10
*)
wenzelm@3761
    11
wenzelm@3761
    12
signature NAME_SPACE =
wenzelm@3761
    13
sig
wenzelm@3833
    14
  val separator: string         (*single char!*)
wenzelm@3761
    15
  val unpack: string -> string list
wenzelm@3761
    16
  val pack: string list -> string
wenzelm@3786
    17
  val base: string -> string
wenzelm@3761
    18
  val qualified: string -> bool
wenzelm@3761
    19
  type T
wenzelm@3761
    20
  val dest: T -> string list
wenzelm@3761
    21
  val empty: T
wenzelm@3786
    22
  val extend: string list * T -> T
wenzelm@3761
    23
  val merge: T * T -> T
wenzelm@3761
    24
  val lookup: T -> string -> string
wenzelm@3761
    25
  val prune: T -> string -> string
wenzelm@3761
    26
end;
wenzelm@3761
    27
wenzelm@3833
    28
structure NameSpace(*: NAME_SPACE FIXME *) =
wenzelm@3761
    29
struct
wenzelm@3761
    30
wenzelm@3761
    31
wenzelm@3761
    32
(** long identifiers **)
wenzelm@3761
    33
wenzelm@3833
    34
val separator = ".";
wenzelm@3761
    35
wenzelm@3833
    36
val unpack = space_explode separator;
wenzelm@3761
    37
val pack = space_implode separator;
wenzelm@3761
    38
wenzelm@3786
    39
val base = last_elem o unpack;
wenzelm@3833
    40
fun qualified name = length (unpack name) > 1;
wenzelm@3761
    41
wenzelm@3761
    42
wenzelm@3761
    43
wenzelm@3761
    44
(** name spaces **)
wenzelm@3761
    45
wenzelm@3761
    46
(* utils *)
wenzelm@3761
    47
wenzelm@3761
    48
fun prefixes1 [] = []
wenzelm@3761
    49
  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
wenzelm@3761
    50
wenzelm@3761
    51
fun suffixes1 xs = map rev (prefixes1 (rev xs));
wenzelm@3761
    52
wenzelm@3761
    53
wenzelm@3761
    54
(* datatype T *)
wenzelm@3761
    55
wenzelm@3761
    56
datatype T =
wenzelm@3761
    57
  NameSpace of string list list * string Symtab.table;
wenzelm@3761
    58
wenzelm@3761
    59
fun entries_of (NameSpace (entries, _)) = entries;
wenzelm@3761
    60
fun tab_of (NameSpace (_, tab)) = tab;
wenzelm@3761
    61
wenzelm@3761
    62
fun make entries =
wenzelm@3761
    63
  let
wenzelm@3833
    64
    fun accesses [] = []		(* FIXME !? *)
wenzelm@3833
    65
      | accesses entry =
wenzelm@3833
    66
          let
wenzelm@3833
    67
            val p = pack entry;
wenzelm@3833
    68
            val (q, b) = split_last entry;
wenzelm@3833
    69
            val sfxs = suffixes1 entry;
wenzelm@3833
    70
            val pfxs = map (fn x => x @ [b]) (prefixes1 q);
wenzelm@3833
    71
          in
wenzelm@3833
    72
            map (rpair p o pack) (sfxs @ pfxs)
wenzelm@3833
    73
          end;
wenzelm@3803
    74
    val mapping = filter_out (op =)
wenzelm@3803
    75
      (gen_distinct eq_fst (flat (map accesses entries)));
wenzelm@3761
    76
  in
wenzelm@3761
    77
    NameSpace (entries, Symtab.make mapping)
wenzelm@3761
    78
  end;
wenzelm@3761
    79
wenzelm@3761
    80
fun dest space = rev (map pack (entries_of space));
wenzelm@3761
    81
wenzelm@3761
    82
wenzelm@3761
    83
wenzelm@3761
    84
(* empty, extend, merge operations *)
wenzelm@3761
    85
wenzelm@3761
    86
val empty = make [];
wenzelm@3761
    87
wenzelm@3786
    88
fun extend (entries, space) =
wenzelm@3786
    89
  make (map unpack (rev entries) @ entries_of space);
wenzelm@3761
    90
wenzelm@3803
    91
fun merge (space1, space2) =    (*2nd overrides 1st*)
wenzelm@3803
    92
  make (merge_lists (entries_of space2) (entries_of space1));
wenzelm@3761
    93
wenzelm@3761
    94
wenzelm@3761
    95
(* lookup / prune names *)
wenzelm@3761
    96
wenzelm@3761
    97
fun lookup space name =
wenzelm@3761
    98
  if_none (Symtab.lookup (tab_of space, name)) name;
wenzelm@3761
    99
wenzelm@3761
   100
fun prune space name =
wenzelm@3786
   101
  if not (qualified name) then name
wenzelm@3786
   102
  else
wenzelm@3786
   103
    let
wenzelm@3833
   104
      fun try [] = "??" ^ separator ^ name      (*hidden name*)
wenzelm@3786
   105
        | try (nm :: nms) =
wenzelm@3786
   106
            if lookup space nm = name then nm
wenzelm@3786
   107
            else try nms;
wenzelm@3786
   108
    in try (map pack (suffixes1 (unpack name))) end;
wenzelm@3761
   109
wenzelm@3761
   110
wenzelm@3761
   111
end;