diff src/elab_util.sml @ 826:78504d97410b

Fix EDLet elab_util bug
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 12:40:55 -0400
parents 7f871c03e3a1
children b2413e4dd109
line wrap: on
line diff
--- a/src/elab_util.sml	Thu May 28 12:07:05 2009 -0400
+++ b/src/elab_util.sml	Thu May 28 12:40:55 2009 -0400
@@ -438,29 +438,30 @@
 
               | 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 @@
                 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 =>