From c2cebdcdb9c36bd1ca754b37719bdf11433b05e1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 21 Aug 2015 01:16:54 +0200
Subject: [PATCH] Fix simplestValue for sets
---
src/main/scala/leon/purescala/ExprOps.scala | 2 +-
.../leon/test/purescala/ExprOpsSuite.scala | 17 +++++++++++++++++
2 files changed, 18 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 25a2d0e93..89770d2cd 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1012,7 +1012,7 @@ object ExprOps {
case CharType => CharLiteral('a')
case BooleanType => BooleanLiteral(false)
case UnitType => UnitLiteral()
- case SetType(baseType) => FiniteSet(Set(), tpe)
+ case SetType(baseType) => FiniteSet(Set(), baseType)
case MapType(fromType, toType) => FiniteMap(Nil, fromType, toType)
case TupleType(tpes) => Tuple(tpes.map(simplestValue))
case ArrayType(tpe) => EmptyArray(tpe)
diff --git a/src/test/scala/leon/test/purescala/ExprOpsSuite.scala b/src/test/scala/leon/test/purescala/ExprOpsSuite.scala
index 482777b74..de304264d 100644
--- a/src/test/scala/leon/test/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/test/purescala/ExprOpsSuite.scala
@@ -6,6 +6,8 @@ import leon.test._
import leon.purescala.Common._
import leon.purescala.Expressions._
import leon.purescala.Types._
+import leon.purescala.TypeOps._
+import leon.purescala.Definitions._
import leon.purescala.ExprOps._
class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.ExpressionsDSL {
@@ -262,4 +264,19 @@ class ExprOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
assert( postMap(op, true)(expr) == Plus(bi(42), Minus(bi(42), bi(3))) )
}
+
+ test("simplestValue") { ctx =>
+ val types = Seq(BooleanType,
+ Int32Type,
+ IntegerType,
+ SetType(BooleanType),
+ TupleType(Seq(BooleanType, BooleanType)),
+ MapType(Int32Type, BooleanType))
+
+ for (t <- types) {
+ val v = simplestValue(t)
+ assert(isSubtypeOf(v.getType, t), "SimplestValue of "+t+": "+v+":"+v.getType)
+ }
+
+ }
}
--
GitLab