changeset 848:e8594cfa3236

Fix MonoReduce unsoundness with lets and fns
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Jun 2009 15:42:24 -0400
parents 0f7e2cca6d9b
children e571fb150a9f
files src/elaborate.sml src/mono_reduce.sml
diffstat 2 files changed, 8 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- 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
--- 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