# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1214496726 14400
# Node ID 144d082b47ae2db4a49fc8915599bb11444e6856
# Parent  8b611ecc5f2d47ef32ec9f15e24633d0a2aa8494
Reduce efold

diff -r 8b611ecc5f2d -r 144d082b47ae src/cloconv.sml
--- 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}
diff -r 8b611ecc5f2d -r 144d082b47ae src/elaborate.sml
--- 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),
diff -r 8b611ecc5f2d -r 144d082b47ae src/reduce.sml
--- 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) =>
diff -r 8b611ecc5f2d -r 144d082b47ae tests/efold.lac
--- 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]