summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:07:05 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:07:05 -0400
commita735f6ea0ef8ec5895dfe7f895f89ee8c126de14 (patch)
tree702dbe43701e15a37f7811983aad78e069812704 /src/elab_util.sml
parent43cd4231dea11d2cbb0151f144e4a98c618df396 (diff)
Destructing local let, to the point where demo compiles
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml31
1 files changed, 23 insertions, 8 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 036aa867..c2101ae3 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -306,6 +306,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
end
val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+ fun doVars ((p, _), ctx) =
+ case p of
+ PWild => ctx
+ | PVar xt => bind (ctx, RelE xt)
+ | PPrim _ => ctx
+ | PCon (_, _, _, NONE) => ctx
+ | PCon (_, _, _, SOME p) => doVars (p, ctx)
+ | PRecord xpcs =>
+ foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
+ ctx xpcs
+
fun mfe ctx e acc =
S.bindP (mfe' ctx e acc, fe ctx)
@@ -425,13 +436,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| EUnif (ref (SOME e)) => mfe ctx e
| EUnif _ => S.return2 eAll
- | ELet (des, e) =>
+ | ELet (des, e, t) =>
let
val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
let
val ctx' =
case #1 ed of
- EDVal (x, t, _) => bind (ctx, RelE (x, t))
+ EDVal (p, _, _) => doVars (p, ctx)
| EDValRec vis =>
foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
in
@@ -445,9 +456,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
in
S.bind2 (des,
fn des' =>
- S.map2 (mfe ctx e,
+ S.bind2 (mfe ctx e,
fn e' =>
- (ELet (des', e'), loc)))
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (ELet (des', e', t'), loc))))
end
| EKAbs (x, e) =>
@@ -463,10 +476,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
and mfed ctx (dAll as (d, loc)) =
case d of
- EDVal vi =>
- S.map2 (mfvi ctx vi,
- fn vi' =>
- (EDVal vi', loc))
+ EDVal (p, t, e) =>
+ S.bind2 (mfc ctx t,
+ fn t' =>
+ S.map2 (mfe (doVars (p, ctx)) e,
+ fn e' =>
+ (EDVal (p, t', e'), loc)))
| EDValRec vis =>
let
val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis