basic support for array working

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)
     }

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) => {