diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-05-28 12:07:05 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-28 12:07:05 -0400 |
| commit | a735f6ea0ef8ec5895dfe7f895f89ee8c126de14 (patch) | |
| tree | 702dbe43701e15a37f7811983aad78e069812704 /src/elab_util.sml | |
| parent | 43cd4231dea11d2cbb0151f144e4a98c618df396 (diff) | |
Destructing local let, to the point where demo compiles
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 31 |
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 |