src/Pure/name_space.ML
author nipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 4318 9b672ea2dfe7
parent 4101 e8ad51c88be9
child 4490 14cd07c16e02
permissions -rw-r--r--
Fixed the definition of `termord': is now antisymmetric.
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@3993
    24
  val declared: T -> string -> bool
wenzelm@3993
    25
  val intern: T -> string -> string
wenzelm@3993
    26
  val extern: T -> string -> string
wenzelm@3761
    27
end;
wenzelm@3761
    28
wenzelm@3876
    29
structure NameSpace: NAME_SPACE =
wenzelm@3761
    30
struct
wenzelm@3761
    31
wenzelm@3761
    32
wenzelm@3761
    33
(** long identifiers **)
wenzelm@3761
    34
wenzelm@3833
    35
val separator = ".";
wenzelm@3761
    36
wenzelm@3833
    37
val unpack = space_explode separator;
wenzelm@3761
    38
val pack = space_implode separator;
wenzelm@3761
    39
wenzelm@3786
    40
val base = last_elem o unpack;
wenzelm@3833
    41
fun qualified name = length (unpack name) > 1;
wenzelm@3761
    42
wenzelm@3761
    43
wenzelm@3761
    44
wenzelm@3761
    45
(** name spaces **)
wenzelm@3761
    46
wenzelm@3761
    47
(* utils *)
wenzelm@3761
    48
wenzelm@3761
    49
fun prefixes1 [] = []
wenzelm@3761
    50
  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
wenzelm@3761
    51
wenzelm@3761
    52
fun suffixes1 xs = map rev (prefixes1 (rev xs));
wenzelm@3761
    53
wenzelm@3761
    54
wenzelm@3761
    55
(* datatype T *)
wenzelm@3761
    56
wenzelm@3761
    57
datatype T =
wenzelm@3761
    58
  NameSpace of string list list * string Symtab.table;
wenzelm@3761
    59
wenzelm@3761
    60
fun entries_of (NameSpace (entries, _)) = entries;
wenzelm@3761
    61
fun tab_of (NameSpace (_, tab)) = tab;
wenzelm@3761
    62
wenzelm@3761
    63
fun make entries =
wenzelm@3761
    64
  let
wenzelm@3876
    65
    fun accesses [] = []
wenzelm@3833
    66
      | accesses entry =
wenzelm@3833
    67
          let
wenzelm@3833
    68
            val p = pack entry;
wenzelm@3833
    69
            val (q, b) = split_last entry;
wenzelm@3833
    70
            val sfxs = suffixes1 entry;
wenzelm@3833
    71
            val pfxs = map (fn x => x @ [b]) (prefixes1 q);
wenzelm@3833
    72
          in
wenzelm@3833
    73
            map (rpair p o pack) (sfxs @ pfxs)
wenzelm@3833
    74
          end;
wenzelm@4101
    75
    val mapping = filter_out (op =) (distinct_fst_string (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@3993
    94
fun declared space name = unpack name mem (entries_of space);
wenzelm@3761
    95
wenzelm@3761
    96
wenzelm@3993
    97
(* intern / extern names *)
wenzelm@3993
    98
wenzelm@3993
    99
fun intern space name =
wenzelm@3761
   100
  if_none (Symtab.lookup (tab_of space, name)) name;
wenzelm@3761
   101
wenzelm@3993
   102
fun extern space name =
wenzelm@3972
   103
  let
wenzelm@3972
   104
    fun try [] = "??" ^ separator ^ name      (*hidden name*)
wenzelm@3972
   105
      | try (nm :: nms) =
wenzelm@3993
   106
          if intern space nm = name then nm
wenzelm@3972
   107
          else try nms;
wenzelm@3972
   108
  in try (map pack (suffixes1 (unpack name))) end;
wenzelm@3761
   109
wenzelm@3761
   110
wenzelm@3761
   111
end;