From 9566dcff6d0ee365565d9da635d5c463ce943935 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 12 May 2016 18:46:48 +0200
Subject: [PATCH] Fix bug in conditionForPattern when handling unapplyPattern
Also add couple of utility functions
---
src/main/scala/leon/purescala/ExprOps.scala | 17 +++++++----------
src/main/scala/leon/purescala/Expressions.scala | 3 +++
src/main/scala/leon/purescala/Path.scala | 5 ++++-
3 files changed, 14 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 96a5605d2..63afebf48 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -692,22 +692,19 @@ object ExprOps extends GenTreeOps[Expr] {
assert(cct.classDef.fields.size == subps.size)
val pairs = cct.classDef.fields.map(_.id).toList zip subps.toList
val subTests = pairs.map(p => rec(caseClassSelector(cct, in, p._1), p._2))
- val together = subTests.foldLeft(bind(ob, in))(_ merge _)
- Path(IsInstanceOf(in, cct)) merge together
+ Path(IsInstanceOf(in, cct)) merge bind(ob, in) merge subTests
case TuplePattern(ob, subps) =>
val TupleType(tpes) = in.getType
assert(tpes.size == subps.size)
- val subTests = subps.zipWithIndex.map{case (p, i) => rec(tupleSelect(in, i+1, subps.size), p)}
- subTests.foldLeft(bind(ob, in))(_ merge _)
+ val subTests = subps.zipWithIndex.map {
+ case (p, i) => rec(tupleSelect(in, i+1, subps.size), p)
+ }
+ bind(ob, in) merge subTests
case up @ UnapplyPattern(ob, fd, subps) =>
- def someCase(e: Expr) = {
- // In the case where unapply returns a Some, it is enough that the subpatterns match
- val subTests = unwrapTuple(e, subps.size) zip subps map { case (ex, p) => rec(ex, p) }
- subTests.foldLeft(Path.empty)(_ merge _).toClause
- }
- Path(up.patternMatch(in, BooleanLiteral(false), someCase).setPos(in)) merge bind(ob, in)
+ val subs = unwrapTuple(up.get(in), subps.size).zip(subps) map (rec _).tupled
+ bind(ob, in) withCond up.isSome(in) merge subs
case LiteralPattern(ob, lit) =>
Path(Equals(in, lit)) merge bind(ob, in)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 8b8f0e300..924949a56 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -358,6 +358,9 @@ object Expressions {
FunctionInvocation(unapplyFun, Seq(scrut)),
someValue.id
)
+
+ def isSome(scrut: Expr) = IsInstanceOf(FunctionInvocation(unapplyFun, Seq(scrut)), someType)
+
}
// Extracts without taking care of the binder. (contrary to Extractos.Pattern)
diff --git a/src/main/scala/leon/purescala/Path.scala b/src/main/scala/leon/purescala/Path.scala
index 77eab7b83..d6e85d938 100644
--- a/src/main/scala/leon/purescala/Path.scala
+++ b/src/main/scala/leon/purescala/Path.scala
@@ -58,7 +58,10 @@ class Path private[purescala](
def --(ids: Set[Identifier]) = new Path(elements.filterNot(_.left.exists(p => ids(p._1))))
/** Appends `that` path at the end of `this` */
- def merge(that: Path) = new Path(elements ++ that.elements)
+ def merge(that: Path): Path = new Path(elements ++ that.elements)
+
+ /** Appends `those` paths at the end of `this` */
+ def merge(those: Traversable[Path]): Path = those.foldLeft(this)(_ merge _)
/** Transforms all expressions inside the path
*
--
GitLab