diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 8278ca3396ab27ac4298881c678231fab122e5a2..a0d5c4830ffd69b47478593e823217960b2aa21d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -11,7 +11,6 @@ object Main {
frontends.scalac.ExtractionPhase,
utils.TypingPhase,
FileOutputPhase,
- ScopingPhase,
purescala.RestoreMethods,
xlang.ArrayTransformation,
xlang.EpsilonElimination,
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index eb010351db8a374196eef1582b3670b7cfe96d05..cbdf4a6e25302b719c32208cb03badceb4d55f4a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -9,10 +9,11 @@ import scala.language.implicitConversions
import purescala._
import purescala.Definitions.{
- ClassDef => LeonClassDef,
- ModuleDef => LeonModuleDef,
- ValDef => LeonValDef,
- Import => LeonImport,
+ ClassDef => LeonClassDef,
+ ModuleDef => LeonModuleDef,
+ ValDef => LeonValDef,
+ Import => LeonImport,
+ Annotation => LeonAnnotation,
_
}
@@ -287,7 +288,7 @@ trait CodeExtraction extends ASTExtractors {
// Default value functions
case ExDefaultValueFunction(sym, _, _, _ ,_ , _, _) =>
val fd = defineFunDef(sym)(DefContext())
- fd.addAnnotation("synthetic")
+ fd.addFlag(IsSynthetic)
Some(fd)
@@ -578,7 +579,7 @@ trait CodeExtraction extends ASTExtractors {
// Default values for parameters
case t@ ExDefaultValueFunction(fsym, _, _, _, owner, index, _) =>
val fd = defineFunDef(fsym)(defCtx)
- fd.addAnnotation("synthetic")
+ fd.addFlag(IsSynthetic)
isMethod += fsym
methodToClass += fd -> cd
@@ -644,11 +645,11 @@ trait CodeExtraction extends ASTExtractors {
val name = sym.name.toString
- val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), tparamsDef, returnType, newParams, DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), tparamsDef, returnType, newParams)
fd.setPos(sym.pos)
- fd.addAnnotation(annotationsOf(sym).toSeq : _*)
+ fd.addFlag(annotationsOf(sym).toSeq.map(LeonAnnotation) : _*)
defsToDefs += sym -> fd
@@ -663,13 +664,12 @@ trait CodeExtraction extends ASTExtractors {
val name = sym.name.toString
- val fieldType = if (isLazy) DefType.LazyFieldDef else DefType.StrictFieldDef
-
- val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), Seq(), returnType, Seq(), fieldType)
+ val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), Seq(), returnType, Seq())
fd.setPos(sym.pos)
+ fd.addFlag(IsField(isLazy))
- fd.addAnnotation(annotationsOf(sym).toSeq : _*)
+ fd.addFlag(annotationsOf(sym).toSeq.map(LeonAnnotation) : _*)
defsToDefs += sym -> fd
@@ -768,7 +768,7 @@ trait CodeExtraction extends ASTExtractors {
// If this is a lazy field definition, drop the assignment/ accessing
val body =
- if (funDef.defType == DefType.LazyFieldDef) { body0 match {
+ if (funDef.flags.contains(IsField(true))) { body0 match {
case Block(List(Assign(_, realBody)),_ ) => realBody
case _ => outOfSubsetError(body0, "Wrong form of lazy accessor")
}} else body0
@@ -799,7 +799,7 @@ trait CodeExtraction extends ASTExtractors {
reporter.warning(funDef.getPos, "Function "+funDef.id.name+" is not fully unavailable to Leon.")
}
- funDef.addAnnotation("abstract")
+ funDef.addFlag(IsAbstract)
NoTree(funDef.returnType)
}
@@ -1062,7 +1062,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
- fd.addAnnotation(annotationsOf(d.symbol).toSeq : _*)
+ fd.addFlag(annotationsOf(d.symbol).toSeq.map(LeonAnnotation) : _*)
val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 439e5445c9b7f086d380faa862c00908ce64aee0..575939a8c7dfc0095df7134b3b158a024dbaff83 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -15,9 +15,7 @@ object Definitions {
sealed abstract class Definition extends Tree {
val id: Identifier
-
- var origOwner : Option[Definition] = None // The definition/scope enclosing this definition
-
+
def subDefinitions : Seq[Definition] // The enclosed scopes/definitions by this definition
def containsDef(df: Definition): Boolean = {
@@ -66,8 +64,6 @@ object Definitions {
case class Program(units: List[UnitDef]) extends Definition {
val id = FreshIdentifier("program")
- origOwner = None
-
lazy val library = Library(this)
def subDefinitions = units
@@ -326,16 +322,21 @@ object Definitions {
lazy val singleCaseClasses : Seq[CaseClassDef] = if (hasParent) Nil else Seq(this)
}
-
- // Definition types (see below)
- object DefType extends Enumeration {
- type DefType = Value
- val MethodDef = Value("def")
- val StrictFieldDef = Value("val")
- val LazyFieldDef = Value("lazy val")
- }
- import DefType._
-
+ // A class that represents flags that annotate a FunDef with different attributes
+ class FunctionFlag
+ // Whether this FunDef was originally a (lazy) field
+ case class IsField(isLazy: Boolean) extends FunctionFlag
+ // Compiler annotations provided with @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
+ case object IsAbstract extends FunctionFlag
+ 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)
@@ -349,13 +350,9 @@ object Definitions {
val id: Identifier,
val tparams: Seq[TypeParameterDef],
val returnType: TypeTree,
- val params: Seq[ValDef],
- val defType: DefType
+ val params: Seq[ValDef]
) extends Definition {
-
- // A copy of the original function before Xlang elimination
- var orig : Option[FunDef] = None
-
+
private var fullBody_ : Expr = NoTree(returnType)
def fullBody = fullBody_
def fullBody_= (e : Expr) {
@@ -382,41 +379,40 @@ object Definitions {
def subDefinitions = params ++ tparams ++ nestedFuns.toList
def duplicate: FunDef = {
- val fd = new FunDef(id.freshen, tparams, returnType, params, defType)
+ val fd = new FunDef(id.freshen, tparams, returnType, params)
fd.copyContentFrom(this)
fd.copiedFrom(this)
}
def copyContentFrom(from : FunDef) {
this.fullBody = from.fullBody
- this.orig = from.orig
- this.origOwner = from.origOwner
- this.addAnnotation(from.annotations.toSeq : _*)
+ this.addFlag(from.flags.toSeq : _*)
}
def hasBody = body.isDefined
def hasPrecondition : Boolean = precondition.isDefined
def hasPostcondition : Boolean = postcondition.isDefined
- /**
- * When this functions has been annotated as a (lazy) field
- * and has no arguments, it can be printed/compiled as a field
- */
- def canBeLazyField = defType == LazyFieldDef && params.isEmpty && tparams.isEmpty
- def canBeStrictField = defType == StrictFieldDef && params.isEmpty && tparams.isEmpty
- def canBeField = canBeLazyField || canBeStrictField
- def isRealFunction = !canBeField
+ private var flags_ : Set[FunctionFlag] = Set()
- def isSynthetic = annotations contains "synthetic"
-
- private var annots: Set[String] = Set.empty[String]
- def addAnnotation(as: String*) : FunDef = {
- annots = annots ++ as
+ def addFlag(flags: FunctionFlag*) : FunDef = {
+ this.flags_ ++= flags
this
}
- def annotations : Set[String] = annots
+ def flags = flags_
+ def annotations : Set[String] = flags_ collect { case Annotation(s) => s }
- def isPrivate : Boolean = annots.contains("private")
+ /**
+ * 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 typed(tps: Seq[TypeTree]) = {
assert(tps.size == tparams.size)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b043da9ac1fcdae8271419544e3aea9d3e192688..ad3216436a99594babc223f25b8b1bb4e539d2de 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1918,7 +1918,7 @@ object ExprOps {
import synthesis.Witnesses.Terminating
val res1 = preMap({
case LetDef(fd, b) =>
- val nfd = new FunDef(fd.id.freshen, fd.tparams, fd.returnType, fd.params, fd.defType)
+ val nfd = new FunDef(fd.id.freshen, fd.tparams, fd.returnType, fd.params)
nfd.copyContentFrom(fd)
nfd.copiedFrom(fd)
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 1eed1d4842d668231538e47aaf01d263823390a4..b91ca4e3f34e2b9ca81decc6fb36d928e1315973 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -60,10 +60,10 @@ object FunctionClosure extends TransformationPhase {
val newBindedVars: Set[Identifier] = bindedVars ++ fd.params.map(_.id)
val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
- val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs, fd.defType).copiedFrom(fd)
+ val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs).copiedFrom(fd)
topLevelFuns += newFunDef
- newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
- newFunDef.orig = Some(fd)
+ newFunDef.copyContentFrom(fd) //TODO: this still has some dangerous side effects (?)
+ newFunDef.addFlag(IsLoop(fd))
def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index f033681b2937046213aa07ff75f4908870242bf2..f8a13009089ee6dc056b10bc3ed408025126c25c 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -41,9 +41,10 @@ object MethodLifting extends TransformationPhase {
val receiver = FreshIdentifier("this", recType).setPos(cd.id)
- val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams, fd.defType)
+ val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams)
nfd.copyContentFrom(fd)
nfd.setPos(fd)
+ nfd.addFlag(IsMethod(cd))
nfd.fullBody = postMap{
case This(ct) if ct.classDef == cd => Some(receiver.toVariable)
case _ => None
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a1f9eb335f50c33442804fbfb4b681e9ffd369fc..7b6ccdcd60b89ac8d3351ff10159da689edd85e3 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -522,8 +522,11 @@ class PrettyPrinter(opts: PrinterOptions,
|"""
}
- if (fd.canBeField) {
- p"""|${fd.defType} ${fd.id} : ${fd.returnType} = {
+ if (fd.canBeStrictField) {
+ p"""|val ${fd.id} : ${fd.returnType} = {
+ |"""
+ } else if (fd.canBeLazyField) {
+ p"""|lazy val ${fd.id} : ${fd.returnType} = {
|"""
} else if (fd.tparams.nonEmpty) {
p"""|def ${fd.id}[${nary(fd.tparams, ",")}](${fd.params}): ${fd.returnType} = {
@@ -572,23 +575,20 @@ class PrettyPrinter(opts: PrinterOptions,
object FcallMethodInvocation {
def unapply(fi: FunctionInvocation): Option[(Expr, FunDef, String, Seq[TypeTree], Seq[Expr])] = {
- val FunctionInvocation(tfd, args) = fi
- tfd.fd.origOwner match {
- case Some(cd: ClassDef) =>
- val (rec, rargs) = (args.head, args.tail)
+ val FunctionInvocation(tfd, args) = fi
+ tfd.fd.methodOwner.map { cd =>
+ val (rec, rargs) = (args.head, args.tail)
- val fid = tfd.fd.id
+ val fid = tfd.fd.id
- val fname = fid.name
+ val fname = fid.name
- val decoded = scala.reflect.NameTransformer.decode(fname)
+ val decoded = scala.reflect.NameTransformer.decode(fname)
- val realtps = tfd.tps.drop(cd.tparams.size)
+ val realtps = tfd.tps.drop(cd.tparams.size)
- Some((rec, tfd.fd, decoded, realtps, rargs))
- case _ =>
- None
- }
+ (rec, tfd.fd, decoded, realtps, rargs)
+ }
}
}
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index 74802b9aff126faf145feb687e7d88a55acd2bab..bd6a51cd00c082d363380f217faabe4a9226ff9b 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -18,7 +18,7 @@ object RestoreMethods extends TransformationPhase {
// @TODO: This code probably needs fixing, but is mostly unused and completely untested.
def apply(ctx: LeonContext, p: Program) = {
- val classMethods = p.definedFunctions.groupBy(_.origOwner).collect {
+ val classMethods = p.definedFunctions.groupBy(_.methodOwner).collect {
case (Some(cd: ClassDef), fds) => cd -> fds
}
@@ -27,10 +27,11 @@ object RestoreMethods extends TransformationPhase {
id = FreshIdentifier(fd.id.name),
tparams = fd.tparams.drop(cd.tparams.size),
params = fd.params.tail, // drop 'this'
- returnType = fd.returnType,
- defType = fd.defType
+ returnType = fd.returnType
).copiedFrom(fd)
+ md.copyContentFrom(fd)
+
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 e15183d54e519876213bbfc80d6f84d5a0820f24..1bc8e9379f88f63bfbfe10bd80d8abab679e5f83 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -44,7 +44,8 @@ class ScopeSimplifier extends Transformer {
ValDef(newArg, tpe)
}
- val newFd = new FunDef(newId, fd.tparams, fd.returnType, newArgs, fd.defType)
+ val newFd = new FunDef(newId, fd.tparams, fd.returnType, newArgs)
+ newFd.copyContentFrom(fd)
newScope = newScope.registerFunDef(fd -> newFd)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 209c6c3ab0c617981d10c16febd3f027131dae17..61693206b0fcf55fdae8beec1814b56792563c5b 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -29,8 +29,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val fakeFunDef = new FunDef(FreshIdentifier("fake", alwaysShowUniqueID = true),
Nil,
body.getType,
- variablesOf(body).toSeq.map(ValDef(_)),
- DefType.MethodDef)
+ variablesOf(body).toSeq.map(ValDef(_)))
fakeFunDef.body = Some(body)
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 90d60d4ebf5433f69f877f308275d3ff6409ec62..4578eab14eb9dcd7e70804f359a85c725bf1ec39 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -79,7 +79,7 @@ case object ADTInduction extends Rule("ADT Induction") {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs, DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs)
val cases = for ((sol, (problem, pre, cct, ids, calls)) <- sols zip subProblemsInfo) yield {
globalPre ::= and(pre, sol.pre)
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 663759335f8e126dabb0f09d1ab3bf66d1d93b34..bcafde3c54dd7ebadfab9eb8417a4c4c4ceb2406 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -129,7 +129,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs, DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs)
val cases = for ((sol, (problem, pat, calls, pc)) <- sols zip subProblemsInfo) yield {
globalPre ::= and(pc, sol.pre)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 0aab04f54277bb77fa41e9d95725e266dc3fc6b6..c97d14d1f0a983e46b8359b9299db076b254881d 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -236,19 +236,19 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private val bArrayId = FreshIdentifier("bArray", ArrayType(BooleanType), true)
- private var cTreeFd = new FunDef(FreshIdentifier("cTree", alwaysShowUniqueID = true),
- Seq(),
- p.outType,
- p.as.map(id => ValDef(id)),
- DefType.MethodDef
- )
-
- private var phiFd = new FunDef(FreshIdentifier("phiFd", alwaysShowUniqueID = true),
- Seq(),
- BooleanType,
- p.as.map(id => ValDef(id)),
- DefType.MethodDef
- )
+ private var cTreeFd = new FunDef(
+ FreshIdentifier("cTree", alwaysShowUniqueID = true),
+ Seq(),
+ p.outType,
+ p.as.map(id => ValDef(id))
+ )
+
+ private var phiFd = new FunDef(
+ FreshIdentifier("phiFd", alwaysShowUniqueID = true),
+ Seq(),
+ BooleanType,
+ p.as.map(id => ValDef(id))
+ )
private var programCTree: Program = _
@@ -280,11 +280,12 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val (prog2, fdMap2) = replaceFunDefs(prog1)({
case fd if affected(fd) =>
// Add the b array argument to all affected functions
- val nfd = new FunDef(fd.id.freshen,
- fd.tparams,
- fd.returnType,
- fd.params :+ ValDef(bArrayId),
- fd.defType)
+ val nfd = new FunDef(
+ fd.id.freshen,
+ fd.tparams,
+ fd.returnType,
+ fd.params :+ ValDef(bArrayId)
+ )
nfd.copyContentFrom(fd)
nfd.copiedFrom(fd)
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index 58747ed6654385f10964a1aeded89de843626f2a..8f619667a9d8be318629c003984dcaa8147a8a77 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -45,7 +45,7 @@ case object IntInduction extends Rule("Int Induction") {
and(LessThan(Variable(inductOn), InfiniteIntegerLiteral(0)), lt.pre))
val preOut = subst(inductOn -> Variable(origId), preIn)
- val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, tpe, Seq(ValDef(inductOn)),DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, tpe, Seq(ValDef(inductOn)))
val idPost = FreshIdentifier("res", tpe)
newFun.precondition = Some(preIn)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index ce20aee56f50e5e021164e2e56cf661a5c060951..9bd49fcebfc4f44ed4e874cfc1a7bf00bb0c0991 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -93,7 +93,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
//define max function
val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b", Int32Type)))
- val maxFun = new FunDef(FreshIdentifier("max"), Nil, Int32Type, maxValDefs, DefType.MethodDef)
+ val maxFun = new FunDef(FreshIdentifier("max"), Nil, Int32Type, maxValDefs)
def maxRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
val v = FreshIdentifier("m", Int32Type)
@@ -107,7 +107,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
def max(xs: Seq[Expr]): Expr = FunctionInvocation(maxFun.typed, xs)
//define min function
val minValDefs: Seq[ValDef] = upperBounds.map(_ => ValDef(FreshIdentifier("b", Int32Type)))
- val minFun = new FunDef(FreshIdentifier("min"), Nil, Int32Type, minValDefs,DefType.MethodDef)
+ val minFun = new FunDef(FreshIdentifier("min"), Nil, Int32Type, minValDefs)
def minRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
val v = FreshIdentifier("m", Int32Type)
@@ -121,12 +121,10 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
def min(xs: Seq[Expr]): Expr = FunctionInvocation(minFun.typed, xs)
val floorFun = new FunDef(FreshIdentifier("floorDiv"), Nil, Int32Type, Seq(
ValDef(FreshIdentifier("x", Int32Type)),
- ValDef(FreshIdentifier("x", Int32Type))),
- DefType.MethodDef)
+ ValDef(FreshIdentifier("x", Int32Type))))
val ceilingFun = new FunDef(FreshIdentifier("ceilingDiv"), Nil, Int32Type, Seq(
ValDef(FreshIdentifier("x", Int32Type)),
- ValDef(FreshIdentifier("x", Int32Type))),
- DefType.MethodDef)
+ ValDef(FreshIdentifier("x", Int32Type))))
ceilingFun.body = Some(IntLiteral(0))
def floorDiv(x: Expr, y: Expr): Expr = FunctionInvocation(floorFun.typed, Seq(x, y))
def ceilingDiv(x: Expr, y: Expr): Expr = FunctionInvocation(ceilingFun.typed, Seq(x, y))
@@ -192,7 +190,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val concretePre = replace(Map(Variable(k) -> loopCounter), pre)
val concreteTerm = replace(Map(Variable(k) -> loopCounter), term)
val returnType = tupleTypeWrap(problem.xs.map(_.getType))
- val funDef = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, returnType, Seq(ValDef(loopCounter.id)),DefType.MethodDef)
+ val funDef = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, returnType, Seq(ValDef(loopCounter.id)))
val funBody = expandAndSimplifyArithmetic(IfExpr(
LessThan(loopCounter, IntLiteral(0)),
Error(returnType, "No solution exists"),
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 11c2b6a66c34e7a3eb6baf9e4f3d0043e2202338..8656a2005ce10781ab219ee703a37d01f4073ba5 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -28,13 +28,13 @@ trait StructuralSize {
FreshIdentifier(name, alwaysShowUniqueID = true),
Seq(), // no type params
tp, // return type
- Seq(ValDef(x)),
- DefType.MethodDef
+ Seq(ValDef(x))
)
absFun.body = Some(IfExpr(
- GreaterEquals(Variable(x), zero),
- Variable(x),
- uminus(Variable(x))))
+ GreaterEquals(Variable(x), zero),
+ Variable(x),
+ uminus(Variable(x))
+ ))
TypedFunDef(absFun, Seq()) // Seq() because no generic type params
}
@@ -56,7 +56,7 @@ trait StructuralSize {
case None =>
val argument = ValDef(FreshIdentifier("x", argumentType, true))
val formalTParams = typeParams.map(TypeParameterDef)
- val fd = new FunDef(FreshIdentifier("size", alwaysShowUniqueID = true), formalTParams, IntegerType, Seq(argument), DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier("size", alwaysShowUniqueID = true), formalTParams, IntegerType, Seq(argument))
sizeCache(argumentType) = fd
val body = simplifyLets(matchToIfThenElse(matchExpr(argument.toVariable, cases(argumentType))))
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 60c2702485c3cdd55abab16e616dcca5d6952a80..be022631ce3c1cb1095b321fcca6bdbd5c824bbe 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -17,7 +17,6 @@ object PreprocessingPhase extends TransformationPhase {
def apply(ctx: LeonContext, p: Program): Program = {
val phases =
- ScopingPhase andThen
MethodLifting andThen
TypingPhase andThen
ConvertWithOracle andThen
diff --git a/src/main/scala/leon/utils/ScopingPhase.scala b/src/main/scala/leon/utils/ScopingPhase.scala
deleted file mode 100644
index d45b7d4671a519d4eff66d661ef7ac9b32517efb..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/utils/ScopingPhase.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.utils
-
-import leon._
-import purescala.Definitions._
-
-object ScopingPhase extends UnitPhase[Program] {
-
- val name = "Scoping phase"
- val description = "Insert scoping information to all definitions in the program"
-
- def apply(ctx: LeonContext, p: Program) {
- insertScopingInformation(p, None)
- }
-
- private def insertScopingInformation(df : Definition , parent : Option[Definition]) {
- df.origOwner = parent
- for (sub <- df.subDefinitions){
- insertScopingInformation(sub, Some(df))
- }
- }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 0af3318395d518743208ce3c7777c3c774354bea..0a487ef2842cc1b5da6e7aac77b585d4113e6335 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -26,8 +26,8 @@ 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), fd.defType).setPos(fd)
- freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType)).setPos(fd)
+ freshFunDef.copyContentFrom(fd)
fun2FreshFun += (fd -> freshFunDef)
} else {
fun2FreshFun += (fd -> fd) //this will make the next step simpler
@@ -97,8 +97,8 @@ 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), fd.defType).setPos(fd)
- freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType)).setPos(fd)
+ freshFunDef.copyContentFrom(fd)
fun2FreshFun += (fd -> freshFunDef)
freshFunDef.fullBody = removeUnit(fd.fullBody)
val restRec = removeUnit(b)
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 3b42be929f2aba4917509f054af463d0fc83a4e6..91b39ad5bf104583025e9791ea97196a517fc7d3 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -23,7 +23,7 @@ object EpsilonElimination extends UnitPhase[Program] {
val newBody = postMap{
case eps@Epsilon(pred, tpe) =>
val freshName = FreshIdentifier("epsilon")
- val newFunDef = new FunDef(freshName, Nil, tpe, Seq(), DefType.MethodDef)
+ val newFunDef = new FunDef(freshName, Nil, tpe, Seq())
val epsilonVar = EpsilonVariable(eps.getPos, tpe)
val resId = FreshIdentifier("res", tpe)
val postcondition = replace(Map(epsilonVar -> Variable(resId)), pred)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index a4d8b18c22db9b0bf47d045c52d08a50a76d91be..5abf808f41fb62b531a416f50345c94dc9a24439 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -152,7 +152,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunValDefs = whileFunVars.map(ValDef(_))
val whileFunReturnType = tupleTypeWrap(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs,DefType.MethodDef).setPos(wh)
+ val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs).setPos(wh)
wasLoop += whileFunDef
val whileFunCond = condScope(condRes)
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 2828a220fbcee0c6ffd470cbc3d1431513c45c1c..1cd0961bc11f3f5f8e23fb99b598303476fffa3f 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -29,20 +29,13 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
PrintTreePhase("Program after xlang transformations").run(ctx)(pgm2)
}
-
- def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
+ def functionWasLoop(fd: FunDef): Boolean = fd.flags.collectFirst{ case IsLoop(fd) => fd } match {
case Some(nested) => // could have been a LetDef originally
wasLoop.contains(nested)
case _ => false //meaning, this was a top level function
}
- var subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
- //pgm2.definedFunctions.foreach { fd => fd.owner match {
- // case Some(p : FunDef) =>
- // subFunctionsOf += p -> (subFunctionsOf(p) + fd)
- // case _ =>
- //}}
-
+ val subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
val newOptions = ctx.options map {
case LeonOption(SharedOptions.optFunctions, fs) => {
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverSuite.scala b/src/test/scala/leon/test/solvers/UnrollingSolverSuite.scala
index c6cfc68388636b381e696a01b59f002ffad492d8..d410aadfa6a1c5eb9222d2450057448808741d80 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverSuite.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverSuite.scala
@@ -15,7 +15,7 @@ class UnrollingSolverSuite extends LeonTestSuite {
private val fx : Identifier = FreshIdentifier("x", IntegerType)
private val fres : Identifier = FreshIdentifier("res", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil)
fDef.body = Some(IfExpr(GreaterThan(Variable(fx), InfiniteIntegerLiteral(0)),
Plus(Variable(fx), FunctionInvocation(fDef.typed, Seq(Minus(Variable(fx), InfiniteIntegerLiteral(1))))),
InfiniteIntegerLiteral(1)
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 544d9cd4ae663bfcd5e102ef3464d26c49e37d26..3df66679b640e3d02a7904c91120f9ba8e584b56 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -38,7 +38,7 @@ class FairZ3SolverTests extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index a6ae287369fdc5b7d1c540ec289c46dfa2b062db..9a5355348698e4ef030110655505cdf257625bd9 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -47,7 +47,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index b59e7437a89ef0a0befdf75a181cc50511c6ee49..99cd00bc9bd718076597310f9bf07e68a5e8ee4c 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -40,17 +40,17 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
// g is a function that is not in the program (on purpose)
- private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
+ private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, IntegerType, ValDef(fx) :: Nil)
gDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
List(UnitDef(
- FreshIdentifier("Minimal"),
- List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false)
+ FreshIdentifier("Minimal"),
+ List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false)
)))
)