From d96e56c2fe44703bc26f4983ee43c73d1385bc1f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 27 Aug 2014 16:35:09 +0200
Subject: [PATCH] Fix liftClosures to not introduce name-clashing functions at
the toplevel
---
src/main/scala/leon/purescala/TreeOps.scala | 32 +++++++++++++++++----
1 file changed, 27 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 4bca1518d..0fa481c68 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1949,17 +1949,39 @@ object TreeOps {
* the necessary information as arguments, no need to close them.
*/
def liftClosures(e: Expr): (Set[FunDef], Expr) = {
- var fds: Set[FunDef] = Set()
+ var fds: Map[FunDef, FunDef] = Map()
- val res = postMap{
+ val res1 = preMap({
+ case LetDef(fd, b) =>
+ val nfd = new FunDef(fd.id.freshen, fd.tparams, fd.returnType, fd.params, fd.defType)
+ nfd.copyContentFrom(fd)
+ nfd.copiedFrom(fd)
+
+ fds += fd -> nfd
+
+ Some(LetDef(nfd, b))
+
+ case fi @ FunctionInvocation(tfd, args) =>
+ if (fds contains tfd.fd) {
+ Some(FunctionInvocation(fds(tfd.fd).typed(tfd.tps), args))
+ } else {
+ None
+ }
+
+ case _ =>
+ None
+ })(e)
+
+ // we now remove LetDefs
+ val res2 = preMap({
case LetDef(fd, b) =>
- fds += fd
Some(b)
case _ =>
None
- }(e)
+ }, applyRec = true)(res1)
+
- (fds, res)
+ (fds.values.toSet, res2)
}
def preTraversalWithParent(f: (Expr, Option[Tree]) => Unit, initParent: Option[Tree] = None)(e: Expr): Unit = {
--
GitLab