From 83f8f8bfaff8970a2d79d146cf6e2ff7a25b0acb Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 17 Jun 2015 21:11:58 +0200
Subject: [PATCH] Let deleting code hides errors
---
src/main/scala/leon/purescala/Constructors.scala | 6 ------
src/main/scala/leon/purescala/ExprOps.scala | 2 +-
src/main/scala/leon/purescala/Extractors.scala | 6 +++---
3 files changed, 4 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index ce97e5912..a64226761 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -27,12 +27,6 @@ object Constructors {
def tupleSelect(t: Expr, index: Int, originalSize: Int): Expr = tupleSelect(t, index, originalSize > 1)
- def let(id: Identifier, e: Expr, bd: Expr) = {
- if (variablesOf(bd) contains id)
- Let(id, e, bd)
- else bd
- }
-
def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
case Nil =>
body
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b3bd13f5d..421ee376e 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -682,7 +682,7 @@ object ExprOps {
}
val (bd, defs) = genericTransform[C](noTransformer, lift, _.flatten)(Seq())(e)
- defs.foldRight(bd){ case ((id, e), body) => let(id, e, body) }
+ defs.foldRight(bd){ case ((id, e), body) => Let(id, e, body) }
}
/**
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index c363c60ba..ed0d630c3 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -83,7 +83,7 @@ object Extractors {
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
- case Let(binder, e, body) => Some((e, body, let(binder, _, _)))
+ case Let(binder, e, body) => Some((e, body, Let(binder, _, _)))
case Require(pre, body) => Some((pre, body, Require))
case Ensuring(body, post) => Some((body, post, Ensuring))
case Assert(const, oerr, body) => Some((const, body, Assert(_, oerr, _)))
@@ -197,7 +197,7 @@ object Extractors {
object TopLevelOrs { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
- case Let(i, e, TopLevelOrs(bs)) => Some(bs map (let(i,e,_)))
+ case Let(i, e, TopLevelOrs(bs)) => Some(bs map (Let(i,e,_)))
case Or(exprs) =>
Some(exprs.flatMap(unapply).flatten)
case e =>
@@ -206,7 +206,7 @@ object Extractors {
}
object TopLevelAnds { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
- case Let(i, e, TopLevelAnds(bs)) => Some(bs map (let(i,e,_)))
+ case Let(i, e, TopLevelAnds(bs)) => Some(bs map (Let(i,e,_)))
case And(exprs) =>
Some(exprs.flatMap(unapply).flatten)
case e =>
--
GitLab