From 54e486c39035118de55ea2a72c05d0da4d197536 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 6 Apr 2016 11:33:12 +0200
Subject: [PATCH] Refactor TreeOps a little
---
src/main/scala/leon/purescala/ExprOps.scala | 14 +++++++-------
src/main/scala/leon/purescala/Expressions.scala | 6 ++++--
src/main/scala/leon/purescala/Extractors.scala | 2 +-
.../{SubTreeOps.scala => GenTreeOps.scala} | 12 +++++-------
src/main/scala/leon/purescala/TypeOps.scala | 5 ++++-
src/main/scala/leon/purescala/Types.scala | 2 +-
6 files changed, 22 insertions(+), 19 deletions(-)
rename src/main/scala/leon/purescala/{SubTreeOps.scala => GenTreeOps.scala} (97%)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b91744794..1d1b03ff9 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -20,19 +20,19 @@ import scala.language.implicitConversions
*
* The generic operations lets you apply operations on a whole tree
* expression. You can look at:
- * - [[SubTreeOps.fold foldRight]]
- * - [[SubTreeOps.preTraversal preTraversal]]
- * - [[SubTreeOps.postTraversal postTraversal]]
- * - [[SubTreeOps.preMap preMap]]
- * - [[SubTreeOps.postMap postMap]]
- * - [[SubTreeOps.genericTransform genericTransform]]
+ * - [[GenTreeOps.fold foldRight]]
+ * - [[GenTreeOps.preTraversal preTraversal]]
+ * - [[GenTreeOps.postTraversal postTraversal]]
+ * - [[GenTreeOps.preMap preMap]]
+ * - [[GenTreeOps.postMap postMap]]
+ * - [[GenTreeOps.genericTransform genericTransform]]
*
* These operations usually take a higher order function that gets applied to the
* expression tree in some strategy. They provide an expressive way to build complex
* operations on Leon expressions.
*
*/
-object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
+object ExprOps extends { val Deconstructor = Operator } with GenTreeOps[Expr] {
/** Replaces bottom-up sub-identifiers by looking up for them in a map */
def replaceFromIDs(substs: Map[Identifier, Expr], expr: Expr) : Expr = {
postMap({
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index a975aa91a..7550b0304 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -361,7 +361,7 @@ object Expressions {
}
// Extracts without taking care of the binder. (contrary to Extractos.Pattern)
- object PatternExtractor extends SubTreeOps.Extractor[Pattern] {
+ object PatternExtractor extends TreeExtractor[Pattern] {
def unapply(e: Pattern): Option[(Seq[Pattern], (Seq[Pattern]) => Pattern)] = e match {
case (_: InstanceOfPattern) | (_: WildcardPattern) | (_: LiteralPattern[_]) =>
Some(Seq(), es => e)
@@ -375,7 +375,9 @@ object Expressions {
}
}
- object PatternOps extends { val Deconstructor = PatternExtractor } with SubTreeOps[Pattern]
+ object PatternOps extends GenTreeOps[Pattern] {
+ val Deconstructor = PatternExtractor
+ }
/** Symbolic I/O examples as a match/case.
* $encodingof `out == (in match { cases; case _ => out })`
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ea5b30430..304f242e7 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -10,7 +10,7 @@ import Constructors._
object Extractors {
- object Operator extends SubTreeOps.Extractor[Expr] {
+ object Operator extends TreeExtractor[Expr] {
def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
/* Unary operators */
case Not(t) =>
diff --git a/src/main/scala/leon/purescala/SubTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
similarity index 97%
rename from src/main/scala/leon/purescala/SubTreeOps.scala
rename to src/main/scala/leon/purescala/GenTreeOps.scala
index 39ed1a455..bcf6002d1 100644
--- a/src/main/scala/leon/purescala/SubTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -6,13 +6,12 @@ package purescala
import Common._
import utils._
-object SubTreeOps {
- trait Extractor[SubTree <: Tree] {
- def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
- }
+trait TreeExtractor[SubTree <: Tree] {
+ def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
}
-trait SubTreeOps[SubTree <: Tree] {
- val Deconstructor: SubTreeOps.Extractor[SubTree]
+
+trait GenTreeOps[SubTree <: Tree] {
+ val Deconstructor: TreeExtractor[SubTree]
/* ========
* Core API
@@ -208,7 +207,6 @@ trait SubTreeOps[SubTree <: Tree] {
the current node
* @param init the initial value
* @param expr the expression on which to apply the transform
- *
* @see [[simpleTransform]]
* @see [[simplePreTransform]]
* @see [[simplePostTransform]]
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 1a33a0883..e0ba119b7 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -10,7 +10,10 @@ import Expressions._
import Extractors._
import Constructors._
-object TypeOps extends { val Deconstructor = NAryType } with SubTreeOps[TypeTree] {
+object TypeOps extends GenTreeOps[TypeTree] {
+
+ val Deconstructor = NAryType
+
def typeDepth(t: TypeTree): Int = t match {
case NAryType(tps, builder) => 1 + (0 +: (tps map typeDepth)).max
}
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 1536395e9..75693c375 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -136,7 +136,7 @@ object Types {
case class AbstractClassType(classDef: AbstractClassDef, tps: Seq[TypeTree]) extends ClassType
case class CaseClassType(classDef: CaseClassDef, tps: Seq[TypeTree]) extends ClassType
- object NAryType extends SubTreeOps.Extractor[TypeTree] {
+ object NAryType extends TreeExtractor[TypeTree] {
def unapply(t: TypeTree): Option[(Seq[TypeTree], Seq[TypeTree] => TypeTree)] = t match {
case CaseClassType(ccd, ts) => Some((ts, ts => CaseClassType(ccd, ts)))
case AbstractClassType(acd, ts) => Some((ts, ts => AbstractClassType(acd, ts)))
--
GitLab