src/Pure/symtab.ML
author lcp
Tue, 21 Jun 1994 17:20:34 +0200
changeset 435 ca5356bd315a
parent 374 caf9a9b7f605
child 475 bf2f285aa316
permissions -rw-r--r--
Addition of cardinals and order types, various tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/symtab.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1989  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
     6
Unbalanced binary trees indexed by strings; no way to delete an entry.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
     9
signature SYMTAB =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
sig
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    11
  exception DUPLICATE of string
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    12
  exception DUPS of string list
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    13
  type 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    14
  val null: 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    15
  val is_null: 'a table -> bool
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    16
  val lookup: 'a table * string -> 'a option
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    17
  val update: (string * 'a) * 'a table -> 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    18
  val update_new: (string * 'a) * 'a table -> 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    19
  val alist_of: 'a table -> (string * 'a) list
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    20
  val balance: 'a table -> 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    21
  val st_of_alist: (string * 'a) list * 'a table -> 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    22
  val st_of_declist: (string list * 'a) list * 'a table -> 'a table
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    23
  val make: (string * 'a) list -> 'a table
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    24
  val dest: 'a table -> (string * 'a) list
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    25
  val extend: ('a * 'a -> bool) -> 'a table * (string * 'a) list -> 'a table
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    26
  val extend_new: 'a table * (string * 'a) list -> 'a table
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    27
  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    28
  val lookup_multi: 'a list table * string -> 'a list
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    29
  val make_multi: (string * 'a) list -> 'a list table
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    30
  val dest_multi: 'a list table -> (string * 'a) list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    33
functor SymtabFun(): SYMTAB =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*symbol table errors, such as from update_new*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
exception DUPLICATE of string;
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    38
exception DUPS of string list;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    40
datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val null = Tip;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
fun is_null Tip = true
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  | is_null _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    49
fun lookup (symtab: 'a table, key: string) : 'a option =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  let fun look  Tip  = None
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    51
        | look (Branch (key', entry, left, right)) =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    52
            if      key < key' then look left
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    53
            else if key' < key then look right
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    54
            else  Some entry
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  in look symtab end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(*update, allows overwriting of an entry*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
fun update ((key: string, entry: 'a), symtab : 'a table)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  : 'a table =
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    60
  let fun upd  Tip  = Branch (key, entry, Tip, Tip)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    61
        | upd (Branch(key', entry', left, right)) =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    62
            if      key < key' then Branch (key', entry', upd left, right)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    63
            else if key' < key then Branch (key', entry', left, upd right)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    64
            else                    Branch (key, entry, left, right)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  in  upd symtab  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(*Like update but fails if key is already defined in table.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  Allows st_of_alist, etc. to detect multiple definitions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
fun update_new ((key: string, entry: 'a), symtab : 'a table)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  : 'a table =
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    71
  let fun upd Tip = Branch (key, entry, Tip, Tip)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    72
        | upd (Branch(key', entry', left, right)) =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    73
            if      key < key' then Branch (key', entry', upd left, right)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    74
            else if key' < key then Branch (key', entry', left, upd right)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    75
            else  raise DUPLICATE(key)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  in  upd symtab  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
(*conversion of symbol table to sorted association list*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
fun alist_of (symtab : 'a table) : (string * 'a) list =
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    80
  let fun ali (symtab, cont) = case symtab of
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    81
                Tip => cont
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    82
        | Branch (key, entry, left, right) =>
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    83
            ali(left, (key, entry) :: ali(right, cont))
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    84
  in  ali (symtab, [])  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    86
val dest = alist_of;
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
    87
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
(*Make a balanced tree of the first n members of the sorted alist (sal).
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  Utility for the function balance.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
fun bal_of (sal, 0) = Tip
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  | bal_of (sal, n) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
      let val mid = n div 2
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    94
      in  case  drop (mid, sal) of
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    95
            [] => bal_of (sal, mid)   (*should not occur*)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    96
          | ((key, entry):: pairs) =>
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
    97
                Branch(key, entry, bal_of(sal, mid), bal_of(pairs, n-mid-1))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
fun balance symtab =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
  let val sal = alist_of symtab
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
  in  bal_of (sal, length sal)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
(*Addition of association list to a symbol table*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
fun st_of_alist (al, symtab) =
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   108
  foldr update_new (al, symtab);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
(*A "declaration" associates the same entry with a list of keys;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
  does not allow overwriting of an entry*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
fun decl_update_new ((keys : string list, entry: 'a), symtab)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  : 'a table =
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   114
  let fun decl (key, symtab) = update_new ((key, entry), symtab)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   115
  in foldr decl (keys, symtab) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(*Addition of a list of declarations to a symbol table*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun st_of_declist (dl, symtab) =
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   119
  balance (foldr decl_update_new (dl, symtab));
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   120
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   121
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   122
(* make, extend, merge tables *)
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   123
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   124
fun eq_pair eq ((key1, entry1), (key2, entry2)) =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   125
  key1 = key2 andalso eq (entry1, entry2);
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   126
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   127
fun make alst =
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   128
  (case gen_duplicates eq_fst alst of
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   129
    [] => balance (st_of_alist (alst, Tip))
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   130
  | dups => raise DUPS (map fst dups));
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   131
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   132
fun extend eq (tab, alst) =
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   133
  generic_extend (eq_pair eq) dest make tab alst;
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   134
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   135
val extend_new = extend (K false);
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   136
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   137
fun merge eq (tab1, tab2) =
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   138
  generic_merge (eq_pair eq) dest make tab1 tab2;
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   139
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   140
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   141
(* tables with multiple entries per key *)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   142
(*order of entries with same key is preserved*)
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   143
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   144
fun lookup_multi (tab, key) =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   145
  (case lookup (tab, key) of
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   146
    Some entries => entries
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   147
  | None => []);
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   148
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   149
fun cons_entry ((key, entry), tab) =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   150
  update ((key, entry :: lookup_multi (tab, key)), tab);
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   151
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   152
fun make_multi alst =
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   153
  balance (foldr cons_entry (alst, Tip));
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   154
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   155
fun dest_multi tab =
374
caf9a9b7f605 added make, dest, extend_new;
wenzelm
parents: 234
diff changeset
   156
  flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
234
1b3bee8d5d7e minor cleanup;
wenzelm
parents: 0
diff changeset
   157
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160