Fix nasty de Bruijn substitution bug; TcSum demo

3 files changed, 86 insertions, 63 deletions

diff --git a/src/core_env.sml b/src/core_env.sml
index a4b48b8d..b399f62f 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -82,13 +82,13 @@ val liftConInExp =
 val subConInExp =
     U.Exp.mapB {kind = fn k => k,
                 con = fn (xn, rep) => fn c =>
-                                  case c of
-                                      CRel xn' =>
-                                      (case Int.compare (xn', xn) of
-                                           EQUAL => #1 rep
-                                         | GREATER => CRel (xn' - 1)
-                                         | LESS => c)
-                                    | _ => c,
+                                         case c of
+                                             CRel xn' =>
+                                             (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)
                         | (ctx, _) => ctx}
diff --git a/src/monoize.sml b/src/monoize.sml
index cacf3d6d..6a12306b 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -104,7 +104,8 @@ fun monoType env =
                     let
                         val t = mt env dtmap t
                     in
-                        (L'.TRecord [("Neg", (L'.TFun (t, t), loc)),
+                        (L'.TRecord [("Zero", t),
+                                     ("Neg", (L'.TFun (t, t), loc)),
                                      ("Plus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                                      ("Minus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                                      ("Times", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
@@ -491,14 +492,16 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
              (dummyExp, fm))
 
         fun numTy t =
-            (L'.TRecord [("Neg", (L'.TFun (t, t), loc)),
+            (L'.TRecord [("Zero", t),
+                         ("Neg", (L'.TFun (t, t), loc)),
                          ("Plus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                          ("Minus", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                          ("Times", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                          ("Div", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                          ("Mod", (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc)
-        fun numEx (t, neg, plus, minus, times, dv, md) =
-            ((L'.ERecord [("Neg", neg, (L'.TFun (t, t), loc)),
+        fun numEx (t, zero, neg, plus, minus, times, dv, md) =
+            ((L'.ERecord [("Zero", (L'.EPrim zero, loc), t),
+                          ("Neg", neg, (L'.TFun (t, t), loc)),
                           ("Plus", plus, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                           ("Minus", minus, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
                           ("Times", times, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)),
@@ -595,6 +598,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                  (L'.EBinop ("!strcmp", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
              fm)
 
+          | L.ECApp ((L.EFfi ("Basis", "zero"), _), t) =>
+            let
+                val t = monoType env t
+            in
+                ((L'.EAbs ("r", numTy t, t,
+                           (L'.EField ((L'.ERel 0, loc), "Zero"), loc)), loc), fm)
+            end
           | L.ECApp ((L.EFfi ("Basis", "neg"), _), t) =>
             let
                 val t = monoType env t
@@ -647,6 +657,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                         (L'.EBinop (s, (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc)
             in
                 numEx ((L'.TFfi ("Basis", "int"), loc),
+                       Prim.Int (Int64.fromInt 0),
                        (L'.EAbs ("x", (L'.TFfi ("Basis", "int"), loc),
                                  (L'.TFfi ("Basis", "int"), loc),
                                  (L'.EUnop ("-", (L'.ERel 0, loc)), loc)), loc),
@@ -666,6 +677,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                         (L'.EBinop (s, (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc)
             in
                 numEx ((L'.TFfi ("Basis", "float"), loc),
+                       Prim.Float 0.0,
                        (L'.EAbs ("x", (L'.TFfi ("Basis", "float"), loc),
                                  (L'.TFfi ("Basis", "float"), loc),
                                  (L'.EUnop ("-", (L'.ERel 0, loc)), loc)), loc),
diff --git a/src/reduce.sml b/src/reduce.sml
index 0250175f..927c8ff1 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -36,6 +36,7 @@ structure U = CoreUtil
 
 val liftConInCon = E.liftConInCon
 val subConInCon = E.subConInCon
+val liftConInExp = E.liftConInExp
 
 val liftExpInExp =
     U.Exp.mapB {kind = fn k => k,
@@ -63,6 +64,7 @@ val subExpInExp =
                                          | LESS => e)
                                     | _ => e,
                 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+                        | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
                         | (ctx, _) => ctx}
 
 val liftConInExp = E.liftConInExp
@@ -106,58 +108,67 @@ fun con env c =
 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
 
 fun exp env e =
-    case e of
-        ENamed n =>
-        (case E.lookupENamed env n of
-             (_, _, 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) =>
-        #1 (reduceExp env (subConInExp (0, c) e1))
-
-      | EField ((ERecord xes, _), (CName x, _), _) =>
-        (case List.find (fn ((CName x', _), _, _) => x' = x
-                          | _ => false) xes of
-             SOME (_, e, _) => #1 e
-           | NONE => e)
-      | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
-        let
-            fun fields (remaining, passed) =
-                case remaining of
-                    [] => []
-                  | (x, t) :: rest =>
-                    (x,
-                     (EField (r, x, {field = t,
-                                     rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
-                     t) :: fields (rest, (x, t) :: passed)
-        in
-            #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
-        end
-      | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
-        let
-            fun fields (remaining, passed) =
-                case remaining of
-                    [] => []
-                  | (x, t) :: rest =>
-                    (x,
-                     (EField (r, x, {field = t,
-                                     rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
-                     t) :: fields (rest, (x, t) :: passed)
-        in
-            #1 (reduceExp env (ERecord (fields (xts, [])), loc))
-        end
-
-      | _ => e
+    let
+        (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*)
+
+        val r = case e of
+                    ENamed n =>
+                    (case E.lookupENamed env n of
+                         (_, _, 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) =>
+                    #1 (reduceExp env (subConInExp (0, c) e1))
+
+                  | EField ((ERecord xes, _), (CName x, _), _) =>
+                    (case List.find (fn ((CName x', _), _, _) => x' = x
+                                      | _ => false) xes of
+                         SOME (_, e, _) => #1 e
+                       | NONE => e)
+                  | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
+                    let
+                        fun fields (remaining, passed) =
+                            case remaining of
+                                [] => []
+                              | (x, t) :: rest =>
+                                (x,
+                                 (EField (r, x, {field = t,
+                                                 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
+                                 t) :: fields (rest, (x, t) :: passed)
+                    in
+                        #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
+                    end
+                  | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
+                    let
+                        fun fields (remaining, passed) =
+                            case remaining of
+                                [] => []
+                              | (x, t) :: rest =>
+                                (x,
+                                 (EField (r, x, {field = t,
+                                                 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
+                                 t) :: fields (rest, (x, t) :: passed)
+                    in
+                        #1 (reduceExp env (ERecord (fields (xts, [])), loc))
+                    end
+
+                  | _ => e
+    in
+        (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)),
+                               ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*)
+
+        r
+    end
 
 and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env