src/Pure/General/name_space.ML
author wenzelm
Wed May 18 11:30:59 2005 +0200 (2005-05-18)
changeset 16002 e0557c452138
parent 15624 484178635bd8
child 16137 00e9ca1e7261
permissions -rw-r--r--
tuned;
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@12588
    14
  val separator: string                 (*single char*)
wenzelm@9120
    15
  val hidden: string -> string
wenzelm@5012
    16
  val append: string -> string -> string
wenzelm@5012
    17
  val unpack: string -> string list
wenzelm@5012
    18
  val pack: string list -> string
wenzelm@5012
    19
  val base: string -> string
wenzelm@11829
    20
  val map_base: (string -> string) -> string -> string
wenzelm@8728
    21
  val is_qualified: string -> bool
wenzelm@5012
    22
  val accesses: string -> string list
wenzelm@13332
    23
  val accesses': string -> string list
wenzelm@5012
    24
  type T
wenzelm@5012
    25
  val empty: T
wenzelm@5012
    26
  val extend: T * string list -> T
ballarin@15624
    27
  val extend': (string -> string list) -> T * string list -> T
wenzelm@5012
    28
  val merge: T * T -> T
wenzelm@12588
    29
  val hide: bool -> T * string list -> T
wenzelm@5012
    30
  val intern: T -> string -> string
wenzelm@5012
    31
  val extern: T -> string -> string
wenzelm@5175
    32
  val long_names: bool ref
berghofe@14382
    33
  val short_names: bool ref
schirmer@15016
    34
  val unique_names: bool ref
wenzelm@5175
    35
  val cond_extern: T -> string -> string
wenzelm@6845
    36
  val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
wenzelm@5012
    37
  val dest: T -> (string * string list) list
wenzelm@5012
    38
end;
wenzelm@5012
    39
wenzelm@5012
    40
structure NameSpace: NAME_SPACE =
wenzelm@5012
    41
struct
wenzelm@5012
    42
wenzelm@5012
    43
(** long identifiers **)
wenzelm@5012
    44
wenzelm@5012
    45
val separator = ".";
wenzelm@8728
    46
fun hidden name = "??." ^ name;
wenzelm@8728
    47
fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false);
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
skalberg@15570
    54
val base = List.last o unpack;
wenzelm@11829
    55
wenzelm@11829
    56
fun map_base f name =
wenzelm@11829
    57
  let val uname = unpack name
wenzelm@11829
    58
  in pack (map_nth_elem (length uname - 1) f uname) end;
wenzelm@11829
    59
wenzelm@8728
    60
fun is_qualified name = length (unpack name) > 1;
wenzelm@5012
    61
wenzelm@5012
    62
fun accesses name =
wenzelm@5012
    63
  let
wenzelm@5012
    64
    val uname = unpack name;
wenzelm@5012
    65
    val (q, b) = split_last uname;
wenzelm@12251
    66
    val sfxs = Library.suffixes1 uname;
wenzelm@12251
    67
    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
wenzelm@5012
    68
  in map pack (sfxs @ pfxs) end;
wenzelm@5012
    69
wenzelm@13332
    70
val accesses' = map pack o Library.suffixes1 o unpack;
wenzelm@13332
    71
wenzelm@5012
    72
wenzelm@5012
    73
wenzelm@5012
    74
(** name spaces **)
wenzelm@5012
    75
wenzelm@8728
    76
(* basic operations *)
wenzelm@8728
    77
wenzelm@8728
    78
fun map_space f xname tab =
wenzelm@16002
    79
  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
wenzelm@8728
    80
wenzelm@8728
    81
fun change f xname (name, tab) =
wenzelm@8728
    82
  map_space (fn (names, names') => (f names name, names')) xname tab;
wenzelm@8728
    83
wenzelm@8728
    84
fun change' f xname (name', tab) =
wenzelm@8728
    85
  map_space (fn (names, names') => (names, f names' name')) xname tab;
wenzelm@8728
    86
wenzelm@8728
    87
fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names;
wenzelm@8728
    88
fun add names nm = nm :: del names nm;
wenzelm@8728
    89
wenzelm@8728
    90
wenzelm@5012
    91
(* datatype T *)
wenzelm@5012
    92
wenzelm@5012
    93
datatype T =
wenzelm@8728
    94
  NameSpace of (string list * string list) Symtab.table;
wenzelm@5012
    95
wenzelm@5012
    96
val empty = NameSpace Symtab.empty;
wenzelm@5012
    97
wenzelm@5012
    98
wenzelm@8728
    99
(* extend *)            (*later entries preferred*)
wenzelm@8728
   100
ballarin@15624
   101
fun gen_extend_aux acc (name, tab) =
wenzelm@8728
   102
  if is_hidden name then
wenzelm@8728
   103
    error ("Attempt to declare hidden name " ^ quote name)
ballarin@15624
   104
  else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, acc name);
wenzelm@5012
   105
ballarin@15624
   106
fun extend' acc (NameSpace tab, names) =
ballarin@15624
   107
  NameSpace (foldr (gen_extend_aux acc) tab names);
ballarin@15624
   108
fun extend (NameSpace tab, names) =
ballarin@15624
   109
  NameSpace (foldr (gen_extend_aux accesses) tab names);
wenzelm@8728
   110
wenzelm@8728
   111
wenzelm@8728
   112
(* merge *)             (*1st preferred over 2nd*)
wenzelm@8728
   113
berghofe@14198
   114
fun merge_aux (tab, (xname, (names1, names1'))) =
berghofe@14198
   115
  map_space (fn (names2, names2') =>
berghofe@14198
   116
    (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab;
wenzelm@5012
   117
wenzelm@8728
   118
fun merge (NameSpace tab1, NameSpace tab2) =
wenzelm@8728
   119
  NameSpace (Symtab.foldl merge_aux (tab2, tab1));
wenzelm@8728
   120
wenzelm@8728
   121
wenzelm@8728
   122
(* hide *)
wenzelm@5012
   123
wenzelm@12588
   124
fun hide_aux fully (name, tab) =
wenzelm@8728
   125
  if not (is_qualified name) then
wenzelm@8728
   126
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   127
  else if is_hidden name then
wenzelm@8728
   128
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@8728
   129
  else (change' add name (name,
skalberg@15570
   130
    Library.foldl (fn (tb, xname) => change del xname (name, tb))
wenzelm@12588
   131
      (tab, if fully then accesses name else [base name])));
wenzelm@8728
   132
skalberg@15574
   133
fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
wenzelm@5012
   134
wenzelm@5012
   135
wenzelm@5012
   136
(* intern / extern names *)
wenzelm@5012
   137
wenzelm@8728
   138
fun lookup (NameSpace tab) xname =
wenzelm@8728
   139
  (case Symtab.lookup (tab, xname) of
skalberg@15531
   140
    NONE => (xname, true)
skalberg@15531
   141
  | SOME ([name], _) => (name, true)
skalberg@15531
   142
  | SOME (name :: _, _) => (name, false)
skalberg@15531
   143
  | SOME ([], []) => (xname, true)
skalberg@15531
   144
  | SOME ([], name' :: _) => (hidden name', true));
wenzelm@8728
   145
wenzelm@8728
   146
fun intern spc xname = #1 (lookup spc xname);
wenzelm@5012
   147
schirmer@15016
   148
fun unique_extern mkunique space name =
wenzelm@5012
   149
  let
wenzelm@8728
   150
    fun try [] = hidden name
wenzelm@5012
   151
      | try (nm :: nms) =
wenzelm@8728
   152
          let val (full_nm, uniq) = lookup space nm
schirmer@15016
   153
          in if full_nm = name andalso (uniq orelse (not mkunique)) then nm else try nms end
wenzelm@13332
   154
  in try (accesses' name) end;
wenzelm@5012
   155
schirmer@15016
   156
(*output unique names by default*)
schirmer@15016
   157
val unique_names = ref true;
schirmer@15016
   158
wenzelm@5175
   159
(*prune names on output by default*)
wenzelm@5175
   160
val long_names = ref false;
wenzelm@5175
   161
berghofe@14382
   162
(*output only base name*)
berghofe@14382
   163
val short_names = ref false;
berghofe@14382
   164
schirmer@15016
   165
fun extern space name = unique_extern (!unique_names) space name; 
schirmer@15016
   166
berghofe@14382
   167
fun cond_extern space =
berghofe@14382
   168
  if ! long_names then I
berghofe@14382
   169
  else if ! short_names then base else extern space;
wenzelm@5175
   170
wenzelm@6845
   171
fun cond_extern_table space tab =
wenzelm@6845
   172
  Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
wenzelm@6845
   173
wenzelm@5012
   174
wenzelm@5012
   175
(* dest *)
wenzelm@5012
   176
skalberg@15531
   177
fun dest_entry (xname, ([], _)) = NONE
skalberg@15531
   178
  | dest_entry (xname, (name :: _, _)) = SOME (name, xname);
wenzelm@8728
   179
wenzelm@5012
   180
fun dest (NameSpace tab) =
wenzelm@5012
   181
  map (apsnd (sort (int_ord o pairself size)))
skalberg@15570
   182
    (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
wenzelm@5012
   183
wenzelm@5012
   184
wenzelm@5012
   185
end;
wenzelm@5175
   186
wenzelm@5175
   187
wenzelm@5175
   188
val long_names = NameSpace.long_names;