From 2848b2911740ba56b89ebb3393136fe72520ebac Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 10 May 2016 19:10:12 +0200
Subject: [PATCH] Bug fix etc
---
src/main/scala/leon/purescala/ExprOps.scala | 5 ++---
src/main/scala/leon/purescala/Expressions.scala | 4 ++--
src/main/scala/leon/purescala/TypeOps.scala | 2 +-
src/main/scala/leon/purescala/Types.scala | 2 +-
4 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 24e54b367..8e778b4d9 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -427,9 +427,8 @@ object ExprOps extends GenTreeOps[Expr] {
// Untuple
case Let(id, Tuple(es), b) =>
- val tps = es map (_.getType)
- val ids = tps.zipWithIndex.map {
- case (tp, ind) => FreshIdentifier(id + (ind + 1).toString, tp, true)
+ val ids = es.zipWithIndex.map { case (e, ind) =>
+ FreshIdentifier(id + (ind + 1).toString, e.getType, true)
}
val theMap: Map[Expr, Expr] = es.zip(ids).zipWithIndex.map {
case ((e, subId), ind) => TupleSelect(Variable(id), ind + 1) -> Variable(subId)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 6620ebb6a..3b9e396b0 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -823,8 +823,8 @@ object Expressions {
require(index >= 1)
val getType = tuple.getType match {
- case TupleType(ts) =>
- require(index <= ts.size)
+ case tp@TupleType(ts) =>
+ require(index <= ts.size, s"Got index $index for '$tuple' of type '$tp")
ts(index - 1)
case _ =>
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index e43c882c2..ac28c93cb 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -122,7 +122,7 @@ object TypeOps extends GenTreeOps[TypeTree] {
prefix.lastOption
- case (TupleType(args1), TupleType(args2)) =>
+ case (TupleType(args1), TupleType(args2)) if args1.size == args2.size =>
val args = (args1 zip args2).map(p => leastUpperBound(p._1, p._2))
if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 6518d65fb..f59761913 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -138,7 +138,7 @@ object Types {
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)))
- case TupleType(ts) => Some((ts, Constructors.tupleTypeWrap _))
+ case TupleType(ts) => Some((ts, TupleType))
case ArrayType(t) => Some((Seq(t), ts => ArrayType(ts.head)))
case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
case BagType(t) => Some((Seq(t), ts => BagType(ts.head)))
--
GitLab