src/Pure/General/name_space.ML
author wenzelm
Wed Jul 22 17:59:49 1998 +0200 (1998-07-22)
changeset 5175 2dbef0104bcf
parent 5012 086b055c4d73
child 5682 9125611c1645
permissions -rw-r--r--
moved long_names / cond_extern to name_space.ML;
wenzelm@5012
     1
(*  Title:      Pure/name_space.ML
wenzelm@5012
     2
    ID:         $Id$
wenzelm@5012
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5012
     4
wenzelm@5012
     5
Hierarchically structured name spaces.
wenzelm@5012
     6
wenzelm@5012
     7
More general than ML-like nested structures, but also slightly more
wenzelm@5012
     8
ad-hoc.  Does not support absolute addressing.  Unknown names are
wenzelm@5012
     9
implicitely considered to be declared outermost.
wenzelm@5012
    10
*)
wenzelm@5012
    11
wenzelm@5012
    12
signature NAME_SPACE =
wenzelm@5012
    13
sig
wenzelm@5012
    14
  val separator: string                 (*single char!*)
wenzelm@5012
    15
  val append: string -> string -> string
wenzelm@5012
    16
  val unpack: string -> string list
wenzelm@5012
    17
  val pack: string list -> string
wenzelm@5012
    18
  val base: string -> string
wenzelm@5012
    19
  val qualified: string -> bool
wenzelm@5012
    20
  val accesses: string -> string list
wenzelm@5012
    21
  type T
wenzelm@5012
    22
  val empty: T
wenzelm@5012
    23
  val extend: T * string list -> T
wenzelm@5012
    24
  val merge: T * T -> T
wenzelm@5012
    25
  val intern: T -> string -> string
wenzelm@5012
    26
  val extern: T -> string -> string
wenzelm@5175
    27
  val long_names: bool ref
wenzelm@5175
    28
  val cond_extern: T -> string -> string
wenzelm@5012
    29
  val dest: T -> (string * string list) list
wenzelm@5012
    30
end;
wenzelm@5012
    31
wenzelm@5012
    32
structure NameSpace: NAME_SPACE =
wenzelm@5012
    33
struct
wenzelm@5012
    34
wenzelm@5012
    35
wenzelm@5012
    36
(** utils **)
wenzelm@5012
    37
wenzelm@5012
    38
fun prefixes1 [] = []
wenzelm@5012
    39
  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
wenzelm@5012
    40
wenzelm@5012
    41
fun suffixes1 xs = map rev (prefixes1 (rev xs));
wenzelm@5012
    42
wenzelm@5012
    43
wenzelm@5012
    44
wenzelm@5012
    45
(** long identifiers **)
wenzelm@5012
    46
wenzelm@5012
    47
val separator = ".";
wenzelm@5012
    48
wenzelm@5012
    49
fun append name1 name2 = name1 ^ separator ^ name2;
wenzelm@5012
    50
wenzelm@5012
    51
val unpack = space_explode separator;
wenzelm@5012
    52
val pack = space_implode separator;
wenzelm@5012
    53
wenzelm@5012
    54
val base = last_elem o unpack;
wenzelm@5012
    55
fun qualified name = length (unpack name) > 1;
wenzelm@5012
    56
wenzelm@5012
    57
fun accesses name =
wenzelm@5012
    58
  let
wenzelm@5012
    59
    val uname = unpack name;
wenzelm@5012
    60
    val (q, b) = split_last uname;
wenzelm@5012
    61
    val sfxs = suffixes1 uname;
wenzelm@5012
    62
    val pfxs = map (fn x => x @ [b]) (prefixes1 q);
wenzelm@5012
    63
  in map pack (sfxs @ pfxs) end;
wenzelm@5012
    64
wenzelm@5012
    65
wenzelm@5012
    66
wenzelm@5012
    67
(** name spaces **)
wenzelm@5012
    68
wenzelm@5012
    69
(* datatype T *)
wenzelm@5012
    70
wenzelm@5012
    71
datatype T =
wenzelm@5012
    72
  NameSpace of string Symtab.table;
wenzelm@5012
    73
wenzelm@5012
    74
val empty = NameSpace Symtab.empty;
wenzelm@5012
    75
wenzelm@5012
    76
wenzelm@5012
    77
(* extend, merge operations *)
wenzelm@5012
    78
wenzelm@5012
    79
fun add (tab, entry) = Symtab.update (entry, tab);
wenzelm@5012
    80
wenzelm@5012
    81
fun extend (NameSpace tab, names) =
wenzelm@5012
    82
  NameSpace (foldl add (tab, flat (map (fn name => map (rpair name) (accesses name)) names)));
wenzelm@5012
    83
wenzelm@5012
    84
fun merge (NameSpace tab1, NameSpace tab2) =    (*2nd overrides 1st*)
wenzelm@5012
    85
  NameSpace (foldl add (tab1, Symtab.dest tab2));
wenzelm@5012
    86
wenzelm@5012
    87
wenzelm@5012
    88
(* intern / extern names *)
wenzelm@5012
    89
wenzelm@5012
    90
fun intern (NameSpace tab) name =
wenzelm@5012
    91
  if_none (Symtab.lookup (tab, name)) name;
wenzelm@5012
    92
wenzelm@5012
    93
fun extern space name =
wenzelm@5012
    94
  let
wenzelm@5012
    95
    fun try [] = "??" ^ separator ^ name      (*hidden name*)
wenzelm@5012
    96
      | try (nm :: nms) =
wenzelm@5012
    97
          if intern space nm = name then nm
wenzelm@5012
    98
          else try nms;
wenzelm@5012
    99
  in try (map pack (suffixes1 (unpack name))) end;
wenzelm@5012
   100
wenzelm@5175
   101
(*prune names on output by default*)
wenzelm@5175
   102
val long_names = ref false;
wenzelm@5175
   103
wenzelm@5175
   104
fun cond_extern space = if ! long_names then I else extern space;
wenzelm@5175
   105
wenzelm@5012
   106
wenzelm@5012
   107
(* dest *)
wenzelm@5012
   108
wenzelm@5012
   109
fun dest (NameSpace tab) =
wenzelm@5012
   110
  map (apsnd (sort (int_ord o pairself size)))
wenzelm@5012
   111
    (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab))));
wenzelm@5012
   112
wenzelm@5012
   113
wenzelm@5012
   114
end;
wenzelm@5175
   115
wenzelm@5175
   116
wenzelm@5175
   117
val long_names = NameSpace.long_names;