Skip to content
Snippets Groups Projects
Commit 98328ea2 authored by Manos Koukoutos's avatar Manos Koukoutos Committed by Etienne Kneuss
Browse files

A slight improvement and a FIXME in tupleSelect

parent abefdb07
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/scala/leon/purescala/Constructors.scala
+ 5
− 2
View file @ 98328ea2
...@@ -15,12 +15,15 @@ object Constructors { ...@@ -15,12 +15,15 @@ object Constructors {
def tupleSelect(t: Expr, index: Int) = t match { def tupleSelect(t: Expr, index: Int) = t match {
case Tuple(es) => case Tuple(es) =>
// @mk FIXME: Notice tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x. This seems wrong.
es(index-1) es(index-1)
case _ if t.getType.isInstanceOf[TupleType] => case _ if t.getType.isInstanceOf[TupleType] =>
TupleSelect(t, index) TupleSelect(t, index)
case _ if (index == 1) =>
// For cases like tupleSelect(tupleWrap(Seq(x)), 1) -> x
t
case _ => case _ =>
if (index == 1) t sys.error(s"Trying to construct TupleSelect with non-tuple $t and index $index!=1")
else 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 { def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment