diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala index 9c5bf63c0f9ceb283bd10a322367d412023ad739..06c31189a731514afbf9ee27c74cfea323ae0622 100644 --- a/src/main/scala/leon/ArrayTransformation.scala +++ b/src/main/scala/leon/ArrayTransformation.scala @@ -31,7 +31,7 @@ object ArrayTransformation extends Pass { case sel@ArraySelect(a, i) => { val ar = transform(a) val ir = transform(i) - val length = TupleSelect(ar, 2) + val length = TupleSelect(ar, 2).setType(Int32Type) IfExpr( And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)), ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType), @@ -43,12 +43,12 @@ object ArrayTransformation extends Pass { val ir = transform(i) val vr = transform(v) val Variable(id) = ar - val length = TupleSelect(ar, 2) - val array = TupleSelect(ar, 1) + val length = TupleSelect(ar, 2).setType(Int32Type) + val array = TupleSelect(ar, 1).setType(ArrayType(v.getType)) //val Tuple(Seq(Variable(id), length)) = ar IfExpr( And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)), - Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)), + Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v).setType(array.getType), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)), Error("Array out of bound access").setType(Int32Type) ).setType(Int32Type) } diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index 8a976a826439459e56988feeea2eee6b6f4fc6f9..a82ad435fe461ba4445e42b273745f1b660b8015 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -249,33 +249,33 @@ object PrettyPrinter { nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl) nsb } - case ArrayFill(size, v) => { + case fill@ArrayFill(size, v) => { sb.append("Array.fill(") pp(size, sb, lvl) sb.append(")(") pp(v, sb, lvl) - sb.append(")") + sb.append(")#" + fill.getType) } - case ArraySelect(ar, i) => { + case sel@ArraySelect(ar, i) => { pp(ar, sb, lvl) sb.append("(") pp(i, sb, lvl) - sb.append(")") + sb.append(")#" + sel.getType) } - case ArrayUpdate(ar, i, v) => { + case up@ArrayUpdate(ar, i, v) => { pp(ar, sb, lvl) sb.append("(") pp(i, sb, lvl) sb.append(") = ") pp(v, sb, lvl) } - case ArrayUpdated(ar, i, v) => { + case up@ArrayUpdated(ar, i, v) => { pp(ar, sb, lvl) sb.append(".updated(") pp(i, sb, lvl) sb.append(", ") pp(v, sb, lvl) - sb.append(")") + sb.append(")#" + up.getType) } case Distinct(exprs) => {