diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 836282b09fbb25f62866b8ae8c9236436ed29006..54da326bdbd954f2cf558f57a16fe4d3c1c9621c 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -19,7 +19,7 @@ import solvers._
*
* The generic operations lets you apply operations on a whole tree
* expression. You can look at:
- * - [[ExprOps.foldRight foldRight]]
+ * - [[ExprOps.fold foldRight]]
* - [[ExprOps.preTraversal preTraversal]]
* - [[ExprOps.postTraversal postTraversal]]
* - [[ExprOps.preMap preMap]]
@@ -53,8 +53,8 @@ object ExprOps {
* @return The expression after applying `f` on all subtrees.
* @note the computation is lazy, hence you should not rely on side-effects of `f`
*/
- def foldRight[T](f: (Expr, Seq[T]) => T)(e: Expr): T = {
- val rec = foldRight(f) _
+ def fold[T](f: (Expr, Seq[T]) => T)(e: Expr): T = {
+ val rec = fold(f) _
val Operator(es, _) = e
//Usages of views makes the computation lazy. (which is useful for
@@ -252,7 +252,6 @@ object ExprOps {
rec(expr, init)
}
-
/*
* =============
* Auxiliary API
@@ -263,16 +262,16 @@ object ExprOps {
/** Checks if the predicate holds in some sub-expression */
def exists(matcher: Expr => Boolean)(e: Expr): Boolean = {
- foldRight[Boolean]({ (e, subs) => matcher(e) || subs.contains(true) } )(e)
+ fold[Boolean]({ (e, subs) => matcher(e) || subs.contains(true) } )(e)
}
/** Collects a set of objects from all sub-expressions */
def collect[T](matcher: Expr => Set[T])(e: Expr): Set[T] = {
- foldRight[Set[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
+ fold[Set[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
}
def collectPreorder[T](matcher: Expr => Seq[T])(e: Expr): Seq[T] = {
- foldRight[Seq[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
+ fold[Seq[T]]({ (e, subs) => matcher(e) ++ subs.flatten } )(e)
}
/** Returns a set of all sub-expressions matching the predicate */
@@ -282,7 +281,7 @@ object ExprOps {
/** Counts how many times the predicate holds in sub-expressions */
def count(matcher: Expr => Int)(e: Expr): Int = {
- foldRight[Int]({ (e, subs) => matcher(e) + subs.sum } )(e)
+ fold[Int]({ (e, subs) => matcher(e) + subs.sum } )(e)
}
/** Replaces bottom-up sub-expressions by looking up for them in a map */
@@ -309,14 +308,13 @@ object ExprOps {
/** Returns the set of identifiers in an expression */
def variablesOf(expr: Expr): Set[Identifier] = {
- foldRight[Set[Identifier]]{
+ fold[Set[Identifier]] {
case (e, subs) =>
val subvs = subs.flatten.toSet
-
e match {
- case Variable(i) => subvs + i
- case LetDef(fd,_) => subvs -- fd.params.map(_.id)
- case Let(i,_,_) => subvs - i
+ case Variable(i) => subvs + i
+ case LetDef(fd, _) => subvs -- fd.params.map(_.id)
+ case Let(i, _, _) => subvs - i
case MatchExpr(_, cses) => subvs -- cses.flatMap(_.pattern.binders)
case Passes(_, _, cses) => subvs -- cses.flatMap(_.pattern.binders)
case Lambda(args, _) => subvs -- args.map(_.id)
@@ -344,7 +342,7 @@ object ExprOps {
/** Returns functions in directly nested LetDefs */
def directlyNestedFunDefs(e: Expr): Set[FunDef] = {
- foldRight[Set[FunDef]]{
+ fold[Set[FunDef]]{
case (LetDef(fd,_), Seq(fromFd, fromBd)) => fromBd + fd
case (_, subs) => subs.flatten.toSet
}(e)
@@ -416,7 +414,7 @@ object ExprOps {
/** Computes the depth of the expression's tree */
def depth(e: Expr): Int = {
- foldRight[Int]{ (e, sub) => 1 + (0 +: sub).max }(e)
+ fold[Int]{ (e, sub) => 1 + (0 +: sub).max }(e)
}
/** Applies the function to the I/O constraint and simplifies the resulting constraint */
@@ -478,7 +476,7 @@ object ExprOps {
* structures and must therefore be synchronized.
*/
def normalizeStructure(expr: Expr): (Expr, Map[Identifier, Identifier]) = synchronized {
- val allVars : Seq[Identifier] = foldRight[Seq[Identifier]] {
+ val allVars : Seq[Identifier] = fold[Seq[Identifier]] {
(expr, idSeqs) => idSeqs.foldLeft(expr match {
case Lambda(args, _) => args.map(_.id)
case Forall(args, _) => args.map(_.id)
@@ -624,7 +622,7 @@ object ExprOps {
// the occurences of all variables in one traversal of the
// expression.
- val occurences : Seq[Int] = foldRight[Seq[Int]]({ case (e, subs) =>
+ val occurences : Seq[Int] = fold[Seq[Int]]({ case (e, subs) =>
e match {
case Variable(x) => idMap.getOrElse(x, zeroVec)
case _ => subs.foldLeft(zeroVec) { case (a1, a2) =>
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index ba25faf4217083a24194871a74be7f648fa3f617..1214af2aa9526abf1f7adb9b875d7829fd2720cf 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -146,7 +146,7 @@ object Quantification {
if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).size >= 1)
ctx.reporter.warning("Multiple matchers must provide bijective matching in " + conjunct)
- foldRight[Set[Identifier]] { case (m, children) =>
+ fold[Set[Identifier]] { case (m, children) =>
val q = children.toSet.flatten
m match {
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index f4714bd9e561335d90d75860770b7bede75d04ee..32d273c3937d6ba4b808b79c16edf1ded4ade785 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -192,7 +192,7 @@ object Template {
case _ => Set.empty
}(e)
- matchInfos ++= foldRight[Map[Expr, Matcher[T]]] { (expr, res) =>
+ matchInfos ++= fold[Map[Expr, Matcher[T]]] { (expr, res) =>
val result = res.flatten.toMap
result ++ (expr match {
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 47b14d99bb9b175965efb088053a5cbd74c3221b..77b451094ae1451ce7e46c9e3312488c7c398058 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -170,8 +170,8 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
}
def removeIns(toRemove: Set[Identifier]) = {
- val toKeep = as.zipWithIndex.filterNot(a => toRemove(a._1)).map(_._2)
- eb mapIns { in => List(toKeep.map(in)) }
+ val toKeep: List[Int] = as.zipWithIndex.filterNot(a => toRemove(a._1)).map(_._2)
+ eb mapIns { (in: Seq[Expr]) => List(toKeep.map(in)) }
}
def filterIns(expr: Expr): ExamplesBank = {
diff --git a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
index 133f0e624bb1c9c27539477213e715092af06a41..b448953acf1856cf1df12289880000226f78f8bf 100644
--- a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
@@ -22,31 +22,31 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
}
test("foldRight works on single variable expression") { ctx =>
- assert(foldRight(foldConcatNames)(x) === x.id.name)
- assert(foldRight(foldConcatNames)(y) === y.id.name)
- assert(foldRight(foldCountVariables)(x) === 1)
- assert(foldRight(foldCountVariables)(y) === 1)
+ assert(fold(foldConcatNames)(x) === x.id.name)
+ assert(fold(foldConcatNames)(y) === y.id.name)
+ assert(fold(foldCountVariables)(x) === 1)
+ assert(fold(foldCountVariables)(y) === 1)
}
test("foldRight works on simple expressions without nested structure") { ctx =>
- 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))) ===
+ assert(fold(foldConcatNames)(And(p, q)) === (p.id.name + q.id.name))
+ assert(fold(foldConcatNames)(And(q, p)) === (q.id.name + p.id.name))
+ assert(fold(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))) ===
+ assert(fold(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(fold(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)
+ assert(fold(foldCountVariables)(And(p, q)) === 2)
+ assert(fold(foldCountVariables)(And(q, p)) === 2)
+ assert(fold(foldCountVariables)(And(p, p)) === 2)
+ assert(fold(foldCountVariables)(And(Seq(p, p, p, q, r))) === 5)
+ assert(fold(foldCountVariables)(Or(Seq(p, p, p, q, r))) === 5)
}
test("foldRight works on simple structure of nested expressions") { ctx =>
- 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))
+ assert(fold(foldConcatNames)(And(And(p, q), r)) === (p.id.name + q.id.name + r.id.name))
+ assert(fold(foldConcatNames)(And(p, Or(q, r))) === (p.id.name + q.id.name + r.id.name))
}
private class LocalCounter {