From 0792563cac00b5efa5b214a0fe83711b9bed3301 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 6 Jan 2016 15:36:43 +0100
Subject: [PATCH] pre map with context helper
---
src/main/scala/leon/purescala/ExprOps.scala | 32 +++++++++++++++++++
.../leon/unit/purescala/ExprOpsSuite.scala | 22 +++++++++++++
2 files changed, 54 insertions(+)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 49d945ec6..6623d1248 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -213,6 +213,38 @@ object ExprOps {
}
+ /** Pre-transformation of the tree, with a context value from "top-down".
+ *
+ * Takes a partial function of replacements.
+ * Substitutes '''before''' recursing down the trees. The function returns
+ * an option of the new value, as well as the new context to be used for
+ * 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 rec(expr: Expr, context: C): Expr = {
+
+ val (newV, newCtx) = {
+ val res = f(expr, context)
+ (res._1.getOrElse(expr), res._2)
+ }
+
+ val Operator(es, builder) = newV
+ val newEs = es.map(e => rec(e, newCtx))
+
+ if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
+ builder(newEs).copiedFrom(newV)
+ } else {
+ newV
+ }
+
+ }
+
+ rec(e, c)
+ }
+
+
/** Applies functions and combines results in a generic way
*
* Start with an initial value, and apply functions to nodes before
diff --git a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
index b448953ac..10b64f75a 100644
--- a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
@@ -279,4 +279,26 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
}
}
+
+ test("preMapWithContext") { ctx =>
+ val expr = Plus(bi(1), Minus(bi(2), bi(3)))
+ def op(e : Expr, set: Set[Int]): (Option[Expr], Set[Int]) = e match {
+ case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => (Some(bi(2)), set)
+ case InfiniteIntegerLiteral(one) if one == BigInt(1) => (Some(bi(2)), set)
+ case InfiniteIntegerLiteral(two) if two == BigInt(2) => (Some(bi(42)), set)
+ case _ => (None, set)
+ }
+
+ assert(preMapWithContext(op)(expr, Set()) === Plus(bi(2), bi(2)))
+
+ 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 {
+ case Let(id, InfiniteIntegerLiteral(v), body) => (None, bindings + (id -> v))
+ case Variable(id) => (bindings.get(id).map(v => InfiniteIntegerLiteral(v)), bindings)
+ case _ => (None, bindings)
+ }
+
+ assert(preMapWithContext(op2)(expr2, Map()) === Let(x.id, bi(1), Let(y.id, bi(2), Plus(bi(1), bi(2)))))
+ }
+
}
--
GitLab