From 78470af40d712f4f01c2e1d08f88a3203e24ec91 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 11 Sep 2015 19:27:23 +0200
Subject: [PATCH] Inliner should continuously inline fun. invocations
---
src/main/scala/leon/utils/InliningPhase.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/utils/InliningPhase.scala b/src/main/scala/leon/utils/InliningPhase.scala
index cc2862c76..8053a8dc1 100644
--- a/src/main/scala/leon/utils/InliningPhase.scala
+++ b/src/main/scala/leon/utils/InliningPhase.scala
@@ -38,13 +38,13 @@ object InliningPhase extends TransformationPhase {
}
for (fd <- p.definedFunctions) {
- fd.fullBody = simplify(preMap {
+ fd.fullBody = simplify(preMap ({
case FunctionInvocation(TypedFunDef(fd, tps), args) if doInline(fd) =>
val newBody = instantiateType(fd.fullBody, (fd.tparams zip tps).toMap, Map())
Some(replaceFromIDs(fd.params.map(_.id).zip(args).toMap, newBody))
case _ =>
None
- }(fd.fullBody))
+ }, applyRec = true)(fd.fullBody))
}
filterFunDefs(p, fd => !doInline(fd))
--
GitLab