src/Pure/General/name_space.ML
author wenzelm
Tue Mar 10 21:18:01 2009 +0100 (2009-03-10)
changeset 30418 b5044aca0729
parent 30412 7f5b0a020ccd
child 30438 c2d49315b93b
permissions -rw-r--r--
add_path: discontinued special meaning of "//", "/", "..";
added root_path, parent_path;
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@5012
    22
  type T
wenzelm@5012
    23
  val empty: T
wenzelm@16137
    24
  val intern: T -> xstring -> string
wenzelm@16137
    25
  val extern: T -> string -> xstring
wenzelm@30215
    26
  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
wenzelm@30215
    27
    T -> string -> xstring
wenzelm@16137
    28
  val hide: bool -> string -> T -> T
wenzelm@5012
    29
  val merge: T * T -> T
wenzelm@16137
    30
  type naming
haftmann@28965
    31
  val default_naming: naming
haftmann@29581
    32
  val declare: naming -> binding -> T -> string * T
haftmann@29581
    33
  val full_name: naming -> binding -> string
wenzelm@25072
    34
  val external_names: naming -> string -> string list
wenzelm@16137
    35
  val add_path: string -> naming -> naming
wenzelm@30418
    36
  val root_path: naming -> naming
wenzelm@30418
    37
  val parent_path: naming -> naming
wenzelm@19015
    38
  val no_base_names: naming -> naming
wenzelm@16137
    39
  val qualified_names: naming -> naming
wenzelm@19055
    40
  val sticky_prefix: string -> naming -> naming
wenzelm@24361
    41
  type 'a table = T * 'a Symtab.table
wenzelm@30233
    42
  val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
wenzelm@16341
    43
  val empty_table: 'a table
wenzelm@30233
    44
  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table  (*exception Symtab.DUP*)
wenzelm@30233
    45
  val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
wenzelm@30233
    46
    'a table * 'a table -> 'a table                                       (*exception Symtab.DUP*)
wenzelm@16848
    47
  val dest_table: 'a table -> (string * 'a) list
wenzelm@16341
    48
  val extern_table: 'a table -> (xstring * 'a) list
wenzelm@5012
    49
end;
wenzelm@5012
    50
wenzelm@5012
    51
structure NameSpace: NAME_SPACE =
wenzelm@5012
    52
struct
wenzelm@5012
    53
wenzelm@30412
    54
wenzelm@30412
    55
(** name spaces **)
wenzelm@30412
    56
wenzelm@30412
    57
(* hidden entries *)
wenzelm@5012
    58
wenzelm@16137
    59
fun hidden name = "??." ^ name;
haftmann@29338
    60
val is_hidden = String.isPrefix "??.";
wenzelm@16137
    61
wenzelm@5012
    62
wenzelm@5012
    63
(* datatype T *)
wenzelm@5012
    64
wenzelm@5012
    65
datatype T =
wenzelm@25072
    66
  NameSpace of
wenzelm@30233
    67
    (string list * string list) Symtab.table *   (*internals, hidden internals*)
wenzelm@30277
    68
    xstring list Symtab.table;                   (*externals*)
wenzelm@5012
    69
wenzelm@25072
    70
val empty = NameSpace (Symtab.empty, Symtab.empty);
wenzelm@5012
    71
wenzelm@25072
    72
fun lookup (NameSpace (tab, _)) xname =
wenzelm@17412
    73
  (case Symtab.lookup tab xname of
wenzelm@16137
    74
    NONE => (xname, true)
wenzelm@30233
    75
  | SOME ([], []) => (xname, true)
wenzelm@30233
    76
  | SOME ([name], _) => (name, true)
wenzelm@30233
    77
  | SOME (name :: _, _) => (name, false)
wenzelm@30233
    78
  | SOME ([], name' :: _) => (hidden name', true));
wenzelm@8728
    79
wenzelm@30233
    80
fun get_accesses (NameSpace (_, xtab)) name =
wenzelm@30233
    81
  (case Symtab.lookup xtab name of
wenzelm@25072
    82
    NONE => [name]
wenzelm@30233
    83
  | SOME xnames => xnames);
wenzelm@25072
    84
wenzelm@25072
    85
fun put_accesses name xnames (NameSpace (tab, xtab)) =
wenzelm@30233
    86
  NameSpace (tab, Symtab.update (name, xnames) xtab);
wenzelm@25072
    87
wenzelm@30233
    88
fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
wenzelm@16444
    89
  if not (null names) andalso hd names = name then cons xname else I) tab [];
wenzelm@8728
    90
wenzelm@8728
    91
wenzelm@16137
    92
(* intern and extern *)
wenzelm@16137
    93
wenzelm@16137
    94
fun intern space xname = #1 (lookup space xname);
wenzelm@16137
    95
wenzelm@30215
    96
fun extern_flags {long_names, short_names, unique_names} space name =
wenzelm@16137
    97
  let
wenzelm@30277
    98
    fun valid require_unique xname =
wenzelm@30277
    99
      let val (name', is_unique) = lookup space xname
wenzelm@30277
   100
      in name = name' andalso (not require_unique orelse is_unique) end;
wenzelm@8728
   101
wenzelm@26440
   102
    fun ext [] = if valid false name then name else hidden name
wenzelm@30215
   103
      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
wenzelm@16137
   104
  in
wenzelm@30215
   105
    if long_names then name
wenzelm@30359
   106
    else if short_names then Long_Name.base_name name
wenzelm@30213
   107
    else ext (get_accesses space name)
wenzelm@16137
   108
  end;
wenzelm@16137
   109
wenzelm@30215
   110
val long_names = ref false;
wenzelm@30215
   111
val short_names = ref false;
wenzelm@30215
   112
val unique_names = ref true;
wenzelm@30215
   113
wenzelm@30215
   114
fun extern space name =
wenzelm@30215
   115
  extern_flags
wenzelm@30215
   116
   {long_names = ! long_names,
wenzelm@30215
   117
    short_names = ! short_names,
wenzelm@30215
   118
    unique_names = ! unique_names} space name;
wenzelm@30215
   119
wenzelm@5012
   120
wenzelm@16137
   121
(* basic operations *)
wenzelm@16137
   122
wenzelm@25072
   123
local
wenzelm@25072
   124
wenzelm@25072
   125
fun map_space f xname (NameSpace (tab, xtab)) =
wenzelm@30233
   126
  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
wenzelm@16137
   127
wenzelm@25072
   128
in
wenzelm@25072
   129
wenzelm@26440
   130
val del_name = map_space o apfst o remove (op =);
wenzelm@27196
   131
fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
wenzelm@26440
   132
val add_name = map_space o apfst o update (op =);
wenzelm@26440
   133
val add_name' = map_space o apsnd o update (op =);
wenzelm@8728
   134
wenzelm@25072
   135
end;
wenzelm@25072
   136
wenzelm@8728
   137
wenzelm@8728
   138
(* hide *)
wenzelm@5012
   139
wenzelm@16137
   140
fun hide fully name space =
wenzelm@30359
   141
  if not (Long_Name.is_qualified name) then
wenzelm@8728
   142
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   143
  else if is_hidden name then
wenzelm@8728
   144
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@16137
   145
  else
wenzelm@16137
   146
    let val names = valid_accesses space name in
wenzelm@16137
   147
      space
wenzelm@16137
   148
      |> add_name' name name
wenzelm@30359
   149
      |> fold (del_name name)
wenzelm@30359
   150
        (if fully then names else names inter_string [Long_Name.base_name name])
wenzelm@30213
   151
      |> fold (del_name_extra name) (get_accesses space name)
wenzelm@16137
   152
    end;
wenzelm@5012
   153
wenzelm@5012
   154
wenzelm@16137
   155
(* merge *)
wenzelm@5012
   156
wenzelm@25072
   157
fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
wenzelm@25072
   158
  let
wenzelm@25072
   159
    val tab' = (tab1, tab2) |> Symtab.join
wenzelm@30233
   160
      (K (fn names as ((names1, names1'), (names2, names2')) =>
wenzelm@30233
   161
        if pointer_eq names then raise Symtab.SAME
wenzelm@30233
   162
        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
wenzelm@25072
   163
    val xtab' = (xtab1, xtab2) |> Symtab.join
wenzelm@30233
   164
      (K (fn xnames =>
wenzelm@30233
   165
        if pointer_eq xnames then raise Symtab.SAME
wenzelm@30233
   166
        else (Library.merge (op =) xnames)));
wenzelm@25072
   167
  in NameSpace (tab', xtab') end;
wenzelm@5012
   168
wenzelm@16137
   169
wenzelm@26440
   170
wenzelm@16137
   171
(** naming contexts **)
wenzelm@16137
   172
wenzelm@16137
   173
(* datatype naming *)
wenzelm@16137
   174
wenzelm@16137
   175
datatype naming = Naming of
wenzelm@30412
   176
 {path: (string * bool) list,
wenzelm@30412
   177
  no_base_names: bool,
wenzelm@30412
   178
  qualified_names: bool};
wenzelm@16137
   179
wenzelm@30412
   180
fun make_naming (path, no_base_names, qualified_names) =
wenzelm@30412
   181
  Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
wenzelm@25072
   182
wenzelm@30412
   183
fun map_naming f (Naming {path, no_base_names, qualified_names}) =
wenzelm@30412
   184
  make_naming (f (path, no_base_names, qualified_names));
wenzelm@30412
   185
wenzelm@30412
   186
fun path_of (Naming {path, ...}) = path;
wenzelm@16137
   187
wenzelm@16137
   188
wenzelm@30412
   189
(* configure naming *)
wenzelm@16137
   190
wenzelm@30412
   191
val default_naming = make_naming ([], false, false);
wenzelm@16137
   192
wenzelm@30412
   193
fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
wenzelm@30418
   194
  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
wenzelm@30418
   195
wenzelm@30418
   196
val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
wenzelm@30418
   197
  ([], no_base_names, qualified_names));
wenzelm@30418
   198
wenzelm@30418
   199
val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
wenzelm@30418
   200
  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
wenzelm@19015
   201
wenzelm@30412
   202
fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
wenzelm@30412
   203
  (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
wenzelm@19015
   204
wenzelm@30412
   205
val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
wenzelm@30412
   206
val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
haftmann@28860
   207
haftmann@28860
   208
wenzelm@30233
   209
(* full name *)
wenzelm@30233
   210
wenzelm@30412
   211
fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
haftmann@28860
   212
wenzelm@30412
   213
fun name_spec (Naming {path, qualified_names, ...}) binding =
wenzelm@30233
   214
  let
wenzelm@30412
   215
    val (prefix, name) = Binding.dest binding;
wenzelm@30412
   216
    val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
wenzelm@30412
   217
wenzelm@30412
   218
    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
wenzelm@30412
   219
    val spec2 =
wenzelm@30412
   220
      (case try split_last (Long_Name.explode name) of
wenzelm@30412
   221
        NONE => []
wenzelm@30412
   222
      | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
wenzelm@30412
   223
wenzelm@30412
   224
    val spec = spec1 @ spec2;
wenzelm@30412
   225
    val _ =
wenzelm@30412
   226
      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
wenzelm@30412
   227
      andalso err_bad binding;
wenzelm@30412
   228
  in if null spec2 then [] else spec end;
wenzelm@30412
   229
wenzelm@30412
   230
fun full naming = name_spec naming #> map fst;
wenzelm@30412
   231
fun full_name naming = full naming #> Long_Name.implode;
wenzelm@30412
   232
wenzelm@30412
   233
wenzelm@30412
   234
(* accesses *)
wenzelm@30412
   235
wenzelm@30412
   236
fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
wenzelm@30412
   237
wenzelm@30412
   238
fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
wenzelm@30412
   239
and mandatory_prefixes1 [] = []
wenzelm@30412
   240
  | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
wenzelm@30412
   241
  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
wenzelm@30412
   242
wenzelm@30412
   243
fun mandatory_suffixes1 xs = map rev (mandatory_prefixes1 (rev xs));
wenzelm@30412
   244
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
wenzelm@30412
   245
wenzelm@30412
   246
fun accesses (naming as Naming {no_base_names, ...}) binding =
wenzelm@30412
   247
  let
wenzelm@30412
   248
    val spec = name_spec naming binding;
wenzelm@30412
   249
    val sfxs = mandatory_suffixes spec;
wenzelm@30412
   250
    val pfxs = mandatory_prefixes spec;
wenzelm@30412
   251
  in
wenzelm@30412
   252
    (sfxs @ pfxs, sfxs)
wenzelm@30412
   253
    |> pairself (no_base_names ? filter (fn [_] => false | _ => true))
wenzelm@30412
   254
    |> pairself (map Long_Name.implode)
wenzelm@30412
   255
  end;
wenzelm@30412
   256
wenzelm@30412
   257
fun external_names naming = #2 o accesses naming o Binding.qualified_name;
wenzelm@30233
   258
wenzelm@30233
   259
wenzelm@30233
   260
(* declaration *)
haftmann@28860
   261
wenzelm@30233
   262
fun declare naming binding space =
wenzelm@30233
   263
  let
wenzelm@30412
   264
    val names = full naming binding;
wenzelm@30412
   265
    val name = Long_Name.implode names;
wenzelm@30412
   266
    val _ = name = "" andalso err_bad binding;
wenzelm@30412
   267
    val (accs, accs') = accesses naming binding;
wenzelm@30233
   268
    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
wenzelm@30233
   269
  in (name, space') end;
haftmann@28860
   270
wenzelm@16137
   271
wenzelm@16341
   272
wenzelm@16341
   273
(** name spaces coupled with symbol tables **)
wenzelm@16341
   274
wenzelm@16341
   275
type 'a table = T * 'a Symtab.table;
wenzelm@16341
   276
wenzelm@30233
   277
fun bind naming (binding, x) (space, tab) =
wenzelm@30233
   278
  let val (name, space') = declare naming binding space
wenzelm@30233
   279
  in (name, (space', Symtab.update_new (name, x) tab)) end;
wenzelm@16341
   280
wenzelm@30233
   281
val empty_table = (empty, Symtab.empty);
haftmann@28860
   282
wenzelm@16341
   283
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
wenzelm@19367
   284
  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
wenzelm@16341
   285
haftmann@28991
   286
fun join_tables f ((space1, tab1), (space2, tab2)) =
haftmann@28991
   287
  (merge (space1, space2), Symtab.join f (tab1, tab2));
haftmann@28991
   288
wenzelm@16848
   289
fun ext_table (space, tab) =
wenzelm@16848
   290
  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
wenzelm@16848
   291
  |> Library.sort_wrt (#2 o #1);
wenzelm@16848
   292
wenzelm@16848
   293
fun dest_table tab = map (apfst #1) (ext_table tab);
wenzelm@16848
   294
fun extern_table tab = map (apfst #2) (ext_table tab);
wenzelm@16341
   295
wenzelm@5012
   296
end;
wenzelm@30215
   297
wenzelm@30215
   298
structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
wenzelm@30215
   299
open BasicNameSpace;
wenzelm@30215
   300