From 06f01708dca04038c0c712f442972607f439a78e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 10 May 2016 17:13:56 +0200
Subject: [PATCH] Improve simplifyLets even more
---
src/main/scala/leon/purescala/ExprOps.scala | 25 ++++++++++++++++++---
1 file changed, 22 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 4eb938d2f..24e54b367 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -413,13 +413,32 @@ object ExprOps extends GenTreeOps[Expr] {
def simplerLet(t: Expr): Option[Expr] = t match {
/* Untangle */
+ case Let(i1, Let(i2, e2, b2), b1) =>
+ Some(Let(i2, e2, Let(i1, b2, b1)))
+
+ case Let(i1, LetTuple(is2, e2, b2), b1) =>
+ Some(letTuple(is2, e2, Let(i1, b2, b1)))
+
+ case LetTuple(ids1, Let(id2, e2, b2), b1) =>
+ Some(Let(id2, e2, letTuple(ids1, b2, b1)))
+
case LetTuple(ids1, LetTuple(ids2, e2, b2), b1) =>
Some(letTuple(ids2, e2, letTuple(ids1, b2, b1)))
- case Let(i1, Let(i2, e2, b2), b1) =>
- Some(Let(i2, e2, Let(i1, b2, b1)))
+ // Untuple
+ case Let(id, Tuple(es), b) =>
+ val tps = es map (_.getType)
+ val ids = tps.zipWithIndex.map {
+ case (tp, ind) => FreshIdentifier(id + (ind + 1).toString, tp, true)
+ }
+ val theMap: Map[Expr, Expr] = es.zip(ids).zipWithIndex.map {
+ case ((e, subId), ind) => TupleSelect(Variable(id), ind + 1) -> Variable(subId)
+ }.toMap
+
+ val replaced0 = replace(theMap, b)
+ val replaced = replace(Map(Variable(id) -> Tuple(ids map Variable)), replaced0)
- // TODO
+ Some(letTuple(ids, Tuple(es), replaced))
case Let(i, e, b) if freeComputable(e) && isPurelyFunctional(e) =>
// computation is very quick and code easy to read, always inline
--
GitLab