From f24a06db48476928a46e2c22f1b6617030da4ac3 Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Thu, 17 Sep 2015 15:37:43 +0200 Subject: [PATCH] Fix directlyNestedFunDefs, plus test --- src/main/scala/leon/purescala/ExprOps.scala | 51 +------------------ .../integration/purescala/ExprOpsSuite.scala | 20 +++++++- 2 files changed, 21 insertions(+), 50 deletions(-) diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index 84f196618..6a8c9ac57 100644 --- a/src/main/scala/leon/purescala/ExprOps.scala +++ b/src/main/scala/leon/purescala/ExprOps.scala @@ -344,8 +344,8 @@ object ExprOps { /** Returns functions in directly nested LetDefs */ def directlyNestedFunDefs(e: Expr): Set[FunDef] = { - foldRight[Set[FunDef]]{ - case (LetDef(fd,bd), _) => Set(fd) + foldRight[Set[FunDef]]{ + case (LetDef(fd,_), Seq(fromFd, fromBd)) => fromBd + fd case (_, subs) => subs.flatten.toSet }(e) } @@ -2095,50 +2095,3 @@ object ExprOps { } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala index 3de0828b6..91156adbb 100644 --- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala +++ b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala @@ -26,7 +26,18 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL | def aMatch(a: Foo) = a match { | case b1 @ Bar4(b2: Bar3) => b2 | } - |}""".stripMargin + |}""".stripMargin, + """object Nested { + | def foo = { + | def bar = { + | def baz = 42 + | baz + | } + | def zoo = 42 + | } + |} + | + """.stripMargin ) test("mapForPattern introduces casts"){ implicit fix => @@ -80,4 +91,11 @@ 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"} + } } -- GitLab