changeset 417:e0e9e9eca1cb

Fix nasty de Bruijn substitution bug; TcSum demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 12:58:35 -0400
parents 679b2fbbd4d0
children ad7e854a518c
files demo/prose demo/tcSum.ur demo/tcSum.urp demo/tcSum.urs lib/basis.urs src/core_env.sml src/monoize.sml src/reduce.sml
diffstat 8 files changed, 99 insertions(+), 59 deletions(-) [+]
line wrap: on
line diff
--- a/demo/prose	Thu Oct 23 11:59:48 2008 -0400
+++ b/demo/prose	Thu Oct 23 12:58:35 2008 -0400
@@ -100,3 +100,7 @@
 <p>The general syntax for constant row types is <tt>[Name1 = t1, ..., NameN = tN]</tt>, and there is a shorthand version <tt>[Name1, ..., NameN]</tt> for records of <tt>Unit</tt>s.</p>
 
 <p>With <tt>sum</tt> defined, it is easy to make some sample calls.  The form of the code for <tt>main</tt> does not make it apparent, but the compiler must "reverse engineer" the appropriate <tt>{Unit}</tt> from the <tt>{Type}</tt> available from the context at each call to <tt>sum</tt>.</p>
+
+tcSum.urp
+
+<p>It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.</p>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/tcSum.ur	Thu Oct 23 12:58:35 2008 -0400
@@ -0,0 +1,9 @@
+fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (x : $(mapUT t fs)) =
+    foldUR [t] [fn _ => t]
+    (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
+    zero [fs] x
+
+fun main () = return <xml><body>
+  {[sum {A = 0, B = 1}]}<br/>
+  {[sum {C = 2.1, D = 3.2, E = 4.3}]}
+</body></xml>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/tcSum.urp	Thu Oct 23 12:58:35 2008 -0400
@@ -0,0 +1,2 @@
+
+tcSum
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/tcSum.urs	Thu Oct 23 12:58:35 2008 -0400
@@ -0,0 +1,1 @@
+val main : unit -> transaction page
--- a/lib/basis.urs	Thu Oct 23 11:59:48 2008 -0400
+++ b/lib/basis.urs	Thu Oct 23 12:58:35 2008 -0400
@@ -20,6 +20,7 @@
 val eq_bool : eq bool
 
 class num
+val zero : t ::: Type -> num t -> t
 val neg : t ::: Type -> num t -> t -> t
 val plus : t ::: Type -> num t -> t -> t -> t
 val minus : t ::: Type -> num t -> t -> t -> t
--- a/src/core_env.sml	Thu Oct 23 11:59:48 2008 -0400
+++ b/src/core_env.sml	Thu Oct 23 12:58:35 2008 -0400
@@ -82,13 +82,13 @@
 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}
--- a/src/monoize.sml	Thu Oct 23 11:59:48 2008 -0400
+++ b/src/monoize.sml	Thu Oct 23 12:58:35 2008 -0400
@@ -104,7 +104,8 @@
                     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 @@
              (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 @@
                                  (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 @@
                                         (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 @@
                                         (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),
--- a/src/reduce.sml	Thu Oct 23 11:59:48 2008 -0400
+++ b/src/reduce.sml	Thu Oct 23 12:58:35 2008 -0400
@@ -36,6 +36,7 @@
 
 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 @@
                                          | 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 @@
 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)
+    let
+        (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*)
 
-      | 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)))
+        val r = case e of
+                    ENamed n =>
+                    (case E.lookupENamed env n of
+                         (_, _, SOME e', _) => #1 e'
+                       | _ => e)
 
-      | EApp ((EAbs (_, _, _, e1), loc), e2) =>
-        #1 (reduceExp env (subExpInExp (0, e2) e1))
-      | ECApp ((ECAbs (_, _, e1), loc), c) =>
-        #1 (reduceExp env (subConInExp (0, c) e1))
+                  | 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)))
 
-      | 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
+                  | EApp ((EAbs (_, _, _, e1), loc), e2) =>
+                    #1 (reduceExp env (subExpInExp (0, e2) e1))
+                  | ECApp ((ECAbs (_, _, e1), loc), c) =>
+                    #1 (reduceExp env (subConInExp (0, c) e1))
 
-      | _ => e
+                  | 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