From 3746271fcb0a5001c0674336321411dcb79625ab Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 6 Oct 2014 17:20:17 +0200
Subject: [PATCH] Reintroduce liftClosures
---
src/main/scala/leon/purescala/TreeOps.scala | 38 +++++++++++++++++++++
1 file changed, 38 insertions(+)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 52e06d4bb..1b0222094 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1946,6 +1946,44 @@ object TreeOps {
}
}
+ /**
+ * Used to lift closures introduced by synthesis. Closures already define all
+ * the necessary information as arguments, no need to close them.
+ */
+ def liftClosures(e: Expr): (Set[FunDef], Expr) = {
+ var fds: Map[FunDef, FunDef] = Map()
+ 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) =>
+ Some(b)
+ case _ =>
+ None
+ }, applyRec = true)(res1)
+
+ (fds.values.toSet, res2)
+ }
+
/**
* Deprecated API
* ========
--
GitLab