From e129890aaa574e9ffadb429e0139537a800e68fe Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 19 Jun 2015 13:53:06 +0200
Subject: [PATCH] Use Constructors in Extractors, always
---
src/main/scala/leon/purescala/Constructors.scala | 7 +++----
src/main/scala/leon/purescala/Extractors.scala | 12 ++++++------
2 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index a64226761..78874c167 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -114,10 +114,7 @@ object Constructors {
MatchExpr(scrutinee, filtered)
else
Error(
- cases match {
- case Seq(hd, _*) => hd.rhs.getType
- case Seq() => Untyped
- },
+ cases.headOption.map{ _.rhs.getType }.getOrElse(Untyped),
"No case matches the scrutinee"
)
}
@@ -255,6 +252,8 @@ object Constructors {
def minus(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => lhs
case (_, IntLiteral(0)) => lhs
+ case (InfiniteIntegerLiteral(bi), _) if bi == 0 => UMinus(rhs)
+ case (IntLiteral(0), _) => BVUMinus(rhs)
case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Minus(lhs, rhs)
case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVMinus(lhs, rhs)
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ed0d630c3..117d8ff5a 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -47,9 +47,9 @@ object Extractors {
))
case Equals(t1,t2) => Some((t1,t2,Equals))
case Implies(t1,t2) => Some((t1,t2, implies))
- case Plus(t1,t2) => Some((t1,t2,Plus))
- case Minus(t1,t2) => Some((t1,t2,Minus))
- case Times(t1,t2) => Some((t1,t2,Times))
+ case Plus(t1,t2) => Some((t1,t2,plus))
+ case Minus(t1,t2) => Some((t1,t2,minus))
+ case Times(t1,t2) => Some((t1,t2,times))
case Division(t1,t2) => Some((t1,t2,Division))
case Remainder(t1,t2) => Some((t1,t2,Remainder))
case Modulo(t1,t2) => Some((t1,t2,Modulo))
@@ -57,9 +57,9 @@ object Extractors {
case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
- case BVPlus(t1,t2) => Some((t1,t2,BVPlus))
- case BVMinus(t1,t2) => Some((t1,t2,BVMinus))
- case BVTimes(t1,t2) => Some((t1,t2,BVTimes))
+ case BVPlus(t1,t2) => Some((t1,t2,plus))
+ case BVMinus(t1,t2) => Some((t1,t2,minus))
+ case BVTimes(t1,t2) => Some((t1,t2,times))
case BVDivision(t1,t2) => Some((t1,t2,BVDivision))
case BVRemainder(t1,t2) => Some((t1,t2,BVRemainder))
case BVAnd(t1,t2) => Some((t1,t2,BVAnd))
--
GitLab