summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 12:58:35 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-23 12:58:35 -0400
commit2e606b03c8dbc594610e62ac260145ac26ebc699 (patch)
tree23055572341487865f0ef6cff685404f796a2410
parent3b7e65be5f6e496c23df7909d50ce8e287d571d7 (diff)
Fix nasty de Bruijn substitution bug; TcSum demo
Diffstat
-rw-r--r--demo/prose4
-rw-r--r--demo/tcSum.ur9
-rw-r--r--demo/tcSum.urp2
-rw-r--r--demo/tcSum.urs1
-rw-r--r--lib/basis.urs1
-rw-r--r--src/core_env.sml14
-rw-r--r--src/monoize.sml20
-rw-r--r--src/reduce.sml115
8 files changed, 103 insertions, 63 deletions
diff --git a/demo/prose b/demo/prose
index 8fedc557..19e9df0f 100644
--- a/demo/prose
+++ b/demo/prose
@@ -100,3 +100,7 @@ An unusual part of the third argument is the syntax <tt>[t1 ~ t2]</tt> within a
<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>
diff --git a/demo/tcSum.ur b/demo/tcSum.ur
new file mode 100644
index 00000000..53679116
--- /dev/null
+++ b/demo/tcSum.ur
@@ -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>
diff --git a/demo/tcSum.urp b/demo/tcSum.urp
new file mode 100644
index 00000000..8b36efc0
--- /dev/null
+++ b/demo/tcSum.urp
@@ -0,0 +1,2 @@
+
+tcSum
diff --git a/demo/tcSum.urs b/demo/tcSum.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/tcSum.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/lib/basis.urs b/lib/basis.urs
index a539f05e..a8c81353 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -20,6 +20,7 @@ val eq_string : eq string
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 --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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:29:58 +0000