From 1c5759720917cc8b654aed93d065a136bd862d8c Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 23 Jul 2015 14:00:42 +0200
Subject: [PATCH] improve doc and testing of core API
---
src/main/scala/leon/purescala/ExprOps.scala | 10 +-
.../scala/leon/purescala/ExprOpsSuite.scala | 103 +++++++++++++++++-
2 files changed, 107 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b5d15e463..369ac9e71 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -65,7 +65,7 @@ object ExprOps {
/** pre-traversal of the tree.
*
* invokes the input function on every node *before* visiting
- * children.
+ * children. Traverse children from left to right subtrees.
*
* e.g.
* {{{
@@ -73,8 +73,11 @@ object ExprOps {
* }}}
* will yield, in order:
* {{{
- * f(Add(a, Minus(b, c))), f(a), f(Minus(b, c)), f(b), f(c)
+ * f(Add(a, Minus(b, c))); f(a); f(Minus(b, c)); f(b); f(c)
* }}}
+ *
+ * @param f a function to apply on each node of the expression
+ * @param e the expression to traverse
*/
def preTraversal(f: Expr => Unit)(e: Expr): Unit = {
val rec = preTraversal(f) _
@@ -96,6 +99,9 @@ object ExprOps {
* {{{
* f(a), f(b), f(c), f(Minus(b, c)), f(Add(a, Minus(b, c)))
* }}}
+ *
+ * @param f a function to apply on each node of the expression
+ * @param e the expression to traverse
*/
def postTraversal(f: Expr => Unit)(e: Expr): Unit = {
val rec = postTraversal(f) _
diff --git a/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala b/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
index 40d442ef6..91e14f1d5 100644
--- a/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
+++ b/src/unit-test/scala/leon/purescala/ExprOpsSuite.scala
@@ -48,15 +48,110 @@ class ExprOpsSuite extends LeonTestSuite with WithLikelyEq with ExpressionsBuild
assert(foldRight(foldConcatNames)(And(p, Or(q, r))) === (p.id.name + q.id.name + r.id.name))
}
+ private class LocalCounter {
+ private var c = 0
+ def inc() = c += 1
+ def get = c
+ }
+
+ test("preTraversal works on a single node") {
+ val c = new LocalCounter
+ preTraversal(e => c.inc())(x)
+ assert(c.get === 1)
+ preTraversal(e => c.inc())(y)
+ assert(c.get === 2)
+
+ var names: List[String] = List()
+ preTraversal({
+ case Variable(id) => names ::= id.name
+ case _ => ()
+ })(x)
+ assert(names === List(x.id.name))
+ }
+ test("preTraversal correctly applies on every nodes on a simple expression") {
+ val c1 = new LocalCounter
+ preTraversal(e => c1.inc())(And(Seq(p, q, r)))
+ assert(c1.get === 4)
+ val c2 = new LocalCounter
+ preTraversal(e => c2.inc())(Or(p, q))
+ assert(c2.get === 3)
+ preTraversal(e => c2.inc())(Plus(x, y))
+ assert(c2.get === 6)
+ }
- test("Path-aware simplifications") {
- // TODO actually testing something here would be better, sorry
- // PS
+ test("preTraversal visits children from left to right") {
+ var names: List[String] = List()
+ preTraversal({
+ case Variable(id) => names ::= id.name
+ case _ => ()
+ })(And(List(p, q, r)))
+ assert(names === List(r.id.name, q.id.name, p.id.name))
+ }
- assert(true)
+ test("preTraversal works on nexted expressions") {
+ val c = new LocalCounter
+ preTraversal(e => c.inc())(And(p, And(q, r)))
+ assert(c.get === 5)
}
+ test("preTraversal traverses in pre-order") {
+ var nodes: List[Expr] = List()
+ val node = And(List(p, q, r))
+ preTraversal(e => nodes ::= e)(node)
+ assert(nodes === List(r, q, p, node))
+ }
+
+
+ test("postTraversal works on a single node") {
+ val c = new LocalCounter
+ postTraversal(e => c.inc())(x)
+ assert(c.get === 1)
+ postTraversal(e => c.inc())(y)
+ assert(c.get === 2)
+
+ var names: List[String] = List()
+ postTraversal({
+ case Variable(id) => names ::= id.name
+ case _ => ()
+ })(x)
+ assert(names === List(x.id.name))
+ }
+
+ test("postTraversal correctly applies on every nodes on a simple expression") {
+ val c1 = new LocalCounter
+ postTraversal(e => c1.inc())(And(Seq(p, q, r)))
+ assert(c1.get === 4)
+ val c2 = new LocalCounter
+ postTraversal(e => c2.inc())(Or(p, q))
+ assert(c2.get === 3)
+ postTraversal(e => c2.inc())(Plus(x, y))
+ assert(c2.get === 6)
+ }
+
+ test("postTraversal visits children from left to right") {
+ var names: List[String] = List()
+ postTraversal({
+ case Variable(id) => names ::= id.name
+ case _ => ()
+ })(And(List(p, q, r)))
+ assert(names === List(r.id.name, q.id.name, p.id.name))
+ }
+
+ test("postTraversal works on nexted expressions") {
+ val c = new LocalCounter
+ postTraversal(e => c.inc())(And(p, And(q, r)))
+ assert(c.get === 5)
+ }
+
+ test("postTraversal traverses in pre-order") {
+ var nodes: List[Expr] = List()
+ val node = And(List(p, q, r))
+ postTraversal(e => nodes ::= e)(node)
+ assert(nodes === List(node, r, q, p))
+ }
+
+
/**
* If the formula consist of some top level AND, find a top level
* Equals and extract it, return the remaining formula as well
--
GitLab