From 7df6ae86122f720f1b12b2fc4ff01afe8fd45d2e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 20 Nov 2015 16:13:18 +0100
Subject: [PATCH] Fix extraction of empty arrays etc.
---
src/main/scala/leon/purescala/Constructors.scala | 6 +++---
src/main/scala/leon/purescala/Extractors.scala | 11 ++++++++---
2 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 728b602f9..7625eddf8 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -161,7 +161,7 @@ object Constructors {
BooleanLiteral(true)
}
}
- /** $encodingof `... match { ... }` but simplified if possible. Throws an error if no case can match the scrutined expression.
+ /** $encodingof `... match { ... }` but simplified if possible. Simplifies to [[Error]] if no case can match the scrutined expression.
* @see [[purescala.Expressions.MatchExpr MatchExpr]]
*/
def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : Expr ={
@@ -249,8 +249,8 @@ object Constructors {
/** $encodingof Simplified `Array(...)` (array length defined at compile-time)
* @see [[purescala.Expressions.NonemptyArray NonemptyArray]]
*/
- def finiteArray(els: Seq[Expr]): Expr = {
- require(els.nonEmpty)
+ def finiteArray(els: Seq[Expr], tpe: TypeTree = Untyped): Expr = {
+ require(els.nonEmpty || tpe != Untyped)
finiteArray(els, None, Untyped) // Untyped is not correct, but will not be used anyway
}
/** $encodingof Simplified `Array[...](...)` (array length and default element defined at run-time) with type information
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index cd57d2187..1337e74d0 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -181,9 +181,14 @@ object Extractors {
val l = as.length
nonemptyArray(as.take(l - 2), Some((as(l - 2), as(l - 1))))
}))
- case NonemptyArray(elems, None) =>
- val all = elems.values.toSeq
- Some((all, finiteArray))
+ case na@NonemptyArray(elems, None) =>
+ val ArrayType(tpe) = na.getType
+ val (indexes, elsOrdered) = elems.toSeq.unzip
+
+ Some((
+ elsOrdered,
+ es => finiteArray(indexes.zip(es).toMap, None, tpe)
+ ))
case Tuple(args) => Some((args, tupleWrap))
case IfExpr(cond, thenn, elze) => Some((
Seq(cond, thenn, elze),
--
GitLab