src/Pure/General/name_space.ML
author haftmann
Mon, 01 Dec 2008 19:41:16 +0100
changeset 28941 128459bd72d2
parent 28923 0a981c596372
child 28965 1de908189869
permissions -rw-r--r--
new Binding module
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5682
diff changeset
     1
(*  Title:      Pure/General/name_space.ML
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     3
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
     4
Generic name spaces with declared and hidden entries.  Unknown names
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
     5
are considered global; no support for absolute addressing.
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
     6
*)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
     7
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
     8
type bstring = string;    (*names to be bound*)
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
     9
type xstring = string;    (*external names*)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    10
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    11
signature NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    12
sig
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    13
  include BASIC_BINDING
9120
04a46ceace35 export hidden: string -> string;
wenzelm
parents: 8806
diff changeset
    14
  val hidden: string -> string
25225
e638164593bf export is_hidden;
wenzelm
parents: 25072
diff changeset
    15
  val is_hidden: string -> bool
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    16
  val separator: string                 (*single char*)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    17
  val is_qualified: string -> bool
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    18
  val implode: string list -> string
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    19
  val explode: string -> string list
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    20
  val append: string -> string -> string
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    21
  val qualified: string -> string -> string
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    22
  val base: string -> string
20530
448594cbd82b renamed NameSpace.drop_base to NameSpace.qualifier;
wenzelm
parents: 19367
diff changeset
    23
  val qualifier: string -> string
11829
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    24
  val map_base: (string -> string) -> string -> string
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    25
  type T
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    26
  val empty: T
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    27
  val intern: T -> xstring -> string
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    28
  val extern: T -> string -> xstring
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    29
  val hide: bool -> string -> T -> T
28923
0a981c596372 exported get_accesses (for diagnostic purpose)
haftmann
parents: 28860
diff changeset
    30
  val get_accesses: T -> string -> xstring list
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    31
  val merge: T * T -> T
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    32
  type naming
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    33
  val path_of: naming -> string
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
    34
  val external_names: naming -> string -> string list
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    35
  val full: naming -> bstring -> string
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    36
  val declare: naming -> string -> T -> T
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    37
  val default_naming: naming
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    38
  val add_path: string -> naming -> naming
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    39
  val no_base_names: naming -> naming
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    40
  val qualified_names: naming -> naming
19055
4f408867f9d4 removed qualified_force_prefix;
wenzelm
parents: 19030
diff changeset
    41
  val sticky_prefix: string -> naming -> naming
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    42
  val full_binding: naming -> Binding.T -> string
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    43
  val declare_binding: naming -> Binding.T -> T -> string * T
24361
52a14669f9e9 tuned signature;
wenzelm
parents: 23668
diff changeset
    44
  type 'a table = T * 'a Symtab.table
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
    45
  val empty_table: 'a table
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    46
  val table_declare: naming -> Binding.T * 'a
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
    47
    -> 'a table -> string * 'a table (*exception Symtab.DUP*)
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    48
  val table_declare_permissive: naming -> Binding.T * 'a
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
    49
    -> 'a table -> string * 'a table
23086
12320f6e2523 tuned Pure/General/name_space.ML
haftmann
parents: 22057
diff changeset
    50
  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
    51
  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
    52
  val dest_table: 'a table -> (string * 'a) list
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
    53
  val extern_table: 'a table -> (xstring * 'a) list
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    54
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    55
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    56
structure NameSpace: NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    57
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    58
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    59
open Basic_Binding;
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    60
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
    61
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    62
(** long identifiers **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    63
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    64
fun hidden name = "??." ^ name;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    65
val is_hidden = String.isPrefix "??."
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    66
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    67
val separator = ".";
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 19055
diff changeset
    68
val is_qualified = exists_string (fn s => s = separator);
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    69
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    70
val implode_name = space_implode separator;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    71
val explode_name = space_explode separator;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    72
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    73
fun append name1 "" = name1
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    74
  | append "" name2 = name2
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    75
  | append name1 name2 = name1 ^ separator ^ name2;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    76
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    77
fun qualified path name =
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    78
  if path = "" orelse name = "" then name
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    79
  else path ^ separator ^ name;
11829
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    80
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    81
fun base "" = ""
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    82
  | base name = List.last (explode_name name);
11829
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    83
20530
448594cbd82b renamed NameSpace.drop_base to NameSpace.qualifier;
wenzelm
parents: 19367
diff changeset
    84
fun qualifier "" = ""
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    85
  | qualifier name = implode_name (#1 (split_last (explode_name name)));
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    86
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    87
fun map_base _ "" = ""
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    88
  | map_base f name =
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    89
      let val names = explode_name name
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
    90
      in implode_name (nth_map (length names - 1) f names) end;
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    91
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    92
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
    93
(* standard accesses *)
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    94
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    95
infixr 6 @@;
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    96
fun ([] @@ yss) = []
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    97
  | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    98
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
    99
fun suffixes_prefixes list =
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   100
  let
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   101
    val (xs, ws) = chop (length list - 1) list;
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   102
    val sfxs = suffixes xs @@ [ws];
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   103
    val pfxs = prefixes1 xs @@ [ws];
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   104
  in (sfxs @ pfxs, sfxs) end;
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   105
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   106
fun suffixes_prefixes_split i k list =
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   107
  let
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   108
    val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   109
    val sfxs =
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   110
      [ys] @@ suffixes zs @@ [ws] @
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   111
      suffixes1 xs @@ [ys @ zs @ ws];
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   112
    val pfxs =
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   113
      prefixes1 xs @@ [ys @ ws] @
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   114
      [xs @ ys] @@ prefixes1 zs @@ [ws];
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   115
  in (sfxs @ pfxs, sfxs) end;
13332
f130bcf29620 added accesses';
wenzelm
parents: 12588
diff changeset
   116
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   117
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   118
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   119
(** name spaces **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   120
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   121
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   122
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   123
datatype T =
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   124
  NameSpace of
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   125
    ((string list * string list) * stamp) Symtab.table *   (*internals, hidden internals*)
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   126
    (string list * stamp) Symtab.table;                    (*externals*)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   127
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   128
val empty = NameSpace (Symtab.empty, Symtab.empty);
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   129
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   130
fun lookup (NameSpace (tab, _)) xname =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
   131
  (case Symtab.lookup tab xname of
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   132
    NONE => (xname, true)
19030
78d43fe9ac65 low-level tuning of merge: maintain identity of accesses;
wenzelm
parents: 19015
diff changeset
   133
  | SOME (([], []), _) => (xname, true)
78d43fe9ac65 low-level tuning of merge: maintain identity of accesses;
wenzelm
parents: 19015
diff changeset
   134
  | SOME (([name], _), _) => (name, true)
78d43fe9ac65 low-level tuning of merge: maintain identity of accesses;
wenzelm
parents: 19015
diff changeset
   135
  | SOME ((name :: _, _), _) => (name, false)
78d43fe9ac65 low-level tuning of merge: maintain identity of accesses;
wenzelm
parents: 19015
diff changeset
   136
  | SOME (([], name' :: _), _) => (hidden name', true));
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   137
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   138
fun get_accesses (NameSpace (_, tab)) name =
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   139
  (case Symtab.lookup tab name of
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   140
    NONE => [name]
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   141
  | SOME (xnames, _) => xnames);
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   142
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   143
fun put_accesses name xnames (NameSpace (tab, xtab)) =
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   144
  NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   145
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   146
fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, ((names, _), _)) =>
16444
80c8f742c6fc Symtab.fold;
wenzelm
parents: 16341
diff changeset
   147
  if not (null names) andalso hd names = name then cons xname else I) tab [];
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   148
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   149
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   150
(* intern and extern *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   151
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   152
fun intern space xname = #1 (lookup space xname);
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   153
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   154
fun extern space name =
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   155
  let
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   156
    fun valid unique xname =
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   157
      let val (name', uniq) = lookup space xname
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   158
      in name = name' andalso (uniq orelse not unique) end;
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   159
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   160
    fun ext [] = if valid false name then name else hidden name
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   161
      | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   162
  in
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   163
    if ! long_names then name
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   164
    else if ! short_names then base name
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   165
    else ext (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   166
  end;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   167
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   168
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   169
(* basic operations *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   170
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   171
local
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   172
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   173
fun map_space f xname (NameSpace (tab, xtab)) =
23086
12320f6e2523 tuned Pure/General/name_space.ML
haftmann
parents: 22057
diff changeset
   174
  NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   175
    (fn (entry, _) => (f entry, stamp ())) tab, xtab);
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   176
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   177
in
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   178
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   179
val del_name = map_space o apfst o remove (op =);
27196
ef2f01da7a12 hide: delete all accesses from extra names -- reduces ambiguity in extern;
wenzelm
parents: 26657
diff changeset
   180
fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   181
val add_name = map_space o apfst o update (op =);
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   182
val add_name' = map_space o apsnd o update (op =);
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   183
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   184
end;
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   185
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   186
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   187
(* hide *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   188
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   189
fun hide fully name space =
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   190
  if not (is_qualified name) then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   191
    error ("Attempt to hide global name " ^ quote name)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   192
  else if is_hidden name then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   193
    error ("Attempt to hide hidden name " ^ quote name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   194
  else
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   195
    let val names = valid_accesses space name in
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   196
      space
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   197
      |> add_name' name name
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   198
      |> fold (del_name name) (if fully then names else names inter_string [base name])
27196
ef2f01da7a12 hide: delete all accesses from extra names -- reduces ambiguity in extern;
wenzelm
parents: 26657
diff changeset
   199
      |> fold (del_name_extra name) (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   200
    end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   201
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   202
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   203
(* merge *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   204
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   205
fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   206
  let
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   207
    val tab' = (tab1, tab2) |> Symtab.join
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   208
      (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   209
        if stamp1 = stamp2 then raise Symtab.SAME
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   210
        else
26657
35249f5367b3 merge: canonical order;
wenzelm
parents: 26440
diff changeset
   211
          ((Library.merge (op =) (names1, names2),
35249f5367b3 merge: canonical order;
wenzelm
parents: 26440
diff changeset
   212
            Library.merge (op =) (names1', names2')), stamp ())));
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   213
    val xtab' = (xtab1, xtab2) |> Symtab.join
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   214
      (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   215
        if stamp1 = stamp2 then raise Symtab.SAME
26657
35249f5367b3 merge: canonical order;
wenzelm
parents: 26440
diff changeset
   216
        else (Library.merge (op =) (xnames1, xnames2), stamp ())));
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   217
  in NameSpace (tab', xtab') end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   218
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   219
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   220
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   221
(** naming contexts **)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   222
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   223
(* datatype naming *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   224
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   225
datatype naming = Naming of
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   226
  string *                                                 (*path*)
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   227
  ((string -> string -> string) *                          (*qualify*)
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   228
   (string list -> string list list * string list list));  (*accesses*)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   229
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   230
fun path_of (Naming (path, _)) = path;
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   231
fun accesses (Naming (_, (_, accs))) = accs;
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   232
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   233
fun external_names naming = map implode_name o #2 o accesses naming o explode_name;
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   234
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   235
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   236
(* manipulate namings *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   237
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   238
fun reject_qualified name =
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   239
  if is_qualified name then
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   240
    error ("Attempt to declare qualified name " ^ quote name)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   241
  else name;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   242
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   243
val default_naming =
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   244
  Naming ("", (fn path => qualified path o reject_qualified, suffixes_prefixes));
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   245
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   246
fun add_path elems (Naming (path, policy)) =
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   247
  if elems = "//" then Naming ("", (qualified, #2 policy))
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   248
  else if elems = "/" then Naming ("", policy)
20530
448594cbd82b renamed NameSpace.drop_base to NameSpace.qualifier;
wenzelm
parents: 19367
diff changeset
   249
  else if elems = ".." then Naming (qualifier path, policy)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   250
  else Naming (append path elems, policy);
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   251
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   252
fun no_base_names (Naming (path, (qualify, accs))) =
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   253
  Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   254
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   255
fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   256
19055
4f408867f9d4 removed qualified_force_prefix;
wenzelm
parents: 19030
diff changeset
   257
fun sticky_prefix prfx (Naming (path, (qualify, _))) =
4f408867f9d4 removed qualified_force_prefix;
wenzelm
parents: 19030
diff changeset
   258
  Naming (append path prfx,
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
   259
    (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
19015
1075db658d91 removed custom_accesses;
wenzelm
parents: 18939
diff changeset
   260
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   261
val apply_prefix =
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   262
  let
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   263
    fun mk_prefix (prfx, true) = sticky_prefix prfx
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   264
      | mk_prefix (prfx, false) = add_path prfx;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   265
  in fold mk_prefix end;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   266
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   267
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   268
(* declarations *)
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   269
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   270
fun full (Naming (path, (qualify, _))) = qualify path;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   271
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   272
fun declare naming name space =
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   273
  if is_hidden name then
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   274
    error ("Attempt to declare hidden name " ^ quote name)
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   275
  else
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   276
    let
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   277
      val names = explode_name name;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   278
      val _ = (null names orelse exists (fn s => s = "") names
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   279
          orelse exists_string (fn s => s = "\"") name) andalso
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   280
        error ("Bad name declaration " ^ quote name);
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   281
      val (accs, accs') = pairself (map implode_name) (accesses naming names);
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   282
    in space |> fold (add_name name) accs |> put_accesses name accs' end;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   283
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
   284
fun declare_binding bnaming b =
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   285
  let
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
   286
    val (prefix, bname) = Binding.dest_binding b;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   287
    val naming = apply_prefix prefix bnaming;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   288
    val name = full naming bname;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   289
  in declare naming name #> pair name end;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   290
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   291
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   292
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   293
(** name spaces coupled with symbol tables **)
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   294
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   295
type 'a table = T * 'a Symtab.table;
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   296
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   297
val empty_table = (empty, Symtab.empty);
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   298
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   299
fun gen_table_declare update naming (binding, x) (space, tab) =
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   300
  let
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   301
    val (name, space') = declare_binding naming binding space;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   302
  in (name, (space', update (name, x) tab)) end;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   303
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   304
fun table_declare naming = gen_table_declare Symtab.update_new naming;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   305
fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   306
28941
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
   307
fun full_binding naming b =
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
   308
  let val (prefix, bname) = Binding.dest_binding b
128459bd72d2 new Binding module
haftmann
parents: 28923
diff changeset
   309
  in full (apply_prefix prefix naming) bname end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   310
23086
12320f6e2523 tuned Pure/General/name_space.ML
haftmann
parents: 22057
diff changeset
   311
fun extend_table naming bentries (space, tab) =
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   312
  let val entries = map (apfst (full naming)) bentries
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   313
  in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   314
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   315
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
19367
wenzelm
parents: 19305
diff changeset
   316
  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   317
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   318
fun ext_table (space, tab) =
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   319
  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   320
  |> Library.sort_wrt (#2 o #1);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   321
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   322
fun dest_table tab = map (apfst #1) (ext_table tab);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   323
fun extern_table tab = map (apfst #2) (ext_table tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   324
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
   325
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
   326
(*final declarations of this structure!*)
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
   327
val implode = implode_name;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
   328
val explode = explode_name;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20530
diff changeset
   329
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   330
end;