|
1 (* Title: unify |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright Cambridge University 1992 |
|
5 |
|
6 Higher-Order Unification |
|
7 |
|
8 Potential problem: type of Vars is often ignored, so two Vars with same |
|
9 indexname but different types can cause errors! |
|
10 *) |
|
11 |
|
12 |
|
13 signature UNIFY = |
|
14 sig |
|
15 structure Sign: SIGN |
|
16 structure Envir : ENVIR |
|
17 structure Sequence : SEQUENCE |
|
18 (*references for control and tracing*) |
|
19 val trace_bound: int ref |
|
20 val trace_simp: bool ref |
|
21 val trace_types: bool ref |
|
22 val search_bound: int ref |
|
23 (*other exports*) |
|
24 val combound : (term*int*int) -> term |
|
25 val rlist_abs: (string*typ)list * term -> term |
|
26 val smash_unifiers : Sign.sg * Envir.env * (term*term)list |
|
27 -> (Envir.env Sequence.seq) |
|
28 val unifiers: Sign.sg * Envir.env * ((term*term)list) |
|
29 -> (Envir.env * (term * term)list) Sequence.seq |
|
30 end; |
|
31 |
|
32 functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE |
|
33 and Pattern:PATTERN |
|
34 sharing type Sign.sg = Pattern.sg |
|
35 and type Envir.env = Pattern.env) |
|
36 : UNIFY = |
|
37 struct |
|
38 |
|
39 structure Sign = Sign; |
|
40 structure Envir = Envir; |
|
41 structure Sequence = Sequence; |
|
42 structure Pretty = Sign.Syntax.Pretty; |
|
43 |
|
44 (*Unification options*) |
|
45 |
|
46 val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*) |
|
47 and search_bound = ref 20 (*unification quits above this depth*) |
|
48 and trace_simp = ref false (*print dpairs before calling SIMPL*) |
|
49 and trace_types = ref false (*announce potential incompleteness |
|
50 of type unification*) |
|
51 |
|
52 val sgr = ref(Sign.pure); |
|
53 |
|
54 type binderlist = (string*typ) list; |
|
55 |
|
56 type dpair = binderlist * term * term; |
|
57 |
|
58 fun body_type(Envir.Envir{iTs,...}) = |
|
59 let fun bT(Type("fun",[_,T])) = bT T |
|
60 | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of |
|
61 None => T | Some(T') => bT T') |
|
62 | bT T = T |
|
63 in bT end; |
|
64 |
|
65 fun binder_types(Envir.Envir{iTs,...}) = |
|
66 let fun bTs(Type("fun",[T,U])) = T :: bTs U |
|
67 | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of |
|
68 None => [] | Some(T') => bTs T') |
|
69 | bTs _ = [] |
|
70 in bTs end; |
|
71 |
|
72 fun strip_type env T = (binder_types env T, body_type env T); |
|
73 |
|
74 |
|
75 (*Put a term into head normal form for unification. |
|
76 Operands need not be in normal form. Does eta-expansions on the head, |
|
77 which involves renumbering (thus copying) the args. To avoid this |
|
78 inefficiency, avoid partial application: if an atom is applied to |
|
79 any arguments at all, apply it to its full number of arguments. |
|
80 For |
|
81 rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!) |
|
82 args = [arg1,...,argn] |
|
83 the value of |
|
84 (xm,...,x1)(head(arg1,...,argn)) remains invariant. |
|
85 *) |
|
86 |
|
87 local exception SAME |
|
88 in |
|
89 fun head_norm (env,t) : term = |
|
90 let fun hnorm (Var (v,T)) = |
|
91 (case Envir.lookup (env,v) of |
|
92 Some u => head_norm (env, u) |
|
93 | None => raise SAME) |
|
94 | hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body) |
|
95 | hnorm (Abs(_,_,body) $ t) = |
|
96 head_norm (env, subst_bounds([t], body)) |
|
97 | hnorm (f $ t) = |
|
98 (case hnorm f of |
|
99 Abs(_,_,body) => |
|
100 head_norm (env, subst_bounds([t], body)) |
|
101 | nf => nf $ t) |
|
102 | hnorm _ = raise SAME |
|
103 in hnorm t handle SAME=> t end |
|
104 end; |
|
105 |
|
106 |
|
107 (*finds type of term without checking that combinations are consistent |
|
108 rbinder holds types of bound variables*) |
|
109 fun fastype (Envir.Envir{iTs,...}) = |
|
110 let val funerr = "fastype: expected function type"; |
|
111 fun fast(rbinder, f$u) = |
|
112 (case (fast (rbinder, f)) of |
|
113 Type("fun",[_,T]) => T |
|
114 | TVar(ixn,_) => |
|
115 (case assoc(iTs,ixn) of |
|
116 Some(Type("fun",[_,T])) => T |
|
117 | _ => raise TERM(funerr, [f$u])) |
|
118 | _ => raise TERM(funerr, [f$u])) |
|
119 | fast (rbinder, Const (_,T)) = T |
|
120 | fast (rbinder, Free (_,T)) = T |
|
121 | fast (rbinder, Bound i) = |
|
122 (#2 (nth_elem (i,rbinder)) |
|
123 handle LIST _=> raise TERM("fastype: Bound", [Bound i])) |
|
124 | fast (rbinder, Var (_,T)) = T |
|
125 | fast (rbinder, Abs (_,T,u)) = T --> fast (("",T) :: rbinder, u) |
|
126 in fast end; |
|
127 |
|
128 |
|
129 (*Eta normal form*) |
|
130 fun eta_norm(env as Envir.Envir{iTs,...}) = |
|
131 let fun etif (Type("fun",[T,U]), t) = |
|
132 Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) |
|
133 | etif (TVar(ixn,_),t) = |
|
134 (case assoc(iTs,ixn) of |
|
135 None => t | Some(T) => etif(T,t)) |
|
136 | etif (_,t) = t; |
|
137 fun eta_nm (rbinder, Abs(a,T,body)) = |
|
138 Abs(a, T, eta_nm ((a,T)::rbinder, body)) |
|
139 | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) |
|
140 in eta_nm end; |
|
141 |
|
142 |
|
143 (*OCCURS CHECK |
|
144 Does the uvar occur in the term t? |
|
145 two forms of search, for whether there is a rigid path to the current term. |
|
146 "seen" is list of variables passed thru, is a memo variable for sharing. |
|
147 This version searches for nonrigid occurrence, returns true if found. *) |
|
148 fun occurs_terms (seen: (indexname list) ref, |
|
149 env: Envir.env, v: indexname, ts: term list): bool = |
|
150 let fun occurs [] = false |
|
151 | occurs (t::ts) = occur t orelse occurs ts |
|
152 and occur (Const _) = false |
|
153 | occur (Bound _) = false |
|
154 | occur (Free _) = false |
|
155 | occur (Var (w,_)) = |
|
156 if w mem !seen then false |
|
157 else if v=w then true |
|
158 (*no need to lookup: v has no assignment*) |
|
159 else (seen := w:: !seen; |
|
160 case Envir.lookup(env,w) of |
|
161 None => false |
|
162 | Some t => occur t) |
|
163 | occur (Abs(_,_,body)) = occur body |
|
164 | occur (f$t) = occur t orelse occur f |
|
165 in occurs ts end; |
|
166 |
|
167 |
|
168 |
|
169 (* f(a1,...,an) ----> (f, [a1,...,an]) using the assignments*) |
|
170 fun head_of_in (env,t) : term = case t of |
|
171 f$_ => head_of_in(env,f) |
|
172 | Var (v,_) => (case Envir.lookup(env,v) of |
|
173 Some u => head_of_in(env,u) | None => t) |
|
174 | _ => t; |
|
175 |
|
176 |
|
177 datatype occ = NoOcc | Nonrigid | Rigid; |
|
178 |
|
179 (* Rigid occur check |
|
180 Returns Rigid if it finds a rigid occurrence of the variable, |
|
181 Nonrigid if it finds a nonrigid path to the variable. |
|
182 NoOcc otherwise. |
|
183 Continues searching for a rigid occurrence even if it finds a nonrigid one. |
|
184 |
|
185 Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ] |
|
186 a rigid path to the variable, appearing with no arguments. |
|
187 Here completeness is sacrificed in order to reduce danger of divergence: |
|
188 reject ALL rigid paths to the variable. |
|
189 Could check for rigid paths to bound variables that are out of scope. |
|
190 Not necessary because the assignment test looks at variable's ENTIRE rbinder. |
|
191 |
|
192 Treatment of head(arg1,...,argn): |
|
193 If head is a variable then no rigid path, switch to nonrigid search |
|
194 for arg1,...,argn. |
|
195 If head is an abstraction then possibly no rigid path (head could be a |
|
196 constant function) so again use nonrigid search. Happens only if |
|
197 term is not in normal form. |
|
198 |
|
199 Warning: finds a rigid occurrence of ?f in ?f(t). |
|
200 Should NOT be called in this case: there is a flex-flex unifier |
|
201 *) |
|
202 fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = |
|
203 let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid |
|
204 else NoOcc |
|
205 fun occurs [] = NoOcc |
|
206 | occurs (t::ts) = |
|
207 (case occur t of |
|
208 Rigid => Rigid |
|
209 | oc => (case occurs ts of NoOcc => oc | oc2 => oc2)) |
|
210 and occomb (f$t) = |
|
211 (case occur t of |
|
212 Rigid => Rigid |
|
213 | oc => (case occomb f of NoOcc => oc | oc2 => oc2)) |
|
214 | occomb t = occur t |
|
215 and occur (Const _) = NoOcc |
|
216 | occur (Bound _) = NoOcc |
|
217 | occur (Free _) = NoOcc |
|
218 | occur (Var (w,_)) = |
|
219 if w mem !seen then NoOcc |
|
220 else if v=w then Rigid |
|
221 else (seen := w:: !seen; |
|
222 case Envir.lookup(env,w) of |
|
223 None => NoOcc |
|
224 | Some t => occur t) |
|
225 | occur (Abs(_,_,body)) = occur body |
|
226 | occur (t as f$_) = (*switch to nonrigid search?*) |
|
227 (case head_of_in (env,f) of |
|
228 Var (w,_) => (*w is not assigned*) |
|
229 if v=w then Rigid |
|
230 else nonrigid t |
|
231 | Abs(_,_,body) => nonrigid t (*not in normal form*) |
|
232 | _ => occomb t) |
|
233 in occur t end; |
|
234 |
|
235 |
|
236 exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) |
|
237 exception ASSIGN; (*Raised if not an assignment*) |
|
238 |
|
239 |
|
240 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) = |
|
241 if T=U then env else |
|
242 let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs) |
|
243 in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'} |
|
244 end handle Sign.Type.TUNIFY => raise CANTUNIFY; |
|
245 |
|
246 fun test_unify_types(args as (T,U,_)) = |
|
247 let val sot = Sign.string_of_typ (!sgr); |
|
248 fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T); |
|
249 val env' = unify_types(args) |
|
250 in if is_TVar(T) orelse is_TVar(U) then warn() else (); |
|
251 env' |
|
252 end; |
|
253 |
|
254 (*Is the term eta-convertible to a single variable with the given rbinder? |
|
255 Examples: ?a ?f(B.0) ?g(B.1,B.0) |
|
256 Result is var a for use in SIMPL. *) |
|
257 fun get_eta_var ([], _, Var vT) = vT |
|
258 | get_eta_var (_::rbinder, n, f $ Bound i) = |
|
259 if n=i then get_eta_var (rbinder, n+1, f) |
|
260 else raise ASSIGN |
|
261 | get_eta_var _ = raise ASSIGN; |
|
262 |
|
263 |
|
264 (* ([xn,...,x1], t) ======> (x1,...,xn)t *) |
|
265 fun rlist_abs ([], body) = body |
|
266 | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); |
|
267 |
|
268 |
|
269 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u. |
|
270 If v occurs rigidly then nonunifiable. |
|
271 If v occurs nonrigidly then must use full algorithm. *) |
|
272 fun assignment (env, rbinder, t, u) = |
|
273 let val (v,T) = get_eta_var(rbinder,0,t) |
|
274 in case rigid_occurs_term (ref[], env, v, u) of |
|
275 NoOcc => let val env = unify_types(body_type env T, |
|
276 fastype env (rbinder,u),env) |
|
277 in Envir.update ((v, rlist_abs(rbinder,u)), env) end |
|
278 | Nonrigid => raise ASSIGN |
|
279 | Rigid => raise CANTUNIFY |
|
280 end; |
|
281 |
|
282 |
|
283 (*Extends an rbinder with a new disagreement pair, if both are abstractions. |
|
284 Tries to unify types of the bound variables! |
|
285 Checks that binders have same length, since terms should be eta-normal; |
|
286 if not, raises TERM, probably indicating type mismatch. |
|
287 Uses variable a (unless the null string) to preserve user's naming.*) |
|
288 fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = |
|
289 let val env' = unify_types(T,U,env) |
|
290 val c = if a="" then b else a |
|
291 in new_dpair((c,T) :: rbinder, body1, body2, env') end |
|
292 | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", []) |
|
293 | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", []) |
|
294 | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); |
|
295 |
|
296 |
|
297 fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env = |
|
298 new_dpair (rbinder, |
|
299 eta_norm env (rbinder, head_norm(env,t)), |
|
300 eta_norm env (rbinder, head_norm(env,u)), env); |
|
301 |
|
302 |
|
303 |
|
304 (*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs |
|
305 Does not perform assignments for flex-flex pairs: |
|
306 may create nonrigid paths, which prevent other assignments*) |
|
307 fun SIMPL0 (dp0, (env,flexflex,flexrigid)) |
|
308 : Envir.env * dpair list * dpair list = |
|
309 let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0); |
|
310 fun SIMRANDS(f$t, g$u, env) = |
|
311 SIMPL0((rbinder,t,u), SIMRANDS(f,g,env)) |
|
312 | SIMRANDS (t as _$_, _, _) = |
|
313 raise TERM ("SIMPL: operands mismatch", [t,u]) |
|
314 | SIMRANDS (t, u as _$_, _) = |
|
315 raise TERM ("SIMPL: operands mismatch", [t,u]) |
|
316 | SIMRANDS(_,_,env) = (env,flexflex,flexrigid); |
|
317 in case (head_of t, head_of u) of |
|
318 (Var(_,T), Var(_,U)) => |
|
319 let val T' = body_type env T and U' = body_type env U; |
|
320 val env = unify_types(T',U',env) |
|
321 in (env, dp::flexflex, flexrigid) end |
|
322 | (Var _, _) => |
|
323 ((assignment (env,rbinder,t,u), flexflex, flexrigid) |
|
324 handle ASSIGN => (env, flexflex, dp::flexrigid)) |
|
325 | (_, Var _) => |
|
326 ((assignment (env,rbinder,u,t), flexflex, flexrigid) |
|
327 handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) |
|
328 | (Const(a,T), Const(b,U)) => |
|
329 if a=b then SIMRANDS(t,u, unify_types(T,U,env)) |
|
330 else raise CANTUNIFY |
|
331 | (Bound i, Bound j) => |
|
332 if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY |
|
333 | (Free(a,T), Free(b,U)) => |
|
334 if a=b then SIMRANDS(t,u, unify_types(T,U,env)) |
|
335 else raise CANTUNIFY |
|
336 | _ => raise CANTUNIFY |
|
337 end; |
|
338 |
|
339 |
|
340 (* changed(env,t) checks whether the head of t is a variable assigned in env*) |
|
341 fun changed (env, f$_) = changed (env,f) |
|
342 | changed (env, Var (v,_)) = |
|
343 (case Envir.lookup(env,v) of None=>false | _ => true) |
|
344 | changed _ = false; |
|
345 |
|
346 |
|
347 (*Recursion needed if any of the 'head variables' have been updated |
|
348 Clever would be to re-do just the affected dpairs*) |
|
349 fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list = |
|
350 let val all as (env',flexflex,flexrigid) = |
|
351 foldr SIMPL0 (dpairs, (env,[],[])); |
|
352 val dps = flexrigid@flexflex |
|
353 in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps |
|
354 then SIMPL(env',dps) else all |
|
355 end; |
|
356 |
|
357 |
|
358 (*computes t(Bound(n+k-1),...,Bound(n)) *) |
|
359 fun combound (t, n, k) = |
|
360 if k>0 then combound (t,n+1,k-1) $ (Bound n) else t; |
|
361 |
|
362 |
|
363 (*Makes the terms E1,...,Em, where Ts = [T...Tm]. |
|
364 Each Ei is ?Gi(B.(n-1),...,B.0), and has type Ti |
|
365 The B.j are bound vars of binder. |
|
366 The terms are not made in eta-normal-form, SIMPL does that later. |
|
367 If done here, eta-expansion must be recursive in the arguments! *) |
|
368 fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*) |
|
369 | make_args name (binder: typ list, env, Ts) : Envir.env * term list = |
|
370 let fun funtype T = binder--->T; |
|
371 val (env', vars) = Envir.genvars name (env, map funtype Ts) |
|
372 in (env', map (fn var=> combound(var, 0, length binder)) vars) end; |
|
373 |
|
374 |
|
375 (*Abstraction over a list of types, like list_abs*) |
|
376 fun types_abs ([],u) = u |
|
377 | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u)); |
|
378 |
|
379 (*Abstraction over the binder of a type*) |
|
380 fun type_abs (env,T,t) = types_abs(binder_types env T, t); |
|
381 |
|
382 |
|
383 (*MATCH taking "big steps". |
|
384 Copies u into the Var v, using projection on targs or imitation. |
|
385 A projection is allowed unless SIMPL raises an exception. |
|
386 Allocates new variables in projection on a higher-order argument, |
|
387 or if u is a variable (flex-flex dpair). |
|
388 Returns long sequence of every way of copying u, for backtracking |
|
389 For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. |
|
390 The order for trying projections is crucial in ?b'(?a) |
|
391 NB "vname" is only used in the call to make_args!! *) |
|
392 fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) |
|
393 : (term * (Envir.env * dpair list))Sequence.seq = |
|
394 let (*Produce copies of uarg and cons them in front of uargs*) |
|
395 fun copycons uarg (uargs, (env, dpairs)) = |
|
396 Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed')) |
|
397 (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)), |
|
398 (env, dpairs))); |
|
399 (*Produce sequence of all possible ways of copying the arg list*) |
|
400 fun copyargs [] = Sequence.cons( ([],ed), Sequence.null) |
|
401 | copyargs (uarg::uargs) = |
|
402 Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs)); |
|
403 val (uhead,uargs) = strip_comb u; |
|
404 val base = body_type env (fastype env (rbinder,uhead)); |
|
405 fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed'); |
|
406 (*attempt projection on argument with given typ*) |
|
407 val Ts = map (curry (fastype env) rbinder) targs; |
|
408 fun projenv (head, (Us,bary), targ, tail) = |
|
409 let val env = if !trace_types then test_unify_types(base,bary,env) |
|
410 else unify_types(base,bary,env) |
|
411 in Sequence.seqof (fn () => |
|
412 let val (env',args) = make_args vname (Ts,env,Us); |
|
413 (*higher-order projection: plug in targs for bound vars*) |
|
414 fun plugin arg = list_comb(head_of arg, targs); |
|
415 val dp = (rbinder, list_comb(targ, map plugin args), u); |
|
416 val (env2,frigid,fflex) = SIMPL (env', dp::dpairs) |
|
417 (*may raise exception CANTUNIFY*) |
|
418 in Some ((list_comb(head,args), (env2, frigid@fflex)), |
|
419 tail) |
|
420 end handle CANTUNIFY => Sequence.pull tail) |
|
421 end handle CANTUNIFY => tail; |
|
422 (*make a list of projections*) |
|
423 fun make_projs (T::Ts, targ::targs) = |
|
424 (Bound(length Ts), T, targ) :: make_projs (Ts,targs) |
|
425 | make_projs ([],[]) = [] |
|
426 | make_projs _ = raise TERM ("make_projs", u::targs); |
|
427 (*try projections and imitation*) |
|
428 fun matchfun ((bvar,T,targ)::projs) = |
|
429 (projenv(bvar, strip_type env T, targ, matchfun projs)) |
|
430 | matchfun [] = (*imitation last of all*) |
|
431 (case uhead of |
|
432 Const _ => Sequence.maps joinargs (copyargs uargs) |
|
433 | Free _ => Sequence.maps joinargs (copyargs uargs) |
|
434 | _ => Sequence.null) (*if Var, would be a loop!*) |
|
435 in case uhead of |
|
436 Abs(a, T, body) => |
|
437 Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) |
|
438 (mc ((a,T)::rbinder, |
|
439 (map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) |
|
440 | Var (w,uary) => |
|
441 (*a flex-flex dpair: make variable for t*) |
|
442 let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base) |
|
443 val tabs = combound(newhd, 0, length Ts) |
|
444 val tsub = list_comb(newhd,targs) |
|
445 in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) |
|
446 end |
|
447 | _ => matchfun(rev(make_projs(Ts, targs))) |
|
448 end |
|
449 in mc end; |
|
450 |
|
451 |
|
452 (*Call matchcopy to produce assignments to the variable in the dpair*) |
|
453 fun MATCH (env, (rbinder,t,u), dpairs) |
|
454 : (Envir.env * dpair list)Sequence.seq = |
|
455 let val (Var(v,T), targs) = strip_comb t; |
|
456 val Ts = binder_types env T; |
|
457 fun new_dset (u', (env',dpairs')) = |
|
458 (*if v was updated to s, must unify s with u' *) |
|
459 case Envir.lookup(env',v) of |
|
460 None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs') |
|
461 | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs') |
|
462 in Sequence.maps new_dset |
|
463 (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs))) |
|
464 end; |
|
465 |
|
466 |
|
467 |
|
468 (**** Flex-flex processing ****) |
|
469 |
|
470 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
|
471 Attempts to update t with u, raising ASSIGN if impossible*) |
|
472 fun ff_assign(env, rbinder, t, u) : Envir.env = |
|
473 let val (v,T) = get_eta_var(rbinder,0,t) |
|
474 in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN |
|
475 else let val env = unify_types(body_type env T,fastype env (rbinder,u),env) |
|
476 in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end |
|
477 end; |
|
478 |
|
479 |
|
480 (*Flex argument: a term, its type, and the index that refers to it.*) |
|
481 type flarg = {t: term, T: typ, j: int}; |
|
482 |
|
483 |
|
484 (*Form the arguments into records for deletion/sorting.*) |
|
485 fun flexargs ([],[],[]) = [] : flarg list |
|
486 | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts) |
|
487 | flexargs _ = error"flexargs"; |
|
488 |
|
489 |
|
490 (*If an argument contains a banned Bound, then it should be deleted. |
|
491 But if the path is flexible, this is difficult; the code gives up!*) |
|
492 exception CHANGE and CHANGE_FAIL; (*rigid and flexible occurrences*) |
|
493 |
|
494 |
|
495 (*Squash down indices at level >=lev to delete the js from a term. |
|
496 flex should initially be false, since the empty path is rigid.*) |
|
497 fun change_bnos (lev, js, flex) t = |
|
498 let val (head,args) = strip_comb t |
|
499 val flex' = flex orelse is_Var head |
|
500 val head' = case head of |
|
501 Bound i => |
|
502 if i<lev then Bound i |
|
503 else if (i-lev) mem js |
|
504 then if flex then raise CHANGE_FAIL |
|
505 else raise CHANGE |
|
506 else Bound (i - length (filter (fn j => j < i-lev) js)) |
|
507 | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t) |
|
508 | _ => head |
|
509 in list_comb (head', map (change_bnos (lev, js, flex')) args) |
|
510 end; |
|
511 |
|
512 |
|
513 (*Change indices, delete the argument if it contains a banned Bound*) |
|
514 fun change_arg js ({j,t,T}, args) : flarg list = |
|
515 {j=j, t= change_bnos(0,js,false)t, T=T} :: args handle CHANGE => args; |
|
516 |
|
517 |
|
518 (*Sort the arguments to create assignments if possible: |
|
519 create eta-terms like ?g(B.1,B.0) *) |
|
520 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1) |
|
521 | arg_less (_:flarg, _:flarg) = false; |
|
522 |
|
523 (*Test whether the new term would be eta-equivalent to a variable -- |
|
524 if so then there is no point in creating a new variable*) |
|
525 fun decreasing n ([]: flarg list) = (n=0) |
|
526 | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args; |
|
527 |
|
528 (*Delete banned indices in the term, simplifying it. |
|
529 Force an assignment, if possible, by sorting the arguments. |
|
530 Update its head; squash indices in arguments. *) |
|
531 fun clean_term banned (env,t) = |
|
532 let val (Var(v,T), ts) = strip_comb t |
|
533 val (Ts,U) = strip_type env T |
|
534 and js = length ts - 1 downto 0 |
|
535 val args = sort arg_less |
|
536 (foldr (change_arg banned) (flexargs (js,ts,Ts), [])) |
|
537 val ts' = map (#t) args |
|
538 in |
|
539 if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts'))) |
|
540 else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U) |
|
541 val body = list_comb(v', map (Bound o #j) args) |
|
542 val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env')) |
|
543 (*the vupdate affects ts' if they contain v*) |
|
544 in |
|
545 (env2, Envir.norm_term env2 (list_comb(v',ts'))) |
|
546 end |
|
547 end; |
|
548 |
|
549 |
|
550 (*Add tpair if not trivial or already there. |
|
551 Should check for swapped pairs??*) |
|
552 fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list = |
|
553 if t0 aconv u0 then tpairs |
|
554 else |
|
555 let val t = rlist_abs(rbinder, t0) and u = rlist_abs(rbinder, u0); |
|
556 fun same(t',u') = (t aconv t') andalso (u aconv u') |
|
557 in if exists same tpairs then tpairs else (t,u)::tpairs end; |
|
558 |
|
559 |
|
560 (*Simplify both terms and check for assignments. |
|
561 Bound vars in the binder are "banned" unless used in both t AND u *) |
|
562 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = |
|
563 let val loot = loose_bnos t and loou = loose_bnos u |
|
564 fun add_index (((a,T), j), (bnos, newbinder)) = |
|
565 if j mem loot andalso j mem loou |
|
566 then (bnos, (a,T)::newbinder) |
|
567 else (j::bnos, newbinder); |
|
568 val indices = 0 upto (length rbinder - 1); |
|
569 val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[])); |
|
570 val (env', t') = clean_term banned (env, t); |
|
571 val (env'',u') = clean_term banned (env',u) |
|
572 in (ff_assign(env'', rbin', t', u'), tpairs) |
|
573 handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs) |
|
574 handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) |
|
575 end |
|
576 handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs)); |
|
577 |
|
578 |
|
579 (*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs |
|
580 eliminates trivial tpairs like t=t, as well as repeated ones |
|
581 trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t |
|
582 Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) |
|
583 fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) |
|
584 : Envir.env * (term*term)list = |
|
585 let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0 |
|
586 in case (head_of t, head_of u) of |
|
587 (Var(v,T), Var(w,U)) => (*Check for identical variables...*) |
|
588 if v=w then (*...occur check would falsely return true!*) |
|
589 if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) |
|
590 else raise TERM ("add_ffpair: Var name confusion", [t,u]) |
|
591 else if xless(v,w) then (*prefer to update the LARGER variable*) |
|
592 clean_ffpair ((rbinder, u, t), (env,tpairs)) |
|
593 else clean_ffpair ((rbinder, t, u), (env,tpairs)) |
|
594 | _ => raise TERM ("add_ffpair: Vars expected", [t,u]) |
|
595 end; |
|
596 |
|
597 |
|
598 (*Print a tracing message + list of dpairs. |
|
599 In t==u print u first because it may be rigid or flexible -- |
|
600 t is always flexible.*) |
|
601 fun print_dpairs msg (env,dpairs) = |
|
602 let fun pdp (rbinder,t,u) = |
|
603 let fun termT t = Sign.pretty_term (!sgr) |
|
604 (Envir.norm_term env (rlist_abs(rbinder,t))) |
|
605 val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, |
|
606 termT t]; |
|
607 in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end; |
|
608 in writeln msg; seq pdp dpairs end; |
|
609 |
|
610 |
|
611 (*Unify the dpairs in the environment. |
|
612 Returns flex-flex disagreement pairs NOT IN normal form. |
|
613 SIMPL may raise exception CANTUNIFY. *) |
|
614 fun hounifiers (sg,env, tus : (term*term)list) |
|
615 : (Envir.env * (term*term)list)Sequence.seq = |
|
616 let fun add_unify tdepth ((env,dpairs), reseq) = |
|
617 Sequence.seqof (fn()=> |
|
618 let val (env',flexflex,flexrigid) = |
|
619 (if tdepth> !trace_bound andalso !trace_simp |
|
620 then print_dpairs "Enter SIMPL" (env,dpairs) else (); |
|
621 SIMPL (env,dpairs)) |
|
622 in case flexrigid of |
|
623 [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq) |
|
624 | dp::frigid' => |
|
625 if tdepth > !search_bound then |
|
626 (prs"***Unification bound exceeded\n"; Sequence.pull reseq) |
|
627 else |
|
628 (if tdepth > !trace_bound then |
|
629 print_dpairs "Enter MATCH" (env',flexrigid@flexflex) |
|
630 else (); |
|
631 Sequence.pull (Sequence.its_right (add_unify (tdepth+1)) |
|
632 (MATCH (env',dp, frigid'@flexflex), reseq))) |
|
633 end |
|
634 handle CANTUNIFY => |
|
635 (if tdepth > !trace_bound then writeln"Failure node" else (); |
|
636 Sequence.pull reseq)); |
|
637 val dps = map (fn(t,u)=> ([],t,u)) tus |
|
638 in sgr := sg; |
|
639 add_unify 1 ((env,dps), Sequence.null) |
|
640 end; |
|
641 |
|
642 fun unifiers(params) = |
|
643 Sequence.cons((Pattern.unify(params), []), Sequence.null) |
|
644 handle Pattern.Unif => Sequence.null |
|
645 | Pattern.Pattern => hounifiers(params); |
|
646 |
|
647 |
|
648 (*For smash_flexflex1*) |
|
649 fun var_head_of (env,t) : indexname * typ = |
|
650 case head_of (strip_abs_body (Envir.norm_term env t)) of |
|
651 Var(v,T) => (v,T) |
|
652 | _ => raise CANTUNIFY; (*not flexible, cannot use trivial substitution*) |
|
653 |
|
654 |
|
655 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975) |
|
656 Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a |
|
657 Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, |
|
658 though just ?g->?f is a more general unifier. |
|
659 Unlike Huet (1975), does not smash together all variables of same type -- |
|
660 requires more work yet gives a less general unifier (fewer variables). |
|
661 Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) |
|
662 fun smash_flexflex1 ((t,u), env) : Envir.env = |
|
663 let val (v,T) = var_head_of (env,t) |
|
664 and (w,U) = var_head_of (env,u); |
|
665 val (env', var) = Envir.genvar (#1v) (env, body_type env T) |
|
666 val env'' = Envir.vupdate((w, type_abs(env',U,var)), env') |
|
667 in if (v,T)=(w,U) then env'' (*the other update would be identical*) |
|
668 else Envir.vupdate((v, type_abs(env',T,var)), env'') |
|
669 end; |
|
670 |
|
671 |
|
672 (*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*) |
|
673 fun smash_flexflex (env,tpairs) : Envir.env = |
|
674 foldr smash_flexflex1 (tpairs, env); |
|
675 |
|
676 (*Returns unifiers with no remaining disagreement pairs*) |
|
677 fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq = |
|
678 Sequence.maps smash_flexflex (unifiers(sg,env,tus)); |
|
679 |
|
680 end; |