From 9edf184021e4d80651f17a3595ee5bb03448fa6b Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 13 Apr 2016 17:48:48 +0200
Subject: [PATCH] test simple definition transformations
---
.../scala/leon/purescala/Extractors.scala | 10 +++---
.../solvers/InputCoverageSuite.scala | 6 +++-
.../leon/test/helpers/ExpressionsDSL.scala | 11 +++----
.../DefinitionTransformerSuite.scala | 33 +++++++++++++++++++
.../leon/unit/purescala/ExtractorsSuite.scala | 2 +-
5 files changed, 49 insertions(+), 13 deletions(-)
create mode 100644 src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 512cb6ebf..42cc07526 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -10,18 +10,18 @@ import Constructors._
object Extractors {
- /** Operator Extractor to extract any Expression in a consistent way
+ /** Operator Extractor to extract any Expression in a consistent way.
*
* You can match on any Leon Expr, and then get both a Seq[Expr] of
- * subterms and a builder fonction that take a Seq of subterm (os same
+ * subterms and a builder fonction that takes a Seq of subterms (of same
* length) and rebuild the original node.
*
* Those extractors do not perform any syntactic simplifications. They
- * rebuild the node using the case class (not the constructor that perform
- * simplifications). The rationals behind this decision is to have core
+ * rebuild the node using the case class (not the constructor, that performs
+ * simplifications). The rational behind this decision is to have core
* tools for performing tree transformations that are very predictable, if
* one need to simplify the tree, it is easy to write/call a simplification
- * function that would simply apply the constructor for each node.
+ * function that would simply apply the corresponding constructor for each node.
*/
object Operator extends TreeExtractor[Expr] {
def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
diff --git a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
index c1c29acbb..3c0376039 100644
--- a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
+++ b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
@@ -49,6 +49,10 @@ import leon.test.helpers.ExpressionsDSLVariables
import leon.purescala.Extractors._
class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables {
+
+ //override a because it comes from both Matchers and ExpressionsDSLVariables
+ override val a = null
+
val sources = List("""
|import leon.lang._
|import leon.collection._
@@ -315,4 +319,4 @@ class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with Sca
}
}
}
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
index 7c6de266e..7a760143c 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
@@ -9,9 +9,7 @@ import leon.purescala.Common._
import leon.purescala.Types._
import leon.purescala.Expressions._
-trait ExpressionsDSLVariables_a {
- val a = FreshIdentifier("a", Int32Type).toVariable
-}
+import scala.language.implicitConversions
trait ExpressionsDSLVariables {
val F = BooleanLiteral(false)
@@ -22,6 +20,7 @@ trait ExpressionsDSLVariables {
def i(x: Int) = IntLiteral(x)
def r(n: BigInt, d: BigInt) = FractionalLiteral(n, d)
+ val a = FreshIdentifier("a", Int32Type).toVariable
val b = FreshIdentifier("b", Int32Type).toVariable
val c = FreshIdentifier("c", Int32Type).toVariable
@@ -100,10 +99,10 @@ self: Assertions =>
}
}
-trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram with ExpressionsDSLVariables_a {
+trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram {
self: Assertions =>
-
-
+
+
implicit def int2IntLit(i: Int): IntLiteral = IntLiteral(i)
implicit def bigInt2IntegerLit(i: BigInt): InfiniteIntegerLiteral = InfiniteIntegerLiteral(i)
diff --git a/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala b/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala
new file mode 100644
index 000000000..88e9aea53
--- /dev/null
+++ b/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala
@@ -0,0 +1,33 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.unit.purescala
+
+import org.scalatest._
+
+import leon.test.helpers.ExpressionsDSL
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Extractors._
+import leon.purescala.DefinitionTransformer
+import leon.purescala.Definitions._
+import leon.purescala.Types._
+
+class DefinitionTransformerSuite extends FunSuite with ExpressionsDSL {
+
+ private val fd1 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
+ fd1.body = Some(x)
+
+ private val fd2 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
+ fd2.body = Some(Plus(x, bi(1)))
+
+ private val fd3 = new FunDef(FreshIdentifier("f1"), Seq(), Seq(ValDef(x.id)), IntegerType)
+ fd3.body = Some(Times(x, bi(1)))
+
+ test("transformation with no rewriting should not change FunDef") {
+ val tr1 = new DefinitionTransformer
+ assert(tr1.transform(fd1) === fd1)
+ assert(tr1.transform(fd2) === fd2)
+ assert(tr1.transform(fd3) === fd3)
+ }
+
+}
diff --git a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
index c09c39fe4..4e7c7d40a 100644
--- a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon.unit.xlang
+package leon.unit.purescala
import org.scalatest._
--
GitLab