From 5611b4e53933aefeb1b6c7bf7a33d38b3250503b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 1 Mar 2016 13:27:31 +0100
Subject: [PATCH] Introduce "Inner" function flag. Exclude inner funs from
synthesis.
---
.../scala/leon/grammars/FunctionCalls.scala | 5 ++---
.../scala/leon/purescala/Definitions.scala | 22 ++++++++++---------
.../leon/purescala/FunctionClosure.scala | 5 +++--
3 files changed, 17 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/grammars/FunctionCalls.scala b/src/main/scala/leon/grammars/FunctionCalls.scala
index 1233fb193..65836341e 100644
--- a/src/main/scala/leon/grammars/FunctionCalls.scala
+++ b/src/main/scala/leon/grammars/FunctionCalls.scala
@@ -63,8 +63,7 @@ case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type
}
}
} else {
- /* All type parameters that used to be free are assigned
- */
+ // All type parameters that used to be free are assigned
List(tfd)
}
case None =>
@@ -75,7 +74,7 @@ case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type
}
}
- val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || (exclude contains tfd.fd)
+ val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || tfd.fd.isInner || (exclude contains tfd.fd)
val funcs = visibleFunDefsFromMain(prog).toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
funcs.map{ tfd =>
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 753e92360..2178a07af 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -190,6 +190,13 @@ object Definitions {
}
}
+ /** A trait that represents flags that annotate a ClassDef with different attributes */
+ sealed trait ClassFlag
+
+ object ClassFlag {
+ def fromName(name: String, args: Seq[Option[Any]]): ClassFlag = Annotation(name, args)
+ }
+
/** A trait that represents flags that annotate a FunDef with different attributes */
sealed trait FunctionFlag
@@ -200,13 +207,6 @@ object Definitions {
}
}
- /** A trait that represents flags that annotate a ClassDef with different attributes */
- sealed trait ClassFlag
-
- object ClassFlag {
- def fromName(name: String, args: Seq[Option[Any]]): ClassFlag = Annotation(name, args)
- }
-
// Whether this FunDef was originally a (lazy) field
case class IsField(isLazy: Boolean) extends FunctionFlag
// Compiler annotations given in the source code as @annot
@@ -224,6 +224,7 @@ object Definitions {
case object IsInlined extends FunctionFlag
// Is an ADT invariant method
case object IsADTInvariant extends FunctionFlag with ClassFlag
+ case object IsInner extends FunctionFlag
/** Represents a class definition (either an abstract- or a case-class) */
sealed trait ClassDef extends Definition {
@@ -357,7 +358,7 @@ object Definitions {
): AbstractClassDef = {
val acd = new AbstractClassDef(id, tparams, parent)
acd.addFlags(this.flags)
- parent.map(_.classDef.ancestors.map(_.registerChild(acd)))
+ parent.foreach(_.classDef.ancestors.foreach(_.registerChild(acd)))
acd.copiedFrom(this)
}
}
@@ -398,7 +399,7 @@ object Definitions {
def typed: CaseClassType = typed(tparams.map(_.tp))
/** Duplication of this [[CaseClassDef]].
- * @note This will not replace recursive case class def calls in [[arguments]] nor the parent abstract class types
+ * @note This will not replace recursive [[CaseClassDef]] calls in [[fields]] nor the parent abstract class types
*/
def duplicate(
id: Identifier = this.id.freshen,
@@ -411,7 +412,7 @@ object Definitions {
cd.setFields(fields)
cd.addFlags(this.flags)
cd.copiedFrom(this)
- parent.map(_.classDef.ancestors.map(_.registerChild(cd)))
+ parent.foreach(_.classDef.ancestors.foreach(_.registerChild(cd)))
cd
}
}
@@ -506,6 +507,7 @@ object Definitions {
def isRealFunction = !canBeField
def isSynthetic = flags contains IsSynthetic
def isInvariant = flags contains IsADTInvariant
+ def isInner = flags contains IsInner
def methodOwner = flags collectFirst { case IsMethod(cd) => cd }
/* Wrapping in TypedFunDef */
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 07c6781a8..ff8feb33e 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -8,8 +8,8 @@ import Expressions._
import ExprOps._
import Constructors._
import TypeOps.instantiateType
-import leon.purescala.Common.Identifier
-import leon.purescala.Types.TypeParameter
+import Common.Identifier
+import Types.TypeParameter
import utils.GraphOps._
object FunctionClosure extends TransformationPhase {
@@ -108,6 +108,7 @@ object FunctionClosure extends TransformationPhase {
}
val funs = closed.values.toSeq.map{ _.newFd }
+ funs foreach (_.addFlag(IsInner))
// Recursively close new functions
fd +: funs.flatMap(close)
--
GitLab