src/Pure/General/name_space.ML
author wenzelm
Sun Aug 28 16:04:47 2005 +0200 (2005-08-28)
changeset 17163 f1455d56e5b5
parent 16848 1c8a5bb7c688
child 17221 6cd180204582
permissions -rw-r--r--
removed unused dest operation;
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@16137
     5
Generic name spaces with declared and hidden entries.  Unknown names
wenzelm@16341
     6
are considered global; no support for absolute addressing.
wenzelm@16137
     7
*)
wenzelm@16137
     8
wenzelm@16137
     9
type bstring = string;    (*names to be bound / internalized*)
wenzelm@16137
    10
type xstring = string;    (*externalized names / to be printed*)
wenzelm@5012
    11
wenzelm@16137
    12
signature BASIC_NAME_SPACE =
wenzelm@16137
    13
sig
wenzelm@16137
    14
  val long_names: bool ref
wenzelm@16137
    15
  val short_names: bool ref
wenzelm@16137
    16
  val unique_names: bool ref
wenzelm@16137
    17
end;
wenzelm@5012
    18
wenzelm@5012
    19
signature NAME_SPACE =
wenzelm@5012
    20
sig
wenzelm@16137
    21
  include BASIC_NAME_SPACE
wenzelm@9120
    22
  val hidden: string -> string
wenzelm@16137
    23
  val separator: string                 (*single char*)
wenzelm@16137
    24
  val is_qualified: string -> bool
wenzelm@16137
    25
  val pack: string list -> string
wenzelm@5012
    26
  val unpack: string -> string list
wenzelm@16137
    27
  val append: string -> string -> string
wenzelm@16137
    28
  val qualified: string -> string -> string
wenzelm@5012
    29
  val base: string -> string
wenzelm@16137
    30
  val drop_base: string -> string
wenzelm@11829
    31
  val map_base: (string -> string) -> string -> string
wenzelm@16137
    32
  val suffixes_prefixes: 'a list -> 'a list list
wenzelm@5012
    33
  val accesses: string -> string list
wenzelm@13332
    34
  val accesses': string -> string list
wenzelm@5012
    35
  type T
wenzelm@5012
    36
  val empty: T
wenzelm@16137
    37
  val valid_accesses: T -> string -> xstring list
wenzelm@16137
    38
  val intern: T -> xstring -> string
wenzelm@16137
    39
  val extern: T -> string -> xstring
wenzelm@16137
    40
  val hide: bool -> string -> T -> T
wenzelm@5012
    41
  val merge: T * T -> T
wenzelm@16137
    42
  type naming
wenzelm@16137
    43
  val path_of: naming -> string
wenzelm@16137
    44
  val full: naming -> bstring -> string
wenzelm@16137
    45
  val declare: naming -> string -> T -> T
wenzelm@16137
    46
  val default_naming: naming
wenzelm@16137
    47
  val add_path: string -> naming -> naming
wenzelm@16137
    48
  val qualified_names: naming -> naming
wenzelm@16137
    49
  val no_base_names: naming -> naming
wenzelm@16137
    50
  val custom_accesses: (string list -> string list list) -> naming -> naming
wenzelm@16137
    51
  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
wenzelm@16137
    52
    naming -> naming
wenzelm@16341
    53
  type 'a table = T * 'a Symtab.table
wenzelm@16341
    54
  val empty_table: 'a table
wenzelm@16341
    55
  val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
wenzelm@16341
    56
  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
wenzelm@16848
    57
  val dest_table: 'a table -> (string * 'a) list
wenzelm@16341
    58
  val extern_table: 'a table -> (xstring * 'a) list
wenzelm@5012
    59
end;
wenzelm@5012
    60
wenzelm@5012
    61
structure NameSpace: NAME_SPACE =
wenzelm@5012
    62
struct
wenzelm@5012
    63
wenzelm@5012
    64
(** long identifiers **)
wenzelm@5012
    65
wenzelm@16137
    66
fun hidden name = "??." ^ name;
wenzelm@16137
    67
val is_hidden = String.isPrefix "??."
wenzelm@16137
    68
wenzelm@5012
    69
val separator = ".";
wenzelm@16137
    70
val is_qualified = exists_string (equal separator);
wenzelm@5012
    71
wenzelm@16137
    72
val pack = space_implode separator;
wenzelm@5012
    73
val unpack = space_explode separator;
wenzelm@5012
    74
wenzelm@16137
    75
fun append name1 "" = name1
wenzelm@16137
    76
  | append "" name2 = name2
wenzelm@16137
    77
  | append name1 name2 = name1 ^ separator ^ name2;
wenzelm@16137
    78
wenzelm@16137
    79
fun qualified path name =
wenzelm@16137
    80
  if path = "" orelse name = "" then name
wenzelm@16137
    81
  else path ^ separator ^ name;
wenzelm@11829
    82
wenzelm@16137
    83
fun base "" = ""
wenzelm@16137
    84
  | base name = List.last (unpack name);
wenzelm@11829
    85
wenzelm@16137
    86
fun drop_base "" = ""
wenzelm@16137
    87
  | drop_base name = pack (#1 (split_last (unpack name)));
wenzelm@5012
    88
wenzelm@16137
    89
fun map_base _ "" = ""
wenzelm@16137
    90
  | map_base f name =
wenzelm@16137
    91
      let val names = unpack name
wenzelm@16137
    92
      in pack (map_nth_elem (length names - 1) f names) end;
wenzelm@16137
    93
wenzelm@16137
    94
fun suffixes_prefixes xs =
wenzelm@5012
    95
  let
wenzelm@16137
    96
    val (qs, b) = split_last xs;
wenzelm@16137
    97
    val sfxs = Library.suffixes1 xs;
wenzelm@16137
    98
    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 qs);
wenzelm@16137
    99
  in sfxs @ pfxs end;
wenzelm@5012
   100
wenzelm@16137
   101
val accesses = map pack o suffixes_prefixes o unpack;
wenzelm@13332
   102
val accesses' = map pack o Library.suffixes1 o unpack;
wenzelm@13332
   103
wenzelm@5012
   104
wenzelm@5012
   105
wenzelm@5012
   106
(** name spaces **)
wenzelm@5012
   107
wenzelm@5012
   108
(* datatype T *)
wenzelm@5012
   109
wenzelm@5012
   110
datatype T =
wenzelm@8728
   111
  NameSpace of (string list * string list) Symtab.table;
wenzelm@5012
   112
wenzelm@5012
   113
val empty = NameSpace Symtab.empty;
wenzelm@5012
   114
wenzelm@16137
   115
fun lookup (NameSpace tab) xname =
wenzelm@16137
   116
  (case Symtab.lookup (tab, xname) of
wenzelm@16137
   117
    NONE => (xname, true)
wenzelm@16137
   118
  | SOME ([], []) => (xname, true)
wenzelm@16137
   119
  | SOME ([name], _) => (name, true)
wenzelm@16137
   120
  | SOME (name :: _, _) => (name, false)
wenzelm@16137
   121
  | SOME ([], name' :: _) => (hidden name', true));
wenzelm@8728
   122
wenzelm@16444
   123
fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, (names, _)) =>
wenzelm@16444
   124
  if not (null names) andalso hd names = name then cons xname else I) tab [];
wenzelm@8728
   125
wenzelm@8728
   126
wenzelm@16137
   127
(* intern and extern *)
wenzelm@16137
   128
wenzelm@16137
   129
fun intern space xname = #1 (lookup space xname);
wenzelm@16137
   130
wenzelm@16137
   131
val long_names = ref false;
wenzelm@16137
   132
val short_names = ref false;
wenzelm@16137
   133
val unique_names = ref true;
wenzelm@16137
   134
wenzelm@16137
   135
fun extern space name =
wenzelm@16137
   136
  let
wenzelm@16137
   137
    fun valid unique xname =
wenzelm@16137
   138
      let val (name', uniq) = lookup space xname
wenzelm@16137
   139
      in name = name' andalso (uniq orelse (not unique)) end;
wenzelm@8728
   140
wenzelm@16137
   141
    fun ex [] = if valid false name then name else hidden name
wenzelm@16137
   142
      | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
wenzelm@16137
   143
  in
wenzelm@16137
   144
    if ! long_names then name
wenzelm@16137
   145
    else if ! short_names then base name
wenzelm@16137
   146
    else ex (accesses' name)
wenzelm@16137
   147
  end;
wenzelm@16137
   148
wenzelm@5012
   149
wenzelm@16137
   150
(* basic operations *)
wenzelm@16137
   151
wenzelm@16137
   152
fun map_space f xname (NameSpace tab) =
wenzelm@16137
   153
  NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
wenzelm@16137
   154
wenzelm@16137
   155
fun del (name: string) = remove (op =) name;
wenzelm@16137
   156
fun add name names = name :: del name names;
wenzelm@16137
   157
wenzelm@16137
   158
val del_name = map_space o apfst o del;
wenzelm@16137
   159
val add_name = map_space o apfst o add;
wenzelm@16137
   160
val add_name' = map_space o apsnd o add;
wenzelm@8728
   161
wenzelm@8728
   162
wenzelm@8728
   163
(* hide *)
wenzelm@5012
   164
wenzelm@16137
   165
fun hide fully name space =
wenzelm@8728
   166
  if not (is_qualified name) then
wenzelm@8728
   167
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   168
  else if is_hidden name then
wenzelm@8728
   169
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@16137
   170
  else
wenzelm@16137
   171
    let val names = valid_accesses space name in
wenzelm@16137
   172
      space
wenzelm@16137
   173
      |> add_name' name name
wenzelm@16137
   174
      |> fold (del_name name) (if fully then names else names inter_string [base name])
wenzelm@16137
   175
    end;
wenzelm@5012
   176
wenzelm@5012
   177
wenzelm@16137
   178
(* merge *)
wenzelm@5012
   179
wenzelm@16444
   180
fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
wenzelm@16444
   181
  xname |> map_space (fn (names2, names2') =>
wenzelm@16444
   182
    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
wenzelm@6845
   183
wenzelm@5012
   184
wenzelm@16137
   185
wenzelm@16137
   186
(** naming contexts **)
wenzelm@16137
   187
wenzelm@16137
   188
(* datatype naming *)
wenzelm@16137
   189
wenzelm@16137
   190
datatype naming = Naming of
wenzelm@16137
   191
  string * ((string -> string -> string) * (string list -> string list list));
wenzelm@16137
   192
wenzelm@16137
   193
fun path_of (Naming (path, _)) = path;
wenzelm@16137
   194
wenzelm@16137
   195
wenzelm@16137
   196
(* declarations *)
wenzelm@16137
   197
wenzelm@16137
   198
fun full (Naming (path, (qualify, _))) = qualify path;
wenzelm@16137
   199
wenzelm@16137
   200
fun declare (Naming (_, (_, accs))) name space =
wenzelm@16137
   201
  if is_hidden name then
wenzelm@16137
   202
    error ("Attempt to declare hidden name " ^ quote name)
wenzelm@16137
   203
  else
wenzelm@16137
   204
    let val names = unpack name in
wenzelm@16137
   205
      conditional (null names orelse exists (equal "") names) (fn () =>
wenzelm@16137
   206
        error ("Bad name declaration " ^ quote name));
wenzelm@16137
   207
      fold (add_name name) (map pack (accs names)) space
wenzelm@16137
   208
    end;
wenzelm@16137
   209
wenzelm@16137
   210
wenzelm@16137
   211
(* manipulate namings *)
wenzelm@16137
   212
wenzelm@16137
   213
fun reject_qualified name =
wenzelm@16137
   214
  if is_qualified name then
wenzelm@16137
   215
    error ("Attempt to declare qualified name " ^ quote name)
wenzelm@16137
   216
  else name;
wenzelm@16137
   217
wenzelm@16137
   218
val default_naming =
wenzelm@16137
   219
  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
wenzelm@16137
   220
wenzelm@16137
   221
fun add_path elems (Naming (path, policy)) =
wenzelm@16137
   222
  if elems = "//" then Naming ("", (qualified, #2 policy))
wenzelm@16137
   223
  else if elems = "/" then Naming ("", policy)
wenzelm@16137
   224
  else if elems = ".." then Naming (drop_base path, policy)
wenzelm@16137
   225
  else Naming (append path elems, policy);
wenzelm@16137
   226
wenzelm@16137
   227
fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
wenzelm@16137
   228
wenzelm@16137
   229
fun no_base_names (Naming (path, (qualify, accs))) =
wenzelm@16137
   230
  Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
wenzelm@16137
   231
wenzelm@16137
   232
fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
wenzelm@16137
   233
fun set_policy policy (Naming (path, _)) = Naming (path, policy);
wenzelm@16137
   234
wenzelm@16137
   235
wenzelm@16341
   236
wenzelm@16341
   237
(** name spaces coupled with symbol tables **)
wenzelm@16341
   238
wenzelm@16341
   239
type 'a table = T * 'a Symtab.table;
wenzelm@16341
   240
wenzelm@16341
   241
val empty_table = (empty, Symtab.empty);
wenzelm@16341
   242
wenzelm@16341
   243
fun extend_table naming ((space, tab), bentries) =
wenzelm@16341
   244
  let val entries = map (apfst (full naming)) bentries
wenzelm@16341
   245
  in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
wenzelm@16341
   246
wenzelm@16341
   247
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
wenzelm@16341
   248
  (merge (space1, space2), (Symtab.merge eq (tab1, tab2)));
wenzelm@16341
   249
wenzelm@16848
   250
fun ext_table (space, tab) =
wenzelm@16848
   251
  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
wenzelm@16848
   252
  |> Library.sort_wrt (#2 o #1);
wenzelm@16848
   253
wenzelm@16848
   254
fun dest_table tab = map (apfst #1) (ext_table tab);
wenzelm@16848
   255
fun extern_table tab = map (apfst #2) (ext_table tab);
wenzelm@16341
   256
wenzelm@5012
   257
end;
wenzelm@5175
   258
wenzelm@16137
   259
structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
wenzelm@16137
   260
open BasicNameSpace;