author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 17412  e26cb20ef0cc 
child 18939  18e2a2676d80 
permissions  rwrr 
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 betaetanormal. 
0  15 
*) 
16 

12319  17 
signature NET = 
16808  18 
sig 
0  19 
type key 
16808  20 
val key_of_term: term > key list 
0  21 
type 'a net 
22 
val empty: 'a net 

16808  23 
exception INSERT 
24 
val insert: ('a * 'a > bool) > key list * 'a > 'a net > 'a net 

25 
val insert_term: ('a * 'a > bool) > term * 'a > 'a net > 'a net 

26 
exception DELETE 

27 
val delete: ('b * 'a > bool) > key list * 'b > 'a net > 'a net 

28 
val delete_term: ('b * 'a > bool) > term * 'b > 'a net > 'a net 

29 
val lookup: 'a net > key list > 'a list 

0  30 
val match_term: 'a net > term > 'a list 
31 
val unify_term: 'a net > term > 'a list 

16808  32 
val entries: 'a net > 'a list 
33 
val subtract: ('b * 'a > bool) > 'a net > 'b net > 'b list 

34 
val merge: ('a * 'a > bool) > 'a net * 'a net > 'a net 

35 
end; 

0  36 

16808  37 
structure Net: NET = 
0  38 
struct 
39 

40 
datatype key = CombK  VarK  AtomK of string; 

41 

228  42 
(*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

43 
Any term whose head is a Var is regarded entirely as a Var. 
228  44 
Abstractions are also regarded as Vars; this covers etaconversion 
45 
and "near" etaconversions such as %x.?P(?f(x)). 

0  46 
*) 
12319  47 
fun add_key_of_terms (t, cs) = 
0  48 
let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) 
12319  49 
 rands (Const(c,_), cs) = AtomK c :: cs 
50 
 rands (Free(c,_), cs) = AtomK c :: cs 

16986  51 
 rands (Bound i, cs) = AtomK (Term.bound i) :: cs 
0  52 
in case (head_of t) of 
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

53 
Var _ => VarK :: cs 
228  54 
 Abs _ => VarK :: cs 
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

55 
 _ => rands(t,cs) 
0  56 
end; 
57 

225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

58 
(*convert a term to a list of keys*) 
0  59 
fun key_of_term t = add_key_of_terms (t, []); 
60 

61 

62 
(*Trees indexed by key lists: each arc is labelled by a key. 

63 
Each node contains a list of items, and arcs to children. 

64 
The empty key addresses the entire net. 

65 
Lookup functions preserve order in items stored at same level. 

66 
*) 

67 
datatype 'a net = Leaf of 'a list 

12319  68 
 Net of {comb: 'a net, 
69 
var: 'a net, 

16708  70 
atoms: 'a net Symtab.table}; 
0  71 

72 
val empty = Leaf[]; 

16708  73 
fun is_empty (Leaf []) = true  is_empty _ = false; 
74 
val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty}; 

0  75 

76 

77 
(*** Insertion into a discrimination net ***) 

78 

12319  79 
exception INSERT; (*duplicate item in the net*) 
0  80 

81 

82 
(*Adds item x to the list at the node addressed by the keys. 

83 
Creates node if not already present. 

12319  84 
eq is the equality test for items. 
0  85 
The empty list of keys generates a Leaf node, others a Net node. 
86 
*) 

16808  87 
fun insert eq (keys,x) net = 
12319  88 
let fun ins1 ([], Leaf xs) = 
16686  89 
if member eq xs x then raise INSERT else Leaf(x::xs) 
0  90 
 ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*) 
16708  91 
 ins1 (CombK :: keys, Net{comb,var,atoms}) = 
92 
Net{comb=ins1(keys,comb), var=var, atoms=atoms} 

93 
 ins1 (VarK :: keys, Net{comb,var,atoms}) = 

94 
Net{comb=comb, var=ins1(keys,var), atoms=atoms} 

95 
 ins1 (AtomK a :: keys, Net{comb,var,atoms}) = 

96 
let 

17412  97 
val net' = if_none (Symtab.lookup atoms a) empty; 
98 
val atoms' = Symtab.update (a, ins1 (keys, net')) atoms; 

16708  99 
in Net{comb=comb, var=var, atoms=atoms'} end 
0  100 
in ins1 (keys,net) end; 
101 

16808  102 
fun insert_safe eq entry net = insert eq entry net handle INSERT => net; 
103 
fun insert_term eq (t, x) = insert eq (key_of_term t, x); 

104 

0  105 

106 
(*** Deletion from a discrimination net ***) 

107 

12319  108 
exception DELETE; (*missing item in the net*) 
0  109 

110 
(*Create a new Net node if it would be nonempty*) 

16708  111 
fun newnet (args as {comb,var,atoms}) = 
112 
if is_empty comb andalso is_empty var andalso Symtab.is_empty atoms 

113 
then empty else Net args; 

0  114 

115 
(*Deletes item x from the list at the node addressed by the keys. 

116 
Raises DELETE if absent. Collapses the net if possible. 

117 
eq is the equality test for items. *) 

16808  118 
fun delete eq (keys, x) net = 
0  119 
let fun del1 ([], Leaf xs) = 
16686  120 
if member eq xs x then Leaf (remove eq x xs) 
0  121 
else raise DELETE 
12319  122 
 del1 (keys, Leaf[]) = raise DELETE 
16708  123 
 del1 (CombK :: keys, Net{comb,var,atoms}) = 
124 
newnet{comb=del1(keys,comb), var=var, atoms=atoms} 

125 
 del1 (VarK :: keys, Net{comb,var,atoms}) = 

126 
newnet{comb=comb, var=del1(keys,var), atoms=atoms} 

127 
 del1 (AtomK a :: keys, Net{comb,var,atoms}) = 

128 
let val atoms' = 

17412  129 
(case Symtab.lookup atoms a of 
16708  130 
NONE => raise DELETE 
131 
 SOME net' => 

132 
(case del1 (keys, net') of 

133 
Leaf [] => Symtab.delete a atoms 

17412  134 
 net'' => Symtab.update (a, net'') atoms)) 
16708  135 
in newnet{comb=comb, var=var, atoms=atoms'} end 
0  136 
in del1 (keys,net) end; 
137 

16808  138 
fun delete_term eq (t, x) = delete eq (key_of_term t, x); 
0  139 

16677  140 

0  141 
(*** Retrieval functions for discrimination nets ***) 
142 

16708  143 
exception ABSENT; 
0  144 

16708  145 
fun the_atom atoms a = 
17412  146 
(case Symtab.lookup atoms a of 
16708  147 
NONE => raise ABSENT 
148 
 SOME net => net); 

0  149 

150 
(*Return the list of items at the given node, [] if no such node*) 

16808  151 
fun lookup (Leaf xs) [] = xs 
152 
 lookup (Leaf _) (_ :: _) = [] (*nonempty keys and empty net*) 

153 
 lookup (Net {comb, var, atoms}) (CombK :: keys) = lookup comb keys 

154 
 lookup (Net {comb, var, atoms}) (VarK :: keys) = lookup var keys 

155 
 lookup (Net {comb, var, atoms}) (AtomK a :: keys) = 

156 
lookup (the_atom atoms a) keys handle ABSENT => []; 

0  157 

158 

159 
(*Skipping a term in a net. Recursively skip 2 levels if a combination*) 

160 
fun net_skip (Leaf _, nets) = nets 

16708  161 
 net_skip (Net{comb,var,atoms}, nets) = 
162 
foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[])); 

0  163 

16808  164 

165 
(** Matching and Unification **) 

0  166 

167 
(*conses the linked net, if present, to nets*) 

16708  168 
fun look1 (atoms, a) nets = 
169 
the_atom atoms a :: nets handle ABSENT => nets; 

0  170 

12319  171 
(*Return the nodes accessible from the term (cons them before nets) 
0  172 
"unif" signifies retrieval for unification rather than matching. 
173 
Var in net matches any term. 

12319  174 
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

175 
else matches only a variable in net. 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

176 
*) 
0  177 
fun matching unif t (net,nets) = 
178 
let fun rands _ (Leaf _, nets) = nets 

16708  179 
 rands t (Net{comb,atoms,...}, nets) = 
12319  180 
case t of 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

181 
f$t => foldr (matching unif t) nets (rands f (comb,[])) 
16708  182 
 Const(c,_) => look1 (atoms, c) nets 
183 
 Free(c,_) => look1 (atoms, c) nets 

16986  184 
 Bound i => look1 (atoms, Term.bound i) nets 
12319  185 
 _ => nets 
186 
in 

0  187 
case net of 
12319  188 
Leaf _ => nets 
0  189 
 Net{var,...} => 
12319  190 
case head_of t of 
191 
Var _ => if unif then net_skip (net,nets) 

192 
else var::nets (*only matches Var in net*) 

2836  193 
(*If "unif" then a var instantiation in the abstraction could allow 
194 
an etareduction, so regard the abstraction as a wildcard.*) 

12319  195 
 Abs _ => if unif then net_skip (net,nets) 
196 
else var::nets (*only a Var can match*) 

197 
 _ => rands t (net, var::nets) (*var could match also*) 

0  198 
end; 
199 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2226
diff
changeset

200 
fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l); 
0  201 

225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

202 
(*return items whose key could match t, WHICH MUST BE BETAETA NORMAL*) 
12319  203 
fun match_term net t = 
0  204 
extract_leaves (matching false t (net,[])); 
205 

206 
(*return items whose key could unify with t*) 

12319  207 
fun unify_term net t = 
0  208 
extract_leaves (matching true t (net,[])); 
209 

3548  210 

16808  211 
(** operations on nets **) 
212 

213 
(*subtraction: collect entries of second net that are NOT present in first net*) 

214 
fun subtract eq net1 net2 = 

215 
let 

216 
fun subtr (Net _) (Leaf ys) = append ys 

217 
 subtr (Leaf xs) (Leaf ys) = 

218 
fold_rev (fn y => if member eq xs y then I else cons y) ys 

219 
 subtr (Leaf _) (net as Net _) = subtr emptynet net 

220 
 subtr (Net {comb = comb1, var = var1, atoms = atoms1}) 

221 
(Net {comb = comb2, var = var2, atoms = atoms2}) = 

16842  222 
subtr comb1 comb2 
223 
#> subtr var1 var2 

224 
#> Symtab.fold (fn (a, net) => 

17412  225 
subtr (if_none (Symtab.lookup atoms1 a) emptynet) net) atoms2 
16808  226 
in subtr net1 net2 [] end; 
227 

228 
fun entries net = subtract (K false) empty net; 

229 

230 

231 
(* merge *) 

3548  232 

233 
fun cons_fst x (xs, y) = (x :: xs, y); 

234 

235 
fun dest (Leaf xs) = map (pair []) xs 

16708  236 
 dest (Net {comb, var, atoms}) = 
3560  237 
map (cons_fst CombK) (dest comb) @ 
238 
map (cons_fst VarK) (dest var) @ 

16808  239 
List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms)); 
3548  240 

16808  241 
fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1; 
3548  242 

0  243 
end; 