# HG changeset patch # User Adam Chlipala # Date 1224781115 14400 # Node ID e0e9e9eca1cbd5414f1d45ccbea61309695fc9c7 # Parent 679b2fbbd4d04961eb7e29066f17c65d0acf745e Fix nasty de Bruijn substitution bug; TcSum demo diff -r 679b2fbbd4d0 -r e0e9e9eca1cb demo/prose --- 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 @@

The general syntax for constant row types is [Name1 = t1, ..., NameN = tN], and there is a shorthand version [Name1, ..., NameN] for records of Units.

With sum defined, it is easy to make some sample calls. The form of the code for main does not make it apparent, but the compiler must "reverse engineer" the appropriate {Unit} from the {Type} available from the context at each call to sum.

+ +tcSum.urp + +

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.

diff -r 679b2fbbd4d0 -r e0e9e9eca1cb demo/tcSum.ur --- /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 + {[sum {A = 0, B = 1}]}
+ {[sum {C = 2.1, D = 3.2, E = 4.3}]} + diff -r 679b2fbbd4d0 -r e0e9e9eca1cb demo/tcSum.urp --- /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 diff -r 679b2fbbd4d0 -r e0e9e9eca1cb demo/tcSum.urs --- /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 diff -r 679b2fbbd4d0 -r e0e9e9eca1cb lib/basis.urs --- 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 diff -r 679b2fbbd4d0 -r e0e9e9eca1cb src/core_env.sml --- 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} diff -r 679b2fbbd4d0 -r e0e9e9eca1cb src/monoize.sml --- 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), diff -r 679b2fbbd4d0 -r e0e9e9eca1cb src/reduce.sml --- 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