From e0306b146561f1772e2ea17c1de5321641e3aef4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 6 Apr 2016 17:31:01 +0200
Subject: [PATCH] Generalize ExprOps if possible. Some documentation
---
src/main/scala/leon/purescala/ExprOps.scala | 44 ++--------------
.../scala/leon/purescala/GenTreeOps.scala | 50 +++++++++++++++++--
src/main/scala/leon/purescala/TypeOps.scala | 2 -
3 files changed, 51 insertions(+), 45 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index fe1412dc6..d099ed2b5 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -966,28 +966,6 @@ object ExprOps extends GenTreeOps[Expr] {
postMap(transform, applyRec = true)(expr)
}
- private def noCombiner(e: Expr, subCs: Seq[Unit]) = ()
- private def noTransformer[C](e: Expr, c: C) = (e, c)
-
- def simpleTransform(pre: Expr => Expr, post: Expr => Expr)(expr: Expr) = {
- val newPre = (e: Expr, c: Unit) => (pre(e), ())
- val newPost = (e: Expr, c: Unit) => (post(e), ())
-
- genericTransform[Unit](newPre, newPost, noCombiner)(())(expr)._1
- }
-
- def simplePreTransform(pre: Expr => Expr)(expr: Expr) = {
- val newPre = (e: Expr, c: Unit) => (pre(e), ())
-
- genericTransform[Unit](newPre, (_, _), noCombiner)(())(expr)._1
- }
-
- def simplePostTransform(post: Expr => Expr)(expr: Expr) = {
- val newPost = (e: Expr, c: Unit) => (post(e), ())
-
- genericTransform[Unit]((e,c) => (e, None), newPost, noCombiner)(())(expr)._1
- }
-
/** Simplify If expressions when the branch is predetermined by the path condition */
def simplifyTautologies(sf: SolverFactory[Solver])(expr : Expr) : Expr = {
val solver = SimpleSolverAPI(sf)
@@ -1080,27 +1058,15 @@ object ExprOps extends GenTreeOps[Expr] {
}
}
-
def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
CollectorWithPaths(f).traverse(expr)
}
- def patternSize(p: Pattern): Int = p match {
- case wp: WildcardPattern =>
- 1
- case _ =>
- 1 + p.binder.size + p.subPatterns.map(patternSize).sum
- }
-
- def formulaSize(e: Expr): Int = e match {
+ override def formulaSize(e: Expr): Int = e match {
case ml: MatchExpr =>
- formulaSize(ml.scrutinee) + ml.cases.map {
- case MatchCase(p, og, rhs) =>
- formulaSize(rhs) + og.map(formulaSize).getOrElse(0) + patternSize(p)
- }.sum
-
- case Deconstructor(es, _) =>
- es.map(formulaSize).sum+1
+ super.formulaSize(e) + ml.cases.map(cs => PatternOps.formulaSize(cs.pattern)).sum
+ case _ =>
+ super.formulaSize(e)
}
/** Returns true if the expression is deterministic / does not contain any [[purescala.Expressions.Choose Choose]] or [[purescala.Expressions.Hole Hole]]*/
@@ -1397,8 +1363,6 @@ object ExprOps extends GenTreeOps[Expr] {
}(apriori)
}
- import synthesis.Witnesses.Terminating
-
val res: Option[Apriori] = (t1, t2) match {
case (Variable(i1), Variable(i2)) =>
idHomo(i1, i2)(apriori)
diff --git a/src/main/scala/leon/purescala/GenTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
index 66a782973..435110c41 100644
--- a/src/main/scala/leon/purescala/GenTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -6,11 +6,22 @@ package purescala
import Common._
import utils._
+/** A type that pattern matches agains a type of [[Tree]] and extracts it subtrees,
+ * and a builder that reconstructs a tree of the same type from subtrees.
+ *
+ * @tparam SubTree The type of the tree
+ */
trait TreeExtractor[SubTree <: Tree] {
def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
}
+/** Generic tree traversals based on a deconstructor of a specific tree type
+ *
+ * @tparam SubTree The type of the tree
+ */
trait GenTreeOps[SubTree <: Tree] {
+
+ /** An extractor for [[SubTree]]*/
val Deconstructor: TreeExtractor[SubTree]
/* ========
@@ -231,7 +242,34 @@ trait GenTreeOps[SubTree <: Tree] {
rec(expr, init)
}
-
+
+ protected def noCombiner(e: SubTree, subCs: Seq[Unit]) = ()
+ protected def noTransformer[C](e: SubTree, c: C) = (e, c)
+
+ /** A [[genericTransform]] with the trivial combiner that returns () */
+ def simpleTransform(pre: SubTree => SubTree, post: SubTree => SubTree)(tree: SubTree) = {
+ val newPre = (e: SubTree, c: Unit) => (pre(e), ())
+ val newPost = (e: SubTree, c: Unit) => (post(e), ())
+
+ genericTransform[Unit](newPre, newPost, noCombiner)(())(tree)._1
+ }
+
+ /** A [[simpleTransform]] without a post-transformation */
+ def simplePreTransform(pre: SubTree => SubTree)(tree: SubTree) = {
+ val newPre = (e: SubTree, c: Unit) => (pre(e), ())
+
+ genericTransform[Unit](newPre, (_, _), noCombiner)(())(tree)._1
+ }
+
+ /** A [[simpleTransform]] without a pre-transformation */
+ def simplePostTransform(post: SubTree => SubTree)(tree: SubTree) = {
+ val newPost = (e: SubTree, c: Unit) => (post(e), ())
+
+ genericTransform[Unit]((e,c) => (e, None), newPost, noCombiner)(())(tree)._1
+ }
+
+
+
/** Pre-transformation of the tree, with a context value from "top-down".
*
* Takes a partial function of replacements.
@@ -316,7 +354,7 @@ trait GenTreeOps[SubTree <: Tree] {
/** Counts how many times the predicate holds in sub-expressions */
def count(matcher: SubTree => Int)(e: SubTree): Int = {
- fold[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 */
@@ -333,7 +371,13 @@ trait GenTreeOps[SubTree <: Tree] {
res
}
- /** Computes the depth of the expression's tree */
+ /** Computes the size of a tree */
+ def formulaSize(t: SubTree): Int = {
+ val Deconstructor(ts, _) = t
+ ts.map(formulaSize).sum + 1
+ }
+
+ /** Computes the depth of the tree */
def depth(e: SubTree): Int = {
fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
}
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 34db65c8a..bd95a8e4f 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -7,8 +7,6 @@ import Types._
import Definitions._
import Common._
import Expressions._
-import Extractors._
-import Constructors._
object TypeOps extends GenTreeOps[TypeTree] {
--
GitLab