1 (* ========================================================================= *) |
|
2 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *) |
|
3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure TermNet :> TermNet = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* Quotient terms *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 datatype qterm = VAR | FN of NameArity.nameArity * qterm list; |
|
16 |
|
17 fun termToQterm (Term.Var _) = VAR |
|
18 | termToQterm (Term.Fn (f,l)) = FN ((f, length l), map termToQterm l); |
|
19 |
|
20 local |
|
21 fun qm [] = true |
|
22 | qm ((VAR,_) :: rest) = qm rest |
|
23 | qm ((FN _, VAR) :: _) = false |
|
24 | qm ((FN (f,a), FN (g,b)) :: rest) = f = g andalso qm (zip a b @ rest); |
|
25 in |
|
26 fun matchQtermQterm qtm qtm' = qm [(qtm,qtm')]; |
|
27 end; |
|
28 |
|
29 local |
|
30 fun qm [] = true |
|
31 | qm ((VAR,_) :: rest) = qm rest |
|
32 | qm ((FN _, Term.Var _) :: _) = false |
|
33 | qm ((FN ((f,n),a), Term.Fn (g,b)) :: rest) = |
|
34 f = g andalso n = length b andalso qm (zip a b @ rest); |
|
35 in |
|
36 fun matchQtermTerm qtm tm = qm [(qtm,tm)]; |
|
37 end; |
|
38 |
|
39 local |
|
40 fun qn qsub [] = SOME qsub |
|
41 | qn qsub ((Term.Var v, qtm) :: rest) = |
|
42 (case NameMap.peek qsub v of |
|
43 NONE => qn (NameMap.insert qsub (v,qtm)) rest |
|
44 | SOME qtm' => if qtm = qtm' then qn qsub rest else NONE) |
|
45 | qn _ ((Term.Fn _, VAR) :: _) = NONE |
|
46 | qn qsub ((Term.Fn (f,a), FN ((g,n),b)) :: rest) = |
|
47 if f = g andalso length a = n then qn qsub (zip a b @ rest) else NONE; |
|
48 in |
|
49 fun matchTermQterm qsub tm qtm = qn qsub [(tm,qtm)]; |
|
50 end; |
|
51 |
|
52 local |
|
53 fun qv VAR x = x |
|
54 | qv x VAR = x |
|
55 | qv (FN (f,a)) (FN (g,b)) = |
|
56 let |
|
57 val _ = f = g orelse raise Error "TermNet.qv" |
|
58 in |
|
59 FN (f, zipwith qv a b) |
|
60 end; |
|
61 |
|
62 fun qu qsub [] = qsub |
|
63 | qu qsub ((VAR, _) :: rest) = qu qsub rest |
|
64 | qu qsub ((qtm, Term.Var v) :: rest) = |
|
65 let |
|
66 val qtm = |
|
67 case NameMap.peek qsub v of NONE => qtm | SOME qtm' => qv qtm qtm' |
|
68 in |
|
69 qu (NameMap.insert qsub (v,qtm)) rest |
|
70 end |
|
71 | qu qsub ((FN ((f,n),a), Term.Fn (g,b)) :: rest) = |
|
72 if f = g andalso n = length b then qu qsub (zip a b @ rest) |
|
73 else raise Error "TermNet.qu"; |
|
74 in |
|
75 fun unifyQtermQterm qtm qtm' = total (qv qtm) qtm'; |
|
76 |
|
77 fun unifyQtermTerm qsub qtm tm = total (qu qsub) [(qtm,tm)]; |
|
78 end; |
|
79 |
|
80 local |
|
81 fun qtermToTerm VAR = Term.Var "" |
|
82 | qtermToTerm (FN ((f,_),l)) = Term.Fn (f, map qtermToTerm l); |
|
83 in |
|
84 val ppQterm = Parser.ppMap qtermToTerm Term.pp; |
|
85 end; |
|
86 |
|
87 (* ------------------------------------------------------------------------- *) |
|
88 (* A type of term sets that can be efficiently matched and unified. *) |
|
89 (* ------------------------------------------------------------------------- *) |
|
90 |
|
91 type parameters = {fifo : bool}; |
|
92 |
|
93 datatype 'a net = |
|
94 RESULT of 'a list |
|
95 | SINGLE of qterm * 'a net |
|
96 | MULTIPLE of 'a net option * 'a net NameArityMap.map; |
|
97 |
|
98 datatype 'a termNet = NET of parameters * int * (int * (int * 'a) net) option; |
|
99 |
|
100 (* ------------------------------------------------------------------------- *) |
|
101 (* Basic operations. *) |
|
102 (* ------------------------------------------------------------------------- *) |
|
103 |
|
104 fun new parm = NET (parm,0,NONE); |
|
105 |
|
106 local |
|
107 fun computeSize (RESULT l) = length l |
|
108 | computeSize (SINGLE (_,n)) = computeSize n |
|
109 | computeSize (MULTIPLE (vs,fs)) = |
|
110 NameArityMap.foldl |
|
111 (fn (_,n,acc) => acc + computeSize n) |
|
112 (case vs of SOME n => computeSize n | NONE => 0) |
|
113 fs; |
|
114 in |
|
115 fun netSize NONE = NONE |
|
116 | netSize (SOME n) = SOME (computeSize n, n); |
|
117 end; |
|
118 |
|
119 fun size (NET (_,_,NONE)) = 0 |
|
120 | size (NET (_, _, SOME (i,_))) = i; |
|
121 |
|
122 fun null net = size net = 0; |
|
123 |
|
124 fun singles qtms a = foldr SINGLE a qtms; |
|
125 |
|
126 local |
|
127 fun pre NONE = (0,NONE) |
|
128 | pre (SOME (i,n)) = (i, SOME n); |
|
129 |
|
130 fun add (RESULT l) [] (RESULT l') = RESULT (l @ l') |
|
131 | add a (input1 as qtm :: qtms) (SINGLE (qtm',n)) = |
|
132 if qtm = qtm' then SINGLE (qtm, add a qtms n) |
|
133 else add a input1 (add n [qtm'] (MULTIPLE (NONE, NameArityMap.new ()))) |
|
134 | add a (VAR :: qtms) (MULTIPLE (vs,fs)) = |
|
135 MULTIPLE (SOME (oadd a qtms vs), fs) |
|
136 | add a (FN (f,l) :: qtms) (MULTIPLE (vs,fs)) = |
|
137 let |
|
138 val n = NameArityMap.peek fs f |
|
139 in |
|
140 MULTIPLE (vs, NameArityMap.insert fs (f, oadd a (l @ qtms) n)) |
|
141 end |
|
142 | add _ _ _ = raise Bug "TermNet.insert: Match" |
|
143 |
|
144 and oadd a qtms NONE = singles qtms a |
|
145 | oadd a qtms (SOME n) = add a qtms n; |
|
146 |
|
147 fun ins a qtm (i,n) = SOME (i + 1, oadd (RESULT [a]) [qtm] n); |
|
148 in |
|
149 fun insert (NET (p,k,n)) (tm,a) = |
|
150 NET (p, k + 1, ins (k,a) (termToQterm tm) (pre n)) |
|
151 handle Error _ => raise Bug "TermNet.insert: should never fail"; |
|
152 end; |
|
153 |
|
154 fun fromList parm l = foldl (fn (tm_a,n) => insert n tm_a) (new parm) l; |
|
155 |
|
156 fun filter pred = |
|
157 let |
|
158 fun filt (RESULT l) = |
|
159 (case List.filter (fn (_,a) => pred a) l of |
|
160 [] => NONE |
|
161 | l => SOME (RESULT l)) |
|
162 | filt (SINGLE (qtm,n)) = |
|
163 (case filt n of |
|
164 NONE => NONE |
|
165 | SOME n => SOME (SINGLE (qtm,n))) |
|
166 | filt (MULTIPLE (vs,fs)) = |
|
167 let |
|
168 val vs = Option.mapPartial filt vs |
|
169 |
|
170 val fs = NameArityMap.mapPartial (fn (_,n) => filt n) fs |
|
171 in |
|
172 if not (Option.isSome vs) andalso NameArityMap.null fs then NONE |
|
173 else SOME (MULTIPLE (vs,fs)) |
|
174 end |
|
175 in |
|
176 fn net as NET (_,_,NONE) => net |
|
177 | NET (p, k, SOME (_,n)) => NET (p, k, netSize (filt n)) |
|
178 end |
|
179 handle Error _ => raise Bug "TermNet.filter: should never fail"; |
|
180 |
|
181 fun toString net = "TermNet[" ^ Int.toString (size net) ^ "]"; |
|
182 |
|
183 (* ------------------------------------------------------------------------- *) |
|
184 (* Specialized fold operations to support matching and unification. *) |
|
185 (* ------------------------------------------------------------------------- *) |
|
186 |
|
187 local |
|
188 fun norm (0 :: ks, (f as (_,n)) :: fs, qtms) = |
|
189 let |
|
190 val (a,qtms) = revDivide qtms n |
|
191 in |
|
192 addQterm (FN (f,a)) (ks,fs,qtms) |
|
193 end |
|
194 | norm stack = stack |
|
195 |
|
196 and addQterm qtm (ks,fs,qtms) = |
|
197 let |
|
198 val ks = case ks of [] => [] | k :: ks => (k - 1) :: ks |
|
199 in |
|
200 norm (ks, fs, qtm :: qtms) |
|
201 end |
|
202 |
|
203 and addFn (f as (_,n)) (ks,fs,qtms) = norm (n :: ks, f :: fs, qtms); |
|
204 in |
|
205 val stackEmpty = ([],[],[]); |
|
206 |
|
207 val stackAddQterm = addQterm; |
|
208 |
|
209 val stackAddFn = addFn; |
|
210 |
|
211 fun stackValue ([],[],[qtm]) = qtm |
|
212 | stackValue _ = raise Bug "TermNet.stackValue"; |
|
213 end; |
|
214 |
|
215 local |
|
216 fun fold _ acc [] = acc |
|
217 | fold inc acc ((0,stack,net) :: rest) = |
|
218 fold inc (inc (stackValue stack, net, acc)) rest |
|
219 | fold inc acc ((n, stack, SINGLE (qtm,net)) :: rest) = |
|
220 fold inc acc ((n - 1, stackAddQterm qtm stack, net) :: rest) |
|
221 | fold inc acc ((n, stack, MULTIPLE (v,fns)) :: rest) = |
|
222 let |
|
223 val n = n - 1 |
|
224 |
|
225 val rest = |
|
226 case v of |
|
227 NONE => rest |
|
228 | SOME net => (n, stackAddQterm VAR stack, net) :: rest |
|
229 |
|
230 fun getFns (f as (_,k), net, x) = |
|
231 (k + n, stackAddFn f stack, net) :: x |
|
232 in |
|
233 fold inc acc (NameArityMap.foldr getFns rest fns) |
|
234 end |
|
235 | fold _ _ _ = raise Bug "TermNet.foldTerms.fold"; |
|
236 in |
|
237 fun foldTerms inc acc net = fold inc acc [(1,stackEmpty,net)]; |
|
238 end; |
|
239 |
|
240 fun foldEqualTerms pat inc acc = |
|
241 let |
|
242 fun fold ([],net) = inc (pat,net,acc) |
|
243 | fold (pat :: pats, SINGLE (qtm,net)) = |
|
244 if pat = qtm then fold (pats,net) else acc |
|
245 | fold (VAR :: pats, MULTIPLE (v,_)) = |
|
246 (case v of NONE => acc | SOME net => fold (pats,net)) |
|
247 | fold (FN (f,a) :: pats, MULTIPLE (_,fns)) = |
|
248 (case NameArityMap.peek fns f of |
|
249 NONE => acc |
|
250 | SOME net => fold (a @ pats, net)) |
|
251 | fold _ = raise Bug "TermNet.foldEqualTerms.fold"; |
|
252 in |
|
253 fn net => fold ([pat],net) |
|
254 end; |
|
255 |
|
256 local |
|
257 fun fold _ acc [] = acc |
|
258 | fold inc acc (([],stack,net) :: rest) = |
|
259 fold inc (inc (stackValue stack, net, acc)) rest |
|
260 | fold inc acc ((VAR :: pats, stack, net) :: rest) = |
|
261 let |
|
262 fun harvest (qtm,n,l) = (pats, stackAddQterm qtm stack, n) :: l |
|
263 in |
|
264 fold inc acc (foldTerms harvest rest net) |
|
265 end |
|
266 | fold inc acc ((pat :: pats, stack, SINGLE (qtm,net)) :: rest) = |
|
267 (case unifyQtermQterm pat qtm of |
|
268 NONE => fold inc acc rest |
|
269 | SOME qtm => |
|
270 fold inc acc ((pats, stackAddQterm qtm stack, net) :: rest)) |
|
271 | fold |
|
272 inc acc |
|
273 (((pat as FN (f,a)) :: pats, stack, MULTIPLE (v,fns)) :: rest) = |
|
274 let |
|
275 val rest = |
|
276 case v of |
|
277 NONE => rest |
|
278 | SOME net => (pats, stackAddQterm pat stack, net) :: rest |
|
279 |
|
280 val rest = |
|
281 case NameArityMap.peek fns f of |
|
282 NONE => rest |
|
283 | SOME net => (a @ pats, stackAddFn f stack, net) :: rest |
|
284 in |
|
285 fold inc acc rest |
|
286 end |
|
287 | fold _ _ _ = raise Bug "TermNet.foldUnifiableTerms.fold"; |
|
288 in |
|
289 fun foldUnifiableTerms pat inc acc net = |
|
290 fold inc acc [([pat],stackEmpty,net)]; |
|
291 end; |
|
292 |
|
293 (* ------------------------------------------------------------------------- *) |
|
294 (* Matching and unification queries. *) |
|
295 (* *) |
|
296 (* These function return OVER-APPROXIMATIONS! *) |
|
297 (* Filter afterwards to get the precise set of satisfying values. *) |
|
298 (* ------------------------------------------------------------------------- *) |
|
299 |
|
300 local |
|
301 fun idwise ((m,_),(n,_)) = Int.compare (m,n); |
|
302 |
|
303 fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l; |
|
304 in |
|
305 fun finally parm l = map snd (fifoize parm l); |
|
306 end; |
|
307 |
|
308 local |
|
309 fun mat acc [] = acc |
|
310 | mat acc ((RESULT l, []) :: rest) = mat (l @ acc) rest |
|
311 | mat acc ((SINGLE (qtm,n), tm :: tms) :: rest) = |
|
312 mat acc (if matchQtermTerm qtm tm then (n,tms) :: rest else rest) |
|
313 | mat acc ((MULTIPLE (vs,fs), tm :: tms) :: rest) = |
|
314 let |
|
315 val rest = case vs of NONE => rest | SOME n => (n,tms) :: rest |
|
316 |
|
317 val rest = |
|
318 case tm of |
|
319 Term.Var _ => rest |
|
320 | Term.Fn (f,l) => |
|
321 case NameArityMap.peek fs (f, length l) of |
|
322 NONE => rest |
|
323 | SOME n => (n, l @ tms) :: rest |
|
324 in |
|
325 mat acc rest |
|
326 end |
|
327 | mat _ _ = raise Bug "TermNet.match: Match"; |
|
328 in |
|
329 fun match (NET (_,_,NONE)) _ = [] |
|
330 | match (NET (p, _, SOME (_,n))) tm = |
|
331 finally p (mat [] [(n,[tm])]) |
|
332 handle Error _ => raise Bug "TermNet.match: should never fail"; |
|
333 end; |
|
334 |
|
335 local |
|
336 fun unseenInc qsub v tms (qtm,net,rest) = |
|
337 (NameMap.insert qsub (v,qtm), net, tms) :: rest; |
|
338 |
|
339 fun seenInc qsub tms (_,net,rest) = (qsub,net,tms) :: rest; |
|
340 |
|
341 fun mat acc [] = acc |
|
342 | mat acc ((_, RESULT l, []) :: rest) = mat (l @ acc) rest |
|
343 | mat acc ((qsub, SINGLE (qtm,net), tm :: tms) :: rest) = |
|
344 (case matchTermQterm qsub tm qtm of |
|
345 NONE => mat acc rest |
|
346 | SOME qsub => mat acc ((qsub,net,tms) :: rest)) |
|
347 | mat acc ((qsub, net as MULTIPLE _, Term.Var v :: tms) :: rest) = |
|
348 (case NameMap.peek qsub v of |
|
349 NONE => mat acc (foldTerms (unseenInc qsub v tms) rest net) |
|
350 | SOME qtm => mat acc (foldEqualTerms qtm (seenInc qsub tms) rest net)) |
|
351 | mat acc ((qsub, MULTIPLE (_,fns), Term.Fn (f,a) :: tms) :: rest) = |
|
352 let |
|
353 val rest = |
|
354 case NameArityMap.peek fns (f, length a) of |
|
355 NONE => rest |
|
356 | SOME net => (qsub, net, a @ tms) :: rest |
|
357 in |
|
358 mat acc rest |
|
359 end |
|
360 | mat _ _ = raise Bug "TermNet.matched.mat"; |
|
361 in |
|
362 fun matched (NET (_,_,NONE)) _ = [] |
|
363 | matched (NET (parm, _, SOME (_,net))) tm = |
|
364 finally parm (mat [] [(NameMap.new (), net, [tm])]) |
|
365 handle Error _ => raise Bug "TermNet.matched: should never fail"; |
|
366 end; |
|
367 |
|
368 local |
|
369 fun inc qsub v tms (qtm,net,rest) = |
|
370 (NameMap.insert qsub (v,qtm), net, tms) :: rest; |
|
371 |
|
372 fun mat acc [] = acc |
|
373 | mat acc ((_, RESULT l, []) :: rest) = mat (l @ acc) rest |
|
374 | mat acc ((qsub, SINGLE (qtm,net), tm :: tms) :: rest) = |
|
375 (case unifyQtermTerm qsub qtm tm of |
|
376 NONE => mat acc rest |
|
377 | SOME qsub => mat acc ((qsub,net,tms) :: rest)) |
|
378 | mat acc ((qsub, net as MULTIPLE _, Term.Var v :: tms) :: rest) = |
|
379 (case NameMap.peek qsub v of |
|
380 NONE => mat acc (foldTerms (inc qsub v tms) rest net) |
|
381 | SOME qtm => mat acc (foldUnifiableTerms qtm (inc qsub v tms) rest net)) |
|
382 | mat acc ((qsub, MULTIPLE (v,fns), Term.Fn (f,a) :: tms) :: rest) = |
|
383 let |
|
384 val rest = case v of NONE => rest | SOME net => (qsub,net,tms) :: rest |
|
385 |
|
386 val rest = |
|
387 case NameArityMap.peek fns (f, length a) of |
|
388 NONE => rest |
|
389 | SOME net => (qsub, net, a @ tms) :: rest |
|
390 in |
|
391 mat acc rest |
|
392 end |
|
393 | mat _ _ = raise Bug "TermNet.unify.mat"; |
|
394 in |
|
395 fun unify (NET (_,_,NONE)) _ = [] |
|
396 | unify (NET (parm, _, SOME (_,net))) tm = |
|
397 finally parm (mat [] [(NameMap.new (), net, [tm])]) |
|
398 handle Error _ => raise Bug "TermNet.unify: should never fail"; |
|
399 end; |
|
400 |
|
401 (* ------------------------------------------------------------------------- *) |
|
402 (* Pretty printing. *) |
|
403 (* ------------------------------------------------------------------------- *) |
|
404 |
|
405 local |
|
406 fun inc (qtm, RESULT l, acc) = |
|
407 foldl (fn ((n,a),acc) => (n,(qtm,a)) :: acc) acc l |
|
408 | inc _ = raise Bug "TermNet.pp.inc"; |
|
409 |
|
410 fun toList (NET (_,_,NONE)) = [] |
|
411 | toList (NET (parm, _, SOME (_,net))) = |
|
412 finally parm (foldTerms inc [] net); |
|
413 in |
|
414 fun pp ppA = |
|
415 Parser.ppMap toList (Parser.ppList (Parser.ppBinop " |->" ppQterm ppA)); |
|
416 end; |
|
417 |
|
418 end |
|