summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-13 15:42:24 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-13 15:42:24 -0400
commitc23f27988ff76b4923a63ced2452c4fd7787a745 (patch)
treefd3763788e9a011e6a90096de94999d80c00c9ec
parentba3e01e524907d85f5cba6af62083fcdee606f33 (diff)
Fix MonoReduce unsoundness with lets and fns
-rw-r--r--src/elaborate.sml9
-rw-r--r--src/mono_reduce.sml9
2 files changed, 8 insertions, 10 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 3b147e00..e78132c4 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -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 normClassConstraint env (c, loc) =
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 --git a/src/mono_reduce.sml b/src/mono_reduce.sml
index 1ea3df36..4bbb430d 100644
--- a/src/mono_reduce.sml
+++ b/src/mono_reduce.sml
@@ -461,11 +461,10 @@ fun reduce file =
(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