author  wenzelm 
Wed, 23 Jul 1997 11:11:14 +0200  
changeset 3560  7db9a44dfa06 
parent 3549  e8c8d76810a6 
child 6539  2e7d2fba9f6c 
permissions  rwrr 
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 betaetanormal. 

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 etaconversion 
47 
and "near" etaconversions 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 _, _::_) = [] (*nonempty 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 etareduction, 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 BETAETA 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; 