diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 304f242e7ed0cd814a506d309d80b26ed3a4a939..f331a1c8f3b4f298783baf0b506772abe50a7ed2 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -10,11 +10,24 @@ import Constructors._
object Extractors {
+ /** 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
+ * 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
+ * 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.
+ */
object Operator extends TreeExtractor[Expr] {
def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
/* Unary operators */
case Not(t) =>
- Some((Seq(t), (es: Seq[Expr]) => not(es.head)))
+ Some((Seq(t), (es: Seq[Expr]) => Not(es.head)))
case Choose(expr) =>
Some((Seq(expr), (es: Seq[Expr]) => Choose(es.head)))
case UMinus(t) =>
@@ -40,11 +53,11 @@ object Extractors {
case SetCardinality(t) =>
Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
case CaseClassSelector(cd, e, sel) =>
- Some((Seq(e), (es: Seq[Expr]) => caseClassSelector(cd, es.head, sel)))
+ Some((Seq(e), (es: Seq[Expr]) => CaseClassSelector(cd, es.head, sel)))
case IsInstanceOf(e, ct) =>
Some((Seq(e), (es: Seq[Expr]) => IsInstanceOf(es.head, ct)))
case AsInstanceOf(e, ct) =>
- Some((Seq(e), (es: Seq[Expr]) => asInstOf(es.head, ct)))
+ Some((Seq(e), (es: Seq[Expr]) => AsInstanceOf(es.head, ct)))
case TupleSelect(t, i) =>
Some((Seq(t), (es: Seq[Expr]) => TupleSelect(es.head, i)))
case ArrayLength(a) =>
@@ -79,15 +92,15 @@ object Extractors {
}
))
case Equals(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => equality(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => Equals(es(0), es(1)))
case Implies(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => implies(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => Implies(es(0), es(1)))
case Plus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => plus(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => Plus(es(0), es(1)))
case Minus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => minus(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => Minus(es(0), es(1)))
case Times(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => times(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => Times(es(0), es(1)))
case Division(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => Division(es(0), es(1)))
case Remainder(t1, t2) =>
@@ -103,11 +116,11 @@ object Extractors {
case GreaterEquals(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => GreaterEquals(es(0), es(1)))
case BVPlus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => plus(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => BVPlus(es(0), es(1)))
case BVMinus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => minus(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => BVMinus(es(0), es(1)))
case BVTimes(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => times(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => BVTimes(es(0), es(1)))
case BVDivision(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => BVDivision(es(0), es(1)))
case BVRemainder(t1, t2) =>
@@ -125,11 +138,11 @@ object Extractors {
case BVLShiftRight(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => BVLShiftRight(es(0), es(1)))
case RealPlus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => plus(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => RealPlus(es(0), es(1)))
case RealMinus(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => minus(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => RealMinus(es(0), es(1)))
case RealTimes(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => times(es(0), es(1)))
+ Some(Seq(t1, t2), (es: Seq[Expr]) => RealTimes(es(0), es(1)))
case RealDivision(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => RealDivision(es(0), es(1)))
case StringConcat(t1, t2) =>
@@ -180,8 +193,8 @@ object Extractors {
case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, as => MethodInvocation(as.head, cd, tfd, as.tail)))
case fa @ Application(caller, args) => Some(caller +: args, as => Application(as.head, as.tail))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
- case And(args) => Some((args, and))
- case Or(args) => Some((args, or))
+ case And(args) => Some((args, es => And(es)))
+ case Or(args) => Some((args, es => Or(es)))
case SubString(t1, a, b) => Some((t1::a::b::Nil, es => SubString(es(0), es(1), es(2))))
case FiniteSet(els, base) =>
Some((els.toSeq, els => FiniteSet(els.toSet, base)))
@@ -228,7 +241,7 @@ object Extractors {
elsOrdered,
es => finiteArray(indexes.zip(es).toMap, None, tpe)
))
- case Tuple(args) => Some((args, tupleWrap))
+ case Tuple(args) => Some((args, es => Tuple(es)))
case IfExpr(cond, thenn, elze) => Some((
Seq(cond, thenn, elze),
{ case Seq(c, t, e) => IfExpr(c, t, e) }
@@ -242,7 +255,7 @@ object Extractors {
case GuardedCase(b, _, _) => i += 2; GuardedCase(b, es(i - 2), es(i - 1))
}
- matchExpr(es.head, newcases).copiedFrom(m)
+ MatchExpr(es.head, newcases)
}
))
case Passes(in, out, cases) => Some((
@@ -255,7 +268,7 @@ object Extractors {
case GuardedCase(b, _, _) => i += 2; GuardedCase(b, es(i - 2), es(i - 1))
}
- passes(in, out, newcases)
+ Passes(in, out, newcases)
}
}
))
diff --git a/src/test/scala/leon/integration/grammars/SimilarToSuite.scala b/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
index b61d6cb942348b8b6821c0a915e8e3415ee3b987..7f4f625be8bee3fcea8fef8f16ce6b973d49ed5f 100644
--- a/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
+++ b/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
@@ -227,8 +227,8 @@ class SimilarToSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
merge(Node(v1, Leaf(), Leaf()), h1)
),
(List(h1, h2),
- GreaterThan(rank(h1), Plus(rank(h2), bi(1))),
- GreaterThan(rank(h1), rank(h2))
+ GreaterThan(rank(h1), Plus(rank(h2), bi(42))),
+ GreaterThan(rank(h1), Minus(Plus(rank(h2), bi(42)), bi(1)))
)
)
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
index 91b77284cc16518a4b86e0bdcb5ad7e98230061f..7c6de266e523f46f94281a556dda2f2d691e783a 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
@@ -103,4 +103,8 @@ self: Assertions =>
trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram with ExpressionsDSLVariables_a {
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/ExtractorsSuite.scala b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8c99385b44d688c2c190a5cbc182b82d16a533de
--- /dev/null
+++ b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
@@ -0,0 +1,41 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.unit.xlang
+
+import org.scalatest._
+
+import leon.test.helpers.ExpressionsDSL
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Extractors._
+
+class ExtractorsSuite extends FunSuite with ExpressionsDSL {
+
+ test("Extractors do not simplify basic arithmetic") {
+ val e1 = BVPlus(1, 1)
+ val e2 = e1 match {
+ case Operator(es, builder) => builder(es)
+ }
+ assert(e1 === e2)
+
+ val e3 = Times(x, BigInt(1))
+ val e4 = e3 match {
+ case Operator(es, builder) => builder(es)
+ }
+ assert(e3 === e4)
+ }
+
+ ignore("Extractors of NonemptyArray with sparse elements") {
+ val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10))))
+
+ val a2 = a1 match {
+ case Operator(es, builder) => {
+ assert(es === Seq(x, y, z, InfiniteIntegerLiteral(0), InfiniteIntegerLiteral(10)))
+ builder(es)
+ }
+ }
+
+ assert(a2 === a1)
+ }
+
+}