src/Pure/General/name_space.ML
author wenzelm
Wed Jan 10 20:17:26 2007 +0100 (2007-01-10)
changeset 22057 d7c91b2f5a9e
parent 21962 279b129498b6
child 23086 12320f6e2523
permissions -rw-r--r--
removed NameSpace.split -- use qualifier/base instead;
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@21858
    25
  val implode: string list -> string
wenzelm@21858
    26
  val explode: 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@20530
    30
  val qualifier: string -> string
wenzelm@11829
    31
  val map_base: (string -> string) -> string -> string
wenzelm@16137
    32
  val suffixes_prefixes: 'a list -> 'a list list
wenzelm@19015
    33
  val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
wenzelm@5012
    34
  val accesses: string -> string list
wenzelm@13332
    35
  val accesses': string -> string list
wenzelm@5012
    36
  type T
wenzelm@5012
    37
  val empty: T
wenzelm@16137
    38
  val valid_accesses: T -> string -> xstring list
wenzelm@16137
    39
  val intern: T -> xstring -> string
wenzelm@16137
    40
  val extern: T -> string -> xstring
wenzelm@16137
    41
  val hide: bool -> string -> T -> T
wenzelm@5012
    42
  val merge: T * T -> T
wenzelm@16137
    43
  type naming
wenzelm@16137
    44
  val path_of: naming -> string
wenzelm@16137
    45
  val full: naming -> bstring -> string
wenzelm@16137
    46
  val declare: naming -> string -> T -> T
wenzelm@16137
    47
  val default_naming: naming
wenzelm@16137
    48
  val add_path: string -> naming -> naming
wenzelm@19015
    49
  val no_base_names: naming -> naming
wenzelm@16137
    50
  val qualified_names: naming -> naming
wenzelm@19055
    51
  val sticky_prefix: string -> naming -> naming
wenzelm@16137
    52
  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
wenzelm@16137
    53
    naming -> naming
wenzelm@17756
    54
  type 'a table (*= T * 'a Symtab.table*)
wenzelm@16341
    55
  val empty_table: 'a table
wenzelm@16341
    56
  val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
wenzelm@16341
    57
  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
wenzelm@16848
    58
  val dest_table: 'a table -> (string * 'a) list
wenzelm@16341
    59
  val extern_table: 'a table -> (xstring * 'a) list
wenzelm@5012
    60
end;
wenzelm@5012
    61
wenzelm@5012
    62
structure NameSpace: NAME_SPACE =
wenzelm@5012
    63
struct
wenzelm@5012
    64
wenzelm@5012
    65
(** long identifiers **)
wenzelm@5012
    66
wenzelm@16137
    67
fun hidden name = "??." ^ name;
wenzelm@16137
    68
val is_hidden = String.isPrefix "??."
wenzelm@16137
    69
wenzelm@5012
    70
val separator = ".";
wenzelm@19305
    71
val is_qualified = exists_string (fn s => s = separator);
wenzelm@5012
    72
wenzelm@21858
    73
val implode_name = space_implode separator;
wenzelm@21858
    74
val explode_name = space_explode separator;
wenzelm@5012
    75
wenzelm@16137
    76
fun append name1 "" = name1
wenzelm@16137
    77
  | append "" name2 = name2
wenzelm@16137
    78
  | append name1 name2 = name1 ^ separator ^ name2;
wenzelm@16137
    79
wenzelm@16137
    80
fun qualified path name =
wenzelm@16137
    81
  if path = "" orelse name = "" then name
wenzelm@16137
    82
  else path ^ separator ^ name;
wenzelm@11829
    83
wenzelm@16137
    84
fun base "" = ""
wenzelm@21858
    85
  | base name = List.last (explode_name name);
wenzelm@11829
    86
wenzelm@20530
    87
fun qualifier "" = ""
wenzelm@21858
    88
  | qualifier name = implode_name (#1 (split_last (explode_name name)));
wenzelm@5012
    89
wenzelm@16137
    90
fun map_base _ "" = ""
wenzelm@16137
    91
  | map_base f name =
wenzelm@21858
    92
      let val names = explode_name name
wenzelm@21858
    93
      in implode_name (nth_map (length names - 1) f names) end;
wenzelm@16137
    94
wenzelm@19015
    95
wenzelm@19015
    96
(* accesses *)
wenzelm@19015
    97
wenzelm@19015
    98
infixr 6 @@;
wenzelm@19015
    99
fun ([] @@ yss) = []
wenzelm@19015
   100
  | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
wenzelm@19015
   101
wenzelm@19015
   102
fun suffixes_prefixes list =
wenzelm@5012
   103
  let
wenzelm@19015
   104
    val (xs, ws) = chop (length list - 1) list;
wenzelm@19015
   105
    val sfxs = suffixes xs @@ [ws];
wenzelm@19015
   106
    val pfxs = prefixes1 xs @@ [ws];
wenzelm@19015
   107
  in sfxs @ pfxs end;
wenzelm@19015
   108
wenzelm@19015
   109
fun suffixes_prefixes_split i k list =
wenzelm@19015
   110
  let
wenzelm@19015
   111
    val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
wenzelm@19015
   112
    val sfxs =
wenzelm@19015
   113
      [ys] @@ suffixes zs @@ [ws] @
wenzelm@19015
   114
      suffixes1 xs @@ [ys @ zs @ ws];
wenzelm@19015
   115
    val pfxs =
wenzelm@19015
   116
      prefixes1 xs @@ [ys @ ws] @
wenzelm@19015
   117
      [xs @ ys] @@ prefixes1 zs @@ [ws];
wenzelm@16137
   118
  in sfxs @ pfxs end;
wenzelm@5012
   119
wenzelm@21858
   120
val accesses = map implode_name o suffixes_prefixes o explode_name;
wenzelm@21858
   121
val accesses' = map implode_name o Library.suffixes1 o explode_name;
wenzelm@13332
   122
wenzelm@5012
   123
wenzelm@5012
   124
wenzelm@5012
   125
(** name spaces **)
wenzelm@5012
   126
wenzelm@5012
   127
(* datatype T *)
wenzelm@5012
   128
wenzelm@5012
   129
datatype T =
wenzelm@19030
   130
  NameSpace of ((string list * string list) * stamp) Symtab.table;
wenzelm@5012
   131
wenzelm@5012
   132
val empty = NameSpace Symtab.empty;
wenzelm@5012
   133
wenzelm@16137
   134
fun lookup (NameSpace tab) xname =
wenzelm@17412
   135
  (case Symtab.lookup tab xname of
wenzelm@16137
   136
    NONE => (xname, true)
wenzelm@19030
   137
  | SOME (([], []), _) => (xname, true)
wenzelm@19030
   138
  | SOME (([name], _), _) => (name, true)
wenzelm@19030
   139
  | SOME ((name :: _, _), _) => (name, false)
wenzelm@19030
   140
  | SOME (([], name' :: _), _) => (hidden name', true));
wenzelm@8728
   141
wenzelm@19030
   142
fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, ((names, _), _)) =>
wenzelm@16444
   143
  if not (null names) andalso hd names = name then cons xname else I) tab [];
wenzelm@8728
   144
wenzelm@8728
   145
wenzelm@16137
   146
(* intern and extern *)
wenzelm@16137
   147
wenzelm@16137
   148
fun intern space xname = #1 (lookup space xname);
wenzelm@16137
   149
wenzelm@16137
   150
val long_names = ref false;
wenzelm@16137
   151
val short_names = ref false;
wenzelm@16137
   152
val unique_names = ref true;
wenzelm@16137
   153
wenzelm@16137
   154
fun extern space name =
wenzelm@16137
   155
  let
wenzelm@16137
   156
    fun valid unique xname =
wenzelm@16137
   157
      let val (name', uniq) = lookup space xname
wenzelm@16137
   158
      in name = name' andalso (uniq orelse (not unique)) end;
wenzelm@8728
   159
wenzelm@16137
   160
    fun ex [] = if valid false name then name else hidden name
wenzelm@16137
   161
      | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
wenzelm@16137
   162
  in
wenzelm@16137
   163
    if ! long_names then name
wenzelm@16137
   164
    else if ! short_names then base name
wenzelm@16137
   165
    else ex (accesses' name)
wenzelm@16137
   166
  end;
wenzelm@16137
   167
wenzelm@5012
   168
wenzelm@16137
   169
(* basic operations *)
wenzelm@16137
   170
wenzelm@16137
   171
fun map_space f xname (NameSpace tab) =
wenzelm@19030
   172
  let val entry' =
wenzelm@19030
   173
    (case Symtab.lookup tab xname of
wenzelm@19030
   174
      NONE => f ([], [])
wenzelm@19030
   175
    | SOME (entry, _) => f entry)
wenzelm@19030
   176
  in NameSpace (Symtab.update (xname, (entry', stamp ())) tab) end;
wenzelm@16137
   177
wenzelm@16137
   178
fun del (name: string) = remove (op =) name;
wenzelm@16137
   179
fun add name names = name :: del name names;
wenzelm@16137
   180
wenzelm@16137
   181
val del_name = map_space o apfst o del;
wenzelm@16137
   182
val add_name = map_space o apfst o add;
wenzelm@16137
   183
val add_name' = map_space o apsnd o add;
wenzelm@8728
   184
wenzelm@8728
   185
wenzelm@8728
   186
(* hide *)
wenzelm@5012
   187
wenzelm@16137
   188
fun hide fully name space =
wenzelm@8728
   189
  if not (is_qualified name) then
wenzelm@8728
   190
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   191
  else if is_hidden name then
wenzelm@8728
   192
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@16137
   193
  else
wenzelm@16137
   194
    let val names = valid_accesses space name in
wenzelm@16137
   195
      space
wenzelm@16137
   196
      |> add_name' name name
wenzelm@16137
   197
      |> fold (del_name name) (if fully then names else names inter_string [base name])
wenzelm@16137
   198
    end;
wenzelm@5012
   199
wenzelm@5012
   200
wenzelm@16137
   201
(* merge *)
wenzelm@5012
   202
wenzelm@19030
   203
fun merge (NameSpace tab1, NameSpace tab2) =
wenzelm@19030
   204
  NameSpace ((tab1, tab2) |> Symtab.join
wenzelm@19030
   205
    (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
wenzelm@19030
   206
      if stamp1 = stamp2 then raise Symtab.SAME
wenzelm@19030
   207
      else
wenzelm@19030
   208
        ((Library.merge (op =) (names2, names1),
wenzelm@19030
   209
          Library.merge (op =) (names2', names1')), stamp ()))));
wenzelm@6845
   210
wenzelm@5012
   211
wenzelm@16137
   212
wenzelm@16137
   213
(** naming contexts **)
wenzelm@16137
   214
wenzelm@16137
   215
(* datatype naming *)
wenzelm@16137
   216
wenzelm@16137
   217
datatype naming = Naming of
wenzelm@16137
   218
  string * ((string -> string -> string) * (string list -> string list list));
wenzelm@16137
   219
wenzelm@16137
   220
fun path_of (Naming (path, _)) = path;
wenzelm@16137
   221
wenzelm@16137
   222
wenzelm@16137
   223
(* declarations *)
wenzelm@16137
   224
wenzelm@16137
   225
fun full (Naming (path, (qualify, _))) = qualify path;
wenzelm@16137
   226
wenzelm@16137
   227
fun declare (Naming (_, (_, accs))) name space =
wenzelm@16137
   228
  if is_hidden name then
wenzelm@16137
   229
    error ("Attempt to declare hidden name " ^ quote name)
wenzelm@16137
   230
  else
wenzelm@21962
   231
    let
wenzelm@21962
   232
      val names = explode_name name;
wenzelm@21962
   233
      val _ = (null names orelse exists (fn s => s = "") names) andalso
wenzelm@21962
   234
        error ("Bad name declaration " ^ quote name);
wenzelm@21962
   235
    in fold (add_name name) (map implode_name (accs names)) space end;
wenzelm@16137
   236
wenzelm@16137
   237
wenzelm@16137
   238
(* manipulate namings *)
wenzelm@16137
   239
wenzelm@16137
   240
fun reject_qualified name =
wenzelm@16137
   241
  if is_qualified name then
wenzelm@16137
   242
    error ("Attempt to declare qualified name " ^ quote name)
wenzelm@16137
   243
  else name;
wenzelm@16137
   244
wenzelm@16137
   245
val default_naming =
wenzelm@16137
   246
  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
wenzelm@16137
   247
wenzelm@16137
   248
fun add_path elems (Naming (path, policy)) =
wenzelm@16137
   249
  if elems = "//" then Naming ("", (qualified, #2 policy))
wenzelm@16137
   250
  else if elems = "/" then Naming ("", policy)
wenzelm@20530
   251
  else if elems = ".." then Naming (qualifier path, policy)
wenzelm@16137
   252
  else Naming (append path elems, policy);
wenzelm@16137
   253
wenzelm@16137
   254
fun no_base_names (Naming (path, (qualify, accs))) =
wenzelm@16137
   255
  Naming (path, (qualify, filter_out (fn [_] => true | _ => false) o accs));
wenzelm@16137
   256
wenzelm@19015
   257
fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
wenzelm@19015
   258
wenzelm@19055
   259
fun sticky_prefix prfx (Naming (path, (qualify, _))) =
wenzelm@19055
   260
  Naming (append path prfx,
wenzelm@21858
   261
    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
wenzelm@19015
   262
wenzelm@16137
   263
fun set_policy policy (Naming (path, _)) = Naming (path, policy);
wenzelm@16137
   264
wenzelm@16137
   265
wenzelm@16341
   266
wenzelm@16341
   267
(** name spaces coupled with symbol tables **)
wenzelm@16341
   268
wenzelm@16341
   269
type 'a table = T * 'a Symtab.table;
wenzelm@16341
   270
wenzelm@16341
   271
val empty_table = (empty, Symtab.empty);
wenzelm@16341
   272
wenzelm@16341
   273
fun extend_table naming ((space, tab), bentries) =
wenzelm@16341
   274
  let val entries = map (apfst (full naming)) bentries
wenzelm@16341
   275
  in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
wenzelm@16341
   276
wenzelm@16341
   277
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
wenzelm@19367
   278
  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
wenzelm@16341
   279
wenzelm@16848
   280
fun ext_table (space, tab) =
wenzelm@16848
   281
  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
wenzelm@16848
   282
  |> Library.sort_wrt (#2 o #1);
wenzelm@16848
   283
wenzelm@16848
   284
fun dest_table tab = map (apfst #1) (ext_table tab);
wenzelm@16848
   285
fun extern_table tab = map (apfst #2) (ext_table tab);
wenzelm@16341
   286
wenzelm@21858
   287
wenzelm@21858
   288
(*final declarations of this structure!*)
wenzelm@21858
   289
val implode = implode_name;
wenzelm@21858
   290
val explode = explode_name;
wenzelm@21858
   291
wenzelm@5012
   292
end;
wenzelm@5175
   293
wenzelm@16137
   294
structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
wenzelm@16137
   295
open BasicNameSpace;