src/Pure/General/name_space.ML
author wenzelm
Tue Mar 03 21:53:52 2009 +0100 (2009-03-03)
changeset 30233 6eb726e43ed1
parent 30222 4102bbf2af21
child 30242 aea5d7fa7ef5
permissions -rw-r--r--
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
misc tuning and polishing;
wenzelm@6118
     1
(*  Title:      Pure/General/name_space.ML
wenzelm@5012
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5012
     3
wenzelm@16137
     4
Generic name spaces with declared and hidden entries.  Unknown names
wenzelm@16341
     5
are considered global; no support for absolute addressing.
wenzelm@16137
     6
*)
wenzelm@16137
     7
wenzelm@26440
     8
type xstring = string;    (*external names*)
wenzelm@5012
     9
wenzelm@30215
    10
signature BASIC_NAME_SPACE =
wenzelm@30215
    11
sig
wenzelm@30215
    12
  val long_names: bool ref
wenzelm@30215
    13
  val short_names: bool ref
wenzelm@30215
    14
  val unique_names: bool ref
wenzelm@30215
    15
end;
wenzelm@30215
    16
wenzelm@5012
    17
signature NAME_SPACE =
wenzelm@5012
    18
sig
wenzelm@30215
    19
  include BASIC_NAME_SPACE
wenzelm@9120
    20
  val hidden: string -> string
wenzelm@25225
    21
  val is_hidden: string -> bool
wenzelm@16137
    22
  val separator: string                 (*single char*)
wenzelm@16137
    23
  val is_qualified: string -> bool
wenzelm@21858
    24
  val implode: string list -> string
wenzelm@21858
    25
  val explode: string -> string list
wenzelm@16137
    26
  val append: string -> string -> string
wenzelm@16137
    27
  val qualified: string -> string -> string
wenzelm@5012
    28
  val base: string -> string
wenzelm@20530
    29
  val qualifier: string -> string
wenzelm@11829
    30
  val map_base: (string -> string) -> string -> string
wenzelm@5012
    31
  type T
wenzelm@5012
    32
  val empty: T
wenzelm@16137
    33
  val intern: T -> xstring -> string
wenzelm@16137
    34
  val extern: T -> string -> xstring
wenzelm@30215
    35
  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
wenzelm@30215
    36
    T -> string -> xstring
wenzelm@16137
    37
  val hide: bool -> string -> T -> T
wenzelm@5012
    38
  val merge: T * T -> T
wenzelm@16137
    39
  type naming
haftmann@28965
    40
  val default_naming: naming
haftmann@29581
    41
  val declare: naming -> binding -> T -> string * T
haftmann@29581
    42
  val full_name: naming -> binding -> string
wenzelm@25072
    43
  val external_names: naming -> string -> string list
haftmann@28965
    44
  val path_of: naming -> string
wenzelm@16137
    45
  val add_path: string -> naming -> naming
wenzelm@19015
    46
  val no_base_names: naming -> naming
wenzelm@16137
    47
  val qualified_names: naming -> naming
wenzelm@19055
    48
  val sticky_prefix: string -> naming -> naming
wenzelm@24361
    49
  type 'a table = T * 'a Symtab.table
wenzelm@30233
    50
  val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
wenzelm@16341
    51
  val empty_table: 'a table
wenzelm@30233
    52
  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table  (*exception Symtab.DUP*)
wenzelm@30233
    53
  val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
wenzelm@30233
    54
    'a table * 'a table -> 'a table                                       (*exception Symtab.DUP*)
wenzelm@16848
    55
  val dest_table: 'a table -> (string * 'a) list
wenzelm@16341
    56
  val extern_table: 'a table -> (xstring * 'a) list
wenzelm@5012
    57
end;
wenzelm@5012
    58
wenzelm@5012
    59
structure NameSpace: NAME_SPACE =
wenzelm@5012
    60
struct
wenzelm@5012
    61
wenzelm@5012
    62
(** long identifiers **)
wenzelm@5012
    63
wenzelm@16137
    64
fun hidden name = "??." ^ name;
haftmann@29338
    65
val is_hidden = String.isPrefix "??.";
wenzelm@16137
    66
wenzelm@30222
    67
val separator = ".";
wenzelm@30222
    68
val is_qualified = exists_string (fn s => s = separator);
wenzelm@5012
    69
wenzelm@21858
    70
val implode_name = space_implode separator;
wenzelm@21858
    71
val explode_name = space_explode separator;
wenzelm@5012
    72
wenzelm@16137
    73
fun append name1 "" = name1
wenzelm@16137
    74
  | append "" name2 = name2
wenzelm@16137
    75
  | append name1 name2 = name1 ^ separator ^ name2;
wenzelm@16137
    76
wenzelm@16137
    77
fun qualified path name =
wenzelm@16137
    78
  if path = "" orelse name = "" then name
wenzelm@16137
    79
  else path ^ separator ^ name;
wenzelm@11829
    80
wenzelm@16137
    81
fun base "" = ""
wenzelm@21858
    82
  | base name = List.last (explode_name name);
wenzelm@11829
    83
wenzelm@20530
    84
fun qualifier "" = ""
wenzelm@21858
    85
  | qualifier name = implode_name (#1 (split_last (explode_name name)));
wenzelm@5012
    86
wenzelm@16137
    87
fun map_base _ "" = ""
wenzelm@16137
    88
  | map_base f name =
wenzelm@21858
    89
      let val names = explode_name name
wenzelm@21858
    90
      in implode_name (nth_map (length names - 1) f names) end;
wenzelm@16137
    91
wenzelm@19015
    92
wenzelm@25072
    93
(* standard accesses *)
wenzelm@19015
    94
wenzelm@19015
    95
infixr 6 @@;
wenzelm@19015
    96
fun ([] @@ yss) = []
wenzelm@19015
    97
  | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
wenzelm@19015
    98
wenzelm@19015
    99
fun suffixes_prefixes list =
wenzelm@5012
   100
  let
wenzelm@19015
   101
    val (xs, ws) = chop (length list - 1) list;
wenzelm@19015
   102
    val sfxs = suffixes xs @@ [ws];
wenzelm@19015
   103
    val pfxs = prefixes1 xs @@ [ws];
wenzelm@25072
   104
  in (sfxs @ pfxs, sfxs) end;
wenzelm@19015
   105
wenzelm@19015
   106
fun suffixes_prefixes_split i k list =
wenzelm@19015
   107
  let
wenzelm@19015
   108
    val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
wenzelm@19015
   109
    val sfxs =
wenzelm@19015
   110
      [ys] @@ suffixes zs @@ [ws] @
wenzelm@19015
   111
      suffixes1 xs @@ [ys @ zs @ ws];
wenzelm@19015
   112
    val pfxs =
wenzelm@19015
   113
      prefixes1 xs @@ [ys @ ws] @
wenzelm@19015
   114
      [xs @ ys] @@ prefixes1 zs @@ [ws];
wenzelm@25072
   115
  in (sfxs @ pfxs, sfxs) end;
wenzelm@13332
   116
wenzelm@5012
   117
wenzelm@5012
   118
wenzelm@5012
   119
(** name spaces **)
wenzelm@5012
   120
wenzelm@5012
   121
(* datatype T *)
wenzelm@5012
   122
wenzelm@5012
   123
datatype T =
wenzelm@25072
   124
  NameSpace of
wenzelm@30233
   125
    (string list * string list) Symtab.table *   (*internals, hidden internals*)
wenzelm@30233
   126
    string list Symtab.table;                    (*externals*)
wenzelm@5012
   127
wenzelm@25072
   128
val empty = NameSpace (Symtab.empty, Symtab.empty);
wenzelm@5012
   129
wenzelm@25072
   130
fun lookup (NameSpace (tab, _)) xname =
wenzelm@17412
   131
  (case Symtab.lookup tab xname of
wenzelm@16137
   132
    NONE => (xname, true)
wenzelm@30233
   133
  | SOME ([], []) => (xname, true)
wenzelm@30233
   134
  | SOME ([name], _) => (name, true)
wenzelm@30233
   135
  | SOME (name :: _, _) => (name, false)
wenzelm@30233
   136
  | SOME ([], name' :: _) => (hidden name', true));
wenzelm@8728
   137
wenzelm@30233
   138
fun get_accesses (NameSpace (_, xtab)) name =
wenzelm@30233
   139
  (case Symtab.lookup xtab name of
wenzelm@25072
   140
    NONE => [name]
wenzelm@30233
   141
  | SOME xnames => xnames);
wenzelm@25072
   142
wenzelm@25072
   143
fun put_accesses name xnames (NameSpace (tab, xtab)) =
wenzelm@30233
   144
  NameSpace (tab, Symtab.update (name, xnames) xtab);
wenzelm@25072
   145
wenzelm@30233
   146
fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
wenzelm@16444
   147
  if not (null names) andalso hd names = name then cons xname else I) tab [];
wenzelm@8728
   148
wenzelm@8728
   149
wenzelm@16137
   150
(* intern and extern *)
wenzelm@16137
   151
wenzelm@16137
   152
fun intern space xname = #1 (lookup space xname);
wenzelm@16137
   153
wenzelm@30215
   154
fun extern_flags {long_names, short_names, unique_names} space name =
wenzelm@16137
   155
  let
wenzelm@16137
   156
    fun valid unique xname =
wenzelm@16137
   157
      let val (name', uniq) = lookup space xname
wenzelm@26440
   158
      in name = name' andalso (uniq orelse not unique) end;
wenzelm@8728
   159
wenzelm@26440
   160
    fun ext [] = if valid false name then name else hidden name
wenzelm@30215
   161
      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
wenzelm@16137
   162
  in
wenzelm@30215
   163
    if long_names then name
wenzelm@30215
   164
    else if short_names then base name
wenzelm@30213
   165
    else ext (get_accesses space name)
wenzelm@16137
   166
  end;
wenzelm@16137
   167
wenzelm@30215
   168
val long_names = ref false;
wenzelm@30215
   169
val short_names = ref false;
wenzelm@30215
   170
val unique_names = ref true;
wenzelm@30215
   171
wenzelm@30215
   172
fun extern space name =
wenzelm@30215
   173
  extern_flags
wenzelm@30215
   174
   {long_names = ! long_names,
wenzelm@30215
   175
    short_names = ! short_names,
wenzelm@30215
   176
    unique_names = ! unique_names} space name;
wenzelm@30215
   177
wenzelm@5012
   178
wenzelm@16137
   179
(* basic operations *)
wenzelm@16137
   180
wenzelm@25072
   181
local
wenzelm@25072
   182
wenzelm@25072
   183
fun map_space f xname (NameSpace (tab, xtab)) =
wenzelm@30233
   184
  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
wenzelm@16137
   185
wenzelm@25072
   186
in
wenzelm@25072
   187
wenzelm@26440
   188
val del_name = map_space o apfst o remove (op =);
wenzelm@27196
   189
fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
wenzelm@26440
   190
val add_name = map_space o apfst o update (op =);
wenzelm@26440
   191
val add_name' = map_space o apsnd o update (op =);
wenzelm@8728
   192
wenzelm@25072
   193
end;
wenzelm@25072
   194
wenzelm@8728
   195
wenzelm@8728
   196
(* hide *)
wenzelm@5012
   197
wenzelm@16137
   198
fun hide fully name space =
wenzelm@8728
   199
  if not (is_qualified name) then
wenzelm@8728
   200
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   201
  else if is_hidden name then
wenzelm@8728
   202
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@16137
   203
  else
wenzelm@16137
   204
    let val names = valid_accesses space name in
wenzelm@16137
   205
      space
wenzelm@16137
   206
      |> add_name' name name
wenzelm@16137
   207
      |> fold (del_name name) (if fully then names else names inter_string [base name])
wenzelm@30213
   208
      |> fold (del_name_extra name) (get_accesses space name)
wenzelm@16137
   209
    end;
wenzelm@5012
   210
wenzelm@5012
   211
wenzelm@16137
   212
(* merge *)
wenzelm@5012
   213
wenzelm@25072
   214
fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
wenzelm@25072
   215
  let
wenzelm@25072
   216
    val tab' = (tab1, tab2) |> Symtab.join
wenzelm@30233
   217
      (K (fn names as ((names1, names1'), (names2, names2')) =>
wenzelm@30233
   218
        if pointer_eq names then raise Symtab.SAME
wenzelm@30233
   219
        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
wenzelm@25072
   220
    val xtab' = (xtab1, xtab2) |> Symtab.join
wenzelm@30233
   221
      (K (fn xnames =>
wenzelm@30233
   222
        if pointer_eq xnames then raise Symtab.SAME
wenzelm@30233
   223
        else (Library.merge (op =) xnames)));
wenzelm@25072
   224
  in NameSpace (tab', xtab') end;
wenzelm@5012
   225
wenzelm@16137
   226
wenzelm@26440
   227
wenzelm@16137
   228
(** naming contexts **)
wenzelm@16137
   229
wenzelm@16137
   230
(* datatype naming *)
wenzelm@16137
   231
wenzelm@16137
   232
datatype naming = Naming of
wenzelm@25072
   233
  string *                                                 (*path*)
wenzelm@25072
   234
  ((string -> string -> string) *                          (*qualify*)
wenzelm@25072
   235
   (string list -> string list list * string list list));  (*accesses*)
wenzelm@16137
   236
wenzelm@16137
   237
fun path_of (Naming (path, _)) = path;
wenzelm@25072
   238
fun accesses (Naming (_, (_, accs))) = accs;
wenzelm@25072
   239
wenzelm@25072
   240
fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
wenzelm@16137
   241
wenzelm@16137
   242
wenzelm@16137
   243
(* manipulate namings *)
wenzelm@16137
   244
wenzelm@16137
   245
fun reject_qualified name =
wenzelm@16137
   246
  if is_qualified name then
wenzelm@16137
   247
    error ("Attempt to declare qualified name " ^ quote name)
wenzelm@16137
   248
  else name;
wenzelm@16137
   249
wenzelm@16137
   250
val default_naming =
wenzelm@16137
   251
  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
wenzelm@16137
   252
wenzelm@16137
   253
fun add_path elems (Naming (path, policy)) =
wenzelm@16137
   254
  if elems = "//" then Naming ("", (qualified, #2 policy))
wenzelm@16137
   255
  else if elems = "/" then Naming ("", policy)
wenzelm@20530
   256
  else if elems = ".." then Naming (qualifier path, policy)
wenzelm@16137
   257
  else Naming (append path elems, policy);
wenzelm@16137
   258
wenzelm@16137
   259
fun no_base_names (Naming (path, (qualify, accs))) =
wenzelm@25072
   260
  Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
wenzelm@16137
   261
wenzelm@19015
   262
fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
wenzelm@19015
   263
wenzelm@19055
   264
fun sticky_prefix prfx (Naming (path, (qualify, _))) =
wenzelm@19055
   265
  Naming (append path prfx,
wenzelm@21858
   266
    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
wenzelm@19015
   267
haftmann@28860
   268
val apply_prefix =
haftmann@28860
   269
  let
haftmann@28860
   270
    fun mk_prefix (prfx, true) = sticky_prefix prfx
haftmann@28860
   271
      | mk_prefix (prfx, false) = add_path prfx;
haftmann@28860
   272
  in fold mk_prefix end;
haftmann@28860
   273
haftmann@28860
   274
wenzelm@30233
   275
(* full name *)
wenzelm@30233
   276
wenzelm@30233
   277
fun full (Naming (path, (qualify, _))) = qualify path;
haftmann@28860
   278
wenzelm@30233
   279
fun full_name naming binding =
wenzelm@30233
   280
  let
wenzelm@30233
   281
    val (prefix, qualifier, bname) = Binding.dest binding;
wenzelm@30233
   282
    val naming' = apply_prefix (prefix @ qualifier) naming;
wenzelm@30233
   283
  in full naming' bname end;
wenzelm@30233
   284
wenzelm@30233
   285
wenzelm@30233
   286
(* declaration *)
haftmann@28860
   287
wenzelm@30233
   288
fun declare naming binding space =
wenzelm@30233
   289
  let
wenzelm@30233
   290
    val (prefix, qualifier, bname) = Binding.dest binding;
wenzelm@30233
   291
    val naming' = apply_prefix (prefix @ qualifier) naming;
wenzelm@30233
   292
    val name = full naming' bname;
wenzelm@30233
   293
    val names = explode_name name;
haftmann@28860
   294
wenzelm@30233
   295
    val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
wenzelm@30233
   296
        orelse exists_string (fn s => s = "\"") name) andalso
wenzelm@30233
   297
      error ("Bad name declaration " ^ quote (Binding.str_of binding));
haftmann@28991
   298
wenzelm@30233
   299
    val (accs, accs') = pairself (map implode_name) (accesses naming' names);
wenzelm@30233
   300
    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
wenzelm@30233
   301
  in (name, space') end;
haftmann@28860
   302
wenzelm@16137
   303
wenzelm@16341
   304
wenzelm@16341
   305
(** name spaces coupled with symbol tables **)
wenzelm@16341
   306
wenzelm@16341
   307
type 'a table = T * 'a Symtab.table;
wenzelm@16341
   308
wenzelm@30233
   309
fun bind naming (binding, x) (space, tab) =
wenzelm@30233
   310
  let val (name, space') = declare naming binding space
wenzelm@30233
   311
  in (name, (space', Symtab.update_new (name, x) tab)) end;
wenzelm@16341
   312
wenzelm@30233
   313
val empty_table = (empty, Symtab.empty);
haftmann@28860
   314
wenzelm@16341
   315
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
wenzelm@19367
   316
  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
wenzelm@16341
   317
haftmann@28991
   318
fun join_tables f ((space1, tab1), (space2, tab2)) =
haftmann@28991
   319
  (merge (space1, space2), Symtab.join f (tab1, tab2));
haftmann@28991
   320
wenzelm@16848
   321
fun ext_table (space, tab) =
wenzelm@16848
   322
  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
wenzelm@16848
   323
  |> Library.sort_wrt (#2 o #1);
wenzelm@16848
   324
wenzelm@16848
   325
fun dest_table tab = map (apfst #1) (ext_table tab);
wenzelm@16848
   326
fun extern_table tab = map (apfst #2) (ext_table tab);
wenzelm@16341
   327
wenzelm@21858
   328
wenzelm@21858
   329
(*final declarations of this structure!*)
wenzelm@21858
   330
val implode = implode_name;
wenzelm@21858
   331
val explode = explode_name;
wenzelm@21858
   332
wenzelm@5012
   333
end;
wenzelm@30215
   334
wenzelm@30215
   335
structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
wenzelm@30215
   336
open BasicNameSpace;
wenzelm@30215
   337