From 925c2afbff656e91e2918a8530e8862d15e4c1d1 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 3 Nov 2014 15:25:05 +0100
Subject: [PATCH] Handle LiteralPatterns correctly everywhere
---
.../leon/evaluators/RecursiveEvaluator.scala | 2 ++
src/main/scala/leon/purescala/TreeOps.scala | 25 +++++++++++++++++++
.../scala/leon/purescala/TypeTreeOps.scala | 4 +++
3 files changed, 31 insertions(+)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index cb3278c09..58a86ac6a 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -477,6 +477,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
} else {
None
}
+ case (LiteralPattern(ob, l1) , l2 : Literal[_]) if l1 == l2 =>
+ Some(obind(ob,l1))
case _ => None
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 6e1a2d041..ee74c46b6 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1646,6 +1646,10 @@ object TreeOps {
} else {
(false, Map())
}
+
+ case (LiteralPattern(ob1, lit1), LiteralPattern(ob2,lit2)) =>
+ (ob1.size == ob2.size && lit1 == lit2, (ob1 zip ob2).toMap)
+
case _ =>
(false, Map())
}
@@ -1789,6 +1793,27 @@ object TreeOps {
}
}
+ case BooleanType =>
+ // make sure ps contains either
+ // - Wildcard or
+ // - both true and false
+ (ps exists { _.isInstanceOf[WildcardPattern] }) || {
+ var found = Set[Boolean]()
+ ps foreach {
+ case LiteralPattern(_, BooleanLiteral(b)) => found += b
+ case _ => ()
+ }
+ (found contains true) && (found contains false)
+ }
+
+ case UnitType =>
+ // Anything matches ()
+ !ps.isEmpty
+
+ case Int32Type =>
+ // Can't possibly pattern match against all Ints one by one
+ ps exists (_.isInstanceOf[WildcardPattern])
+
case _ =>
true
}
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 469b7606b..2f6ff8c36 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -245,6 +245,10 @@ object TypeTreeOps {
(WildcardPattern(newOb), (ob zip newOb).toMap)
+ case (LiteralPattern(ob, lit), expType) =>
+ val newOb = ob.map(id => freshId(id, expType))
+ (LiteralPattern(newOb,lit), (ob zip newOb).toMap)
+
case _ =>
sys.error("woot!?")
}
--
GitLab