author  nipkow 
Fri, 14 Jan 1994 08:09:07 +0100  
changeset 225  76f60e6400e8 
parent 0  a5a9c433f639 
child 228  4f43430f226e 
permissions  rwrr 
0  1 
(* Title: net 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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 

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

13 
match_term no longer treats abstractions as wildcards but as the constant 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

14 
*Abs*. 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 

31 
end; 

32 

33 

34 
functor NetFun () : NET = 

35 
struct 

36 

37 
datatype key = CombK  VarK  AtomK of string; 

38 

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

39 
(*Bound variables*) 
0  40 
fun string_of_bound i = "*B*" ^ chr i; 
41 

42 
(*Keys are preorder lists of symbols  constants, Vars, bound vars, ... 

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. 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

44 
Abstractions are also regarded as Vars. This covers etaconversion 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

45 
and "near" etaconversions such as %x.P(?f(x)). 
0  46 
*) 
47 
fun add_key_of_terms (t, cs) = 

48 
let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) 

49 
 rands (Const(c,_), cs) = AtomK c :: cs 

50 
 rands (Free(c,_), cs) = AtomK c :: cs 

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

51 
 rands (Bound i, cs) = AtomK (string_of_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 
0  54 
 Abs (_,_,t) => 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 
Keys in the association list (alist) are stored in ascending order. 

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 

69 
 Net of {comb: 'a net, 

70 
var: 'a net, 

71 
alist: (string * 'a net) list}; 

72 

73 
val empty = Leaf[]; 

74 
val emptynet = Net{comb=empty, var=empty, alist=[]}; 

75 

76 

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

78 

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

80 

81 

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

83 
Creates node if not already present. 

84 
eq is the equality test for items. 

85 
The empty list of keys generates a Leaf node, others a Net node. 

86 
*) 

87 
fun insert ((keys,x), net, eq) = 

88 
let fun ins1 ([], Leaf xs) = 

89 
if gen_mem eq (x,xs) then raise INSERT else Leaf(x::xs) 

90 
 ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*) 

91 
 ins1 (CombK :: keys, Net{comb,var,alist}) = 

92 
Net{comb=ins1(keys,comb), var=var, alist=alist} 

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

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

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

96 
let fun newpair net = (a, ins1(keys,net)) 

97 
fun inslist [] = [newpair empty] 

98 
 inslist((b: string, netb) :: alist) = 

99 
if a=b then newpair netb :: alist 

100 
else if a<b then (*absent, ins1ert in alist*) 

101 
newpair empty :: (b,netb) :: alist 

102 
else (*a>b*) (b,netb) :: inslist alist 

103 
in Net{comb=comb, var=var, alist= inslist alist} end 

104 
in ins1 (keys,net) end; 

105 

106 
fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq); 

107 

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

109 

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

111 

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

113 
fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty 

114 
 newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist}; 

115 

116 
(*add new (b,net) pair to the alist provided net is nonempty*) 

117 
fun conspair((b, Leaf[]), alist) = alist 

118 
 conspair((b, net), alist) = (b, net) :: alist; 

119 

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

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

122 
eq is the equality test for items. *) 

123 
fun delete ((keys, x), net, eq) = 

124 
let fun del1 ([], Leaf xs) = 

125 
if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x)) 

126 
else raise DELETE 

127 
 del1 (keys, Leaf[]) = raise DELETE 

128 
 del1 (CombK :: keys, Net{comb,var,alist}) = 

129 
newnet{comb=del1(keys,comb), var=var, alist=alist} 

130 
 del1 (VarK :: keys, Net{comb,var,alist}) = 

131 
newnet{comb=comb, var=del1(keys,var), alist=alist} 

132 
 del1 (AtomK a :: keys, Net{comb,var,alist}) = 

133 
let fun newpair net = (a, del1(keys,net)) 

134 
fun dellist [] = raise DELETE 

135 
 dellist((b: string, netb) :: alist) = 

136 
if a=b then conspair(newpair netb, alist) 

137 
else if a<b then (*absent*) raise DELETE 

138 
else (*a>b*) (b,netb) :: dellist alist 

139 
in newnet{comb=comb, var=var, alist= dellist alist} end 

140 
in del1 (keys,net) end; 

141 

142 
fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq); 

143 

144 
(*** Retrieval functions for discrimination nets ***) 

145 

146 
exception OASSOC; 

147 

148 
(*Ordered association list lookup*) 

149 
fun oassoc ([], a: string) = raise OASSOC 

150 
 oassoc ((b,x)::pairs, a) = 

151 
if b<a then oassoc(pairs,a) 

152 
else if a=b then x 

153 
else raise OASSOC; 

154 

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

156 
fun lookup (Leaf(xs), []) = xs 

157 
 lookup (Leaf _, _::_) = [] (*nonempty keys and empty net*) 

158 
 lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys) 

159 
 lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys) 

160 
 lookup (Net{comb,var,alist}, AtomK a :: keys) = 

161 
lookup(oassoc(alist,a),keys) handle OASSOC => []; 

162 

163 

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

165 
fun net_skip (Leaf _, nets) = nets 

166 
 net_skip (Net{comb,var,alist}, nets) = 

167 
foldr net_skip 

168 
(net_skip (comb,[]), 

169 
foldr (fn ((_,net), nets) => net::nets) (alist, var::nets)); 

170 

171 
(** Matching and Unification**) 

172 

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

174 
fun look1 (alist, a) nets = 

175 
oassoc(alist,a) :: nets handle OASSOC => nets; 

176 

177 
(*Return the nodes accessible from the term (cons them before nets) 

178 
"unif" signifies retrieval for unification rather than matching. 

179 
Var in net matches any term. 

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

180 
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

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

182 
*) 
0  183 
fun matching unif t (net,nets) = 
184 
let fun rands _ (Leaf _, nets) = nets 

185 
 rands t (Net{comb,alist,...}, nets) = 

186 
case t of 

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

187 
f$t => foldr (matching unif t) (rands f (comb,[]), nets) 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

188 
 Const(c,_) => look1 (alist, c) nets 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

189 
 Free(c,_) => look1 (alist, c) nets 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

190 
 Bound i => look1 (alist, string_of_bound i) nets 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

191 
 Abs _ => look1 (alist, "*Abs*") nets 
0  192 
in 
193 
case net of 

194 
Leaf _ => nets 

195 
 Net{var,...} => 

196 
case (head_of t) of 

197 
Var _ => if unif then net_skip (net,nets) 

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

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

199 
(*If "unif" then a var instantiation in the abstraction could allow 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

200 
an etareduction, so regard the abstraction as a wildcard.*) 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

201 
 Abs(_,_,u) => if unif then net_skip (net,nets) 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
0
diff
changeset

202 
else rands t (net, var::nets) 
0  203 
 _ => rands t (net, var::nets) (*var could match also*) 
204 
end; 

205 

206 
val extract_leaves = flat o map (fn Leaf(xs) => xs); 

207 

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

208 
(*return items whose key could match t, WHICH MUST BE BETAETA NORMAL*) 
0  209 
fun match_term net t = 
210 
extract_leaves (matching false t (net,[])); 

211 

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

213 
fun unify_term net t = 

214 
extract_leaves (matching true t (net,[])); 

215 

216 
end; 