author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23178  07ba6b58b3d2 
child 29606  fedb8be05f24 
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 

20011  35 
val content: 'a net > 'a list 
16808  36 
end; 
0  37 

16808  38 
structure Net: NET = 
0  39 
struct 
40 

41 
datatype key = CombK  VarK  AtomK of string; 

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 etaconversion 
46 
and "near" etaconversions 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 

20080  52 
 rands (Bound i, cs) = AtomK (Name.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 
*) 

16808  88 
fun insert eq (keys,x) net = 
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 

18939  98 
val net' = the_default empty (Symtab.lookup atoms a); 
17412  99 
val atoms' = Symtab.update (a, ins1 (keys, net')) atoms; 
16708  100 
in Net{comb=comb, var=var, atoms=atoms'} end 
0  101 
in ins1 (keys,net) end; 
102 

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

105 

0  106 

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

108 

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

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

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

114 
then empty else Net args; 

0  115 

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

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

118 
eq is the equality test for items. *) 

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

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

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

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

129 
let val atoms' = 

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

133 
(case del1 (keys, net') of 

134 
Leaf [] => Symtab.delete a atoms 

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

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

16677  141 

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

16708  144 
exception ABSENT; 
0  145 

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

0  150 

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

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

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

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

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

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

0  158 

159 

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

23178  161 
fun net_skip (Leaf _) nets = nets 
162 
 net_skip (Net{comb,var,atoms}) nets = 

163 
fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets)); 

0  164 

16808  165 

166 
(** Matching and Unification **) 

0  167 

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

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

0  171 

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

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

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

177 
*) 
23178  178 
fun matching unif t net nets = 
0  179 
let fun rands _ (Leaf _, nets) = nets 
16708  180 
 rands t (Net{comb,atoms,...}, nets) = 
12319  181 
case t of 
23178  182 
f$t => fold_rev (matching unif t) (rands f (comb,[])) nets 
16708  183 
 Const(c,_) => look1 (atoms, c) nets 
184 
 Free(c,_) => look1 (atoms, c) nets 

20080  185 
 Bound i => look1 (atoms, Name.bound i) nets 
12319  186 
 _ => nets 
187 
in 

0  188 
case net of 
12319  189 
Leaf _ => nets 
0  190 
 Net{var,...} => 
12319  191 
case head_of t of 
23178  192 
Var _ => if unif then net_skip net nets 
12319  193 
else var::nets (*only matches Var in net*) 
2836  194 
(*If "unif" then a var instantiation in the abstraction could allow 
195 
an etareduction, so regard the abstraction as a wildcard.*) 

23178  196 
 Abs _ => if unif then net_skip net nets 
12319  197 
else var::nets (*only a Var can match*) 
198 
 _ => rands t (net, var::nets) (*var could match also*) 

0  199 
end; 
200 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
18939
diff
changeset

201 
fun extract_leaves l = maps (fn Leaf xs => xs) l; 
0  202 

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

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

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

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

3548  211 

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

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

215 
fun subtract eq net1 net2 = 

216 
let 

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

218 
 subtr (Leaf xs) (Leaf ys) = 

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

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

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

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

16842  223 
subtr comb1 comb2 
224 
#> subtr var1 var2 

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

18939  226 
subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2 
16808  227 
in subtr net1 net2 [] end; 
228 

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

230 

231 

232 
(* merge *) 

3548  233 

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

235 

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

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

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
18939
diff
changeset

240 
maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms); 
3548  241 

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

20011  244 
fun content net = map #2 (dest net); 
245 

0  246 
end; 