diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index d24bd0322eff1c7b7caa9ca9f2c2078eabef12f8..5b5f48d27219cd3c8b1e72b59f34efcca9c522ae 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 a17c189b187772ce1c6631acb9bd1956f598f76f..30999a647dc613a959ce8a3d95f2cf491bae24df 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 71a76ce9018e946f11462285aad69dbd59c4199f..dafb2e37c345f5f3898d80e19de92b5f7badc32f 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 25b58c1dcaeb64a0d874d7a9b26e76749021594d..2d4024360fdb2dd861a4a321e30d0662c1dfe3df 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 cedc3a4378c468084c935e3afb3953602c9ae686..98d552977738aea4f2dadd8658962b8caa2ef317 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 7fb5699e34290a8a1bd079201cce0092c7fb1e4e..9eca530580c248510f266520306834734d4746fa 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 2d79403a083cced55dfc8564ecd763cd46710332..3d4c5af13b433fd597de398f9b7d84d3d0387c73 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 d8acc2a21c12dc2497ab7acd792a403d15858a85..9cad1cc49fe2790fcd6ed876acc453b3b6599d6f 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 891ff435c98594c02a075e3a751fc2185213785a..7ed4d56a8a74e5a16301026ff2328ba8243d8716 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 fef3dd376b49e3559c6c633e2d7cde4e05890263..168c462087473cdb2c6ce2fbfdc99bf02211c57f 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 fb881892221fb477c1e19f5b193ba2316711d5b6..6b8f5abb670a4d61192ace440b604d99d0f6d706 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 0336a8aaea93f6a3b919cd5f69b62f77d46ca584..5b63221a08d80c1e4f44fa21e517b1a65ab130e2 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)