author | wenzelm |
Mon, 06 Oct 1997 18:22:22 +0200 | |
changeset 3776 | 38f8ec304b95 |
parent 3560 | 7db9a44dfa06 |
child 6539 | 2e7d2fba9f6c |
permissions | -rw-r--r-- |
3549 | 1 |
(* Title: Pure/net.ML |
0 | 2 |
ID: $Id$ |
1460 | 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 |
||
8 |
From the book |
|
9 |
E. Charniak, C. K. Riesbeck, D. V. McDermott. |
|
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 |
|
228 | 13 |
match_term no longer treats abstractions as wildcards; instead they match |
14 |
only wildcards in patterns. Requires operands to be beta-eta-normal. |
|
0 | 15 |
*) |
16 |
||
17 |
signature NET = |
|
18 |
sig |
|
19 |
type key |
|
20 |
type 'a net |
|
21 |
exception DELETE and INSERT |
|
22 |
val delete: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net |
|
23 |
val delete_term: (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net |
|
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 |
||
35 |
||
1500 | 36 |
structure Net : NET = |
0 | 37 |
struct |
38 |
||
39 |
datatype key = CombK | VarK | AtomK of string; |
|
40 |
||
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
41 |
(*Bound variables*) |
0 | 42 |
fun string_of_bound i = "*B*" ^ chr i; |
43 |
||
228 | 44 |
(*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
|
45 |
Any term whose head is a Var is regarded entirely as a Var. |
228 | 46 |
Abstractions are also regarded as Vars; this covers eta-conversion |
47 |
and "near" eta-conversions such as %x.?P(?f(x)). |
|
0 | 48 |
*) |
49 |
fun add_key_of_terms (t, cs) = |
|
50 |
let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) |
|
1460 | 51 |
| rands (Const(c,_), cs) = AtomK c :: cs |
52 |
| rands (Free(c,_), cs) = AtomK c :: cs |
|
53 |
| rands (Bound i, cs) = AtomK (string_of_bound i) :: cs |
|
0 | 54 |
in case (head_of t) of |
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
55 |
Var _ => VarK :: cs |
228 | 56 |
| Abs _ => VarK :: cs |
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
57 |
| _ => rands(t,cs) |
0 | 58 |
end; |
59 |
||
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
60 |
(*convert a term to a list of keys*) |
0 | 61 |
fun key_of_term t = add_key_of_terms (t, []); |
62 |
||
63 |
||
64 |
(*Trees indexed by key lists: each arc is labelled by a key. |
|
65 |
Each node contains a list of items, and arcs to children. |
|
66 |
Keys in the association list (alist) are stored in ascending order. |
|
67 |
The empty key addresses the entire net. |
|
68 |
Lookup functions preserve order in items stored at same level. |
|
69 |
*) |
|
70 |
datatype 'a net = Leaf of 'a list |
|
1460 | 71 |
| Net of {comb: 'a net, |
72 |
var: 'a net, |
|
73 |
alist: (string * 'a net) list}; |
|
0 | 74 |
|
75 |
val empty = Leaf[]; |
|
76 |
val emptynet = Net{comb=empty, var=empty, alist=[]}; |
|
77 |
||
78 |
||
79 |
(*** Insertion into a discrimination net ***) |
|
80 |
||
1460 | 81 |
exception INSERT; (*duplicate item in the net*) |
0 | 82 |
|
83 |
||
84 |
(*Adds item x to the list at the node addressed by the keys. |
|
85 |
Creates node if not already present. |
|
86 |
eq is the equality test for items. |
|
87 |
The empty list of keys generates a Leaf node, others a Net node. |
|
88 |
*) |
|
89 |
fun insert ((keys,x), net, eq) = |
|
90 |
let fun ins1 ([], Leaf xs) = |
|
91 |
if gen_mem eq (x,xs) then raise INSERT else Leaf(x::xs) |
|
92 |
| ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*) |
|
93 |
| ins1 (CombK :: keys, Net{comb,var,alist}) = |
|
1460 | 94 |
Net{comb=ins1(keys,comb), var=var, alist=alist} |
95 |
| ins1 (VarK :: keys, Net{comb,var,alist}) = |
|
96 |
Net{comb=comb, var=ins1(keys,var), alist=alist} |
|
97 |
| ins1 (AtomK a :: keys, Net{comb,var,alist}) = |
|
98 |
let fun newpair net = (a, ins1(keys,net)) |
|
99 |
fun inslist [] = [newpair empty] |
|
100 |
| inslist((b: string, netb) :: alist) = |
|
101 |
if a=b then newpair netb :: alist |
|
102 |
else if a<b then (*absent, ins1ert in alist*) |
|
103 |
newpair empty :: (b,netb) :: alist |
|
104 |
else (*a>b*) (b,netb) :: inslist alist |
|
105 |
in Net{comb=comb, var=var, alist= inslist alist} end |
|
0 | 106 |
in ins1 (keys,net) end; |
107 |
||
108 |
fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq); |
|
109 |
||
110 |
(*** Deletion from a discrimination net ***) |
|
111 |
||
1460 | 112 |
exception DELETE; (*missing item in the net*) |
0 | 113 |
|
114 |
(*Create a new Net node if it would be nonempty*) |
|
115 |
fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty |
|
116 |
| newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist}; |
|
117 |
||
118 |
(*add new (b,net) pair to the alist provided net is nonempty*) |
|
119 |
fun conspair((b, Leaf[]), alist) = alist |
|
120 |
| conspair((b, net), alist) = (b, net) :: alist; |
|
121 |
||
122 |
(*Deletes item x from the list at the node addressed by the keys. |
|
123 |
Raises DELETE if absent. Collapses the net if possible. |
|
124 |
eq is the equality test for items. *) |
|
125 |
fun delete ((keys, x), net, eq) = |
|
126 |
let fun del1 ([], Leaf xs) = |
|
127 |
if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x)) |
|
128 |
else raise DELETE |
|
1460 | 129 |
| del1 (keys, Leaf[]) = raise DELETE |
130 |
| del1 (CombK :: keys, Net{comb,var,alist}) = |
|
131 |
newnet{comb=del1(keys,comb), var=var, alist=alist} |
|
132 |
| del1 (VarK :: keys, Net{comb,var,alist}) = |
|
133 |
newnet{comb=comb, var=del1(keys,var), alist=alist} |
|
134 |
| del1 (AtomK a :: keys, Net{comb,var,alist}) = |
|
135 |
let fun newpair net = (a, del1(keys,net)) |
|
136 |
fun dellist [] = raise DELETE |
|
137 |
| dellist((b: string, netb) :: alist) = |
|
138 |
if a=b then conspair(newpair netb, alist) |
|
139 |
else if a<b then (*absent*) raise DELETE |
|
140 |
else (*a>b*) (b,netb) :: dellist alist |
|
141 |
in newnet{comb=comb, var=var, alist= dellist alist} end |
|
0 | 142 |
in del1 (keys,net) end; |
143 |
||
144 |
fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq); |
|
145 |
||
146 |
(*** Retrieval functions for discrimination nets ***) |
|
147 |
||
148 |
exception OASSOC; |
|
149 |
||
150 |
(*Ordered association list lookup*) |
|
151 |
fun oassoc ([], a: string) = raise OASSOC |
|
152 |
| oassoc ((b,x)::pairs, a) = |
|
153 |
if b<a then oassoc(pairs,a) |
|
154 |
else if a=b then x |
|
155 |
else raise OASSOC; |
|
156 |
||
157 |
(*Return the list of items at the given node, [] if no such node*) |
|
158 |
fun lookup (Leaf(xs), []) = xs |
|
1460 | 159 |
| lookup (Leaf _, _::_) = [] (*non-empty keys and empty net*) |
0 | 160 |
| lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys) |
161 |
| lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys) |
|
162 |
| lookup (Net{comb,var,alist}, AtomK a :: keys) = |
|
163 |
lookup(oassoc(alist,a),keys) handle OASSOC => []; |
|
164 |
||
165 |
||
166 |
(*Skipping a term in a net. Recursively skip 2 levels if a combination*) |
|
167 |
fun net_skip (Leaf _, nets) = nets |
|
168 |
| net_skip (Net{comb,var,alist}, nets) = |
|
169 |
foldr net_skip |
|
170 |
(net_skip (comb,[]), |
|
1460 | 171 |
foldr (fn ((_,net), nets) => net::nets) (alist, var::nets)); |
0 | 172 |
|
173 |
(** Matching and Unification**) |
|
174 |
||
175 |
(*conses the linked net, if present, to nets*) |
|
176 |
fun look1 (alist, a) nets = |
|
177 |
oassoc(alist,a) :: nets handle OASSOC => nets; |
|
178 |
||
179 |
(*Return the nodes accessible from the term (cons them before nets) |
|
180 |
"unif" signifies retrieval for unification rather than matching. |
|
181 |
Var in net matches any term. |
|
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
182 |
Abs or Var in object: if "unif", regarded as wildcard, |
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
183 |
else matches only a variable in net. |
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
184 |
*) |
0 | 185 |
fun matching unif t (net,nets) = |
186 |
let fun rands _ (Leaf _, nets) = nets |
|
1460 | 187 |
| rands t (Net{comb,alist,...}, nets) = |
188 |
case t of |
|
189 |
f$t => foldr (matching unif t) (rands f (comb,[]), nets) |
|
190 |
| Const(c,_) => look1 (alist, c) nets |
|
191 |
| Free(c,_) => look1 (alist, c) nets |
|
192 |
| Bound i => look1 (alist, string_of_bound i) nets |
|
193 |
| _ => nets |
|
0 | 194 |
in |
195 |
case net of |
|
1460 | 196 |
Leaf _ => nets |
0 | 197 |
| Net{var,...} => |
2836 | 198 |
let val etat = Pattern.eta_contract_atom t |
199 |
in case (head_of etat) of |
|
200 |
Var _ => if unif then net_skip (net,nets) |
|
201 |
else var::nets (*only matches Var in net*) |
|
202 |
(*If "unif" then a var instantiation in the abstraction could allow |
|
203 |
an eta-reduction, so regard the abstraction as a wildcard.*) |
|
204 |
| Abs _ => if unif then net_skip (net,nets) |
|
205 |
else var::nets (*only a Var can match*) |
|
206 |
| _ => rands etat (net, var::nets) (*var could match also*) |
|
207 |
end |
|
0 | 208 |
end; |
209 |
||
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2226
diff
changeset
|
210 |
fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l); |
0 | 211 |
|
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset
|
212 |
(*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*) |
0 | 213 |
fun match_term net t = |
214 |
extract_leaves (matching false t (net,[])); |
|
215 |
||
216 |
(*return items whose key could unify with t*) |
|
217 |
fun unify_term net t = |
|
218 |
extract_leaves (matching true t (net,[])); |
|
219 |
||
3548 | 220 |
|
221 |
(** dest **) |
|
222 |
||
223 |
fun cons_fst x (xs, y) = (x :: xs, y); |
|
224 |
||
225 |
fun dest (Leaf xs) = map (pair []) xs |
|
226 |
| dest (Net {comb, var, alist}) = |
|
3560 | 227 |
map (cons_fst CombK) (dest comb) @ |
228 |
map (cons_fst VarK) (dest var) @ |
|
229 |
flat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) alist); |
|
3548 | 230 |
|
231 |
||
232 |
(** merge **) |
|
233 |
||
234 |
fun add eq (net, keys_x) = |
|
235 |
insert (keys_x, net, eq) handle INSERT => net; |
|
236 |
||
237 |
fun merge (net1, net2, eq) = |
|
238 |
foldl (add eq) (net1, dest net2); |
|
239 |
||
240 |
||
0 | 241 |
end; |