From 045a7274de2c8071459919ce5884060430b44ac6 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 13 Apr 2016 16:42:56 +0200
Subject: [PATCH] fix extractors for Arrays
---
src/main/scala/leon/purescala/Extractors.scala | 8 +++++---
.../scala/leon/unit/purescala/ExtractorsSuite.scala | 13 ++++++++++---
2 files changed, 15 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index f331a1c8f..512cb6ebf 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -228,10 +228,12 @@ object Extractors {
(as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))
))
case NonemptyArray(elems, Some((default, length))) =>
- val all = elems.values.toSeq :+ default :+ length
+ val elemsSeq: Seq[(Int, Expr)] = elems.toSeq
+ val all = elemsSeq.map(_._2) :+ default :+ length
Some((all, as => {
val l = as.length
- nonemptyArray(as.take(l - 2), Some((as(l - 2), as(l - 1))))
+ NonemptyArray(elemsSeq.map(_._1).zip(as.take(l - 2)).toMap,
+ Some((as(l - 2), as(l - 1))))
}))
case na @ NonemptyArray(elems, None) =>
val ArrayType(tpe) = na.getType
@@ -239,7 +241,7 @@ object Extractors {
Some((
elsOrdered,
- es => finiteArray(indexes.zip(es).toMap, None, tpe)
+ es => NonemptyArray(indexes.zip(es).toMap, None)
))
case Tuple(args) => Some((args, es => Tuple(es)))
case IfExpr(cond, thenn, elze) => Some((
diff --git a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
index 8c99385b4..c09c39fe4 100644
--- a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
@@ -25,17 +25,24 @@ class ExtractorsSuite extends FunSuite with ExpressionsDSL {
assert(e3 === e4)
}
- ignore("Extractors of NonemptyArray with sparse elements") {
+ test("Extractors of NonemptyArray with sparse elements") {
val a1 = NonemptyArray(Map(0 -> x, 3 -> y, 5 -> z), Some((BigInt(0), BigInt(10))))
-
val a2 = a1 match {
case Operator(es, builder) => {
assert(es === Seq(x, y, z, InfiniteIntegerLiteral(0), InfiniteIntegerLiteral(10)))
builder(es)
}
}
-
assert(a2 === a1)
+
+ val a3 = NonemptyArray(Map(0 -> x, 1 -> y, 2 -> z), None)
+ val a4 = a3 match {
+ case Operator(es, builder) => {
+ assert(es === Seq(x, y, z))
+ builder(es)
+ }
+ }
+ assert(a3 === a4)
}
}
--
GitLab