author  paulson 
Tue, 25 Mar 1997 10:41:44 +0100  
changeset 2836  148829646a51 
parent 2792  6c17c5ec3d8b 
child 3548  108d09eb3454 
permissions  rwrr 
1460  1 
(* Title: net 
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 

31 
end; 

32 

33 

1500  34 
structure Net : NET = 
0  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 

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 
*) 
47 
fun add_key_of_terms (t, cs) = 

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

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

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

1460  69 
 Net of {comb: 'a net, 
70 
var: 'a net, 

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

0  72 

73 
val empty = Leaf[]; 

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

75 

76 

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

78 

1460  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. 

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}) = 

1460  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 

0  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 

1460  110 
exception DELETE; (*missing item in the net*) 
0  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 

1460  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 

0  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 

1460  157 
 lookup (Leaf _, _::_) = [] (*nonempty keys and empty net*) 
0  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,[]), 

1460  169 
foldr (fn ((_,net), nets) => net::nets) (alist, var::nets)); 
0  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 

1460  185 
 rands t (Net{comb,alist,...}, nets) = 
186 
case t of 

187 
f$t => foldr (matching unif t) (rands f (comb,[]), nets) 

188 
 Const(c,_) => look1 (alist, c) nets 

189 
 Free(c,_) => look1 (alist, c) nets 

190 
 Bound i => look1 (alist, string_of_bound i) nets 

191 
 _ => nets 

0  192 
in 
193 
case net of 

1460  194 
Leaf _ => nets 
0  195 
 Net{var,...} => 
2836  196 
let val etat = Pattern.eta_contract_atom t 
197 
in case (head_of etat) of 

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

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

200 
(*If "unif" then a var instantiation in the abstraction could allow 

201 
an etareduction, so regard the abstraction as a wildcard.*) 

202 
 Abs _ => if unif then net_skip (net,nets) 

203 
else var::nets (*only a Var can match*) 

204 
 _ => rands etat (net, var::nets) (*var could match also*) 

205 
end 

0  206 
end; 
207 

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

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

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

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

213 

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

215 
fun unify_term net t = 

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

217 

218 
end; 