From 7252b1a90fbbd8e9721944e80db9d0a6777dfc44 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 19 May 2015 11:41:20 +0200
Subject: [PATCH] Simplify traverse a little
---
src/main/scala/leon/purescala/ExprOps.scala | 8 +++-----
1 file changed, 3 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b4866c399..0c158ec32 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1185,11 +1185,9 @@ object ExprOps {
}
def traverse(funDef: FunDef): Seq[T] = {
- // @mk FIXME: This seems overly compicated
- val precondition = funDef.precondition.map(e => matchToIfThenElse(e)).toSeq
- val precTs = funDef.precondition.map(e => traverse(e)).toSeq.flatten
- val bodyTs = funDef.body.map(e => traverse(e, precondition)).toSeq.flatten
- val postTs = funDef.postcondition.map(p => traverse(p)).toSeq.flatten
+ val precTs = funDef.precondition.toSeq.flatMap(traverse)
+ val bodyTs = funDef.body.toSeq.flatMap(traverse(_, funDef.precondition.toSeq))
+ val postTs = funDef.postcondition.toSeq.flatMap(traverse)
precTs ++ bodyTs ++ postTs
}
--
GitLab