175 |
172 |
176 exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) |
173 exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) |
177 exception ASSIGN; (*Raised if not an assignment*) |
174 exception ASSIGN; (*Raised if not an assignment*) |
178 |
175 |
179 |
176 |
180 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) = |
177 fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) = |
181 if T=U then env |
178 if T=U then env |
182 else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T) |
179 else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T) |
183 in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end |
180 in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end |
184 handle Type.TUNIFY => raise CANTUNIFY; |
181 handle Type.TUNIFY => raise CANTUNIFY; |
185 |
182 |
186 fun test_unify_types(args as (T,U,_)) = |
183 fun test_unify_types thy (args as (T,U,_)) = |
187 let val sot = Sign.string_of_typ (thy ()); |
184 let val str_of = Sign.string_of_typ thy; |
188 fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T); |
185 fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T); |
189 val env' = unify_types(args) |
186 val env' = unify_types thy args |
190 in if is_TVar(T) orelse is_TVar(U) then warn() else (); |
187 in if is_TVar(T) orelse is_TVar(U) then warn() else (); |
191 env' |
188 env' |
192 end; |
189 end; |
193 |
190 |
194 (*Is the term eta-convertible to a single variable with the given rbinder? |
191 (*Is the term eta-convertible to a single variable with the given rbinder? |
207 |
204 |
208 |
205 |
209 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u. |
206 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u. |
210 If v occurs rigidly then nonunifiable. |
207 If v occurs rigidly then nonunifiable. |
211 If v occurs nonrigidly then must use full algorithm. *) |
208 If v occurs nonrigidly then must use full algorithm. *) |
212 fun assignment (env, rbinder, t, u) = |
209 fun assignment thy (env, rbinder, t, u) = |
213 let val vT as (v,T) = get_eta_var (rbinder, 0, t) |
210 let val vT as (v,T) = get_eta_var (rbinder, 0, t) |
214 in case rigid_occurs_term (ref [], env, v, u) of |
211 in case rigid_occurs_term (ref [], env, v, u) of |
215 NoOcc => let val env = unify_types(body_type env T, |
212 NoOcc => let val env = unify_types thy (body_type env T, |
216 fastype env (rbinder,u),env) |
213 fastype env (rbinder,u),env) |
217 in Envir.update ((vT, rlist_abs (rbinder, u)), env) end |
214 in Envir.update ((vT, rlist_abs (rbinder, u)), env) end |
218 | Nonrigid => raise ASSIGN |
215 | Nonrigid => raise ASSIGN |
219 | Rigid => raise CANTUNIFY |
216 | Rigid => raise CANTUNIFY |
220 end; |
217 end; |
223 (*Extends an rbinder with a new disagreement pair, if both are abstractions. |
220 (*Extends an rbinder with a new disagreement pair, if both are abstractions. |
224 Tries to unify types of the bound variables! |
221 Tries to unify types of the bound variables! |
225 Checks that binders have same length, since terms should be eta-normal; |
222 Checks that binders have same length, since terms should be eta-normal; |
226 if not, raises TERM, probably indicating type mismatch. |
223 if not, raises TERM, probably indicating type mismatch. |
227 Uses variable a (unless the null string) to preserve user's naming.*) |
224 Uses variable a (unless the null string) to preserve user's naming.*) |
228 fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = |
225 fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = |
229 let val env' = unify_types(T,U,env) |
226 let val env' = unify_types thy (T,U,env) |
230 val c = if a="" then b else a |
227 val c = if a="" then b else a |
231 in new_dpair((c,T) :: rbinder, body1, body2, env') end |
228 in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end |
232 | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", []) |
229 | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", []) |
233 | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", []) |
230 | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", []) |
234 | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); |
231 | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); |
235 |
232 |
236 |
233 |
237 fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env = |
234 fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env = |
238 new_dpair (rbinder, |
235 new_dpair thy (rbinder, |
239 eta_norm env (rbinder, Envir.head_norm env t), |
236 eta_norm env (rbinder, Envir.head_norm env t), |
240 eta_norm env (rbinder, Envir.head_norm env u), env); |
237 eta_norm env (rbinder, Envir.head_norm env u), env); |
241 |
238 |
242 |
239 |
243 |
240 |
245 Does not perform assignments for flex-flex pairs: |
242 Does not perform assignments for flex-flex pairs: |
246 may create nonrigid paths, which prevent other assignments. |
243 may create nonrigid paths, which prevent other assignments. |
247 Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to |
244 Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to |
248 do so caused numerous problems with no compensating advantage. |
245 do so caused numerous problems with no compensating advantage. |
249 *) |
246 *) |
250 fun SIMPL0 (dp0, (env,flexflex,flexrigid)) |
247 fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) |
251 : Envir.env * dpair list * dpair list = |
248 : Envir.env * dpair list * dpair list = |
252 let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0); |
249 let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0); |
253 fun SIMRANDS(f$t, g$u, env) = |
250 fun SIMRANDS(f$t, g$u, env) = |
254 SIMPL0((rbinder,t,u), SIMRANDS(f,g,env)) |
251 SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env)) |
255 | SIMRANDS (t as _$_, _, _) = |
252 | SIMRANDS (t as _$_, _, _) = |
256 raise TERM ("SIMPL: operands mismatch", [t,u]) |
253 raise TERM ("SIMPL: operands mismatch", [t,u]) |
257 | SIMRANDS (t, u as _$_, _) = |
254 | SIMRANDS (t, u as _$_, _) = |
258 raise TERM ("SIMPL: operands mismatch", [t,u]) |
255 raise TERM ("SIMPL: operands mismatch", [t,u]) |
259 | SIMRANDS(_,_,env) = (env,flexflex,flexrigid); |
256 | SIMRANDS(_,_,env) = (env,flexflex,flexrigid); |
260 in case (head_of t, head_of u) of |
257 in case (head_of t, head_of u) of |
261 (Var(_,T), Var(_,U)) => |
258 (Var(_,T), Var(_,U)) => |
262 let val T' = body_type env T and U' = body_type env U; |
259 let val T' = body_type env T and U' = body_type env U; |
263 val env = unify_types(T',U',env) |
260 val env = unify_types thy (T',U',env) |
264 in (env, dp::flexflex, flexrigid) end |
261 in (env, dp::flexflex, flexrigid) end |
265 | (Var _, _) => |
262 | (Var _, _) => |
266 ((assignment (env,rbinder,t,u), flexflex, flexrigid) |
263 ((assignment thy (env,rbinder,t,u), flexflex, flexrigid) |
267 handle ASSIGN => (env, flexflex, dp::flexrigid)) |
264 handle ASSIGN => (env, flexflex, dp::flexrigid)) |
268 | (_, Var _) => |
265 | (_, Var _) => |
269 ((assignment (env,rbinder,u,t), flexflex, flexrigid) |
266 ((assignment thy (env,rbinder,u,t), flexflex, flexrigid) |
270 handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) |
267 handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) |
271 | (Const(a,T), Const(b,U)) => |
268 | (Const(a,T), Const(b,U)) => |
272 if a=b then SIMRANDS(t,u, unify_types(T,U,env)) |
269 if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) |
273 else raise CANTUNIFY |
270 else raise CANTUNIFY |
274 | (Bound i, Bound j) => |
271 | (Bound i, Bound j) => |
275 if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY |
272 if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY |
276 | (Free(a,T), Free(b,U)) => |
273 | (Free(a,T), Free(b,U)) => |
277 if a=b then SIMRANDS(t,u, unify_types(T,U,env)) |
274 if a=b then SIMRANDS(t,u, unify_types thy (T,U,env)) |
278 else raise CANTUNIFY |
275 else raise CANTUNIFY |
279 | _ => raise CANTUNIFY |
276 | _ => raise CANTUNIFY |
280 end; |
277 end; |
281 |
278 |
282 |
279 |
287 | changed _ = false; |
284 | changed _ = false; |
288 |
285 |
289 |
286 |
290 (*Recursion needed if any of the 'head variables' have been updated |
287 (*Recursion needed if any of the 'head variables' have been updated |
291 Clever would be to re-do just the affected dpairs*) |
288 Clever would be to re-do just the affected dpairs*) |
292 fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list = |
289 fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = |
293 let val all as (env',flexflex,flexrigid) = |
290 let val all as (env',flexflex,flexrigid) = |
294 foldr SIMPL0 (env,[],[]) dpairs; |
291 foldr (SIMPL0 thy) (env,[],[]) dpairs; |
295 val dps = flexrigid@flexflex |
292 val dps = flexrigid@flexflex |
296 in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps |
293 in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps |
297 then SIMPL(env',dps) else all |
294 then SIMPL thy (env',dps) else all |
298 end; |
295 end; |
299 |
296 |
300 |
297 |
301 (*computes t(Bound(n+k-1),...,Bound(n)) *) |
298 (*computes t(Bound(n+k-1),...,Bound(n)) *) |
302 fun combound (t, n, k) = |
299 fun combound (t, n, k) = |
330 or if u is a variable (flex-flex dpair). |
327 or if u is a variable (flex-flex dpair). |
331 Returns long sequence of every way of copying u, for backtracking |
328 Returns long sequence of every way of copying u, for backtracking |
332 For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. |
329 For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. |
333 The order for trying projections is crucial in ?b'(?a) |
330 The order for trying projections is crucial in ?b'(?a) |
334 NB "vname" is only used in the call to make_args!! *) |
331 NB "vname" is only used in the call to make_args!! *) |
335 fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) |
332 fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) |
336 : (term * (Envir.env * dpair list))Seq.seq = |
333 : (term * (Envir.env * dpair list))Seq.seq = |
337 let (*Produce copies of uarg and cons them in front of uargs*) |
334 let (*Produce copies of uarg and cons them in front of uargs*) |
338 fun copycons uarg (uargs, (env, dpairs)) = |
335 fun copycons uarg (uargs, (env, dpairs)) = |
339 Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) |
336 Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) |
340 (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), |
337 (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), |
347 val base = body_type env (fastype env (rbinder,uhead)); |
344 val base = body_type env (fastype env (rbinder,uhead)); |
348 fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed'); |
345 fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed'); |
349 (*attempt projection on argument with given typ*) |
346 (*attempt projection on argument with given typ*) |
350 val Ts = map (curry (fastype env) rbinder) targs; |
347 val Ts = map (curry (fastype env) rbinder) targs; |
351 fun projenv (head, (Us,bary), targ, tail) = |
348 fun projenv (head, (Us,bary), targ, tail) = |
352 let val env = if !trace_types then test_unify_types(base,bary,env) |
349 let val env = if !trace_types then test_unify_types thy (base,bary,env) |
353 else unify_types(base,bary,env) |
350 else unify_types thy (base,bary,env) |
354 in Seq.make (fn () => |
351 in Seq.make (fn () => |
355 let val (env',args) = make_args vname (Ts,env,Us); |
352 let val (env',args) = make_args vname (Ts,env,Us); |
356 (*higher-order projection: plug in targs for bound vars*) |
353 (*higher-order projection: plug in targs for bound vars*) |
357 fun plugin arg = list_comb(head_of arg, targs); |
354 fun plugin arg = list_comb(head_of arg, targs); |
358 val dp = (rbinder, list_comb(targ, map plugin args), u); |
355 val dp = (rbinder, list_comb(targ, map plugin args), u); |
359 val (env2,frigid,fflex) = SIMPL (env', dp::dpairs) |
356 val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs) |
360 (*may raise exception CANTUNIFY*) |
357 (*may raise exception CANTUNIFY*) |
361 in SOME ((list_comb(head,args), (env2, frigid@fflex)), |
358 in SOME ((list_comb(head,args), (env2, frigid@fflex)), |
362 tail) |
359 tail) |
363 end handle CANTUNIFY => Seq.pull tail) |
360 end handle CANTUNIFY => Seq.pull tail) |
364 end handle CANTUNIFY => tail; |
361 end handle CANTUNIFY => tail; |
391 end |
388 end |
392 in mc end; |
389 in mc end; |
393 |
390 |
394 |
391 |
395 (*Call matchcopy to produce assignments to the variable in the dpair*) |
392 (*Call matchcopy to produce assignments to the variable in the dpair*) |
396 fun MATCH (env, (rbinder,t,u), dpairs) |
393 fun MATCH thy (env, (rbinder,t,u), dpairs) |
397 : (Envir.env * dpair list)Seq.seq = |
394 : (Envir.env * dpair list)Seq.seq = |
398 let val (Var (vT as (v, T)), targs) = strip_comb t; |
395 let val (Var (vT as (v, T)), targs) = strip_comb t; |
399 val Ts = binder_types env T; |
396 val Ts = binder_types env T; |
400 fun new_dset (u', (env',dpairs')) = |
397 fun new_dset (u', (env',dpairs')) = |
401 (*if v was updated to s, must unify s with u' *) |
398 (*if v was updated to s, must unify s with u' *) |
402 case Envir.lookup (env', vT) of |
399 case Envir.lookup (env', vT) of |
403 NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') |
400 NONE => (Envir.update ((vT, types_abs(Ts, u')), env'), dpairs') |
404 | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') |
401 | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs') |
405 in Seq.map new_dset |
402 in Seq.map new_dset |
406 (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs))) |
403 (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs))) |
407 end; |
404 end; |
408 |
405 |
409 |
406 |
410 |
407 |
411 (**** Flex-flex processing ****) |
408 (**** Flex-flex processing ****) |
412 |
409 |
413 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
410 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
414 Attempts to update t with u, raising ASSIGN if impossible*) |
411 Attempts to update t with u, raising ASSIGN if impossible*) |
415 fun ff_assign(env, rbinder, t, u) : Envir.env = |
412 fun ff_assign thy (env, rbinder, t, u) : Envir.env = |
416 let val vT as (v,T) = get_eta_var(rbinder,0,t) |
413 let val vT as (v,T) = get_eta_var(rbinder,0,t) |
417 in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN |
414 in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN |
418 else let val env = unify_types(body_type env T, |
415 else let val env = unify_types thy (body_type env T, |
419 fastype env (rbinder,u), |
416 fastype env (rbinder,u), |
420 env) |
417 env) |
421 in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end |
418 in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end |
422 end; |
419 end; |
423 |
420 |
512 in if exists same tpairs then tpairs else (t,u)::tpairs end; |
509 in if exists same tpairs then tpairs else (t,u)::tpairs end; |
513 |
510 |
514 |
511 |
515 (*Simplify both terms and check for assignments. |
512 (*Simplify both terms and check for assignments. |
516 Bound vars in the binder are "banned" unless used in both t AND u *) |
513 Bound vars in the binder are "banned" unless used in both t AND u *) |
517 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = |
514 fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = |
518 let val loot = loose_bnos t and loou = loose_bnos u |
515 let val loot = loose_bnos t and loou = loose_bnos u |
519 fun add_index (((a,T), j), (bnos, newbinder)) = |
516 fun add_index (((a,T), j), (bnos, newbinder)) = |
520 if j mem_int loot andalso j mem_int loou |
517 if j mem_int loot andalso j mem_int loou |
521 then (bnos, (a,T)::newbinder) (*needed by both: keep*) |
518 then (bnos, (a,T)::newbinder) (*needed by both: keep*) |
522 else (j::bnos, newbinder); (*remove*) |
519 else (j::bnos, newbinder); (*remove*) |
523 val indices = 0 upto (length rbinder - 1); |
520 val indices = 0 upto (length rbinder - 1); |
524 val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices); |
521 val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices); |
525 val (env', t') = clean_term banned (env, t); |
522 val (env', t') = clean_term banned (env, t); |
526 val (env'',u') = clean_term banned (env',u) |
523 val (env'',u') = clean_term banned (env',u) |
527 in (ff_assign(env'', rbin', t', u'), tpairs) |
524 in (ff_assign thy (env'', rbin', t', u'), tpairs) |
528 handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs) |
525 handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs) |
529 handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) |
526 handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) |
530 end |
527 end |
531 handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs)); |
528 handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs)); |
532 |
529 |
533 |
530 |
534 (*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs |
531 (*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs |
535 eliminates trivial tpairs like t=t, as well as repeated ones |
532 eliminates trivial tpairs like t=t, as well as repeated ones |
536 trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t |
533 trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t |
537 Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) |
534 Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) |
538 fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) |
535 fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) |
539 : Envir.env * (term*term)list = |
536 : Envir.env * (term*term)list = |
540 let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0 |
537 let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0 |
541 in case (head_of t, head_of u) of |
538 in case (head_of t, head_of u) of |
542 (Var(v,T), Var(w,U)) => (*Check for identical variables...*) |
539 (Var(v,T), Var(w,U)) => (*Check for identical variables...*) |
543 if eq_ix(v,w) then (*...occur check would falsely return true!*) |
540 if eq_ix(v,w) then (*...occur check would falsely return true!*) |
544 if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) |
541 if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) |
545 else raise TERM ("add_ffpair: Var name confusion", [t,u]) |
542 else raise TERM ("add_ffpair: Var name confusion", [t,u]) |
546 else if xless(v,w) then (*prefer to update the LARGER variable*) |
543 else if xless(v,w) then (*prefer to update the LARGER variable*) |
547 clean_ffpair ((rbinder, u, t), (env,tpairs)) |
544 clean_ffpair thy ((rbinder, u, t), (env,tpairs)) |
548 else clean_ffpair ((rbinder, t, u), (env,tpairs)) |
545 else clean_ffpair thy ((rbinder, t, u), (env,tpairs)) |
549 | _ => raise TERM ("add_ffpair: Vars expected", [t,u]) |
546 | _ => raise TERM ("add_ffpair: Vars expected", [t,u]) |
550 end; |
547 end; |
551 |
548 |
552 |
549 |
553 (*Print a tracing message + list of dpairs. |
550 (*Print a tracing message + list of dpairs. |
554 In t==u print u first because it may be rigid or flexible -- |
551 In t==u print u first because it may be rigid or flexible -- |
555 t is always flexible.*) |
552 t is always flexible.*) |
556 fun print_dpairs msg (env,dpairs) = |
553 fun print_dpairs thy msg (env,dpairs) = |
557 let fun pdp (rbinder,t,u) = |
554 let fun pdp (rbinder,t,u) = |
558 let fun termT t = Sign.pretty_term (thy ()) |
555 let fun termT t = Sign.pretty_term thy |
559 (Envir.norm_term env (rlist_abs(rbinder,t))) |
556 (Envir.norm_term env (rlist_abs(rbinder,t))) |
560 val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, |
557 val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, |
561 termT t]; |
558 termT t]; |
562 in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end; |
559 in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end; |
563 in tracing msg; List.app pdp dpairs end; |
560 in tracing msg; List.app pdp dpairs end; |
570 : (Envir.env * (term*term)list)Seq.seq = |
567 : (Envir.env * (term*term)list)Seq.seq = |
571 let fun add_unify tdepth ((env,dpairs), reseq) = |
568 let fun add_unify tdepth ((env,dpairs), reseq) = |
572 Seq.make (fn()=> |
569 Seq.make (fn()=> |
573 let val (env',flexflex,flexrigid) = |
570 let val (env',flexflex,flexrigid) = |
574 (if tdepth> !trace_bound andalso !trace_simp |
571 (if tdepth> !trace_bound andalso !trace_simp |
575 then print_dpairs "Enter SIMPL" (env,dpairs) else (); |
572 then print_dpairs thy "Enter SIMPL" (env,dpairs) else (); |
576 SIMPL (env,dpairs)) |
573 SIMPL thy (env,dpairs)) |
577 in case flexrigid of |
574 in case flexrigid of |
578 [] => SOME (foldr add_ffpair (env',[]) flexflex, reseq) |
575 [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq) |
579 | dp::frigid' => |
576 | dp::frigid' => |
580 if tdepth > !search_bound then |
577 if tdepth > !search_bound then |
581 (warning "Unification bound exceeded"; Seq.pull reseq) |
578 (warning "Unification bound exceeded"; Seq.pull reseq) |
582 else |
579 else |
583 (if tdepth > !trace_bound then |
580 (if tdepth > !trace_bound then |
584 print_dpairs "Enter MATCH" (env',flexrigid@flexflex) |
581 print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) |
585 else (); |
582 else (); |
586 Seq.pull (Seq.it_right (add_unify (tdepth+1)) |
583 Seq.pull (Seq.it_right (add_unify (tdepth+1)) |
587 (MATCH (env',dp, frigid'@flexflex), reseq))) |
584 (MATCH thy (env',dp, frigid'@flexflex), reseq))) |
588 end |
585 end |
589 handle CANTUNIFY => |
586 handle CANTUNIFY => |
590 (if tdepth > !trace_bound then tracing"Failure node" else (); |
587 (if tdepth > !trace_bound then tracing"Failure node" else (); |
591 Seq.pull reseq)); |
588 Seq.pull reseq)); |
592 val dps = map (fn(t,u)=> ([],t,u)) tus |
589 val dps = map (fn(t,u)=> ([],t,u)) tus |
593 val _ = thy_ref := SOME thy; |
|
594 in add_unify 1 ((env, dps), Seq.empty) end; |
590 in add_unify 1 ((env, dps), Seq.empty) end; |
595 |
591 |
596 fun unifiers params = |
592 fun unifiers params = |
597 Seq.cons ((Pattern.unify params, []), Seq.empty) |
593 Seq.cons ((Pattern.unify params, []), Seq.empty) |
598 handle Pattern.Unif => Seq.empty |
594 handle Pattern.Unif => Seq.empty |