From 05dbaeabbff0dd516bb0b3e384c74d8a91fd2160 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 9 Oct 2015 12:32:43 +0200
Subject: [PATCH] Boost FunDef.duplicate, get rid of FunDef.copyContentFrom
---
.../scala/leon/purescala/Definitions.scala | 18 +++++++++-------
src/main/scala/leon/purescala/ExprOps.scala | 4 ++--
.../leon/purescala/FunctionClosure.scala | 3 +--
.../scala/leon/purescala/MethodLifting.scala | 7 ++-----
.../scala/leon/purescala/RestoreMethods.scala | 11 +++-------
.../leon/purescala/ScopeSimplifier.scala | 3 +--
src/main/scala/leon/purescala/TypeOps.scala | 3 +--
.../solvers/isabelle/AdaptationPhase.scala | 4 +---
.../scala/leon/synthesis/Synthesizer.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 4 ++--
.../leon/termination/TerminationChecker.scala | 2 +-
.../scala/leon/utils/UnitElimination.scala | 21 +++++++------------
12 files changed, 32 insertions(+), 50 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index d24bd0322..5b5f48d27 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -3,6 +3,7 @@
package leon
package purescala
+import sun.reflect.generics.tree.ReturnType
import utils.Library
import Common._
import Expressions._
@@ -410,16 +411,17 @@ object Definitions {
/* Duplication */
- def duplicate: FunDef = {
- val fd = new FunDef(id.freshen, tparams, returnType, params)
- fd.copyContentFrom(this)
+ def duplicate(
+ id: Identifier = this.id.freshen,
+ tparams: Seq[TypeParameterDef] = this.tparams,
+ returnType: TypeTree = this.returnType,
+ params: Seq[ValDef] = this.params
+ ): FunDef = {
+ val fd = new FunDef(id, tparams, returnType, params)
+ fd.fullBody = this.fullBody
+ fd.addFlags(this.flags)
fd.copiedFrom(this)
}
-
- def copyContentFrom(from : FunDef) {
- this.fullBody = from.fullBody
- this.addFlags(from.flags)
- }
/* Flags */
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index a17c189b1..30999a647 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1822,7 +1822,7 @@ object ExprOps {
)))
}
- val newFd = fdOuter.duplicate
+ val newFd = fdOuter.duplicate()
val simp = Simplifiers.bestEffort(ctx, p) _
@@ -2022,7 +2022,7 @@ object ExprOps {
import synthesis.Witnesses.Terminating
val res1 = preMap({
case LetDef(fd, b) =>
- val nfd = fd.duplicate
+ val nfd = fd.duplicate()
fds += fd -> nfd
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 71a76ce90..dafb2e37c 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -118,13 +118,12 @@ object FunctionClosure extends TransformationPhase {
val freshVals = (inner.paramIds ++ free).map{_.freshen}.map(instantiateType(_, tparamsMap))
val freeMap = (inner.paramIds ++ free).zip(freshVals).toMap
- val newFd = new FunDef(
+ val newFd = inner.duplicate(
inner.id.freshen,
inner.tparams ++ tpFresh,
instantiateType(inner.returnType, tparamsMap),
freshVals.map(ValDef(_))
)
- newFd.copyContentFrom(inner)
newFd.precondition = Some(and(pc, inner.precOrTrue))
val instBody = instantiateType(
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 25b58c1dc..2d4024360 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -117,8 +117,7 @@ object MethodLifting extends TransformationPhase {
val paramsMap = fd.params.zip(fdParams).map{ case (from, to) => from.id -> to.id }.toMap
val eSubst: Expr => Expr = instantiateType(_, tMap, paramsMap)
- val newFd = new FunDef(fd.id, fd.tparams, tSubst(fd.returnType), fdParams).copiedFrom(fd)
- newFd.copyContentFrom(fd)
+ val newFd = fd.duplicate(fd.id, fd.tparams, tSubst(fd.returnType), fdParams) // FIXME: I don't like reusing the Identifier
mdToCls += newFd -> c
@@ -146,9 +145,7 @@ object MethodLifting extends TransformationPhase {
val receiver = FreshIdentifier("thiss", recType).setPos(cd.id)
- val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams)
- nfd.copyContentFrom(fd)
- nfd.setPos(fd)
+ val nfd = fd.duplicate(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams)
nfd.addFlag(IsMethod(cd))
def classPre(fd: FunDef) = mdToCls.get(fd) match {
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index cedc3a437..98d552977 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -4,7 +4,6 @@ package leon
package purescala
import Definitions._
-import Common._
import Expressions._
import ExprOps.replaceFromIDs
import DefOps.replaceFunDefs
@@ -23,14 +22,10 @@ object RestoreMethods extends TransformationPhase {
}
val fdToMd = for( (cd, fds) <- classMethods; fd <- fds) yield {
- val md = new FunDef(
- id = FreshIdentifier(fd.id.name),
+ val md = fd.duplicate(
tparams = fd.tparams.drop(cd.tparams.size),
- params = fd.params.tail, // drop 'this'
- returnType = fd.returnType
- ).copiedFrom(fd)
-
- md.copyContentFrom(fd)
+ params = fd.params.tail // drop 'this'
+ )
val thisArg = fd.params.head
val thisExpr = This(thisArg.getType.asInstanceOf[ClassType])
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 7fb5699e3..9eca53058 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -44,8 +44,7 @@ class ScopeSimplifier extends Transformer {
ValDef(newArg, tpe)
}
- val newFd = new FunDef(newId, fd.tparams, fd.returnType, newArgs)
- newFd.copyContentFrom(fd)
+ val newFd = fd.duplicate(id = newId, params = newArgs)
newScope = newScope.registerFunDef(fd -> newFd)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 2d79403a0..3d4c5af13 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -314,8 +314,7 @@ object TypeOps {
}
val returnType = tpeSub(fd.returnType)
val params = fd.params map (instantiateType(_, tps))
- val newFd = new FunDef(id, tparams, returnType, params).copiedFrom(fd)
- newFd.copyContentFrom(fd)
+ val newFd = fd.duplicate(id, tparams, returnType, params)
val subCalls = preMap {
case fi @ FunctionInvocation(tfd, args) if tfd.fd == fd =>
diff --git a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
index d8acc2a21..9cad1cc49 100644
--- a/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
+++ b/src/main/scala/leon/solvers/isabelle/AdaptationPhase.scala
@@ -48,9 +48,7 @@ object AdaptationPhase extends TransformationPhase {
val diff: List[TypeParameter] = (expected -- actual).toList
context.reporter.debug(s"Rewriting function definition ${fd.qualifiedName(program)}: adding dummies for hidden type parameter(s) ${diff.map(_.id).mkString(" and ")}")
val nid = FreshIdentifier(fd.id.name, FunctionType(fd.params.map(_.getType) ++ diff.map(mkDummyTyp), fd.returnType))
- val nfd = new FunDef(nid, fd.tparams, fd.returnType, fd.params ++ diff.map(mkDummyParameter))
- nfd.copyContentFrom(fd)
- nfd.setPos(fd.getPos)
+ val nfd = fd.duplicate(id = nid, params = fd.params ++ diff.map(mkDummyParameter))
Some(fd -> ((nfd, diff)))
}
}.toMap
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 891ff435c..7ed4d56a8 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -108,7 +108,7 @@ class Synthesizer(val context : LeonContext,
val (npr, fdMap) = replaceFunDefs(program)({
case fd if fd eq ci.fd =>
- val nfd = fd.duplicate
+ val nfd = fd.duplicate()
nfd.fullBody = replace(Map(ci.source -> solutionExpr), nfd.fullBody)
Some(nfd)
case _ => None
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index fef3dd376..168c46208 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -349,7 +349,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
replaceFunDefs(program0){
case fd if fd == hctx.ci.fd =>
- val nfd = fd.duplicate
+ val nfd = fd.duplicate()
nfd.fullBody = postMap {
case src if src eq hctx.ci.source =>
@@ -366,7 +366,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
None
case fd =>
- Some(fd.duplicate)
+ Some(fd.duplicate())
}
}
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index fb8818922..6b8f5abb6 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -9,7 +9,7 @@ import purescala.DefOps._
abstract class TerminationChecker(val context: LeonContext, initProgram: Program) extends LeonComponent {
val program = {
- val (pgm, _) = replaceFunDefs(initProgram){ fd => Some(fd.duplicate) }
+ val (pgm, _) = replaceFunDefs(initProgram){ fd => Some(fd.duplicate()) }
pgm
}
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 0336a8aae..5b63221a0 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -10,6 +10,7 @@ import purescala.Extractors._
import purescala.Constructors._
import purescala.Types._
+// FIXME: Unused and untested
object UnitElimination extends TransformationPhase {
val name = "Unit Elimination"
@@ -26,13 +27,9 @@ object UnitElimination extends TransformationPhase {
//first introduce new signatures without Unit parameters
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.params.exists(vd => vd.getType == UnitType)) {
- val freshFunDef = new FunDef(
- FreshIdentifier(fd.id.name),
- fd.tparams,
- fd.returnType,
- fd.params.filterNot(vd => vd.getType == UnitType)
- ).setPos(fd)
- freshFunDef.copyContentFrom(fd)
+ val freshFunDef = fd.duplicate(
+ params = fd.params.filterNot(vd => vd.getType == UnitType)
+ )
fun2FreshFun += (fd -> freshFunDef)
} else {
fun2FreshFun += (fd -> fd) //this will make the next step simpler
@@ -103,13 +100,9 @@ object UnitElimination extends TransformationPhase {
removeUnit(b)
else {
val (newFd, rest) = if(fd.params.exists(vd => vd.getType == UnitType)) {
- val freshFunDef = new FunDef(
- FreshIdentifier(fd.id.name),
- fd.tparams,
- fd.returnType,
- fd.params.filterNot(vd => vd.getType == UnitType)
- ).setPos(fd)
- freshFunDef.copyContentFrom(fd)
+ val freshFunDef = fd.duplicate(
+ params = fd.params.filterNot(vd => vd.getType == UnitType)
+ )
fun2FreshFun += (fd -> freshFunDef)
freshFunDef.fullBody = removeUnit(fd.fullBody)
val restRec = removeUnit(b)
--
GitLab