diff --git a/src/main/scala/inox/ast/Constructors.scala b/src/main/scala/inox/ast/Constructors.scala index 5262b7355cd8434b4bd7d70aebf86fd6a2990246..314cc16f21055932b40283009e3899da14a5d475 100644 --- a/src/main/scala/inox/ast/Constructors.scala +++ b/src/main/scala/inox/ast/Constructors.scala @@ -20,11 +20,7 @@ trait Constructors { self: Trees => def tupleWrap(es: Seq[Expr]): Expr = es match { case Seq() => UnitLiteral() case Seq(elem) => elem - case more => - more.zipWithIndex.collect { case (TupleSelect(e, idx), i) if idx == i + 1 => e } match { - case ls @ (e +: es) if ls.size == more.size && es.forall(_ == e) => e - case _ => Tuple(more) - } + case more => Tuple(more) } /** Wraps the sequence of types as a tuple. If the sequence contains a single type, it is returned instead. diff --git a/src/main/scala/inox/transformers/SimplifierWithPC.scala b/src/main/scala/inox/transformers/SimplifierWithPC.scala index c063783d24a35c7ae93d3eaf25cd608a21901a6a..f98300f14aa378a80037738fec5269b563c3d7e4 100644 --- a/src/main/scala/inox/transformers/SimplifierWithPC.scala +++ b/src/main/scala/inox/transformers/SimplifierWithPC.scala @@ -267,12 +267,23 @@ trait SimplifierWithPC extends Transformer { self => case n @ Not(e) => simplifyAndCons(Seq(e), path, es => not(es.head).copiedFrom(n)) case Equals(l, r) => simplifyAndCons(Seq(l, r), path, es => equality(es(0), es(1)).copiedFrom(e)) - case Tuple(es) => simplifyAndCons(es, path, es => tupleWrap(es).copiedFrom(e)) case UMinus(t) => simplifyAndCons(Seq(t), path, es => uminus(es.head).copiedFrom(e)) case Plus(l, r) => simplifyAndCons(Seq(l, r), path, es => plus(es(0), es(1)).copiedFrom(e)) case Minus(l, r) => simplifyAndCons(Seq(l, r), path, es => minus(es(0), es(1)).copiedFrom(e)) case Times(l, r) => simplifyAndCons(Seq(l, r), path, es => times(es(0), es(1)).copiedFrom(e)) + case Tuple(es) => + val (res, pes) = es.map(simplify(_, path)).unzip + (res.zipWithIndex.collect { case (TupleSelect(e, idx), i) if idx == i + 1 => e } match { + case ls @ (x +: xs) if ls.size == es.size && xs.forall(_ == x) => + x.getType match { + case TupleType(ts) if ts.size == es.size => x + case _ => Tuple(es) + } + case _ => Tuple(es) + }, + pes.foldLeft(false)(_ || _)) + case Forall(params, body) => simplifyAndCons(Seq(body), path withBounds params, es => simpForall(params, es.head).copiedFrom(e))