From 6dad0efb71a93a0e001578b542187add6fe5d36a Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 6 Jan 2016 16:33:01 +0100
Subject: [PATCH] improve mapping with context
---
src/main/scala/leon/purescala/ExprOps.scala | 17 +++++++++++---
.../leon/unit/purescala/ExprOpsSuite.scala | 22 +++++++++++++++++--
2 files changed, 34 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6623d1248..92ce18e2c 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -221,13 +221,24 @@ object ExprOps {
* the recursion in its children. The context is "lost" when going back up,
* so changes made by one node will not be see by its siblings.
*/
- def preMapWithContext[C](f: (Expr, C) => (Option[Expr], C))(e: Expr, c: C): Expr = {
+ def preMapWithContext[C](f: (Expr, C) => (Option[Expr], C), applyRec: Boolean = false)
+ (e: Expr, c: C): Expr = {
def rec(expr: Expr, context: C): Expr = {
val (newV, newCtx) = {
- val res = f(expr, context)
- (res._1.getOrElse(expr), res._2)
+ if(applyRec) {
+ var ctx = context
+ val finalV = fixpoint{ e: Expr => {
+ val res = f(e, ctx)
+ ctx = res._2
+ res._1.getOrElse(e)
+ }} (expr)
+ (finalV, ctx)
+ } else {
+ val res = f(expr, context)
+ (res._1.getOrElse(expr), res._2)
+ }
}
val Operator(es, builder) = newV
diff --git a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
index 10b64f75a..827596fc6 100644
--- a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
@@ -289,7 +289,8 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
case _ => (None, set)
}
- assert(preMapWithContext(op)(expr, Set()) === Plus(bi(2), bi(2)))
+ assert(preMapWithContext(op, false)(expr, Set()) === Plus(bi(2), bi(2)))
+ assert(preMapWithContext(op, true)(expr, Set()) === Plus(bi(42), bi(42)))
val expr2 = Let(x.id, bi(1), Let(y.id, bi(2), Plus(x, y)))
def op2(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
@@ -298,7 +299,24 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
case _ => (None, bindings)
}
- assert(preMapWithContext(op2)(expr2, Map()) === Let(x.id, bi(1), Let(y.id, bi(2), Plus(bi(1), bi(2)))))
+ assert(preMapWithContext(op2, false)(expr2, Map()) === Let(x.id, bi(1), Let(y.id, bi(2), Plus(bi(1), bi(2)))))
+
+ def op3(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
+ case Let(id, InfiniteIntegerLiteral(v), body) => (Some(body), bindings + (id -> v))
+ case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ case _ => (None, bindings)
+ }
+ assert(preMapWithContext(op3, true)(expr2, Map()) === Plus(bi(1), bi(2)))
+
+
+ val expr4 = Plus(Let(y.id, bi(2), y),
+ Let(y.id, bi(4), y))
+ def op4(e: Expr, bindings: Map[Identifier, BigInt]): (Option[Expr], Map[Identifier, BigInt]) = e match {
+ case Let(id, InfiniteIntegerLiteral(v), body) => (Some(body), if(bindings.contains(id)) bindings else (bindings + (id -> v)))
+ case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ case _ => (None, bindings)
+ }
+ assert(preMapWithContext(op4, true)(expr4, Map()) === Plus(bi(2), bi(4)))
}
}
--
GitLab