diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index f5cd07d4172902aee5a63da9464dec2e3ffbc822..63bf384f24187a5ede39dcbdf39e90400803fccf 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -13,5 +13,7 @@ package object annotation {
class ignore extends StaticAnnotation
@ignore
class extern extends StaticAnnotation
+ @ignore
+ class inline extends StaticAnnotation
}
diff --git a/library/lang/package.scala b/library/lang/package.scala
index 5902e46b15947f968d3ff383e6c1510a563f1c26..21535202b8cc2a5333a6372bde62a48b5fe52576 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -6,17 +6,30 @@ import leon.annotation._
import scala.language.implicitConversions
package object lang {
- @ignore
+
implicit class BooleanDecorations(val underlying: Boolean) {
+ @inline
def holds : Boolean = {
- assert(underlying)
underlying
+ } ensuring {
+ _ == true
}
+
+ @inline
def ==> (that: Boolean): Boolean = {
!underlying || that
}
}
+ implicit class SpecsDecorations[A](val underlying: A) {
+ @inline
+ def computes(target: A) = {
+ underlying
+ } ensuring {
+ res => res == target
+ }
+ }
+
@ignore
object InvariantFunction {
def invariant(x: Boolean): Unit = ()
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 89dca4fcbae9866abb336e27bcadd97d2ad4ee60..79eb4d614ed6ff2ef3f2f5f80e71b2fc5308189f 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -450,7 +450,7 @@ trait CodeGeneration {
// list
// Static lazy fields/ functions
- case FunctionInvocation(tfd, as) =>
+ case fi @ FunctionInvocation(tfd, as) =>
val (cn, mn, ms) = leonFunDefToJVMInfo(tfd.fd).getOrElse {
throw CompilationException("Unknown method : " + tfd.id)
}
@@ -814,11 +814,9 @@ trait CodeGeneration {
ch << InvokeStatic(GenericValuesClass, "get", "(I)Ljava/lang/Object;")
case nt @ NoTree( tp@(Int32Type | BooleanType | UnitType | CharType)) =>
- println("COMPILING "+nt+" TO "+simplestValue(tp))
mkExpr(simplestValue(tp), ch)
case nt @ NoTree(_) =>
- println("COMPILING "+nt+" TO NULL")
ch << ACONST_NULL
case This(ct) =>
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index bee85f77dd6e619de01ed97ca5f09f1de813b0ca..211b7dfc072d7773d7166ddab14c831ada2739ff 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -20,6 +20,17 @@ trait ASTExtractors {
rootMirror.getClassByName(newTermName(str))
}
+ def annotationsOf(s: Symbol): Set[String] = {
+ val actualSymbol = s.accessedOrSelf
+
+ (for {
+ a <- actualSymbol.annotations ++ actualSymbol.owner.annotations
+ name = a.atp.safeToString.replaceAll("\\.package\\.", ".")
+ if (name startsWith "leon.annotation.")
+ } yield {
+ name.split("\\.", 3)(2)
+ }).toSet
+ }
protected lazy val tuple2Sym = classFromName("scala.Tuple2")
protected lazy val tuple3Sym = classFromName("scala.Tuple3")
@@ -295,9 +306,17 @@ trait ASTExtractors {
}
}
+ private def isCaseClass(cd: ClassDef): Boolean = {
+ cd.symbol.isCase && !cd.symbol.isAbstractClass && cd.impl.body.size >= 8
+ }
+
+ private def isImplicitClass(cd: ClassDef): Boolean = {
+ cd.symbol.isImplicit
+ }
+
object ExCaseClass {
def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(Symbol,ValDef)], Template)] = cd match {
- case ClassDef(_, name, tparams, impl) if cd.symbol.isCase && !cd.symbol.isAbstractClass && impl.body.size >= 8 => {
+ case ClassDef(_, name, tparams, impl) if isCaseClass(cd) || isImplicitClass(cd) => {
val constructor: DefDef = impl.children.find {
case ExConstructorDef() => true
case _ => false
@@ -361,10 +380,19 @@ trait ASTExtractors {
* and regardless of its visibility.
*/
def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, Tree)] = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
- name != nme.CONSTRUCTOR && !dd.symbol.isSynthetic && !dd.symbol.isAccessor
- ) =>
- Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if name != nme.CONSTRUCTOR && !dd.symbol.isAccessor =>
+ if (dd.symbol.isSynthetic && dd.symbol.isImplicit && dd.symbol.isMethod) {
+ // Check that the class it was generated from is not ignored
+ if (annotationsOf(tpt.symbol)("ignore")) {
+ None
+ } else {
+ Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
+ }
+ } else if (!dd.symbol.isSynthetic) {
+ Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
+ } else {
+ None
+ }
case _ => None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 7a77450a7b41a8248b85fdddc3d19448588a9035..b159fdbdba34313cbe538767910750010456d45d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -13,7 +13,6 @@ import Definitions.{
ModuleDef => LeonModuleDef,
ValDef => LeonValDef,
Import => LeonImport,
- Annotation => LeonAnnotation,
_
}
@@ -45,18 +44,6 @@ trait CodeExtraction extends ASTExtractors {
val reporter = self.ctx.reporter
- def annotationsOf(s: Symbol): Set[String] = {
- val actualSymbol = s.accessedOrSelf
-
- (for {
- a <- actualSymbol.annotations ++ actualSymbol.owner.annotations
- name = a.atp.safeToString.replaceAll("\\.package\\.", ".")
- if (name startsWith "leon.annotation.")
- } yield {
- name.split("\\.", 3)(2)
- }).toSet
- }
-
implicit def scalaPosToLeonPos(p: global.Position): LeonPosition = {
if (p == NoPosition) {
leon.utils.NoPosition
@@ -655,7 +642,11 @@ trait CodeExtraction extends ASTExtractors {
fd.setPos(sym.pos)
- fd.addFlag(annotationsOf(sym).toSeq.map(LeonAnnotation) : _*)
+ fd.addFlags(annotationsOf(sym).map(FunctionFlag.fromName))
+
+ if (sym.isImplicit) {
+ fd.addFlag(IsInlined)
+ }
defsToDefs += sym -> fd
@@ -675,7 +666,7 @@ trait CodeExtraction extends ASTExtractors {
fd.setPos(sym.pos)
fd.addFlag(IsField(isLazy))
- fd.addFlag(annotationsOf(sym).toSeq.map(LeonAnnotation) : _*)
+ fd.addFlags(annotationsOf(sym).map(FunctionFlag.fromName))
defsToDefs += sym -> fd
@@ -1068,7 +1059,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
- fd.addFlag(annotationsOf(d.symbol).toSeq.map(LeonAnnotation) : _*)
+ fd.addFlags(annotationsOf(d.symbol).map(FunctionFlag.fromName))
val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 64a0dca50c0b66ceb685be331588fa703f2f62e3..7e4d216a32bbef4801936cb76f6bf8588820e52e 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -347,6 +347,20 @@ object DefOps {
res
}
+ // @Note: This function does not remove functions in classdefs
+ def removeDefs(p: Program, dds: Set[Definition]): Program = {
+ p.copy(units = for (u <- p.units if !dds(u)) yield {
+ u.copy(
+ defs = for (d <- u.defs if !dds(d)) yield d match {
+ case md: ModuleDef =>
+ md.copy(defs = md.defs.filterNot(dds))
+
+ case cd => cd
+ }
+ )
+ })
+ }
+
/**
* Returns a call graph starting from the given sources, taking into account
* instantiations of function type parameters,
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 9f56f7ba1fcf3d190a5e9d37f529acdc580a44b2..127c562217fbb8d64329d87db3bbff969231405a 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -303,7 +303,15 @@ object Definitions {
}
// A class that represents flags that annotate a FunDef with different attributes
- class FunctionFlag
+ sealed abstract class FunctionFlag
+
+ object FunctionFlag {
+ def fromName(name: String): FunctionFlag = name match {
+ case "inline" => IsInlined
+ case _ => Annotation(name)
+ }
+ }
+
// Whether this FunDef was originally a (lazy) field
case class IsField(isLazy: Boolean) extends FunctionFlag
// Compiler annotations given in the source code as @annot
@@ -317,6 +325,8 @@ object Definitions {
case object IsAbstract extends FunctionFlag
// Currently, the only synthetic functions are those that calculate default values of parameters
case object IsSynthetic extends FunctionFlag
+ // Is inlined
+ case object IsInlined extends FunctionFlag
/** Functions
* This class represents methods or fields of objects. By "fields" we mean
@@ -376,20 +386,22 @@ object Definitions {
def copyContentFrom(from : FunDef) {
this.fullBody = from.fullBody
- this.addFlag(from.flags.toSeq : _*)
+ this.addFlags(from.flags)
}
/* Flags */
- private var flags_ : Set[FunctionFlag] = Set()
-
- def addFlag(flags: FunctionFlag*): FunDef = {
+ private[this] var flags_ : Set[FunctionFlag] = Set()
+
+ def addFlags(flags: Set[FunctionFlag]): FunDef = {
this.flags_ ++= flags
this
}
-
+
+ def addFlag(flag: FunctionFlag): FunDef = addFlags(Set(flag))
+
def flags = flags_
-
+
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
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b156a4bde8b102ee148dd2cbb4774868d7fc5480..66b1ed28a43b7849049d4a8bf726c8b49ab47c6d 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -472,6 +472,9 @@ object ExprOps {
case TupleSelect(LetTuple(ids, v, b), ts) =>
Some(letTuple(ids, v, tupleSelect(b, ts, true)))
+ case CaseClassSelector(cct, cc: CaseClass, id) =>
+ Some(CaseClassSelector(cct, cc, id))
+
case IfExpr(c, thenn, elze) if (thenn == elze) && isDeterministic(e) =>
Some(thenn)
diff --git a/src/main/scala/leon/utils/InliningPhase.scala b/src/main/scala/leon/utils/InliningPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5382275db54b3508a63aee57a11b5f229078f545
--- /dev/null
+++ b/src/main/scala/leon/utils/InliningPhase.scala
@@ -0,0 +1,51 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.utils
+
+import leon._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.TypeOps._
+import purescala.ExprOps._
+import purescala.DefOps._
+
+object InliningPhase extends TransformationPhase {
+
+ val name = "Inline @inline functions"
+ val description = "Inline functions marked as @inline and remove their definitions"
+
+ def apply(ctx: LeonContext, p: Program): Program = {
+ val toInline = p.definedFunctions.filter(_.flags(IsInlined)).toSet
+
+ val substs = toInline.map { fd =>
+ fd -> { (tps: Seq[TypeTree], s: Seq[Expr]) =>
+ val newBody = replaceFromIDs(fd.params.map(_.id).zip(s).toMap, fd.fullBody)
+ instantiateType(newBody, (fd.tparams zip tps).toMap, Map())
+ }
+ }.toMap
+
+ def simplifyImplicitClass(e: Expr) = e match {
+ case CaseClassSelector(cct, cc: CaseClass, id) =>
+ Some(CaseClassSelector(cct, cc, id))
+
+ case _ =>
+ None
+ }
+
+ def simplify(e: Expr) = {
+ fixpoint(postMap(simplifyImplicitClass _))(e)
+ }
+
+ val (np, _) = replaceFunDefs(p)({fd => None}, {(fi, fd) =>
+ if (substs contains fd) {
+ Some(simplify(substs(fd)(fi.tfd.tps, fi.args)))
+ } else {
+ None
+ }
+ })
+
+ removeDefs(np, toInline.map { fd => (fd: Definition) })
+ }
+
+}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index be022631ce3c1cb1095b321fcca6bdbd5c824bbe..8fdf84f8d733e5e476ed0b4f0688138f7bd9989e 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -23,7 +23,8 @@ object PreprocessingPhase extends TransformationPhase {
ConvertHoles andThen
CompleteAbstractDefinitions andThen
CheckADTFieldsTypes andThen
- InjectAsserts
+ InjectAsserts andThen
+ InliningPhase
phases.run(ctx)(p)