diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index 5cd45f2dc5b57b9c5090e08392f0761be6c64955..59f82c209b4b44f982edaceedbf1fe5d1420d9ff 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala
@@ -41,7 +41,7 @@ object EvaluationPhase extends LeonPhase[Program, Unit] {
for (fd <- toEvaluate) {
reporter.info(s" - Evaluating ${fd.id}")
- val call = FunctionInvocation(fd.typedWithDef, Seq())
+ val call = FunctionInvocation(fd.typed, Seq())
eval.eval(call) match {
case EvaluationResults.Successful(ex) =>
reporter.info(s" => $ex")
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index f49e8c86365282cadc8bbcea74628093eb95ffc5..08d33ccf66b10aab3c05650feede133014d8765b 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -51,7 +51,7 @@ object Definitions {
val getType = tpe getOrElse id.getType
var defaultValue : Option[FunDef] = None
-
+
def subDefinitions = Seq()
// Warning: the variable will not have the same type as the ValDef, but
@@ -329,26 +329,26 @@ object Definitions {
class FunctionFlag
// Whether this FunDef was originally a (lazy) field
case class IsField(isLazy: Boolean) extends FunctionFlag
- // Compiler annotations provided with @annot
+ // Compiler annotations given in the source code as @annot
case class Annotation(annot: String) extends FunctionFlag
// If this class was a method. owner is the original owner of the method
case class IsMethod(owner: ClassDef) extends FunctionFlag
// If this function represents a loop that was there before XLangElimination
// Contains a copy of the original looping function
case class IsLoop(orig: FunDef) extends FunctionFlag
- case object IsPrivate extends FunctionFlag
+ // If extraction fails of the function's body fais, it is marked as abstract
case object IsAbstract extends FunctionFlag
+ // Currently, the only synthetic functions are those that calculate default values of parameters
case object IsSynthetic extends FunctionFlag
/** Functions
- * This class represents methods or fields of objects (as specified by the defType field)
- * that appear ONLY in the class/object's body (not the constructors)
- * All of these are treated as functions for verification.
- * Under circumstances (see canBeField and canBeLazyField methods)
- * they can be differentiated when it comes to code generation/pretty printing.
- *
- * Default type is DefDef (method)
- */
+ * This class represents methods or fields of objects. By "fields" we mean
+ * fields defined in the body, not the constructor arguments of a case class.
+ * When it comes to verification, all are treated the same (as functions).
+ * They are only differentiated when it comes to code generation/ pretty printing.
+ * By default, the FunDef represents a function/method, unless otherwise specified
+ * by its flags.
+ */
class FunDef(
val id: Identifier,
val tparams: Seq[TypeParameterDef],
@@ -356,6 +356,8 @@ object Definitions {
val params: Seq[ValDef]
) extends Definition {
+ /* Body manipulation */
+
private var fullBody_ : Expr = NoTree(returnType)
def fullBody = fullBody_
def fullBody_= (e : Expr) {
@@ -377,10 +379,18 @@ object Definitions {
fullBody = withPostcondition(fullBody, op)
}
- def nestedFuns = directlyNestedFunDefs(fullBody)
+ def hasBody = body.isDefined
+ def hasPrecondition : Boolean = precondition.isDefined
+ def hasPostcondition : Boolean = postcondition.isDefined
+
+ def isRecursive(p: Program) = p.callGraph.transitiveCallees(this) contains this
+ /* Nested definitions */
+ def nestedFuns = directlyNestedFunDefs(fullBody)
def subDefinitions = params ++ tparams ++ nestedFuns.toList
+ /* Duplication */
+
def duplicate: FunDef = {
val fd = new FunDef(id.freshen, tparams, returnType, params)
fd.copyContentFrom(this)
@@ -392,54 +402,36 @@ object Definitions {
this.addFlag(from.flags.toSeq : _*)
}
- def hasBody = body.isDefined
- def hasPrecondition : Boolean = precondition.isDefined
- def hasPostcondition : Boolean = postcondition.isDefined
+ /* Flags */
private var flags_ : Set[FunctionFlag] = Set()
-
- def addFlag(flags: FunctionFlag*) : FunDef = {
+
+ def addFlag(flags: FunctionFlag*): FunDef = {
this.flags_ ++= flags
this
}
+
def flags = flags_
- def annotations : Set[String] = flags_ collect { case Annotation(s) => s }
-
- /**
- * When this functions has been annotated as a (lazy) field
- * and has no arguments, it can be printed/compiled as a field
- */
- def canBeLazyField = flags.contains(IsField(true)) && params.isEmpty && tparams.isEmpty
- def canBeStrictField = flags.contains(IsField(false)) && params.isEmpty && tparams.isEmpty
- def canBeField = canBeLazyField || canBeStrictField
- def isRealFunction = !canBeField
- def isPrivate = flags contains IsPrivate
- def isSynthetic = flags contains IsSynthetic
- def methodOwner = flags collectFirst { case IsMethod(cd) => cd }
-
+
+ def annotations: Set[String] = flags_ collect { case Annotation(s) => s }
+ def canBeLazyField = flags.contains(IsField(true)) && params.isEmpty && tparams.isEmpty
+ def canBeStrictField = flags.contains(IsField(false)) && params.isEmpty && tparams.isEmpty
+ def canBeField = canBeLazyField || canBeStrictField
+ def isRealFunction = !canBeField
+ def isSynthetic = flags contains IsSynthetic
+ def methodOwner = flags collectFirst { case IsMethod(cd) => cd }
+
+ /* Wrapping in TypedFunDef */
+
def typed(tps: Seq[TypeTree]) = {
assert(tps.size == tparams.size)
TypedFunDef(this, tps)
}
def typed = {
- assert(tparams.isEmpty)
- TypedFunDef(this, Nil)
- }
-
- def typedWithDef = {
TypedFunDef(this, tparams.map(_.tp))
}
-
- def isRecursive(p: Program) = p.callGraph.transitiveCallees(this) contains this
-
- // Deprecated, old API
- @deprecated("Use .body instead", "2.3")
- def implementation : Option[Expr] = body
-
- @deprecated("Use .hasBody instead", "2.3")
- def hasImplementation : Boolean = hasBody
-
+
}
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 724300879d28b843c6b20058fac923d6c1972d2b..9e4b00d8c62c3cf0f932241d8b8c9fcedace6d99 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -32,7 +32,7 @@ object ChooseInfo {
def extractFromFunction(prog: Program, fd: FunDef): Seq[ChooseInfo] = {
val actualBody = and(fd.precondition.getOrElse(BooleanLiteral(true)), fd.body.get)
- val term = Terminating(fd.typedWithDef, fd.params.map(_.id.toVariable))
+ val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) yield {
ChooseInfo(fd, and(path, term), ch, ch)
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 678796e1b8901043216ea8eed0bfe3a319f43438..11874f798ed07ce751e0c20a56be65fc1f344770 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -77,7 +77,7 @@ final case class Chain(relations: List[Relation]) {
}
- rec(relations, funDef.typedWithDef, (funDef.params.map(_.id) zip initialArgs).toMap)
+ rec(relations, funDef.typed, (funDef.params.map(_.id) zip initialArgs).toMap)
}
/*