477 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
477 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
478 Attempts to update t with u, raising ASSIGN if impossible*) |
478 Attempts to update t with u, raising ASSIGN if impossible*) |
479 fun ff_assign(env, rbinder, t, u) : Envir.env = |
479 fun ff_assign(env, rbinder, t, u) : Envir.env = |
480 let val (v,T) = get_eta_var(rbinder,0,t) |
480 let val (v,T) = get_eta_var(rbinder,0,t) |
481 in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN |
481 in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN |
482 else let val env = unify_types(body_type env T,fastype env (rbinder,u),env) |
482 else let val env = unify_types(body_type env T, |
|
483 fastype env (rbinder,u), |
|
484 env) |
483 in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end |
485 in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end |
484 end; |
486 end; |
485 |
487 |
486 |
488 |
487 (*Flex argument: a term, its type, and the index that refers to it.*) |
489 (*Flex argument: a term, its type, and the index that refers to it.*) |
493 | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts) |
495 | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts) |
494 | flexargs _ = error"flexargs"; |
496 | flexargs _ = error"flexargs"; |
495 |
497 |
496 |
498 |
497 (*If an argument contains a banned Bound, then it should be deleted. |
499 (*If an argument contains a banned Bound, then it should be deleted. |
498 But if the path is flexible, this is difficult; the code gives up!*) |
500 But if the only path is flexible, this is difficult; the code gives up! |
499 exception CHANGE and CHANGE_FAIL; (*rigid and flexible occurrences*) |
501 In %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *) |
500 |
502 exception CHANGE_FAIL; (*flexible occurrence of banned variable*) |
501 |
503 |
502 (*Squash down indices at level >=lev to delete the js from a term. |
504 |
503 flex should initially be false, since the empty path is rigid.*) |
505 (*Check whether the 'banned' bound var indices occur rigidly in t*) |
504 fun change_bnos (lev, js, flex) t = |
506 fun rigid_bound (lev, banned) t = |
505 let val (head,args) = strip_comb t |
507 let val (head,args) = strip_comb t |
506 val flex' = flex orelse is_Var head |
508 in |
507 val head' = case head of |
509 case head of |
508 Bound i => |
510 Bound i => (i-lev) mem banned orelse |
509 if i<lev then Bound i |
511 exists (rigid_bound (lev, banned)) args |
510 else if (i-lev) mem js |
512 | Var _ => false (*no rigid occurrences here!*) |
511 then if flex then raise CHANGE_FAIL |
513 | Abs (_,_,u) => |
512 else raise CHANGE |
514 rigid_bound(lev+1, banned) u orelse |
513 else Bound (i - length (filter (fn j => j < i-lev) js)) |
515 exists (rigid_bound (lev, banned)) args |
514 | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t) |
516 | _ => exists (rigid_bound (lev, banned)) args |
515 | _ => head |
|
516 in list_comb (head', map (change_bnos (lev, js, flex')) args) |
|
517 end; |
517 end; |
518 |
518 |
|
519 (*Squash down indices at level >=lev to delete the banned from a term.*) |
|
520 fun change_bnos banned = |
|
521 let fun change lev (Bound i) = |
|
522 if i<lev then Bound i |
|
523 else if (i-lev) mem banned |
|
524 then raise CHANGE_FAIL (**flexible occurrence: give up**) |
|
525 else Bound (i - length (filter (fn j => j < i-lev) banned)) |
|
526 | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) |
|
527 | change lev (t$u) = change lev t $ change lev u |
|
528 | change lev t = t |
|
529 in change 0 end; |
519 |
530 |
520 (*Change indices, delete the argument if it contains a banned Bound*) |
531 (*Change indices, delete the argument if it contains a banned Bound*) |
521 fun change_arg js ({j,t,T}, args) : flarg list = |
532 fun change_arg banned ({j,t,T}, args) : flarg list = |
522 {j=j, t= change_bnos(0,js,false)t, T=T} :: args handle CHANGE => args; |
533 if rigid_bound (0, banned) t then args (*delete argument!*) |
|
534 else {j=j, t= change_bnos banned t, T=T} :: args; |
523 |
535 |
524 |
536 |
525 (*Sort the arguments to create assignments if possible: |
537 (*Sort the arguments to create assignments if possible: |
526 create eta-terms like ?g(B.1,B.0) *) |
538 create eta-terms like ?g(B.1,B.0) *) |
527 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1) |
539 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1) |
568 Bound vars in the binder are "banned" unless used in both t AND u *) |
580 Bound vars in the binder are "banned" unless used in both t AND u *) |
569 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = |
581 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = |
570 let val loot = loose_bnos t and loou = loose_bnos u |
582 let val loot = loose_bnos t and loou = loose_bnos u |
571 fun add_index (((a,T), j), (bnos, newbinder)) = |
583 fun add_index (((a,T), j), (bnos, newbinder)) = |
572 if j mem loot andalso j mem loou |
584 if j mem loot andalso j mem loou |
573 then (bnos, (a,T)::newbinder) |
585 then (bnos, (a,T)::newbinder) (*needed by both: keep*) |
574 else (j::bnos, newbinder); |
586 else (j::bnos, newbinder); (*remove*) |
575 val indices = 0 upto (length rbinder - 1); |
587 val indices = 0 upto (length rbinder - 1); |
576 val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[])); |
588 val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[])); |
577 val (env', t') = clean_term banned (env, t); |
589 val (env', t') = clean_term banned (env, t); |
578 val (env'',u') = clean_term banned (env',u) |
590 val (env'',u') = clean_term banned (env',u) |
579 in (ff_assign(env'', rbin', t', u'), tpairs) |
591 in (ff_assign(env'', rbin', t', u'), tpairs) |