From 99d4cef72bd1224d1c4e13298a28b4c6baea521e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 4 Dec 2014 16:27:35 +0100
Subject: [PATCH] Make some tree constructors more robust
---
.../scala/leon/purescala/Constructors.scala | 26 ++++++++++++++++---
.../scala/leon/purescala/Extractors.scala | 4 +--
src/main/scala/leon/purescala/TreeOps.scala | 4 +--
src/main/scala/leon/purescala/Trees.scala | 1 -
4 files changed, 26 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 6d4d1575e..9d69aab80 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -59,12 +59,30 @@ object Constructors {
def gives(scrutinee : Expr, cases : Seq[MatchCase]) : Gives =
Gives(scrutinee, filterCases(scrutinee.getType, cases))
- def passes(in : Expr, out : Expr, cases : Seq[MatchCase]) : Passes = {
- Passes(in, out, filterCases(in.getType, cases))
+ def passes(in : Expr, out : Expr, cases : Seq[MatchCase]): Expr = {
+ val resultingCases = filterCases(in.getType, cases)
+ if (resultingCases.nonEmpty) {
+ Passes(in, out, resultingCases)
+ } else {
+ BooleanLiteral(true)
+ }
}
- def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : MatchExpr =
- MatchExpr(scrutinee, filterCases(scrutinee.getType, cases))
+ def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : Expr ={
+ val filtered = filterCases(scrutinee.getType, cases)
+ if (filtered.nonEmpty)
+ MatchExpr(scrutinee, filtered)
+ else
+ Error(
+ cases match {
+ case Seq(hd, _*) => hd.rhs.getType
+ case Seq() => Untyped
+ },
+ "No case matches the scrutinee"
+ )
+ }
+
+
def and(exprs: Expr*): Expr = {
val flat = exprs.flatMap(_ match {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 5ee398048..3ba2da4f3 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -226,7 +226,7 @@ object Extractors {
}
object MatchLike {
- def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => MatchLike)] = {
+ def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => Expr)] = {
Option(m) map { m =>
(m.scrutinee, m.cases, m match {
case _ : MatchExpr => matchExpr
@@ -234,7 +234,7 @@ object Extractors {
case _ : Passes =>
(s, cases) => {
val Tuple(Seq(in, out)) = s
- passes(in,out,cases)
+ passes(in, out, cases)
}
})
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 33d2b564c..56249605f 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -2332,10 +2332,10 @@ object TreeOps {
Seq(c)
}}
- var finalMatch = matchExpr(scrutinee, List(newCases.head))
+ var finalMatch = matchExpr(scrutinee, List(newCases.head)).asInstanceOf[MatchExpr]
for (toAdd <- newCases.tail if !isMatchExhaustive(finalMatch)) {
- finalMatch = matchExpr(scrutinee, finalMatch.cases :+ toAdd)
+ finalMatch = matchExpr(scrutinee, finalMatch.cases :+ toAdd).asInstanceOf[MatchExpr]
}
finalMatch
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 88fd34b3e..778306cba 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -192,7 +192,6 @@ object Trees {
}
case class Gives(scrutinee: Expr, cases : Seq[MatchCase]) extends MatchLike {
- require(cases.nonEmpty)
def asIncompleteMatch = {
val theHole = SimpleCase(WildcardPattern(None), Hole(this.getType, Seq()))
MatchExpr(scrutinee, cases :+ theHole)
--
GitLab