From 98328ea2315f2e65bb5f18a7ebb21f0fe6da9033 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Sun, 1 Mar 2015 16:57:22 +0100
Subject: [PATCH] A slight improvement and a FIXME in tupleSelect
---
src/main/scala/leon/purescala/Constructors.scala | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index fd1058926..f82ea8a6d 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -15,12 +15,15 @@ object Constructors {
def tupleSelect(t: Expr, index: Int) = t match {
case Tuple(es) =>
+ // @mk FIXME: Notice tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x. This seems wrong.
es(index-1)
case _ if t.getType.isInstanceOf[TupleType] =>
TupleSelect(t, index)
+ case _ if (index == 1) =>
+ // For cases like tupleSelect(tupleWrap(Seq(x)), 1) -> x
+ t
case _ =>
- if (index == 1) t
- else sys.error(s"Trying to construct TupleSelect with non-tuple $t and index $index!=1")
+ sys.error(s"Trying to construct TupleSelect with non-tuple $t and index $index!=1")
}
def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
--
GitLab