author | wenzelm |
Wed, 06 Jul 2005 20:00:42 +0200 | |
changeset 16730 | ff304c52bf86 |
parent 16708 | 479f7ac538b5 |
child 16808 | 644fc45c7292 |
permissions | -rw-r--r-- |
12319 | 1 |
(* Title: Pure/net.ML |
0 | 2 |
ID: $Id$ |
12319 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Discrimination nets: a data structure for indexing items |
|
7 |
||
12319 | 8 |
From the book |
9 |
E. Charniak, C. K. Riesbeck, D. V. McDermott. |
|
0 | 10 |
Artificial Intelligence Programming. |
11 |
(Lawrence Erlbaum Associates, 1980). [Chapter 14] |
|
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
12 |
|
12319 | 13 |
match_term no longer treats abstractions as wildcards; instead they match |
228 | 14 |
only wildcards in patterns. Requires operands to be beta-eta-normal. |
0 | 15 |
*) |
16 |
||
12319 | 17 |
signature NET = |
0 | 18 |
sig |
19 |
type key |
|
20 |
type 'a net |
|
21 |
exception DELETE and INSERT |
|
12319 | 22 |
val delete: (key list * 'a) * 'b net * ('a * 'b -> bool) -> 'b net |
23 |
val delete_term: (term * 'a) * 'b net * ('a * 'b -> bool) -> 'b net |
|
0 | 24 |
val empty: 'a net |
25 |
val insert: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net |
|
26 |
val insert_term: (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net |
|
27 |
val lookup: 'a net * key list -> 'a list |
|
28 |
val match_term: 'a net -> term -> 'a list |
|
29 |
val key_of_term: term -> key list |
|
30 |
val unify_term: 'a net -> term -> 'a list |
|
3548 | 31 |
val dest: 'a net -> (key list * 'a) list |
32 |
val merge: 'a net * 'a net * ('a*'a -> bool) -> 'a net |
|
0 | 33 |
end; |
34 |
||
12319 | 35 |
structure Net : NET = |
0 | 36 |
struct |
37 |
||
38 |
datatype key = CombK | VarK | AtomK of string; |
|
39 |
||
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
40 |
(*Bound variables*) |
7943
e31a3c0c2c1e
now more than 256 generated bound variables possible
oheimb
parents:
6539
diff
changeset
|
41 |
fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256); |
0 | 42 |
|
228 | 43 |
(*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. |
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
44 |
Any term whose head is a Var is regarded entirely as a Var. |
228 | 45 |
Abstractions are also regarded as Vars; this covers eta-conversion |
46 |
and "near" eta-conversions such as %x.?P(?f(x)). |
|
0 | 47 |
*) |
12319 | 48 |
fun add_key_of_terms (t, cs) = |
0 | 49 |
let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) |
12319 | 50 |
| rands (Const(c,_), cs) = AtomK c :: cs |
51 |
| rands (Free(c,_), cs) = AtomK c :: cs |
|
52 |
| rands (Bound i, cs) = AtomK (string_of_bound i) :: cs |
|
0 | 53 |
in case (head_of t) of |
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
54 |
Var _ => VarK :: cs |
228 | 55 |
| Abs _ => VarK :: cs |
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
56 |
| _ => rands(t,cs) |
0 | 57 |
end; |
58 |
||
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
59 |
(*convert a term to a list of keys*) |
0 | 60 |
fun key_of_term t = add_key_of_terms (t, []); |
61 |
||
62 |
||
63 |
(*Trees indexed by key lists: each arc is labelled by a key. |
|
64 |
Each node contains a list of items, and arcs to children. |
|
65 |
The empty key addresses the entire net. |
|
66 |
Lookup functions preserve order in items stored at same level. |
|
67 |
*) |
|
68 |
datatype 'a net = Leaf of 'a list |
|
12319 | 69 |
| Net of {comb: 'a net, |
70 |
var: 'a net, |
|
16708 | 71 |
atoms: 'a net Symtab.table}; |
0 | 72 |
|
73 |
val empty = Leaf[]; |
|
16708 | 74 |
fun is_empty (Leaf []) = true | is_empty _ = false; |
75 |
val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty}; |
|
0 | 76 |
|
77 |
||
78 |
(*** Insertion into a discrimination net ***) |
|
79 |
||
12319 | 80 |
exception INSERT; (*duplicate item in the net*) |
0 | 81 |
|
82 |
||
83 |
(*Adds item x to the list at the node addressed by the keys. |
|
84 |
Creates node if not already present. |
|
12319 | 85 |
eq is the equality test for items. |
0 | 86 |
The empty list of keys generates a Leaf node, others a Net node. |
87 |
*) |
|
88 |
fun insert ((keys,x), net, eq) = |
|
12319 | 89 |
let fun ins1 ([], Leaf xs) = |
16686 | 90 |
if member eq xs x then raise INSERT else Leaf(x::xs) |
0 | 91 |
| ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*) |
16708 | 92 |
| ins1 (CombK :: keys, Net{comb,var,atoms}) = |
93 |
Net{comb=ins1(keys,comb), var=var, atoms=atoms} |
|
94 |
| ins1 (VarK :: keys, Net{comb,var,atoms}) = |
|
95 |
Net{comb=comb, var=ins1(keys,var), atoms=atoms} |
|
96 |
| ins1 (AtomK a :: keys, Net{comb,var,atoms}) = |
|
97 |
let |
|
98 |
val net' = if_none (Symtab.lookup (atoms, a)) empty; |
|
99 |
val atoms' = Symtab.update ((a, ins1(keys,net')), atoms); |
|
100 |
in Net{comb=comb, var=var, atoms=atoms'} end |
|
0 | 101 |
in ins1 (keys,net) end; |
102 |
||
103 |
fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq); |
|
104 |
||
105 |
(*** Deletion from a discrimination net ***) |
|
106 |
||
12319 | 107 |
exception DELETE; (*missing item in the net*) |
0 | 108 |
|
109 |
(*Create a new Net node if it would be nonempty*) |
|
16708 | 110 |
fun newnet (args as {comb,var,atoms}) = |
111 |
if is_empty comb andalso is_empty var andalso Symtab.is_empty atoms |
|
112 |
then empty else Net args; |
|
0 | 113 |
|
114 |
(*Deletes item x from the list at the node addressed by the keys. |
|
115 |
Raises DELETE if absent. Collapses the net if possible. |
|
116 |
eq is the equality test for items. *) |
|
12319 | 117 |
fun delete ((keys, x), net, eq) = |
0 | 118 |
let fun del1 ([], Leaf xs) = |
16686 | 119 |
if member eq xs x then Leaf (remove eq x xs) |
0 | 120 |
else raise DELETE |
12319 | 121 |
| del1 (keys, Leaf[]) = raise DELETE |
16708 | 122 |
| del1 (CombK :: keys, Net{comb,var,atoms}) = |
123 |
newnet{comb=del1(keys,comb), var=var, atoms=atoms} |
|
124 |
| del1 (VarK :: keys, Net{comb,var,atoms}) = |
|
125 |
newnet{comb=comb, var=del1(keys,var), atoms=atoms} |
|
126 |
| del1 (AtomK a :: keys, Net{comb,var,atoms}) = |
|
127 |
let val atoms' = |
|
128 |
(case Symtab.lookup (atoms, a) of |
|
129 |
NONE => raise DELETE |
|
130 |
| SOME net' => |
|
131 |
(case del1 (keys, net') of |
|
132 |
Leaf [] => Symtab.delete a atoms |
|
133 |
| net'' => Symtab.update ((a, net''), atoms))) |
|
134 |
in newnet{comb=comb, var=var, atoms=atoms'} end |
|
0 | 135 |
in del1 (keys,net) end; |
136 |
||
137 |
fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq); |
|
138 |
||
16677 | 139 |
|
0 | 140 |
(*** Retrieval functions for discrimination nets ***) |
141 |
||
16708 | 142 |
exception ABSENT; |
0 | 143 |
|
16708 | 144 |
fun the_atom atoms a = |
145 |
(case Symtab.lookup (atoms, a) of |
|
146 |
NONE => raise ABSENT |
|
147 |
| SOME net => net); |
|
0 | 148 |
|
149 |
(*Return the list of items at the given node, [] if no such node*) |
|
150 |
fun lookup (Leaf(xs), []) = xs |
|
12319 | 151 |
| lookup (Leaf _, _::_) = [] (*non-empty keys and empty net*) |
16708 | 152 |
| lookup (Net{comb,var,atoms}, CombK :: keys) = lookup(comb,keys) |
153 |
| lookup (Net{comb,var,atoms}, VarK :: keys) = lookup(var,keys) |
|
154 |
| lookup (Net{comb,var,atoms}, AtomK a :: keys) = |
|
155 |
lookup (the_atom atoms a, keys) handle ABSENT => []; |
|
0 | 156 |
|
157 |
||
158 |
(*Skipping a term in a net. Recursively skip 2 levels if a combination*) |
|
159 |
fun net_skip (Leaf _, nets) = nets |
|
16708 | 160 |
| net_skip (Net{comb,var,atoms}, nets) = |
161 |
foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[])); |
|
0 | 162 |
|
163 |
(** Matching and Unification**) |
|
164 |
||
165 |
(*conses the linked net, if present, to nets*) |
|
16708 | 166 |
fun look1 (atoms, a) nets = |
167 |
the_atom atoms a :: nets handle ABSENT => nets; |
|
0 | 168 |
|
12319 | 169 |
(*Return the nodes accessible from the term (cons them before nets) |
0 | 170 |
"unif" signifies retrieval for unification rather than matching. |
171 |
Var in net matches any term. |
|
12319 | 172 |
Abs or Var in object: if "unif", regarded as wildcard, |
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
173 |
else matches only a variable in net. |
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
174 |
*) |
0 | 175 |
fun matching unif t (net,nets) = |
176 |
let fun rands _ (Leaf _, nets) = nets |
|
16708 | 177 |
| rands t (Net{comb,atoms,...}, nets) = |
12319 | 178 |
case t of |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
179 |
f$t => foldr (matching unif t) nets (rands f (comb,[])) |
16708 | 180 |
| Const(c,_) => look1 (atoms, c) nets |
181 |
| Free(c,_) => look1 (atoms, c) nets |
|
182 |
| Bound i => look1 (atoms, string_of_bound i) nets |
|
12319 | 183 |
| _ => nets |
184 |
in |
|
0 | 185 |
case net of |
12319 | 186 |
Leaf _ => nets |
0 | 187 |
| Net{var,...} => |
12319 | 188 |
case head_of t of |
189 |
Var _ => if unif then net_skip (net,nets) |
|
190 |
else var::nets (*only matches Var in net*) |
|
2836 | 191 |
(*If "unif" then a var instantiation in the abstraction could allow |
192 |
an eta-reduction, so regard the abstraction as a wildcard.*) |
|
12319 | 193 |
| Abs _ => if unif then net_skip (net,nets) |
194 |
else var::nets (*only a Var can match*) |
|
195 |
| _ => rands t (net, var::nets) (*var could match also*) |
|
0 | 196 |
end; |
197 |
||
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2226
diff
changeset
|
198 |
fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l); |
0 | 199 |
|
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
200 |
(*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*) |
12319 | 201 |
fun match_term net t = |
0 | 202 |
extract_leaves (matching false t (net,[])); |
203 |
||
204 |
(*return items whose key could unify with t*) |
|
12319 | 205 |
fun unify_term net t = |
0 | 206 |
extract_leaves (matching true t (net,[])); |
207 |
||
3548 | 208 |
|
209 |
(** dest **) |
|
210 |
||
211 |
fun cons_fst x (xs, y) = (x :: xs, y); |
|
212 |
||
213 |
fun dest (Leaf xs) = map (pair []) xs |
|
16708 | 214 |
| dest (Net {comb, var, atoms}) = |
3560 | 215 |
map (cons_fst CombK) (dest comb) @ |
216 |
map (cons_fst VarK) (dest var) @ |
|
16708 | 217 |
List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) |
218 |
(Symtab.dest atoms)); |
|
3548 | 219 |
|
220 |
||
221 |
(** merge **) |
|
222 |
||
16686 | 223 |
fun add eq keys_x net = insert (keys_x, net, eq) handle INSERT => net; |
224 |
fun merge (net1, net2, eq) = fold (add eq) (dest net2) net1; |
|
3548 | 225 |
|
226 |
||
0 | 227 |
end; |