equal
deleted
inserted
replaced
527 let |
527 let |
528 val n = length args; |
528 val n = length args; |
529 fun subst' lev (Bound i) = |
529 fun subst' lev (Bound i) = |
530 (if i<lev then raise Same.SAME (*var is locally bound*) |
530 (if i<lev then raise Same.SAME (*var is locally bound*) |
531 else incr_boundvars lev (nth args (i-lev)) |
531 else incr_boundvars lev (nth args (i-lev)) |
532 handle Subscript => Bound (i-n)) (*loose: change it*) |
532 handle General.Subscript => Bound (i-n)) (*loose: change it*) |
533 | subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body) |
533 | subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body) |
534 | subst' lev (f $ t) = (subst' lev f $ substh' lev t |
534 | subst' lev (f $ t) = (subst' lev f $ substh' lev t |
535 handle Same.SAME => f $ subst' lev t) |
535 handle Same.SAME => f $ subst' lev t) |
536 | subst' _ _ = raise Same.SAME |
536 | subst' _ _ = raise Same.SAME |
537 and substh' lev t = (subst' lev t handle Same.SAME => t); |
537 and substh' lev t = (subst' lev t handle Same.SAME => t); |
552 let |
552 let |
553 val n = length args; |
553 val n = length args; |
554 fun subst (PBound i) Plev tlev = |
554 fun subst (PBound i) Plev tlev = |
555 (if i < Plev then raise Same.SAME (*var is locally bound*) |
555 (if i < Plev then raise Same.SAME (*var is locally bound*) |
556 else incr_pboundvars Plev tlev (nth args (i-Plev)) |
556 else incr_pboundvars Plev tlev (nth args (i-Plev)) |
557 handle Subscript => PBound (i-n) (*loose: change it*)) |
557 handle General.Subscript => PBound (i-n) (*loose: change it*)) |
558 | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev) |
558 | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev) |
559 | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1)) |
559 | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1)) |
560 | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev |
560 | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev |
561 handle Same.SAME => prf %% subst prf' Plev tlev) |
561 handle Same.SAME => prf %% subst prf' Plev tlev) |
562 | subst (prf % t) Plev tlev = subst prf Plev tlev % t |
562 | subst (prf % t) Plev tlev = subst prf Plev tlev % t |