From 2d0578dd1552595ed10dd46c7adf3ad08dcc2948 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 3 May 2012 16:34:08 +0200
Subject: [PATCH] basic support for array working
---
src/main/scala/leon/ArrayTransformation.scala | 8 ++++----
src/main/scala/leon/purescala/PrettyPrinter.scala | 14 +++++++-------
2 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 9c5bf63c0..06c31189a 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 8a976a826..a82ad435f 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) => {
--
GitLab