summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:40:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:40:55 -0400
commit8327f190c80287003048eaa10857d0f081b551bb (patch)
tree1ebd4c0f5a8f22a6ddd0dbb86cd2cc741b610e0e /src/elab_util.sml
parenta735f6ea0ef8ec5895dfe7f895f89ee8c126de14 (diff)
Fix EDLet elab_util bug
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml35
1 files changed, 18 insertions, 17 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index c2101ae3..8082cb1e 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -438,29 +438,30 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
| ELet (des, e, t) =>
let
- val (des, ctx) = foldl (fn (ed, (des, ctx)) =>
- let
- val ctx' =
- case #1 ed of
- EDVal (p, _, _) => doVars (p, ctx)
- | EDValRec vis =>
- foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
- in
- (S.bind2 (des,
- fn des' =>
- S.map2 (mfed ctx ed,
- fn ed' => des' @ [ed'])),
- ctx')
- end)
+ val (des, ctx') = foldl (fn (ed, (des, ctx)) =>
+ let
+ val ctx' =
+ case #1 ed of
+ EDVal (p, _, _) => doVars (p, ctx)
+ | EDValRec vis =>
+ foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t)))
+ ctx vis
+ in
+ (S.bind2 (des,
+ fn des' =>
+ S.map2 (mfed ctx ed,
+ fn ed' => ed' :: des')),
+ ctx')
+ end)
(S.return2 [], ctx) des
in
S.bind2 (des,
fn des' =>
- S.bind2 (mfe ctx e,
+ S.bind2 (mfe ctx' e,
fn e' =>
S.map2 (mfc ctx t,
fn t' =>
- (ELet (des', e', t'), loc))))
+ (ELet (rev des', e', t'), loc))))
end
| EKAbs (x, e) =>
@@ -479,7 +480,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
EDVal (p, t, e) =>
S.bind2 (mfc ctx t,
fn t' =>
- S.map2 (mfe (doVars (p, ctx)) e,
+ S.map2 (mfe ctx e,
fn e' =>
(EDVal (p, t', e'), loc)))
| EDValRec vis =>