Mercurial > urweb
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