summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 11:17:29 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 11:17:29 -0400
commit3f497272d327fea2638006c751d812dbbc449c78 (patch)
tree60d3ec0e0ab4ba36e8ad9396aad35e05d4725153 /src/elab_util.sml
parent89f97891a33b5c0a8971d3508059a139a8815091 (diff)
Elaborating 'let'
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml42
1 files changed, 42 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 247e2b3a..28fe8f22 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -352,6 +352,48 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| EError => S.return2 eAll
| EUnif (ref (SOME e)) => mfe ctx e
| EUnif _ => S.return2 eAll
+
+ | ELet (des, e) =>
+ let
+ val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
+ (S.bind2 (des,
+ fn des' =>
+ S.map2 (mfed ctx ed,
+ fn ed' => des' @ [ed'])),
+ case #1 ed of
+ EDVal (x, t, _) => bind (ctx, RelE (x, t))
+ | EDValRec vis =>
+ foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis))
+ (S.return2 [], ctx) des
+ in
+ S.bind2 (des,
+ fn des' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (ELet (des', e'), loc)))
+ end
+
+ and mfed ctx (dAll as (d, loc)) =
+ case d of
+ EDVal vi =>
+ S.map2 (mfvi ctx vi,
+ fn vi' =>
+ (EDVal vi', loc))
+ | EDValRec vis =>
+ let
+ val ctx = foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis
+ in
+ S.map2 (ListUtil.mapfold (mfvi ctx) vis,
+ fn vis' =>
+ (EDValRec vis', loc))
+ end
+
+ and mfvi ctx (x, c, e) =
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (x, c', e')))
in
mfe
end