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