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