From f727a8fad736334ba5789cbce10c7d530fc1de9d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 7 Oct 2015 16:35:43 +0200
Subject: [PATCH] Add integration for simplestValue, and fix closure test

---
 src/main/scala/leon/purescala/ExprOps.scala   |  2 +-
 .../integration/purescala/ExprOpsSuite.scala  | 24 +++++++++++--------
 .../leon/test/helpers/ExpressionsDSL.scala    |  8 +++++++
 3 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 2f1c610c0..a17c189b1 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1101,7 +1101,7 @@ object ExprOps {
   /** Returns simplest value of a given type */
   def simplestValue(tpe: TypeTree) : Expr = tpe match {
     case Int32Type                  => IntLiteral(0)
-    case RealType               	=> FractionalLiteral(0, 1)
+    case RealType               	  => FractionalLiteral(0, 1)
     case IntegerType                => InfiniteIntegerLiteral(0)
     case CharType                   => CharLiteral('a')
     case BooleanType                => BooleanLiteral(false)
diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
index 91156adbb..17260f7e5 100644
--- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
@@ -4,14 +4,10 @@ package leon.integration.purescala
 
 import leon.test._
 
-import leon._
 import leon.purescala.Constructors._
-import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.ExprOps._
-import leon.purescala.DefOps._
 import leon.purescala.Common._
-import leon.utils._
 
 class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
 
@@ -27,6 +23,7 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
         |    case b1 @ Bar4(b2: Bar3) => b2
         |  }
         |}""".stripMargin,
+
       """object Nested {
         |  def foo = {
         |    def bar = {
@@ -43,7 +40,6 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
   test("mapForPattern introduces casts"){ implicit fix =>
     funDef("Casts1.aMatch").body match {
       case Some(MatchExpr(scrut, Seq(MatchCase(p, None, b)))) =>
-        val m = mapForPattern(scrut, p)
         val bar4 = caseClassDef("Casts1.Bar4").typed
         val i    = caseClassDef("Casts1.Bar4").fields.head.id
 
@@ -92,10 +88,18 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
     assert(asInstOf(expr, cct) === AsInstanceOf(expr, cct))
   }
 
-  test("directlyNestedFunDefs") { implicit fix =>
-    val foo = funDef("Nested.foo")
-    val nested = directlyNestedFunDefs(foo.fullBody)
-    nested.exists { _.id.name == "bar"} &&
-    nested.exists { _.id.name == "zoo"}
+  test("closing functions") { implicit fix =>
+    val nested = moduleDef("Nested")
+    assert(nested.definedFunctions.size === 4)
   }
+
+  test("simplestValue") { implicit fix =>
+    import leon.purescala.TypeOps.isSubtypeOf
+    val act = classDef("Casts1.Foo").typed
+    val cct = caseClassDef("Casts1.Bar1").typed
+
+    assert(isSubtypeOf(simplestValue(act).getType, act))
+    assert(simplestValue(cct).getType == cct)
+  }
+
 }
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
index 74cd84c2c..a7c9692e1 100644
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
@@ -59,6 +59,14 @@ trait ExpressionsDSL {
     }
   }
 
+  def moduleDef(name: String)(implicit pgm: Program): ModuleDef = {
+    pgm.lookupAll(name).collect {
+      case m: ModuleDef => m
+    }.headOption.getOrElse {
+      fail(s"Failed to lookup module '$name' in program")
+    }
+  }
+
   def cc(name: String)(args: Expr*)(implicit pgm: Program): Expr = {
     val cct = caseClassDef(name).typed(Seq())
     CaseClass(cct, args.toSeq)
-- 
GitLab