Mercurial > urweb
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