From 9cc63017c70fc9fb8011e3d9a410a06f491045a0 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 4 Mar 2015 16:09:13 +0100
Subject: [PATCH] Simplify needlessly complicated Extractors
---
.../scala/leon/purescala/Constructors.scala | 6 ++-
.../scala/leon/purescala/Extractors.scala | 45 ++++++++-----------
src/main/scala/leon/purescala/Trees.scala | 6 +--
3 files changed, 27 insertions(+), 30 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 04ba31d95..e757612b1 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -211,7 +211,11 @@ object Constructors {
if (els.isEmpty && defaultLength.isEmpty) EmptyArray(tpe)
else NonemptyArray(els, defaultLength)
}
-
+
+ def nonemptyArray(els: Seq[Expr], defaultLength: Option[(Expr, Expr)]): Expr = {
+ NonemptyArray(els.zipWithIndex.map{ _.swap }.toMap, defaultLength)
+ }
+
def finiteLambda(default: Expr, els: Seq[(Expr, Expr)], inputTypes: Seq[TypeTree]): Lambda = {
val args = inputTypes map { tpe => ValDef(FreshIdentifier("x", tpe, true)) }
if (els.isEmpty) {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 0d9508a58..ebd13edb7 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -100,47 +100,40 @@ object Extractors {
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, and))
case Or(args) => Some((args, or))
- case FiniteSet(args) =>
- val SetType(tpe) = expr.getType
- Some((args.toSeq, els => finiteSet(els.toSet, tpe)))
- case FiniteMap(args) => {
+ case NonemptySet(els) =>
+ Some(( els.toSeq, els => NonemptySet(els.toSet) ))
+ case NonemptyMap(args) => {
val subArgs = args.flatMap{case (k, v) => Seq(k, v)}
- val builder: (Seq[Expr]) => Expr = (as: Seq[Expr]) => {
+ val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]) : Seq[(Expr, Expr)] = kvs match {
case Seq(k, v, t@_*) =>
(k,v) +: rec(t)
case Seq() => Seq()
case _ => sys.error("odd number of key/value expressions")
}
- val MapType(keyType, valueType) = expr.getType
- finiteMap(rec(as), keyType, valueType)
+ NonemptyMap(rec(as))
}
Some((subArgs, builder))
}
- case FiniteMultiset(args) =>
- val MultisetType(tpe) = expr.getType
- Some((args, finiteMultiset(_, tpe)))
+ case NonemptyMultiset(args) =>
+ Some((args, NonemptyMultiset))
case ArrayUpdated(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) =>
ArrayUpdated(as(0), as(1), as(2))))
- case FiniteArray(elems, default, length) => {
- val fixedElems: Seq[(Int, Expr)] = elems.toSeq
- val all: Seq[Expr] = fixedElems.map(_._2) ++ default ++ Seq(length)
- Some((all, (as: Seq[Expr]) => {
- val ArrayType(tpe) = expr.getType
- val (newElems, newDefault, newSize) = default match {
- case None => (as.init, None, as.last)
- case Some(_) => (as.init.init, Some(as.init.last), as.last)
- }
- finiteArray(
- fixedElems.zip(newElems).map(p => (p._1._1, p._2)).toMap,
- newDefault map ((_, newSize)),
- tpe
- )
+ case NonemptyArray(elems, Some((default, length))) => {
+ val all = elems.map(_._2).toSeq :+ default :+ length
+ Some(( all, as => {
+ val l = as.length
+ nonemptyArray(as.take(l-2), Some( (as(l-2), as(l-1)) ) )
}))
}
-
+ case NonemptyArray(elems, None) =>
+ val all = elems.map(_._2).toSeq
+ Some(( all, finiteArray _ ))
case Tuple(args) => Some((args, Tuple))
- case IfExpr(cond, thenn, elze) => Some((Seq(cond, thenn, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))))
+ case IfExpr(cond, thenn, elze) => Some((
+ Seq(cond, thenn, elze),
+ (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))
+ ))
case MatchLike(scrut, cases, builder) => Some((
scrut +: cases.flatMap {
case SimpleCase(_, e) => Seq(e)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 059f2f00f..561e9c903 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -404,7 +404,7 @@ object Trees {
val getType = SetType(optionToType(leastUpperBound(elements.toSeq.map(_.getType)))).unveilUntyped
}
- case class EmptySet(tpe: TypeTree) extends Expr {
+ case class EmptySet(tpe: TypeTree) extends Expr with Terminal {
val getType = SetType(tpe).unveilUntyped
}
@@ -440,7 +440,7 @@ object Trees {
}
}
- case class EmptyMap(keyType: TypeTree, valueType: TypeTree) extends Expr {
+ case class EmptyMap(keyType: TypeTree, valueType: TypeTree) extends Expr with Terminal {
val getType = MapType(keyType, valueType).unveilUntyped
}
@@ -489,7 +489,7 @@ object Trees {
val getType = ArrayType(optionToType(leastUpperBound(elements map { _.getType}))).unveilUntyped
}
- case class EmptyArray(tpe: TypeTree) extends Expr {
+ case class EmptyArray(tpe: TypeTree) extends Expr with Terminal {
val getType = ArrayType(tpe).unveilUntyped
}
--
GitLab