summaryrefslogtreecommitdiff
path: root/src/reduce.sml
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
commit0fa422bfaf3931aacff958cb73d44ebfa4191f4a (patch)
tree23055572341487865f0ef6cff685404f796a2410 /src/reduce.sml
parent833f4d2e0474ec3ff772107b52711289c4b648cf (diff)
Fix nasty de Bruijn substitution bug; TcSum demo
Diffstat (limited to 'src/reduce.sml')
-rw-r--r--src/reduce.sml115
1 files changed, 63 insertions, 52 deletions
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