diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-06-26 12:12:06 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-06-26 12:12:06 -0400 |
| commit | aedc1a079416569be9bf63de2d7c1d9d2262b915 (patch) | |
| tree | 55f3106e3992dbc280f17afdf37dff476a8a7a64 /src | |
| parent | 140f5079a41a0aae9ad3e577c96b443eb5337ca5 (diff) | |
Reduce efold
Diffstat (limited to 'src')
| -rw-r--r-- | src/cloconv.sml | 8 | ||||
| -rw-r--r-- | src/elaborate.sml | 28 | ||||
| -rw-r--r-- | src/reduce.sml | 32 |
3 files changed, 45 insertions, 23 deletions
diff --git a/src/cloconv.sml b/src/cloconv.sml index 8e962f17..b403b659 100644 --- a/src/cloconv.sml +++ b/src/cloconv.sml @@ -55,10 +55,10 @@ val subExpInExp = 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} diff --git a/src/elaborate.sml b/src/elaborate.sml index e31bf908..e656d156 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -420,10 +420,10 @@ val subConInCon = 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 @@ and hnormCon env (cAll as (c, loc)) = | 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 @@ and hnormCon env (cAll as (c, loc)) = | 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), diff --git a/src/reduce.sml b/src/reduce.sml index 887bc0e2..967eb790 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -41,10 +41,10 @@ val subConInCon = 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 @@ val subExpInExp = 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 @@ val subConInExp = 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 @@ fun exp env e = (_, _, 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) => |