Mercurial > urweb
changeset 74:144d082b47ae
Reduce efold
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 26 Jun 2008 12:12:06 -0400 |
| parents | 8b611ecc5f2d |
| children | 88ffb3d61817 |
| files | src/cloconv.sml src/elaborate.sml src/reduce.sml tests/efold.lac |
| diffstat | 4 files changed, 46 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cloconv.sml Thu Jun 26 11:32:29 2008 -0400 +++ b/src/cloconv.sml Thu Jun 26 12:12:06 2008 -0400 @@ -55,10 +55,10 @@ exp = fn (xn, rep) => fn e => case e of L'.ERel xn' => - if xn = xn' then - #1 rep - else - e + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => L'.ERel (xn' - 1) + | _ => e) | _ => e, bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) | (ctx, _) => ctx}
--- a/src/elaborate.sml Thu Jun 26 11:32:29 2008 -0400 +++ b/src/elaborate.sml Thu Jun 26 12:12:06 2008 -0400 @@ -420,10 +420,10 @@ con = fn (xn, rep) => fn c => case c of L'.CRel xn' => - if xn = xn' then - #1 rep - else - c + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => L'.CRel (xn' - 1) + | LESS => c) (*| L'.CUnif _ => raise SynUnif*) | _ => c, bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) @@ -650,9 +650,18 @@ | L'.CApp (c1, c2) => (case #1 (hnormCon env c1) of - L'.CAbs (_, _, cb) => - ((hnormCon env (subConInCon (0, c2) cb)) - handle SynUnif => cAll) + L'.CAbs (x, k, cb) => + let + val sc = (hnormCon env (subConInCon (0, c2) cb)) + handle SynUnif => cAll + (*val env' = E.pushCRel env x k*) + in + (*eprefaces "Subst" [("x", Print.PD.string x), + ("cb", p_con env' cb), + ("c2", p_con env c2), + ("sc", p_con env sc)];*) + sc + end | L'.CApp (c', i) => (case #1 (hnormCon env c') of L'.CApp (c', f) => @@ -668,7 +677,12 @@ | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') => let val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc) + + (*val ccc = (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), + (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), + rest''), loc)), loc)*) in + (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) hnormCon env (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
--- a/src/reduce.sml Thu Jun 26 11:32:29 2008 -0400 +++ b/src/reduce.sml Thu Jun 26 12:12:06 2008 -0400 @@ -41,10 +41,10 @@ con = fn (xn, rep) => fn c => case c of CRel xn' => - if xn = xn' then - #1 rep - else - c + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => CRel (xn' - 1) + | LESS => c) | _ => c, bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} @@ -69,10 +69,10 @@ exp = fn (xn, rep) => fn e => case e of ERel xn' => - if xn = xn' then - #1 rep - else - e + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER=> ERel (xn' - 1) + | LESS => e) | _ => e, bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) | (ctx, _) => ctx} @@ -96,10 +96,10 @@ con = fn (xn, rep) => fn c => case c of CRel xn' => - if xn = xn' then - #1 rep - else - c + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => CRel (xn' - 1) + | LESS => c) | _ => c, exp = fn _ => fn e => e, bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) @@ -146,6 +146,14 @@ (_, _, SOME e') => #1 e' | _ => e) + | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) => + (case xcs of + [] => #1 i + | (n, v) :: rest => + #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc), + (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc), + (CRecord (k, rest), loc)), loc)), loc))) + | EApp ((EAbs (_, _, _, e1), loc), e2) => #1 (reduceExp env (subExpInExp (0, e2) e1)) | ECApp ((ECAbs (_, _, e1), loc), c) =>
--- a/tests/efold.lac Thu Jun 26 11:32:29 2008 -0400 +++ b/tests/efold.lac Thu Jun 26 12:12:06 2008 -0400 @@ -1,5 +1,5 @@ val currier : rs :: {Type} -> Cfold.currier rs = - fold [Cfold.currier] (fn nm :: Name => fn t :: Type => fn rest :: {Type} => fn acc => fn x => acc) {} + fold [Cfold.currier] (fn nm :: Name => fn t :: Type => fn rest :: {Type} => fn acc => fn x : t => acc) {} val greenCurry : Cfold.greenCurry = currier [Cfold.greenCurryIngredients] val redCurry : Cfold.redCurry = currier [Cfold.redCurryIngredients]