diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index 84f196618d8fc6b84af18c7dfd83c1ae578a1fa0..6a8c9ac57aa2dbd14773c8c420189526e3b5802e 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 3de0828b68b005348bbd2b5398d998fad9c9c142..91156adbb5ea0cd39da19885e413d2ba5750840f 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"} + } }