# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1244922144 14400
# Node ID e8594cfa3236c36d1e5f62078852b7dc03e93d95
# Parent  0f7e2cca6d9b40977ee1eeff95152f015893f899
Fix MonoReduce unsoundness with lets and fns

diff -r 0f7e2cca6d9b -r e8594cfa3236 src/elaborate.sml
--- a/src/elaborate.sml	Sat Jun 13 14:29:36 2009 -0400
+++ b/src/elaborate.sml	Sat Jun 13 15:42:24 2009 -0400
@@ -697,10 +697,9 @@
  and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
      let
          val loc = #2 k
-         val pdescs = [("#1", p_summary env s1),
-                       ("#2", p_summary env s2)]
-         (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
-                                         ("#2", p_summary env s2)]*)
+         (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)),
+                                           ("#1", p_summary env s1),
+                                           ("#2", p_summary env s2)]*)
 
          fun eatMatching p (ls1, ls2) =
              let
@@ -1595,7 +1594,7 @@
 
 fun elabExp (env, denv) (eAll as (e, loc)) =
     let
-        (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
+        (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
         (*val befor = Time.now ()*)
 
         val r = case e of
diff -r 0f7e2cca6d9b -r e8594cfa3236 src/mono_reduce.sml
--- a/src/mono_reduce.sml	Sat Jun 13 14:29:36 2009 -0400
+++ b/src/mono_reduce.sml	Sat Jun 13 15:42:24 2009 -0400
@@ -461,11 +461,10 @@
                                                  (EApp (b, liftExpInExp 0 e'), loc)), loc))
 
                       | ELet (x, t, e', (EAbs (x', t' as (TRecord [], _), ran, e''), loc)) =>
-                        (*if impure e' then
-                              e
-                          else*)
-                        (* Seems unsound in general without the check... should revisit later *)
-                        EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e', swapExpVars 0 e''), loc))
+                        if impure e' then
+                            e
+                        else
+                            EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e', swapExpVars 0 e''), loc))
 
                       | ELet (x, t, e', b) =>
                         let