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