src/Pure/General/name_space.ML
author wenzelm
Mon Apr 17 14:10:38 2000 +0200 (2000-04-17)
changeset 8728 33a9643ba626
parent 6845 598d2f32d452
child 8806 a202293db3f6
permissions -rw-r--r--
improved output of ambiguous entries;
support hiding;
wenzelm@6118
     1
(*  Title:      Pure/General/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@8728
    19
  val is_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@8728
    25
  val hide: T * string list -> T
wenzelm@5012
    26
  val intern: T -> string -> string
wenzelm@5012
    27
  val extern: T -> string -> string
wenzelm@5175
    28
  val long_names: bool ref
wenzelm@5175
    29
  val cond_extern: T -> string -> string
wenzelm@6845
    30
  val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
wenzelm@5012
    31
  val dest: T -> (string * string list) list
wenzelm@5012
    32
end;
wenzelm@5012
    33
wenzelm@5012
    34
structure NameSpace: NAME_SPACE =
wenzelm@5012
    35
struct
wenzelm@5012
    36
wenzelm@5012
    37
wenzelm@5012
    38
(** utils **)
wenzelm@5012
    39
wenzelm@5012
    40
fun prefixes1 [] = []
wenzelm@5012
    41
  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
wenzelm@5012
    42
wenzelm@5012
    43
fun suffixes1 xs = map rev (prefixes1 (rev xs));
wenzelm@5012
    44
wenzelm@5012
    45
wenzelm@5012
    46
wenzelm@5012
    47
(** long identifiers **)
wenzelm@5012
    48
wenzelm@5012
    49
val separator = ".";
wenzelm@8728
    50
fun hidden name = "??." ^ name;
wenzelm@8728
    51
fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false);
wenzelm@5012
    52
wenzelm@5012
    53
fun append name1 name2 = name1 ^ separator ^ name2;
wenzelm@5012
    54
wenzelm@5012
    55
val unpack = space_explode separator;
wenzelm@5012
    56
val pack = space_implode separator;
wenzelm@5012
    57
wenzelm@5012
    58
val base = last_elem o unpack;
wenzelm@8728
    59
fun is_qualified name = length (unpack name) > 1;
wenzelm@5012
    60
wenzelm@5012
    61
fun accesses name =
wenzelm@5012
    62
  let
wenzelm@5012
    63
    val uname = unpack name;
wenzelm@5012
    64
    val (q, b) = split_last uname;
wenzelm@5012
    65
    val sfxs = suffixes1 uname;
wenzelm@5012
    66
    val pfxs = map (fn x => x @ [b]) (prefixes1 q);
wenzelm@5012
    67
  in map pack (sfxs @ pfxs) end;
wenzelm@5012
    68
wenzelm@5012
    69
wenzelm@5012
    70
wenzelm@5012
    71
(** name spaces **)
wenzelm@5012
    72
wenzelm@8728
    73
(* basic operations *)
wenzelm@8728
    74
wenzelm@8728
    75
fun map_space f xname tab =
wenzelm@8728
    76
  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
wenzelm@8728
    77
wenzelm@8728
    78
fun change f xname (name, tab) =
wenzelm@8728
    79
  map_space (fn (names, names') => (f names name, names')) xname tab;
wenzelm@8728
    80
wenzelm@8728
    81
fun change' f xname (name', tab) =
wenzelm@8728
    82
  map_space (fn (names, names') => (names, f names' name')) xname tab;
wenzelm@8728
    83
wenzelm@8728
    84
fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names;
wenzelm@8728
    85
fun add names nm = nm :: del names nm;
wenzelm@8728
    86
wenzelm@8728
    87
wenzelm@5012
    88
(* datatype T *)
wenzelm@5012
    89
wenzelm@5012
    90
datatype T =
wenzelm@8728
    91
  NameSpace of (string list * string list) Symtab.table;
wenzelm@5012
    92
wenzelm@5012
    93
val empty = NameSpace Symtab.empty;
wenzelm@5012
    94
wenzelm@5012
    95
wenzelm@8728
    96
(* extend *)            (*later entries preferred*)
wenzelm@8728
    97
wenzelm@8728
    98
fun extend_aux (name, tab) =
wenzelm@8728
    99
  if is_hidden name then
wenzelm@8728
   100
    error ("Attempt to declare hidden name " ^ quote name)
wenzelm@8728
   101
  else foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
wenzelm@5012
   102
wenzelm@8728
   103
fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux (names, tab));
wenzelm@8728
   104
wenzelm@8728
   105
wenzelm@8728
   106
(* merge *)             (*1st preferred over 2nd*)
wenzelm@8728
   107
wenzelm@8728
   108
fun merge_aux (tab, (xname, (names, names'))) =
wenzelm@8728
   109
  foldr (change add xname) (names, foldr (change' add xname) (names', tab));
wenzelm@5012
   110
wenzelm@8728
   111
fun merge (NameSpace tab1, NameSpace tab2) =
wenzelm@8728
   112
  NameSpace (Symtab.foldl merge_aux (tab2, tab1));
wenzelm@8728
   113
wenzelm@8728
   114
wenzelm@8728
   115
(* hide *)
wenzelm@5012
   116
wenzelm@8728
   117
fun hide_aux (name, tab) =
wenzelm@8728
   118
  if not (is_qualified name) then
wenzelm@8728
   119
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   120
  else if is_hidden name then
wenzelm@8728
   121
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@8728
   122
  else (change' add name (name,
wenzelm@8728
   123
    foldl (fn (tb, xname) => change del xname (name, tb)) (tab, accesses name)));
wenzelm@8728
   124
wenzelm@8728
   125
fun hide (NameSpace tab, names) = NameSpace (foldr hide_aux (names, tab));
wenzelm@5012
   126
wenzelm@5012
   127
wenzelm@5012
   128
(* intern / extern names *)
wenzelm@5012
   129
wenzelm@8728
   130
fun lookup (NameSpace tab) xname =
wenzelm@8728
   131
  (case Symtab.lookup (tab, xname) of
wenzelm@8728
   132
    None => (xname, true)
wenzelm@8728
   133
  | Some ([name], _) => (name, true)
wenzelm@8728
   134
  | Some (name :: _, _) => (name, false)
wenzelm@8728
   135
  | Some ([], []) => (xname, true)
wenzelm@8728
   136
  | Some ([], name' :: _) => (hidden name', true));
wenzelm@8728
   137
wenzelm@8728
   138
fun intern spc xname = #1 (lookup spc xname);
wenzelm@5012
   139
wenzelm@5012
   140
fun extern space name =
wenzelm@5012
   141
  let
wenzelm@8728
   142
    fun try [] = hidden name
wenzelm@5012
   143
      | try (nm :: nms) =
wenzelm@8728
   144
          let val (full_nm, uniq) = lookup space nm
wenzelm@8728
   145
          in if full_nm = name andalso uniq then nm else try nms end
wenzelm@5012
   146
  in try (map pack (suffixes1 (unpack name))) end;
wenzelm@5012
   147
wenzelm@5175
   148
(*prune names on output by default*)
wenzelm@5175
   149
val long_names = ref false;
wenzelm@5175
   150
wenzelm@5175
   151
fun cond_extern space = if ! long_names then I else extern space;
wenzelm@5175
   152
wenzelm@6845
   153
fun cond_extern_table space tab =
wenzelm@6845
   154
  Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
wenzelm@6845
   155
wenzelm@5012
   156
wenzelm@5012
   157
(* dest *)
wenzelm@5012
   158
wenzelm@8728
   159
fun dest_entry (xname, ([], _)) = None
wenzelm@8728
   160
  | dest_entry (xname, (name :: _, _)) = Some (name, xname);
wenzelm@8728
   161
wenzelm@5012
   162
fun dest (NameSpace tab) =
wenzelm@5012
   163
  map (apsnd (sort (int_ord o pairself size)))
wenzelm@8728
   164
    (Symtab.dest (Symtab.make_multi (mapfilter dest_entry (Symtab.dest tab))));
wenzelm@5012
   165
wenzelm@5012
   166
wenzelm@5012
   167
end;
wenzelm@5175
   168
wenzelm@5175
   169
wenzelm@5175
   170
val long_names = NameSpace.long_names;