diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 7a0a76427b085588831add1d3e7a18f44817b3ea..b5d15e4637ea84ed90b3dbbd644ac1cad761ab0f 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -14,8 +14,21 @@ import solvers._
/** Provides functions to manipulate [[purescala.Expressions]].
*
- * This object provides generic operations on Leon expressions, which
- * are used throughout the system.
+ * This object provides a few generic operations on Leon expressions,
+ * as well as some common operations.
+ *
+ * The generic operations enable to apply an operation on a whole tree
+ * expression. You can look at:
+ * - [[ExprOps.foldRight]]
+ * - [[ExprOps.preTraversal]]
+ * - [[ExprOps.postTraversal]]
+ * - [[ExprOps.preMap]]
+ * - [[ExprOps.postMap]]
+ *
+ * These operations usually take a higher order function that gets apply to the
+ * expression tree in some strategy. They provide an expressive way to build complex
+ * operation on Leon expressions.
+ *
*/
object ExprOps {
@@ -31,10 +44,14 @@ object ExprOps {
/**
* Do a right tree fold
*
+ * A right tree fold applies the input function to the subnodes first (from left
+ * to right), and combine the results along with the current node value.
+ *
* @param f a function that takes the current node and the seq
* of results form the subtrees.
* @param e the Expr on which to apply the fold.
* @return The expression after applying ``f`` on all subtrees.
+ * @note the computation is lazy, hence you should rely on side-effects of `f`
*/
def foldRight[T](f: (Expr, Seq[T]) => T)(e: Expr): T = {
val rec = foldRight(f) _
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 5a0626bd0c99f249b412076f87240ecfc05af7f8..46d114f3dc77c1d88703c21e19a00ed876e53141 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -493,6 +493,7 @@ object Expressions {
/* Integer arithmetic */
+
/** $encodingof `... + ...`
*
* If you are not sure about the requirement you should use
diff --git a/src/unit-test/scala/leon/purescala/TreeOpsSuite.scala b/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
similarity index 71%
rename from src/unit-test/scala/leon/purescala/TreeOpsSuite.scala
rename to src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
index b73eec580ce50ed4dbde963b3ddeffe6db50d2d7..40d442ef61c19a3fe85181c15f8e2e829294fdd8 100644
--- a/src/unit-test/scala/leon/purescala/TreeOpsSuite.scala
+++ b/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
@@ -1,15 +1,55 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-package leon.test.purescala
+package leon
+package purescala
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.ExprOps._
+import Common._
+import Expressions._
+import Types._
+import ExprOps._
-class TreeOpsSuite extends LeonTestSuite with WithLikelyEq {
+class ExprOpsSuite extends LeonTestSuite with WithLikelyEq with ExpressionsBuilder {
+
+ private def foldConcatNames(e: Expr, subNames: Seq[String]): String = e match {
+ case Variable(id) => subNames.mkString + id.name
+ case _ => subNames.mkString
+ }
+ private def foldCountVariables(e: Expr, subCounts: Seq[Int]): Int = e match {
+ case Variable(_) => subCounts.sum + 1
+ case _ => subCounts.sum
+ }
+
+ test("foldRight works on single variable expression") {
+ assert(foldRight(foldConcatNames)(x) === x.id.name)
+ assert(foldRight(foldConcatNames)(y) === y.id.name)
+ assert(foldRight(foldCountVariables)(x) === 1)
+ assert(foldRight(foldCountVariables)(y) === 1)
+ }
+
+ test("foldRight works on simple expressions without nested structure") {
+ assert(foldRight(foldConcatNames)(And(p, q)) === (p.id.name + q.id.name))
+ assert(foldRight(foldConcatNames)(And(q, p)) === (q.id.name + p.id.name))
+ assert(foldRight(foldConcatNames)(And(Seq(p, p, p, q, r))) ===
+ (p.id.name + p.id.name + p.id.name + q.id.name + r.id.name))
+ assert(foldRight(foldConcatNames)(Or(Seq(p, p, p, q, r))) ===
+ (p.id.name + p.id.name + p.id.name + q.id.name + r.id.name))
+ assert(foldRight(foldConcatNames)(Plus(x, y)) === (x.id.name + y.id.name))
+
+ assert(foldRight(foldCountVariables)(And(p, q)) === 2)
+ assert(foldRight(foldCountVariables)(And(q, p)) === 2)
+ assert(foldRight(foldCountVariables)(And(p, p)) === 2)
+ assert(foldRight(foldCountVariables)(And(Seq(p, p, p, q, r))) === 5)
+ assert(foldRight(foldCountVariables)(Or(Seq(p, p, p, q, r))) === 5)
+ }
+
+ test("foldRight works on simple structure of nested expressions") {
+ assert(foldRight(foldConcatNames)(And(And(p, q), r)) === (p.id.name + q.id.name + r.id.name))
+ assert(foldRight(foldConcatNames)(And(p, Or(q, r))) === (p.id.name + q.id.name + r.id.name))
+ }
+
+
+
test("Path-aware simplifications") {
// TODO actually testing something here would be better, sorry
// PS
@@ -34,18 +74,7 @@ class TreeOpsSuite extends LeonTestSuite with WithLikelyEq {
}
- def i(x: Int) = InfiniteIntegerLiteral(x)
-
- val xId = FreshIdentifier("x", IntegerType)
- val x = Variable(xId)
- val yId = FreshIdentifier("y", IntegerType)
- val y = Variable(yId)
val xs = Set(xId, yId)
-
- val aId = FreshIdentifier("a", IntegerType)
- val a = Variable(aId)
- val bId = FreshIdentifier("b", IntegerType)
- val b = Variable(bId)
val as = Set(aId, bId)
def checkSameExpr(e1: Expr, e2: Expr, vs: Set[Identifier]) {
diff --git a/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala b/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b634dd686d3119d3bf1b47af9f3bc7a3da9b8d39
--- /dev/null
+++ b/src/unit-test/scala/leon/purescala/ExpressionsBuilder.scala
@@ -0,0 +1,34 @@
+package leon
+package purescala
+
+
+import Expressions._
+import Types._
+import Common._
+
+trait ExpressionsBuilder {
+
+ protected def i(x: Int) = InfiniteIntegerLiteral(x)
+ protected def v(name: String, tpe: TypeTree = IntegerType) = Variable(FreshIdentifier(name, tpe))
+
+ protected val xId = FreshIdentifier("x", IntegerType)
+ protected val x = Variable(xId)
+ protected val yId = FreshIdentifier("y", IntegerType)
+ protected val y = Variable(yId)
+ protected val zId = FreshIdentifier("z", IntegerType)
+ protected val z = Variable(zId)
+
+ protected val aId = FreshIdentifier("a", IntegerType)
+ protected val a = Variable(aId)
+ protected val bId = FreshIdentifier("b", IntegerType)
+ protected val b = Variable(bId)
+ protected val cId = FreshIdentifier("c", IntegerType)
+ protected val c = Variable(cId)
+
+ protected val pId = FreshIdentifier("p", BooleanType)
+ protected val p = Variable(pId)
+ protected val qId = FreshIdentifier("q", BooleanType)
+ protected val q = Variable(qId)
+ protected val rId = FreshIdentifier("r", BooleanType)
+ protected val r = Variable(rId)
+}