src/Pure/General/name_space.ML
author berghofe
Mon, 22 Sep 2003 16:19:46 +0200
changeset 14198 8ea2645b8132
parent 13332 f130bcf29620
child 14382 9fb68cd74719
permissions -rw-r--r--
Modified merge_aux to prevent newer names from getting overwritten by older names.
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
    ID:         $Id$
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
8806
wenzelm
parents: 8728
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     5
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     6
Hierarchically structured name spaces.
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     7
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     8
More general than ML-like nested structures, but also slightly more
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     9
ad-hoc.  Does not support absolute addressing.  Unknown names are
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    10
implicitely considered to be declared outermost.
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    11
*)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    12
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    13
signature NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    14
sig
12588
0361fd72f1a7 hide: flag for full/base name;
wenzelm
parents: 12251
diff changeset
    15
  val separator: string                 (*single char*)
9120
04a46ceace35 export hidden: string -> string;
wenzelm
parents: 8806
diff changeset
    16
  val hidden: string -> string
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    17
  val append: string -> string -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    18
  val unpack: string -> string list
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    19
  val pack: string list -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    20
  val base: string -> string
11829
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    21
  val map_base: (string -> string) -> string -> string
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    22
  val is_qualified: string -> bool
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    23
  val accesses: string -> string list
13332
f130bcf29620 added accesses';
wenzelm
parents: 12588
diff changeset
    24
  val accesses': string -> string list
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
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    27
  val extend: T * string list -> T
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    28
  val merge: T * T -> T
12588
0361fd72f1a7 hide: flag for full/base name;
wenzelm
parents: 12251
diff changeset
    29
  val hide: bool -> T * string list -> T
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    30
  val intern: T -> string -> string
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    31
  val extern: T -> string -> string
5175
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
    32
  val long_names: bool ref
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
    33
  val cond_extern: T -> string -> string
6845
598d2f32d452 added cond_extern_table;
wenzelm
parents: 6118
diff changeset
    34
  val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    35
  val dest: T -> (string * string list) list
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    36
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    37
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    38
structure NameSpace: NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    39
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    40
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    41
(** long identifiers **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    42
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    43
val separator = ".";
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    44
fun hidden name = "??." ^ name;
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    45
fun is_hidden name = (case explode name of "?" :: "?" :: "." :: _ => true | _ => false);
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    46
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    47
fun append name1 name2 = name1 ^ separator ^ name2;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    48
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    49
val unpack = space_explode separator;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    50
val pack = space_implode separator;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    51
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    52
val base = last_elem o unpack;
11829
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    53
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    54
fun map_base f name =
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    55
  let val uname = unpack name
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    56
  in pack (map_nth_elem (length uname - 1) f uname) end;
f252646080fc added map_base;
wenzelm
parents: 9120
diff changeset
    57
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    58
fun is_qualified name = length (unpack name) > 1;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    59
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    60
fun accesses name =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    61
  let
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    62
    val uname = unpack name;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    63
    val (q, b) = split_last uname;
12251
53b7962bcdb1 moved prefixes1, suffixes1 to library.ML;
wenzelm
parents: 11829
diff changeset
    64
    val sfxs = Library.suffixes1 uname;
53b7962bcdb1 moved prefixes1, suffixes1 to library.ML;
wenzelm
parents: 11829
diff changeset
    65
    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    66
  in map pack (sfxs @ pfxs) end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    67
13332
f130bcf29620 added accesses';
wenzelm
parents: 12588
diff changeset
    68
val accesses' = map pack o Library.suffixes1 o unpack;
f130bcf29620 added accesses';
wenzelm
parents: 12588
diff changeset
    69
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    70
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    71
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    72
(** name spaces **)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    73
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    74
(* basic operations *)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    75
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    76
fun map_space f xname tab =
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    77
  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    78
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    79
fun change f xname (name, tab) =
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    80
  map_space (fn (names, names') => (f names name, names')) xname tab;
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    81
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    82
fun change' f xname (name', tab) =
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    83
  map_space (fn (names, names') => (names, f names' name')) xname tab;
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    84
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    85
fun del names nm = if nm mem_string names then Library.gen_rem (op =) (names, nm) else names;
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    86
fun add names nm = nm :: del names nm;
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    87
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    88
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    89
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    90
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    91
datatype T =
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    92
  NameSpace of (string list * string list) Symtab.table;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    93
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    94
val empty = NameSpace Symtab.empty;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    95
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    96
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    97
(* extend *)            (*later entries preferred*)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    98
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
    99
fun extend_aux (name, tab) =
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   100
  if is_hidden name then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   101
    error ("Attempt to declare hidden name " ^ quote name)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   102
  else foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   103
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   104
fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux (names, tab));
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   105
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   106
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   107
(* merge *)             (*1st preferred over 2nd*)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   108
14198
8ea2645b8132 Modified merge_aux to prevent newer names from getting overwritten
berghofe
parents: 13332
diff changeset
   109
fun merge_aux (tab, (xname, (names1, names1'))) =
8ea2645b8132 Modified merge_aux to prevent newer names from getting overwritten
berghofe
parents: 13332
diff changeset
   110
  map_space (fn (names2, names2') =>
8ea2645b8132 Modified merge_aux to prevent newer names from getting overwritten
berghofe
parents: 13332
diff changeset
   111
    (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   112
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   113
fun merge (NameSpace tab1, NameSpace tab2) =
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   114
  NameSpace (Symtab.foldl merge_aux (tab2, tab1));
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   115
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   116
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   117
(* hide *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   118
12588
0361fd72f1a7 hide: flag for full/base name;
wenzelm
parents: 12251
diff changeset
   119
fun hide_aux fully (name, tab) =
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   120
  if not (is_qualified name) then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   121
    error ("Attempt to hide global name " ^ quote name)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   122
  else if is_hidden name then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   123
    error ("Attempt to hide hidden name " ^ quote name)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   124
  else (change' add name (name,
12588
0361fd72f1a7 hide: flag for full/base name;
wenzelm
parents: 12251
diff changeset
   125
    foldl (fn (tb, xname) => change del xname (name, tb))
0361fd72f1a7 hide: flag for full/base name;
wenzelm
parents: 12251
diff changeset
   126
      (tab, if fully then accesses name else [base name])));
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   127
12588
0361fd72f1a7 hide: flag for full/base name;
wenzelm
parents: 12251
diff changeset
   128
fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) (names, tab));
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   129
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   130
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   131
(* intern / extern names *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   132
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   133
fun lookup (NameSpace tab) xname =
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   134
  (case Symtab.lookup (tab, xname) of
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   135
    None => (xname, true)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   136
  | Some ([name], _) => (name, true)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   137
  | Some (name :: _, _) => (name, false)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   138
  | Some ([], []) => (xname, true)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   139
  | Some ([], name' :: _) => (hidden name', true));
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   140
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   141
fun intern spc xname = #1 (lookup spc xname);
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   142
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   143
fun extern space name =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   144
  let
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   145
    fun try [] = hidden name
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   146
      | try (nm :: nms) =
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   147
          let val (full_nm, uniq) = lookup space nm
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   148
          in if full_nm = name andalso uniq then nm else try nms end
13332
f130bcf29620 added accesses';
wenzelm
parents: 12588
diff changeset
   149
  in try (accesses' name) end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   150
5175
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   151
(*prune names on output by default*)
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   152
val long_names = ref false;
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   153
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   154
fun cond_extern space = if ! long_names then I else extern space;
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   155
6845
598d2f32d452 added cond_extern_table;
wenzelm
parents: 6118
diff changeset
   156
fun cond_extern_table space tab =
598d2f32d452 added cond_extern_table;
wenzelm
parents: 6118
diff changeset
   157
  Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));
598d2f32d452 added cond_extern_table;
wenzelm
parents: 6118
diff changeset
   158
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   159
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   160
(* dest *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   161
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   162
fun dest_entry (xname, ([], _)) = None
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   163
  | dest_entry (xname, (name :: _, _)) = Some (name, xname);
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   164
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   165
fun dest (NameSpace tab) =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   166
  map (apsnd (sort (int_ord o pairself size)))
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   167
    (Symtab.dest (Symtab.make_multi (mapfilter dest_entry (Symtab.dest tab))));
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   168
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   169
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   170
end;
5175
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   171
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   172
2dbef0104bcf moved long_names / cond_extern to name_space.ML;
wenzelm
parents: 5012
diff changeset
   173
val long_names = NameSpace.long_names;