diff --git a/build.sbt b/build.sbt
index 4de988e5dc18eb4aa5c9dbf6a9c8e7f6178f1ef9..359c39a0bcd372b0d337eb80c11760c95a792b6f 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,17 +4,15 @@ version := "2.0"
organization := "ch.epfl.lara"
-scalaVersion := "2.9.2"
+scalaVersion := "2.10.2"
scalacOptions += "-deprecation"
scalacOptions += "-unchecked"
-javacOptions += "-Xlint:unchecked"
-
-libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.2"
+scalacOptions += "-feature"
-libraryDependencies += "org.scalatest" %% "scalatest" % "1.8" % "test"
+javacOptions += "-Xlint:unchecked"
if(System.getProperty("sun.arch.data.model") == "64") {
unmanagedBase <<= baseDirectory { base => base / "unmanaged" / "64" }
@@ -24,7 +22,11 @@ if(System.getProperty("sun.arch.data.model") == "64") {
resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/"
-libraryDependencies += "com.typesafe.akka" % "akka-actor" % "2.0.4"
+libraryDependencies ++= Seq(
+ "org.scala-lang" % "scala-compiler" % "2.10.2",
+ "org.scalatest" %% "scalatest" % "1.9.1" excludeAll(ExclusionRule(organization="org.scala-lang")),
+ "com.typesafe.akka" %% "akka-actor" % "2.1.4"
+)
fork in run := true
diff --git a/library/build.sbt b/library/build.sbt
index 6d2b7989698b6b07736a2a0ba5c2189e5b73e36c..0c4c88e13c3096c5e4b9976ab021083f8569aa38 100644
--- a/library/build.sbt
+++ b/library/build.sbt
@@ -4,10 +4,12 @@ version := "2.0"
organization := "ch.epfl.lara"
-scalaVersion := "2.9.2"
+scalaVersion := "2.10.2"
scalacOptions += "-deprecation"
scalacOptions += "-unchecked"
-libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.9.2"
+scalacOptions += "-feature"
+
+libraryDependencies += "org.scala-lang" % "scala-compiler" % "2.10.2"
diff --git a/library/src/main/scala/leon/Annotations.scala b/library/src/main/scala/leon/Annotations.scala
index a441066401489312eefcb1261da1722a9184f561..aac4cf423a28fd79d9df4a95ef094c83d765b136 100644
--- a/library/src/main/scala/leon/Annotations.scala
+++ b/library/src/main/scala/leon/Annotations.scala
@@ -2,6 +2,8 @@
package leon
+import scala.annotation.StaticAnnotation
+
object Annotations {
class induct extends StaticAnnotation
class axiomatize extends StaticAnnotation
diff --git a/library/src/main/scala/leon/Utils.scala b/library/src/main/scala/leon/Utils.scala
index ab3e84eb52acb45abc724f9935f0268142f1fc8f..d34bcd0e9c36c572fa9b4948e71a7b7b09185b7e 100644
--- a/library/src/main/scala/leon/Utils.scala
+++ b/library/src/main/scala/leon/Utils.scala
@@ -2,6 +2,8 @@
package leon
+import scala.language.implicitConversions
+
object Utils {
sealed class IsValid(val property : Boolean) {
def holds : Boolean = {
diff --git a/project/Build.scala b/project/Build.scala
index eff96902f72a6c297c0760677bd9832dffdd78d7..02a430d7676d6eefb5da891ef602f213b77de7b2 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -43,7 +43,7 @@ object Leon extends Build {
val ldLibPath = if (is64) ldLibraryDir64.absolutePath else ldLibraryDir32.absolutePath
- val leonLibPath = depsPaths.find(_.endsWith("/library/target/scala-2.9.2/classes")) match {
+ val leonLibPath = depsPaths.find(_.endsWith("/library/target/scala-2.10/classes")) match {
case None => throw new Exception("Couldn't find leon-library in the classpath.")
case Some(p) => p
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 9055d9bee9ce9d42bc81efe872b427db445991e2..88c072dcf52c8c7a024b84bac6bf064374c4e6fd 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -78,7 +78,7 @@ object Main {
val leonOpt: LeonOption = opt.substring(2, opt.length).split("=", 2).toList match {
case List(name, value) =>
LeonValueOption(name, value)
- case List(name) => name
+ case List(name) =>
LeonFlagOption(name)
case _ =>
reporter.fatalError("Woot?")
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 80c834506198d3e673a6f5ad8f42f625d4fa0cdc..6438bb8d19538d50a663c87b9299fc79aa2d0e7c 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -5,8 +5,8 @@ package leon
abstract class Pipeline[-F, +T] {
self =>
- def andThen[G](then: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
- def run(ctx : LeonContext)(v : F) : G = then.run(ctx)(self.run(ctx)(v))
+ def andThen[G](thenn: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
+ def run(ctx : LeonContext)(v : F) : G = thenn.run(ctx)(self.run(ctx)(v))
}
def run(ctx: LeonContext)(v: F): T
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 83b9aec06b0c5fd8199127553cc170b1730c90d1..8db2e5acf8b5db8e6829232e0b25c56f6bce54d9 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -49,7 +49,7 @@ class DefaultReporter extends Reporter {
Console.BLUE
}
"[" + color + pfx.substring(1, pfx.length-2) + Console.RESET + "] " +
- msg.trim.replaceAll("\n", "\n" + (" " * (pfx.size)))
+ msg.replaceAll("\n", "\n" + (" " * (pfx.size)))
}
def errorFunction(msg: Any) = output(reline(errorPfx, msg.toString))
@@ -65,5 +65,5 @@ class QuietReporter extends DefaultReporter {
class SilentReporter extends QuietReporter {
override def errorFunction(msg : Any) = {}
- override def fatalErrorFunction(msg : Any) = throw new Exception("Fatal error: " + msg.toString)
+ override def fatalErrorFunction(msg: Any) = throw LeonFatalError()
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 4271bf85d31b619698752928cacc3c420f0d2202..a9605e6203fe948439fb2f8a84d29387b0b6f1c0 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -8,7 +8,6 @@ object Settings {
lazy val reporter: Reporter = new DefaultReporter
var showIDs: Boolean = false
- var silentlyTolerateNonPureBodies: Boolean = false
def defaultClassPath() = {
val leonLib = System.getenv("LEON_LIBRARY_PATH")
@@ -35,12 +34,13 @@ object Settings {
}
case class Settings(
- val termination: Boolean = false,
- val synthesis: Boolean = false,
- val xlang: Boolean = false,
- val verify: Boolean = true,
+ val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
+ val termination: Boolean = false,
+ val synthesis: Boolean = false,
+ val xlang: Boolean = false,
+ val verify: Boolean = true,
// This is a list of directories that is passed as class-path of the inner-compiler.
// It needs to contain at least a directory containing scala-library.jar, and
// one for the leon runtime library.
- val classPath: List[String] = Settings.defaultClassPath()
+ val classPath: List[String] = Settings.defaultClassPath()
)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 9e23300c03f0affd2d51d25862ec88b62f8508ee..80d55ab9eef90931627ac82d1fd8ff3dd775899d 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -414,10 +414,10 @@ object CodeGeneration {
}
}
- private[codegen] def mkBranch(cond : Expr, then : String, elze : String, ch : CodeHandler, canDelegateToMkExpr : Boolean = true)(implicit env : CompilationEnvironment) {
+ private[codegen] def mkBranch(cond : Expr, thenn : String, elze : String, ch : CodeHandler, canDelegateToMkExpr : Boolean = true)(implicit env : CompilationEnvironment) {
cond match {
case BooleanLiteral(true) =>
- ch << Goto(then)
+ ch << Goto(thenn)
case BooleanLiteral(false) =>
ch << Goto(elze)
@@ -426,63 +426,63 @@ object CodeGeneration {
val fl = ch.getFreshLabel("andnext")
mkBranch(es.head, fl, elze, ch)
ch << Label(fl)
- mkBranch(And(es.tail), then, elze, ch)
+ mkBranch(And(es.tail), thenn, elze, ch)
case Or(es) =>
val fl = ch.getFreshLabel("ornext")
- mkBranch(es.head, then, fl, ch)
+ mkBranch(es.head, thenn, fl, ch)
ch << Label(fl)
- mkBranch(Or(es.tail), then, elze, ch)
+ mkBranch(Or(es.tail), thenn, elze, ch)
case Implies(l, r) =>
- mkBranch(Or(Not(l), r), then, elze, ch)
+ mkBranch(Or(Not(l), r), thenn, elze, ch)
case Not(c) =>
- mkBranch(c, elze, then, ch)
+ mkBranch(c, elze, thenn, ch)
case Variable(b) =>
- ch << ILoad(slotFor(b)) << IfEq(elze) << Goto(then)
+ ch << ILoad(slotFor(b)) << IfEq(elze) << Goto(thenn)
case Equals(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
l.getType match {
case Int32Type | BooleanType | UnitType =>
- ch << If_ICmpEq(then) << Goto(elze)
+ ch << If_ICmpEq(thenn) << Goto(elze)
case _ =>
ch << InvokeVirtual("java/lang/Object", "equals", "(Ljava/lang/Object;)Z")
- ch << IfEq(elze) << Goto(then)
+ ch << IfEq(elze) << Goto(thenn)
}
case Iff(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpEq(then) << Goto(elze)
+ ch << If_ICmpEq(thenn) << Goto(elze)
case LessThan(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpLt(then) << Goto(elze)
+ ch << If_ICmpLt(thenn) << Goto(elze)
case GreaterThan(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpGt(then) << Goto(elze)
+ ch << If_ICmpGt(thenn) << Goto(elze)
case LessEquals(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpLe(then) << Goto(elze)
+ ch << If_ICmpLe(thenn) << Goto(elze)
case GreaterEquals(l,r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << If_ICmpGe(then) << Goto(elze)
+ ch << If_ICmpGe(thenn) << Goto(elze)
case other if canDelegateToMkExpr =>
mkExpr(other, ch, canDelegateToMkBranch = false)
- ch << IfEq(elze) << Goto(then)
+ ch << IfEq(elze) << Goto(thenn)
case other => throw CompilationException("Unsupported branching expr. : " + other)
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 1c5b5eac369b435e2a9970a399dfff74482ac347..d62fb9fbc3a621b0037b881914fbfb8f046cc943 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -43,6 +43,8 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
}).toMap
}
+ val a = 42
+
private def writeClassFiles() {
for ((d, cl) <- classes) {
cl.writeToFile(cl.className + ".class")
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index d29f91c508d968e370543d2f276e807d41a50dd3..024665d055e99e93ab594ebbb7ba201074c6b200 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -56,10 +56,10 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
rec(ctx + ((i -> first)), b)
}
case Error(desc) => throw RuntimeError("Error reached in evaluation: " + desc)
- case IfExpr(cond, then, elze) => {
+ case IfExpr(cond, thenn, elze) => {
val first = rec(ctx, cond)
first match {
- case BooleanLiteral(true) => rec(ctx, then)
+ case BooleanLiteral(true) => rec(ctx, thenn)
case BooleanLiteral(false) => rec(ctx, elze)
case _ => throw EvalError(typeErrorMsg(first, BooleanType))
}
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
deleted file mode 100644
index 49a62fcb4b521e308b42a33477feef70f9557287..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ /dev/null
@@ -1,44 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-package plugin
-
-import scala.tools.nsc._
-import scala.tools.nsc.plugins._
-
-import purescala.Definitions.Program
-import synthesis.SynthesisPhase
-
-class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
- extends PluginComponent
- with CodeExtraction
-{
- import global._
-
- // This is how it works from 2.8 on..
- override val runsRightAfter: Option[String] = None
- override val runsAfter: List[String] = List("refchecks")
-
- val phaseName = pluginInstance.name
-
- /** this is initialized when the Leon phase starts*/
- var fresh: scala.tools.nsc.util.FreshNameCreator = null
-
- protected def stopIfErrors: Unit = {
- if(reporter.hasErrors) {
- throw LeonFatalError()
- }
- }
-
- def newPhase(prev: Phase) = new AnalysisPhase(prev)
-
- class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
- def apply(unit: CompilationUnit): Unit = {
- //global ref to freshName creator
- fresh = unit.fresh
-
-
- pluginInstance.global.program = Some(extractCode(unit))
- }
- }
-}
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index b03a8438f9dd661caec6d034f5fdf5f51e4162ab..bd07bf48b594a144b27ab9d48b16e5ba451eacc5 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -6,16 +6,18 @@ package plugin
import scala.tools.nsc._
import scala.tools.nsc.plugins._
+import scala.language.implicitConversions
+
import purescala.Definitions._
-import purescala.Trees._
-import xlang.Trees.{Block => PBlock, _}
+import purescala.Trees.{Expr => LeonExpr, _}
+import xlang.Trees.{Block => LeonBlock, _}
import xlang.TreeOps._
-import purescala.TypeTrees._
+import purescala.TypeTrees.{TypeTree => LeonType, _}
import purescala.Common._
import purescala.TreeOps._
trait CodeExtraction extends Extractors {
- self: AnalysisComponent =>
+ self: LeonExtraction =>
import global._
import global.definitions._
@@ -23,1114 +25,1009 @@ trait CodeExtraction extends Extractors {
import ExpressionExtractors._
import ExtractorHelpers._
-
- private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
- private lazy val mapTraitSym = definitions.getClass("scala.collection.immutable.Map")
- private lazy val multisetTraitSym = try {
- definitions.getClass("scala.collection.immutable.Multiset")
- } catch {
- case _ => null
- }
- private lazy val optionClassSym = definitions.getClass("scala.Option")
- private lazy val someClassSym = definitions.getClass("scala.Some")
- private lazy val function1TraitSym = definitions.getClass("scala.Function1")
-
- private lazy val arraySym = definitions.getClass("scala.Array")
-
- def isArrayClassSym(sym: Symbol): Boolean = sym == arraySym
-
- def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
- def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
- def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
- def isTuple5(sym : Symbol) : Boolean = sym == tuple5Sym
-
- def isSetTraitSym(sym : Symbol) : Boolean = {
- sym == setTraitSym || sym.tpe.toString.startsWith("scala.Predef.Set")
- }
-
- def isMapTraitSym(sym : Symbol) : Boolean = {
- sym == mapTraitSym || sym.tpe.toString.startsWith("scala.Predef.Map")
+ class ScalaPos(p: global.Position) extends ScalacPositional {
+ setPosInfo(p.line, p.column)
}
- def isMultisetTraitSym(sym : Symbol) : Boolean = {
- sym == multisetTraitSym
+ implicit def scalaPosToLeonPos(p: global.Position): ScalacPositional = {
+ new ScalaPos(p)
}
- def isOptionClassSym(sym : Symbol) : Boolean = {
- sym == optionClassSym || sym == someClassSym
- }
-
- def isFunction1TraitSym(sym : Symbol) : Boolean = {
- sym == function1TraitSym
- }
-
- private val mutableVarSubsts: scala.collection.mutable.Map[Symbol,Function0[Expr]] =
- scala.collection.mutable.Map.empty[Symbol,Function0[Expr]]
- private val varSubsts: scala.collection.mutable.Map[Symbol,Function0[Expr]] =
- scala.collection.mutable.Map.empty[Symbol,Function0[Expr]]
+ private val mutableVarSubsts: scala.collection.mutable.Map[Symbol,Function0[LeonExpr]] =
+ scala.collection.mutable.Map.empty[Symbol,Function0[LeonExpr]]
+ private val varSubsts: scala.collection.mutable.Map[Symbol,Function0[LeonExpr]] =
+ scala.collection.mutable.Map.empty[Symbol,Function0[LeonExpr]]
private val classesToClasses: scala.collection.mutable.Map[Symbol,ClassTypeDef] =
scala.collection.mutable.Map.empty[Symbol,ClassTypeDef]
private val defsToDefs: scala.collection.mutable.Map[Symbol,FunDef] =
scala.collection.mutable.Map.empty[Symbol,FunDef]
- def extractCode(unit: CompilationUnit): Program = {
- import scala.collection.mutable.HashMap
+ /** An exception thrown when non-purescala compatible code is encountered. */
+ sealed case class ImpureCodeEncounteredException(tree: Tree) extends Exception
- def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
- case Some(ex) => ex
- case None => stopIfErrors; scala.sys.error("unreachable error.")
- }
+ /** Attempts to convert a scalac AST to a pure scala AST. */
+ private var currentFunDef: FunDef = null
- def st2ps(tree: Type): purescala.TypeTrees.TypeTree = toPureScalaType(unit)(tree) match {
- case Some(tt) => tt
- case None => stopIfErrors; scala.sys.error("unreachable error.")
- }
+ //This is a bit missleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
+ //that it can have any owner
+ private var owners: Map[LeonExpr, Option[FunDef]] = Map()
- def extractTopLevelDef: ObjectDef = {
- val top = unit.body match {
- case p @ PackageDef(name, lst) if lst.size == 0 => {
- unit.error(p.pos, "No top-level definition found.")
+
+ class Extraction(unit: CompilationUnit) {
+ def toPureScala(tree: Tree): Option[LeonExpr] = {
+ try {
+ Some(extractTree(tree))
+ } catch {
+ case e: ImpureCodeEncounteredException =>
None
- }
+ }
+ }
- case PackageDef(name, lst) if lst.size > 1 => {
- unit.error(lst(1).pos, "Too many top-level definitions.")
+ // This one never fails, on error, it returns Untyped
+ def toPureScalaType(tpt: Type): LeonType = {
+ try {
+ extractType(tpt)
+ } catch {
+ case e: ImpureCodeEncounteredException =>
+ Untyped
+ }
+ }
+
+ private def extractTopLevelDef: Option[ObjectDef] = {
+ unit.body match {
+ case p @ PackageDef(name, lst) if lst.size == 0 =>
+ reporter.error(p.pos, "No top-level definition found.")
None
- }
- case PackageDef(name, lst) => {
- assert(lst.size == 1)
+ case PackageDef(name, lst) =>
+ if (lst.size > 1) {
+ reporter.error(lst(1).pos, "More than one top-level object. Rest will be ignored.")
+ }
lst(0) match {
- case ExObjectDef(n, templ) => Some(extractObjectDef(n.toString, templ))
- case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
- None
+ case ExObjectDef(n, templ) =>
+ Some(extractObjectDef(n.toString, templ))
+
+ case other @ _ =>
+ reporter.error(other.pos, "Expected: top-level single object.")
+ None
}
}
- }
-
- stopIfErrors
- top.get
}
- def extractObjectDef(nameStr: String, tmpl: Template): ObjectDef = {
+ private def extractObjectDef(nameStr: String, tmpl: Template): ObjectDef = {
// we assume that the template actually corresponds to an object
// definition. Typically it should have been obtained from the proper
// extractor (ExObjectDef)
- var classDefs: List[ClassTypeDef] = Nil
- var objectDefs: List[ObjectDef] = Nil
- var funDefs: List[FunDef] = Nil
-
- val scalaClassSyms: scala.collection.mutable.Map[Symbol,Identifier] =
- scala.collection.mutable.Map.empty[Symbol,Identifier]
- val scalaClassArgs: scala.collection.mutable.Map[Symbol,Seq[(String,Tree)]] =
- scala.collection.mutable.Map.empty[Symbol,Seq[(String,Tree)]]
- val scalaClassNames: scala.collection.mutable.Set[String] =
- scala.collection.mutable.Set.empty[String]
+ var scalaClassSyms = Map[Symbol,Identifier]()
+ var scalaClassArgs = Map[Symbol,Seq[(String,Tree)]]()
+ var scalaClassNames = Set[String]()
// we need the new type definitions before we can do anything...
- tmpl.body.foreach(t =>
- t match {
- case ExAbstractClass(o2, sym) => {
- if(scalaClassNames.contains(o2)) {
- unit.error(t.pos, "A class with the same name already exists.")
- } else {
- scalaClassSyms += (sym -> FreshIdentifier(o2))
- scalaClassNames += o2
- }
+ for (t <- tmpl.body) t match {
+ case ExAbstractClass(o2, sym) =>
+ if(scalaClassNames.contains(o2)) {
+ reporter.error(t.pos, "A class with the same name already exists.")
+ } else {
+ scalaClassSyms += sym -> FreshIdentifier(o2)
+ scalaClassNames += o2
}
- case ExCaseClass(o2, sym, args) => {
- if(scalaClassNames.contains(o2)) {
- unit.error(t.pos, "A class with the same name already exists.")
- } else {
- scalaClassSyms += (sym -> FreshIdentifier(o2))
- scalaClassNames += o2
- scalaClassArgs += (sym -> args)
- }
+
+ case ExCaseClass(o2, sym, args) =>
+ if(scalaClassNames.contains(o2)) {
+ reporter.error(t.pos, "A class with the same name already exists.")
+ } else {
+ scalaClassSyms += sym -> FreshIdentifier(o2)
+ scalaClassNames += o2
+ scalaClassArgs += sym -> args
}
- case _ => ;
- }
- )
- stopIfErrors
+ case _ =>
+ }
- scalaClassSyms.foreach(p => {
- if(p._1.isAbstractClass) {
- classesToClasses += (p._1 -> new AbstractClassDef(p._2))
- } else if(p._1.isCase) {
- val ccd = new CaseClassDef(p._2)
- ccd.isCaseObject = p._1.isModuleClass
- classesToClasses += (p._1 -> ccd)
- }
- })
+ for ((sym, id) <- scalaClassSyms) {
+ if (sym.isAbstractClass) {
+ classesToClasses += sym -> new AbstractClassDef(id)
+ } else {
+ val ccd = new CaseClassDef(id)
+ ccd.isCaseObject = sym.isModuleClass
+ classesToClasses += sym -> ccd
+ }
+ }
- classesToClasses.foreach(p => {
- val superC: List[ClassTypeDef] = p._1.tpe.baseClasses.filter(bcs => scalaClassSyms.exists(pp => pp._1 == bcs) && bcs != p._1).map(s => classesToClasses(s)).toList
+ for ((sym, ctd) <- classesToClasses) {
+ val superClasses: List[ClassTypeDef] = sym.tpe.baseClasses
+ .filter(bcs => scalaClassSyms.contains(bcs) && bcs != sym)
+ .map(s => classesToClasses(s)).toList
- val superAC: List[AbstractClassDef] = superC.map(c => {
- if(!c.isInstanceOf[AbstractClassDef]) {
- unit.error(p._1.pos, "Class is inheriting from non-abstract class.")
- null
- } else {
- c.asInstanceOf[AbstractClassDef]
- }
- }).filter(_ != null)
- if(superAC.length > 1) {
- unit.error(p._1.pos, "Multiple inheritance.")
+ val superAClasses: List[AbstractClassDef] = superClasses.flatMap {
+ case acd: AbstractClassDef =>
+ Some(acd)
+ case c =>
+ reporter.error(sym.pos, "Class "+ctd.id+" is inheriting from non-abstract class "+c.id+".")
+ None
}
- if(superAC.length == 1) {
- p._2.setParent(superAC.head)
+ if (superAClasses.size > 2) {
+ reporter.error(sym.pos, "Multiple inheritance is not permitted, ignoring extra parents.")
}
- if(p._2.isInstanceOf[CaseClassDef]) {
- // this should never fail
- val ccargs = scalaClassArgs(p._1)
- p._2.asInstanceOf[CaseClassDef].fields = ccargs.map(cca => {
- val cctpe = st2ps(cca._2.tpe)
- VarDecl(FreshIdentifier(cca._1).setType(cctpe), cctpe)
- })
- }
- })
+ superAClasses.headOption.foreach{ parent => ctd.setParent(parent) }
- classDefs = classesToClasses.valuesIterator.toList
-
- // end of class (type) extraction
-
- // we now extract the function signatures.
- tmpl.body.foreach(
- _ match {
- case ExMainFunctionDef() => ;
- case dd @ ExFunctionDef(n,p,t,b) => {
- val mods = dd.mods
- val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
- if(mods.isPrivate) funDef.addAnnotation("private")
- for(a <- dd.symbol.annotations) {
- a.atp.safeToString match {
- case "leon.Annotations.induct" => funDef.addAnnotation("induct")
- case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
- case "leon.Annotations.main" => funDef.addAnnotation("main")
- case _ => ;
- }
+ ctd match {
+ case ccd: CaseClassDef =>
+ assert(scalaClassArgs contains sym)
+
+ ccd.fields = scalaClassArgs(sym).map{ case (name, asym) =>
+ val tpe = toPureScalaType(asym.tpe)
+ VarDecl(FreshIdentifier(name).setType(tpe), tpe)
}
- defsToDefs += (dd.symbol -> funDef)
- }
- case _ => ;
+ case _ =>
+ // no fields to set
}
- )
-
- // then their bodies.
- tmpl.body.foreach(
- _ match {
- case ExMainFunctionDef() => ;
- case dd @ ExFunctionDef(n,p,t,b) => {
- val fd = defsToDefs(dd.symbol)
- defsToDefs(dd.symbol) = extractFunDef(fd, b)
+ }
+
+ var classDefs: List[ClassTypeDef] = classesToClasses.values.toList
+
+ // First pass to instanciate all FunDefs
+ for (d <- tmpl.body) d match {
+ case ExMainFunctionDef() =>
+ // we ignore the main function
+
+ case dd @ ExFunctionDef(name, params, tpe, body) =>
+ val funDef = extractFunSig(name, params, tpe).setPosInfo(dd.pos)
+
+ if (dd.mods.isPrivate) {
+ funDef.addAnnotation("private")
}
- case _ => ;
- }
- )
-
- funDefs = defsToDefs.valuesIterator.toList
-
- // we check nothing else is polluting the object.
- tmpl.body.foreach(
- _ match {
- case ExCaseClassSyntheticJunk() => ;
- // case ExObjectDef(o2, t2) => { objectDefs = extractObjectDef(o2, t2) :: objectDefs }
- case ExAbstractClass(_,_) => ;
- case ExCaseClass(_,_,_) => ;
- case ExConstructorDef() => ;
- case ExMainFunctionDef() => ;
- case ExFunctionDef(_,_,_,_) => ;
- case tree => { unit.error(tree.pos, "Don't know what to do with this. Not purescala?"); println(tree) }
- }
- )
- val name: Identifier = FreshIdentifier(nameStr)
- val theDef = new ObjectDef(name, objectDefs.reverse ::: classDefs ::: funDefs, Nil)
-
- theDef
+ for(a <- dd.symbol.annotations) {
+ a.atp.safeToString match {
+ case "leon.Annotations.induct" => funDef.addAnnotation("induct")
+ case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+ case "leon.Annotations.main" => funDef.addAnnotation("main")
+ case _ => ;
+ }
+ }
+
+ defsToDefs += dd.symbol -> funDef
+
+ case _ =>
+ }
+
+ // Second pass to convert function bodies
+ for (d <- tmpl.body) d match {
+ case dd @ ExFunctionDef(_, _, _, body) if defsToDefs contains dd.symbol =>
+ val fd = defsToDefs(dd.symbol)
+
+ extractFunDef(fd, body)
+ case _ =>
+ }
+
+ var funDefs: List[FunDef] = defsToDefs.values.toList
+
+ // FIXME: we check nothing else is polluting the object
+ for (t <- tmpl.body) t match {
+ case ExCaseClassSyntheticJunk() =>
+ case ExAbstractClass(_,_) =>
+ case ExCaseClass(_,_,_) =>
+ case ExConstructorDef() =>
+ case ExMainFunctionDef() =>
+ case ExFunctionDef(_,_,_,_) =>
+ case tree =>
+ unsupported(tree, "Don't know what to do with this. Not purescala?");
+ }
+
+ new ObjectDef(FreshIdentifier(nameStr), classDefs ::: funDefs, Nil)
}
- def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
+ private def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
val newParams = params.map(p => {
- val ptpe = st2ps(p.tpt.tpe)
+ val ptpe = toPureScalaType(p.tpt.tpe)
val newID = FreshIdentifier(p.name.toString).setType(ptpe)
owners += (Variable(newID) -> None)
varSubsts(p.symbol) = (() => Variable(newID))
VarDecl(newID, ptpe)
})
- new FunDef(FreshIdentifier(nameStr), st2ps(tpt.tpe), newParams)
+ new FunDef(FreshIdentifier(nameStr), toPureScalaType(tpt.tpe), newParams)
}
- def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
- var realBody = body
- var reqCont: Option[Expr] = None
- var ensCont: Option[Expr] = None
-
+ private def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
currentFunDef = funDef
- realBody match {
- case ExEnsuredExpression(body2, resSym, contract) => {
+ val (body2, ensuring) = body match {
+ case ExEnsuredExpression(body2, resSym, contract) =>
varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
- val c1 = s2ps(contract)
- // varSubsts.remove(resSym)
- realBody = body2
- ensCont = Some(c1)
- }
- case ExHoldsExpression(body2) => {
- realBody = body2
- ensCont = Some(ResultVariable().setType(BooleanType))
- }
- case _ => ;
+ (body2, toPureScala(contract))
+
+ case ExHoldsExpression(body2) =>
+ (body2, Some(ResultVariable().setType(BooleanType)))
+
+ case _ =>
+ (body, None)
}
- realBody match {
- case ExRequiredExpression(body3, contract) => {
- realBody = body3
- reqCont = Some(s2ps(contract))
- }
- case _ => ;
+ val (body3, require) = body2 match {
+ case ExRequiredExpression(body3, contract) =>
+ (body3, toPureScala(contract))
+
+ case _ =>
+ (body2, None)
}
-
- val bodyAttempt = try {
- Some(flattenBlocks(scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies)(realBody)))
+
+ val finalBody = try {
+ toPureScala(body3).map(flattenBlocks) match {
+ case Some(e) if e.getType.isInstanceOf[ArrayType] =>
+ getOwner(e) match {
+ case Some(Some(fd)) if fd == funDef =>
+ Some(e)
+
+ case None =>
+ Some(e)
+
+ case _ =>
+ reporter.error(body3.pos, "Function cannot return an array that is not locally defined")
+ None
+ }
+ case e =>
+ e
+ }
} catch {
- case e: ImpureCodeEncounteredException => None
+ case e: ImpureCodeEncounteredException =>
+ None
}
- bodyAttempt.foreach(e =>
- if(e.getType.isInstanceOf[ArrayType]) {
- //println(owners)
- //println(getOwner(e))
- getOwner(e) match {
- case Some(Some(fd)) if fd == funDef =>
- case None =>
- case _ => unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
- }
- })
- reqCont.map(e =>
+ val finalRequire = require.filter{ e =>
if(containsLetDef(e)) {
- unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
- })
- ensCont.map(e =>
+ reporter.error(body3.pos, "Function precondtion should not contain nested function definition")
+ false
+ } else {
+ true
+ }
+ }
+
+ val finalEnsuring = ensuring.filter{ e =>
if(containsLetDef(e)) {
- unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
- })
- funDef.body = bodyAttempt
- funDef.precondition = reqCont
- funDef.postcondition = ensCont
+ reporter.error(body3.pos, "Function postcondition should not contain nested function definition")
+ false
+ } else {
+ true
+ }
+ }
+
+ funDef.body = finalBody
+ funDef.precondition = finalRequire
+ funDef.postcondition = finalEnsuring
funDef
}
- // THE EXTRACTION CODE STARTS HERE
- val topLevelObjDef: ObjectDef = extractTopLevelDef
-
- stopIfErrors
-
- val programName: Identifier = unit.body match {
- case PackageDef(name, _) => FreshIdentifier(name.toString)
- case _ => FreshIdentifier("<program>")
+ def unsupported(msg: String): Nothing = {
+ reporter.error(NoPosition, msg)
+ throw new ImpureCodeEncounteredException(null)
}
-
- //Program(programName, ObjectDef("Object", Nil, Nil))
- Program(programName, topLevelObjDef)
- }
-
- /** An exception thrown when non-purescala compatible code is encountered. */
- sealed case class ImpureCodeEncounteredException(tree: Tree) extends Exception
-
- /** Attempts to convert a scalac AST to a pure scala AST. */
- def toPureScala(unit: CompilationUnit)(tree: Tree): Option[Expr] = {
- try {
- Some(scala2PureScala(unit, false)(tree))
- } catch {
- case ImpureCodeEncounteredException(_) => None
+ def unsupported(tr: Tree, msg: String): Nothing = {
+ reporter.error(tr.pos, tr.toString)
+ reporter.error(tr.pos, msg)
+ throw new ImpureCodeEncounteredException(tr)
}
- }
-
- def toPureScalaType(unit: CompilationUnit)(typeTree: Type): Option[purescala.TypeTrees.TypeTree] = {
- try {
- Some(scalaType2PureScala(unit, false)(typeTree))
- } catch {
- case ImpureCodeEncounteredException(_) => None
- }
- }
- private var currentFunDef: FunDef = null
+ private def extractPattern(p: Tree, binder: Option[Identifier] = None): Pattern = p match {
+ case b @ Bind(name, Typed(pat, tpe)) =>
+ val newID = FreshIdentifier(name.toString).setType(extractType(tpe.tpe))
+ varSubsts(b.symbol) = (() => Variable(newID))
+ extractPattern(pat, Some(newID))
+
+ case b @ Bind(name, pat) =>
+ val newID = FreshIdentifier(name.toString).setType(extractType(b.symbol.tpe))
+ varSubsts(b.symbol) = (() => Variable(newID))
+ extractPattern(pat, Some(newID))
+
+ case Ident(nme.WILDCARD) =>
+ WildcardPattern(binder)
+
+ case s @ Select(This(_), b) if s.tpe.typeSymbol.isCase &&
+ classesToClasses.contains(s.tpe.typeSymbol) =>
+ // case Obj =>
+ val cd = classesToClasses(s.tpe.typeSymbol).asInstanceOf[CaseClassDef]
+ assert(cd.fields.size == 0)
+ CaseClassPattern(binder, cd, Seq())
+
+ case a @ Apply(fn, args) if fn.isType &&
+ a.tpe.typeSymbol.isCase &&
+ classesToClasses.contains(a.tpe.typeSymbol) =>
+
+ val cd = classesToClasses(a.tpe.typeSymbol).asInstanceOf[CaseClassDef]
+ assert(args.size == cd.fields.size)
+ CaseClassPattern(binder, cd, args.map(extractPattern(_)))
+
+ case a @ Apply(fn, args) =>
+ extractType(a.tpe) match {
+ case TupleType(argsTpes) =>
+ TuplePattern(binder, args.map(extractPattern(_)))
+ case _ =>
+ unsupported(p, "Unsupported pattern")
+ }
- //This is a bit missleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
- //that it can have any owner
- private var owners: Map[Expr, Option[FunDef]] = Map()
-
- /** Forces conversion from scalac AST to purescala AST, throws an Exception
- * if impossible. If not in 'silent mode', non-pure AST nodes are reported as
- * errors. */
- private def scala2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Tree): Expr = {
- def rewriteCaseDef(cd: CaseDef): MatchCase = {
-
- def pat2pat(p: Tree, binder: Option[Identifier] = None): Pattern = p match {
- case b @ Bind(name, Typed(pat, tpe)) =>
- val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(tpe.tpe))
- varSubsts(b.symbol) = (() => Variable(newID))
- pat2pat(pat, Some(newID))
-
- case b @ Bind(name, pat) =>
- val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(b.symbol.tpe))
- varSubsts(b.symbol) = (() => Variable(newID))
- pat2pat(pat, Some(newID))
-
- case Ident(nme.WILDCARD) =>
- WildcardPattern(binder)
-
- case s @ Select(This(_), b) if s.tpe.typeSymbol.isCase &&
- classesToClasses.keySet.contains(s.tpe.typeSymbol) =>
- // case Obj =>
- val cd = classesToClasses(s.tpe.typeSymbol).asInstanceOf[CaseClassDef]
- assert(cd.fields.size == 0)
- CaseClassPattern(binder, cd, Seq())
-
- case a @ Apply(fn, args) if fn.isType &&
- a.tpe.typeSymbol.isCase &&
- classesToClasses.keySet.contains(a.tpe.typeSymbol) =>
-
- val cd = classesToClasses(a.tpe.typeSymbol).asInstanceOf[CaseClassDef]
- assert(args.size == cd.fields.size)
- CaseClassPattern(binder, cd, args.map(pat2pat(_)))
-
- case a @ Apply(fn, args) =>
- val pst = scalaType2PureScala(unit, silent)(a.tpe)
- pst match {
- case TupleType(argsTpes) => TuplePattern(binder, args.map(pat2pat(_)))
- case _ => throw ImpureCodeEncounteredException(p)
- }
+ case _ =>
+ unsupported(p, "Unsupported pattern")
+ }
- case _ =>
- if (!silent) {
- unit.error(p.pos, "Unsupported pattern.")
- }
- throw ImpureCodeEncounteredException(p)
- }
+ private def extractMatchCase(cd: CaseDef): MatchCase = {
+ val recPattern = extractPattern(cd.pat)
+ val recBody = extractTree(cd.body)
if(cd.guard == EmptyTree) {
- SimpleCase(pat2pat(cd.pat), rec(cd.body))
+ SimpleCase(recPattern, recBody)
} else {
- val recPattern = pat2pat(cd.pat)
- val recGuard = rec(cd.guard)
- val recBody = rec(cd.body)
+ val recGuard = extractTree(cd.guard)
+
if(!isPure(recGuard)) {
- unit.error(cd.guard.pos, "Guard expression must be pure")
+ reporter.error(cd.guard.pos, "Guard expression must be pure")
throw ImpureCodeEncounteredException(cd)
}
+
GuardedCase(recPattern, recGuard, recBody)
}
}
- def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
- val newParams = params.map(p => {
- val ptpe = scalaType2PureScala(unit, silent) (p.tpt.tpe)
- val newID = FreshIdentifier(p.name.toString).setType(ptpe)
- owners += (Variable(newID) -> None)
- varSubsts(p.symbol) = (() => Variable(newID))
- VarDecl(newID, ptpe)
- })
- new FunDef(FreshIdentifier(nameStr), scalaType2PureScala(unit, silent)(tpt.tpe), newParams)
- }
-
- def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
- var realBody = body
- var reqCont: Option[Expr] = None
- var ensCont: Option[Expr] = None
-
- currentFunDef = funDef
-
- realBody match {
- case ExEnsuredExpression(body2, resSym, contract) => {
- varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
- val c1 = scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies) (contract)
- // varSubsts.remove(resSym)
- realBody = body2
- ensCont = Some(c1)
- }
- case ExHoldsExpression(body2) => {
- realBody = body2
- ensCont = Some(ResultVariable().setType(BooleanType))
- }
- case _ => ;
+ private def extractTree(tr: Tree): LeonExpr = {
+ val (current, tmpRest) = tr match {
+ case Block(Block(e :: es1, l1) :: es2, l2) =>
+ (e, Some(Block(es1 ++ Seq(l1) ++ es2, l2)))
+ case Block(e :: Nil, last) =>
+ (e, Some(last))
+ case Block(e :: es, last) =>
+ (e, Some(Block(es, last)))
+ case e =>
+ (e, None)
}
- realBody match {
- case ExRequiredExpression(body3, contract) => {
- realBody = body3
- reqCont = Some(scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies) (contract))
- }
- case _ => ;
- }
-
- val bodyAttempt = try {
- Some(flattenBlocks(scala2PureScala(unit, Settings.silentlyTolerateNonPureBodies)(realBody)))
- } catch {
- case e: ImpureCodeEncounteredException => None
- }
-
- bodyAttempt.foreach(e =>
- if(e.getType.isInstanceOf[ArrayType]) {
- getOwner(e) match {
- case Some(Some(fd)) if fd == funDef =>
- case None =>
- case _ => unit.error(realBody.pos, "Function cannot return an array that is not locally defined")
- }
- })
-
- reqCont.foreach(e =>
- if(containsLetDef(e)) {
- unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
- })
- ensCont.foreach(e =>
- if(containsLetDef(e)) {
- unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
- })
- funDef.body = bodyAttempt
- funDef.precondition = reqCont
- funDef.postcondition = ensCont
- funDef
- }
+ var rest = tmpRest
- def rec(tr: Tree): Expr = {
-
- val (nextExpr, rest) = tr match {
- case Block(Block(e :: es1, l1) :: es2, l2) => (e, Some(Block(es1 ++ Seq(l1) ++ es2, l2)))
- case Block(e :: Nil, last) => (e, Some(last))
- case Block(e :: es, last) => (e, Some(Block(es, last)))
- case _ => (tr, None)
- }
-
- val e2: Option[Expr] = nextExpr match {
+ val res = current match {
case ExCaseObject(sym) =>
classesToClasses.get(sym) match {
case Some(ccd: CaseClassDef) =>
- Some(CaseClass(ccd, Seq()))
+ CaseClass(ccd, Seq())
+
case _ =>
- None
+ unsupported(tr, "Unknown case class "+sym.name)
}
- case ExParameterlessMethodCall(t,n) => {
- val selector = rec(t)
+ case ExParameterlessMethodCall(t,n) if extractTree(t).getType.isInstanceOf[CaseClassType] =>
+ val selector = extractTree(t)
val selType = selector.getType
- if(!selType.isInstanceOf[CaseClassType])
- None
- else {
-
- val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+ val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
- val fieldID = selDef.fields.find(_.id.name == n.toString) match {
- case None => {
- if(!silent)
- unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
- throw ImpureCodeEncounteredException(tr)
- }
- case Some(vd) => vd.id
- }
+ val fieldID = selDef.fields.find(_.id.name == n.toString) match {
+ case None =>
+ unsupported(tr, "Invalid method or field invocation (not a case class arg?)")
- Some(CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType))
- }
- }
- case _ => None
- }
- var handleRest = true
- val psExpr = e2 match {
- case Some(e3) => e3
- case None => nextExpr match {
- case ExTuple(tpes, exprs) => {
- val tupleExprs = exprs.map(e => rec(e))
- val tupleType = TupleType(tupleExprs.map(expr => expr.getType))
- Tuple(tupleExprs).setType(tupleType)
- }
- case ExErrorExpression(str, tpe) =>
- Error(str).setType(scalaType2PureScala(unit, silent)(tpe))
-
- case ExTupleExtract(tuple, index) => {
- val tupleExpr = rec(tuple)
- val TupleType(tpes) = tupleExpr.getType
- if(tpes.size < index)
- throw ImpureCodeEncounteredException(tree)
- else
- TupleSelect(tupleExpr, index).setType(tpes(index-1))
+ case Some(vd) =>
+ vd.id
}
- case ExValDef(vs, tpt, bdy) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val valTree = rec(bdy)
- handleRest = false
- if(valTree.getType.isInstanceOf[ArrayType]) {
- getOwner(valTree) match {
- case None =>
- owners += (Variable(newID) -> Some(currentFunDef))
- case Some(_) =>
- unit.error(nextExpr.pos, "Cannot alias array")
- throw ImpureCodeEncounteredException(nextExpr)
- }
- }
- val restTree = rest match {
- case Some(rst) => {
- varSubsts(vs) = (() => Variable(newID))
- val res = rec(rst)
- varSubsts.remove(vs)
- res
- }
- case None => UnitLiteral
- }
- val res = Let(newID, valTree, restTree)
- res
- }
- case dd@ExFunctionDef(n, p, t, b) => {
- val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
- defsToDefs += (dd.symbol -> funDef)
- val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
- val oldCurrentFunDef = currentFunDef
- mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
- val funDefWithBody = extractFunDef(funDef, b)
- mutableVarSubsts ++= oldMutableVarSubst
- currentFunDef = oldCurrentFunDef
- val restTree = rest match {
- case Some(rst) => rec(rst)
- case None => UnitLiteral
- }
- defsToDefs.remove(dd.symbol)
- handleRest = false
- LetDef(funDefWithBody, restTree)
+
+ CaseClassSelector(selDef, selector, fieldID).setType(fieldID.getType)
+
+ case ExTuple(tpes, exprs) =>
+ val tupleExprs = exprs.map(e => extractTree(e))
+ val tupleType = TupleType(tupleExprs.map(expr => expr.getType))
+ Tuple(tupleExprs)
+
+ case ExErrorExpression(str, tpe) =>
+ Error(str).setType(extractType(tpe))
+
+ case ExTupleExtract(tuple, index) =>
+ val tupleExpr = extractTree(tuple)
+
+ tupleExpr.getType match {
+ case TupleType(tpes) if tpes.size >= index =>
+ TupleSelect(tupleExpr, index)
+
+ case _ =>
+ unsupported(tr, "Invalid tupple access")
}
- case ExVarDef(vs, tpt, bdy) => {
- val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
- //binderTpe match {
- // case ArrayType(_) =>
- // unit.error(tree.pos, "Cannot declare array variables, only val are alllowed")
- // throw ImpureCodeEncounteredException(tree)
- // case _ =>
- //}
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
- val valTree = rec(bdy)
- mutableVarSubsts += (vs -> (() => Variable(newID)))
- handleRest = false
- if(valTree.getType.isInstanceOf[ArrayType]) {
- getOwner(valTree) match {
- case None =>
- owners += (Variable(newID) -> Some(currentFunDef))
- case Some(_) =>
- unit.error(nextExpr.pos, "Cannot alias array")
- throw ImpureCodeEncounteredException(nextExpr)
- }
- }
- val restTree = rest match {
- case Some(rst) => {
- varSubsts(vs) = (() => Variable(newID))
- val res = rec(rst)
- varSubsts.remove(vs)
- res
- }
- case None => UnitLiteral
+
+ case ExValDef(vs, tpt, bdy) =>
+ val binderTpe = extractType(tpt.tpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val valTree = extractTree(bdy)
+
+ if(valTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(valTree) match {
+ case None =>
+ owners += (Variable(newID) -> Some(currentFunDef))
+ case _ =>
+ unsupported(tr, "Cannot alias array")
}
- val res = LetVar(newID, valTree, restTree)
- res
}
- case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
- case Some(fun) => {
- val Variable(id) = fun()
- val rhsTree = rec(rhs)
- if(rhsTree.getType.isInstanceOf[ArrayType]) {
- getOwner(rhsTree) match {
- case None =>
- case Some(_) =>
- unit.error(nextExpr.pos, "Cannot alias array")
- throw ImpureCodeEncounteredException(nextExpr)
- }
- }
- Assignment(id, rhsTree)
- }
- case None => {
- unit.error(tr.pos, "Undeclared variable.")
- throw ImpureCodeEncounteredException(tr)
+ val restTree = rest match {
+ case Some(rst) => {
+ varSubsts(vs) = (() => Variable(newID))
+ val res = extractTree(rst)
+ varSubsts.remove(vs)
+ res
}
- }
- case wh@ExWhile(cond, body) => {
- val condTree = rec(cond)
- val bodyTree = rec(body)
- While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
- }
- case wh@ExWhileWithInvariant(cond, body, inv) => {
- val condTree = rec(cond)
- val bodyTree = rec(body)
- val invTree = rec(inv)
- val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
- w.invariant = Some(invTree)
- w
+ case None => UnitLiteral
}
- case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
- case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
- case ExUnitLiteral() => UnitLiteral
- case ExLocally(body) => rec(body)
- case ExTyped(e,tpt) => rec(e)
- case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
- case Some(fun) => fun()
- case None => mutableVarSubsts.get(sym) match {
- case Some(fun) => fun()
- case None => {
- unit.error(tr.pos, "Unidentified variable.")
- throw ImpureCodeEncounteredException(tr)
- }
- }
+ rest = None
+ Let(newID, valTree, restTree)
+
+ /**
+ * XLang Extractors
+ */
+
+ case dd @ ExFunctionDef(n, p, t, b) =>
+ val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
+ defsToDefs += (dd.symbol -> funDef)
+ val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
+ val oldCurrentFunDef = currentFunDef
+ mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
+ val funDefWithBody = extractFunDef(funDef, b)
+ mutableVarSubsts ++= oldMutableVarSubst
+ currentFunDef = oldCurrentFunDef
+ val restTree = rest match {
+ case Some(rst) => extractTree(rst)
+ case None => UnitLiteral
}
- case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
- val pstpe = scalaType2PureScala(unit, silent)(tpe)
- val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
- varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
- val c1 = rec(predBody)
- previousVarSubst match {
- case Some(f) => varSubsts(varSym) = f
- case None => varSubsts.remove(varSym)
+ defsToDefs.remove(dd.symbol)
+ rest = None
+ LetDef(funDefWithBody, restTree)
+
+ case ExVarDef(vs, tpt, bdy) => {
+ val binderTpe = extractType(tpt.tpe)
+ val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
+ val valTree = extractTree(bdy)
+ mutableVarSubsts += (vs -> (() => Variable(newID)))
+
+ if(valTree.getType.isInstanceOf[ArrayType]) {
+ getOwner(valTree) match {
+ case None =>
+ owners += (Variable(newID) -> Some(currentFunDef))
+ case Some(_) =>
+ unsupported(tr, "Cannot alias array")
}
- if(containsEpsilon(c1)) {
- unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
- throw ImpureCodeEncounteredException(epsi)
+ }
+ val restTree = rest match {
+ case Some(rst) => {
+ varSubsts(vs) = (() => Variable(newID))
+ val res = extractTree(rst)
+ varSubsts.remove(vs)
+ res
}
- Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
+ case None => UnitLiteral
}
- case chs @ ExChooseExpression(args, tpe, body, select) => {
- val cTpe = scalaType2PureScala(unit, silent)(tpe)
+ rest = None
+
+ LetVar(newID, valTree, restTree)
+ }
- val vars = args map { case (tpe, sym) =>
- val aTpe = scalaType2PureScala(unit, silent)(tpe)
- val newID = FreshIdentifier(sym.name.toString).setType(aTpe)
- owners += (Variable(newID) -> None)
- varSubsts(sym) = (() => Variable(newID))
- newID
+ case ExAssign(sym, rhs) => mutableVarSubsts.get(sym) match {
+ case Some(fun) =>
+ val Variable(id) = fun()
+ val rhsTree = extractTree(rhs)
+ if(rhsTree.getType.isInstanceOf[ArrayType] && getOwner(rhsTree).isDefined) {
+ unsupported(tr, "Cannot alias array")
}
+ Assignment(id, rhsTree)
- val cBody = rec(body)
+ case None =>
+ unsupported(tr, "Undeclared variable.")
+ }
- Choose(vars, cBody).setType(cTpe).setPosInfo(select.pos.line, select.pos.column)
+ case wh @ ExWhile(cond, body) =>
+ val condTree = extractTree(cond)
+ val bodyTree = extractTree(body)
+ While(condTree, bodyTree).setPosInfo(wh.pos)
+
+ case wh @ ExWhileWithInvariant(cond, body, inv) =>
+ val condTree = extractTree(cond)
+ val bodyTree = extractTree(body)
+ val invTree = extractTree(inv)
+
+ val w = While(condTree, bodyTree).setPosInfo(wh.pos)
+ w.invariant = Some(invTree)
+ w
+
+ case epsi @ ExEpsilonExpression(tpe, varSym, predBody) =>
+ val pstpe = extractType(tpe)
+ val previousVarSubst: Option[Function0[LeonExpr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
+ varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
+ val c1 = extractTree(predBody)
+ previousVarSubst match {
+ case Some(f) => varSubsts(varSym) = f
+ case None => varSubsts.remove(varSym)
}
-
- case ExWaypointExpression(tpe, i, tree) => {
- val pstpe = scalaType2PureScala(unit, silent)(tpe)
- val IntLiteral(ri) = rec(i)
- Waypoint(ri, rec(tree)).setType(pstpe)
- }
- case ExCaseClassConstruction(tpt, args) => {
- val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
- if(!cctype.isInstanceOf[CaseClassType]) {
- if(!silent) {
- unit.error(tr.pos, "Construction of a non-case class.")
- }
- throw ImpureCodeEncounteredException(tree)
- }
- val nargs = args.map(rec(_))
- val cct = cctype.asInstanceOf[CaseClassType]
- CaseClass(cct.classDef, nargs).setType(cct)
+ if(containsEpsilon(c1)) {
+ unsupported(epsi, "Usage of nested epsilon is not allowed")
}
+ Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
- case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
- case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
- case ExNot(e) => Not(rec(e)).setType(BooleanType)
- case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
- case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
- case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
- case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
- case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
- case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
- case ExEquals(l, r) => {
- val rl = rec(l)
- val rr = rec(r)
- ((rl.getType,rr.getType) match {
- case (SetType(_), SetType(_)) => SetEquals(rl, rr)
- case (BooleanType, BooleanType) => Iff(rl, rr)
- case (_, _) => Equals(rl, rr)
- }).setType(BooleanType)
- }
- case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
- case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
- case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
- case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
- case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
- case ExFiniteSet(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteSet(args.map(rec(_))).setType(SetType(underlying))
- }
- case ExFiniteMultiset(tt, args) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteMultiset(args.map(rec(_))).setType(MultisetType(underlying))
+ case ExWaypointExpression(tpe, i, tree) =>
+ val pstpe = extractType(tpe)
+ val IntLiteral(ri) = extractTree(i)
+ Waypoint(ri, extractTree(tree)).setType(pstpe)
+
+ case update @ ExUpdate(lhs, index, newValue) =>
+ val lhsRec = extractTree(lhs)
+ lhsRec match {
+ case Variable(_) =>
+ case _ =>
+ unsupported(tr, "Array update only works on variables")
}
- case ExEmptySet(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- FiniteSet(Seq()).setType(SetType(underlying))
+
+ getOwner(lhsRec) match {
+ case Some(Some(fd)) if fd != currentFunDef =>
+ unsupported(tr, "cannot update an array that is not defined locally")
+
+ case Some(None) =>
+ unsupported(tr, "cannot update an array that is not defined locally")
+
+ case Some(_) =>
+
+ case None => sys.error("This array: " + lhsRec + " should have had an owner")
}
- case ExEmptyMultiset(tt) => {
- val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMultiset(underlying).setType(MultisetType(underlying))
+
+ val indexRec = extractTree(index)
+ val newValueRec = extractTree(newValue)
+ ArrayUpdate(lhsRec, indexRec, newValueRec).setPosInfo(update.pos)
+
+ case ExInt32Literal(v) =>
+ IntLiteral(v)
+
+ case ExBooleanLiteral(v) =>
+ BooleanLiteral(v)
+
+ case ExUnitLiteral() =>
+ UnitLiteral
+
+ case ExLocally(body) =>
+ extractTree(body)
+
+ case ExTyped(e,tpt) =>
+ // TODO: refine type here?
+ extractTree(e)
+
+ case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None => mutableVarSubsts.get(sym) match {
+ case Some(fun) => fun()
+ case None =>
+ unsupported(tr, "Unidentified variable.")
}
- case ExEmptyMap(ft, tt) => {
- val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
- val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
- val tpe = MapType(fromUnderlying, toUnderlying)
+ }
+
+ case chs @ ExChooseExpression(args, tpe, body, select) =>
+ val cTpe = extractType(tpe)
- FiniteMap(Seq()).setType(tpe)
+ val vars = args map { case (tpe, sym) =>
+ val aTpe = extractType(tpe)
+ val newID = FreshIdentifier(sym.name.toString).setType(aTpe)
+ owners += (Variable(newID) -> None)
+ varSubsts(sym) = (() => Variable(newID))
+ newID
}
- case ExLiteralMap(ft, tt, elems) => {
- val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
- val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
- val tpe = MapType(fromUnderlying, toUnderlying)
- val singletons: Seq[(Expr, Expr)] = elems.collect { case ExTuple(tpes, trees) if (trees.size == 2) =>
- (rec(trees(0)), rec(trees(1)))
- }
+ val cBody = extractTree(body)
- if (singletons.size != elems.size) {
- unit.error(nextExpr.pos, "Some map elements could not be extracted as Tuple2")
- throw ImpureCodeEncounteredException(nextExpr)
- }
+ Choose(vars, cBody).setPosInfo(select.pos)
- FiniteMap(singletons).setType(tpe)
- }
+ case ExCaseClassConstruction(tpt, args) =>
+ extractType(tpt.tpe) match {
+ case cct: CaseClassType =>
+ val nargs = args.map(extractTree(_))
+ CaseClass(cct.classDef, nargs)
+
+ case _ =>
+ unsupported(tr, "Construction of a non-case class.")
- case ExSetMin(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Min should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
- }
- SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
}
- case ExSetMax(t) => {
- val set = rec(t)
- if(!set.getType.isInstanceOf[SetType]) {
- if(!silent) unit.error(t.pos, "Max should be computed on a set.")
- throw ImpureCodeEncounteredException(tree)
- }
- SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
+
+ case ExAnd(l, r) => And(extractTree(l), extractTree(r))
+ case ExOr(l, r) => Or(extractTree(l), extractTree(r))
+ case ExNot(e) => Not(extractTree(e))
+ case ExUMinus(e) => UMinus(extractTree(e))
+ case ExPlus(l, r) => Plus(extractTree(l), extractTree(r))
+ case ExMinus(l, r) => Minus(extractTree(l), extractTree(r))
+ case ExTimes(l, r) => Times(extractTree(l), extractTree(r))
+ case ExDiv(l, r) => Division(extractTree(l), extractTree(r))
+ case ExMod(l, r) => Modulo(extractTree(l), extractTree(r))
+ case ExNotEquals(l, r) => Not(Equals(extractTree(l), extractTree(r)))
+ case ExGreaterThan(l, r) => GreaterThan(extractTree(l), extractTree(r))
+ case ExGreaterEqThan(l, r) => GreaterEquals(extractTree(l), extractTree(r))
+ case ExLessThan(l, r) => LessThan(extractTree(l), extractTree(r))
+ case ExLessEqThan(l, r) => LessEquals(extractTree(l), extractTree(r))
+ case ExEquals(l, r) =>
+ val rl = extractTree(l)
+ val rr = extractTree(r)
+
+ (rl.getType, rr.getType) match {
+ case (SetType(_), SetType(_)) =>
+ SetEquals(rl, rr)
+
+ case (BooleanType, BooleanType) =>
+ Iff(rl, rr)
+
+ case (rt, lt) if isSubtypeOf(rt, lt) || isSubtypeOf(lt, rt) =>
+ Equals(rl, rr)
+
+ case (rt, lt) =>
+ unsupported(tr, "Invalid comparison: (_: "+rt+") == (_: "+lt+")")
}
- case ExUnion(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetUnion(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetUnion(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Union of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ case ExFiniteSet(tt, args) =>
+ val underlying = extractType(tt.tpe)
+ FiniteSet(args.map(extractTree(_))).setType(SetType(underlying))
+
+ case ExFiniteMultiset(tt, args) =>
+ val underlying = extractType(tt.tpe)
+ FiniteMultiset(args.map(extractTree(_))).setType(MultisetType(underlying))
+
+ case ExEmptySet(tt) =>
+ val underlying = extractType(tt.tpe)
+ FiniteSet(Seq()).setType(SetType(underlying))
+
+ case ExEmptyMultiset(tt) =>
+ val underlying = extractType(tt.tpe)
+ EmptyMultiset(underlying).setType(MultisetType(underlying))
+
+ case ExEmptyMap(ft, tt) =>
+ val fromUnderlying = extractType(ft.tpe)
+ val toUnderlying = extractType(tt.tpe)
+ val tpe = MapType(fromUnderlying, toUnderlying)
+
+ FiniteMap(Seq()).setType(tpe)
+
+ case ExLiteralMap(ft, tt, elems) =>
+ val fromUnderlying = extractType(ft.tpe)
+ val toUnderlying = extractType(tt.tpe)
+ val tpe = MapType(fromUnderlying, toUnderlying)
+
+ val singletons: Seq[(LeonExpr, LeonExpr)] = elems.collect {
+ case ExTuple(tpes, trees) if (trees.size == 2) =>
+ (extractTree(trees(0)), extractTree(trees(1)))
}
- case ExIntersection(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetIntersection(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetIntersection(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Intersection of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ if (singletons.size != elems.size) {
+ unsupported(tr, "Some map elements could not be extracted as Tuple2")
}
- case ExSetContains(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => ElementOfSet(rr, rl)
- case _ => {
- if(!silent) unit.error(tree.pos, ".contains on non set expression.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ FiniteMap(singletons).setType(tpe)
+
+ case ExSetMin(t) =>
+ val set = extractTree(t)
+ set.getType match {
+ case SetType(base) =>
+ SetMin(set).setType(base)
+
+ case _ =>
+ unsupported(t, "Min should be computer on a set.")
}
- case ExSetSubset(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SubsetOf(rl, rr)
- case _ => {
- if(!silent) unit.error(tree.pos, "Subset on non set expression.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ case ExSetMax(t) =>
+ val set = extractTree(t)
+ set.getType match {
+ case SetType(base) =>
+ SetMax(set).setType(base)
+
+ case _ =>
+ unsupported(t, "Max should be computer on a set.")
}
- case ExSetMinus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- rl.getType match {
- case s @ SetType(_) => SetDifference(rl, rr).setType(s)
- case m @ MultisetType(_) => MultisetDifference(rl, rr).setType(m)
- case _ => {
- if(!silent) unit.error(tree.pos, "Difference of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
- }
- case ExSetCard(t) => {
- val rt = rec(t)
- rt.getType match {
- case s @ SetType(_) => SetCardinality(rt)
- case m @ MultisetType(_) => MultisetCardinality(rt)
- case _ => {
- if(!silent) unit.error(tree.pos, "Cardinality of non set/multiset expressions.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ case ExUnion(t1,t2) =>
+ val rl = extractTree(t1)
+ val rr = extractTree(t2)
+
+ (rl.getType, rr.getType) match {
+ case (SetType(b1), SetType(b2)) if b1 == b2 =>
+ SetUnion(rl, rr).setType(SetType(b1))
+
+ case (MultisetType(b1), MultisetType(b2)) if b1 == b2 =>
+ MultisetUnion(rl, rr).setType(SetType(b1))
+
+ case (lt, rt) =>
+ unsupported(tr, "Unsupported union between "+lt+" and "+rt)
}
- case ExMultisetToSet(t) => {
- val rt = rec(t)
- rt.getType match {
- case m @ MultisetType(u) => MultisetToSet(rt).setType(SetType(u))
- case _ => {
- if(!silent) unit.error(tree.pos, "toSet can only be applied to multisets.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ case ExIntersection(t1,t2) =>
+ val rl = extractTree(t1)
+ val rr = extractTree(t2)
+
+ (rl.getType, rr.getType) match {
+ case (SetType(b1), SetType(b2)) if b1 == b2 =>
+ SetIntersection(rl, rr).setType(SetType(b1))
+
+ case (MultisetType(b1), MultisetType(b2)) if b1 == b2 =>
+ MultisetIntersection(rl, rr).setType(SetType(b1))
+
+ case (lt, rt) =>
+ unsupported(tr, "Unsupported intersection between "+lt+" and "+rt)
}
- case up@ExUpdated(m,f,t) => {
- val rm = rec(m)
- val rf = rec(f)
- val rt = rec(t)
- rm.getType match {
- case MapType(ft, tt) => {
- MapUnion(rm, FiniteMap(Seq((rf, rt))).setType(rm.getType)).setType(rm.getType)
- }
- case ArrayType(bt) => {
- ArrayUpdated(rm, rf, rt).setType(rm.getType).setPosInfo(up.pos.line, up.pos.column)
- }
- case _ => {
- if (!silent) unit.error(tree.pos, "updated can only be applied to maps.")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ case ExSetContains(t1,t2) =>
+ val rl = extractTree(t1)
+ val rr = extractTree(t2)
+
+ (rl.getType, rr.getType) match {
+ case (SetType(base), elem) if isSubtypeOf(elem, base) =>
+ ElementOfSet(rr, rl)
+
+ case (lt, rt) =>
+ unsupported(tr, "Invalid "+lt+".contains("+rt+")")
}
- case ExMapIsDefinedAt(m,k) => {
- val rm = rec(m)
- val rk = rec(k)
- MapIsDefinedAt(rm, rk)
+
+ case ExSetSubset(t1,t2) =>
+ val rl = extractTree(t1)
+ val rr = extractTree(t2)
+
+ (rl.getType, rr.getType) match {
+ case (SetType(base1), SetType(base2)) if base2 == base1 =>
+ SubsetOf(rl, rr)
+
+ case (lt, rt) =>
+ unsupported(tr, "Invalid "+lt+" isSubsetOf "+rt+"")
}
- case ExPlusPlusPlus(t1,t2) => {
- val rl = rec(t1)
- val rr = rec(t2)
- MultisetPlus(rl, rr).setType(rl.getType)
+ case ExSetMinus(t1,t2) =>
+ val rl = extractTree(t1)
+ val rr = extractTree(t2)
+
+ (rl.getType, rr.getType) match {
+ case (SetType(base1), SetType(base2)) if base2 == base1 =>
+ SetDifference(rl, rr).setType(SetType(base1))
+
+ case (MultisetType(base1), MultisetType(base2)) if base2 == base1 =>
+ MultisetDifference(rl, rr).setType(MultisetType(base1))
+
+ case (lt, rt) =>
+ unsupported(tr, "Invalid "+lt+" -- "+rt+"")
}
- case app@ExApply(lhs,args) => {
- val rlhs = rec(lhs)
- val rargs = args map rec
- rlhs.getType match {
- case MapType(_,tt) =>
- assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
- case ArrayType(bt) => {
- assert(rargs.size == 1)
- ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
- }
- case _ => {
- if (!silent) unit.error(tree.pos, "apply on unexpected type")
- throw ImpureCodeEncounteredException(tree)
- }
- }
+
+ case ExSetCard(t) =>
+ val rt = extractTree(t)
+ rt.getType match {
+ case SetType(_) =>
+ SetCardinality(rt)
+
+ case MultisetType(_) =>
+ MultisetCardinality(rt)
+
+ case _ =>
+ unsupported(tr, "Cardinality of non set/multiset expressions.")
}
- // for now update only occurs on Array. later we might have to distinguished depending on the type of the lhs
- case update@ExUpdate(lhs, index, newValue) => {
- val lhsRec = rec(lhs)
- lhsRec match {
- case Variable(_) =>
- case _ => {
- unit.error(tree.pos, "array update only works on variables")
- throw ImpureCodeEncounteredException(tree)
- }
- }
- getOwner(lhsRec) match {
- case Some(Some(fd)) if fd != currentFunDef =>
- unit.error(nextExpr.pos, "cannot update an array that is not defined locally")
- throw ImpureCodeEncounteredException(nextExpr)
- case Some(None) =>
- unit.error(nextExpr.pos, "cannot update an array that is not defined locally")
- throw ImpureCodeEncounteredException(nextExpr)
- case Some(_) =>
- case None => sys.error("This array: " + lhsRec + " should have had an owner")
- }
- val indexRec = rec(index)
- val newValueRec = rec(newValue)
- ArrayUpdate(lhsRec, indexRec, newValueRec).setPosInfo(update.pos.line, update.pos.column)
+
+ case ExMultisetToSet(t) =>
+ val rt = extractTree(t)
+
+ rt.getType match {
+ case MultisetType(u) =>
+ MultisetToSet(rt).setType(SetType(u))
+
+ case _ =>
+ unsupported(tr, "toSet can only be applied to multisets.")
}
- case ExArrayLength(t) => {
- val rt = rec(t)
- ArrayLength(rt)
+
+ case up @ ExUpdated(m, f, t) =>
+ val rm = extractTree(m)
+ val rf = extractTree(f)
+ val rt = extractTree(t)
+
+ rm.getType match {
+ case t @ MapType(ft, tt) =>
+ MapUnion(rm, FiniteMap(Seq((rf, rt))).setType(t)).setType(t)
+
+ case t @ ArrayType(bt) =>
+ ArrayUpdated(rm, rf, rt).setType(t).setPosInfo(up.pos)
+
+ case _ =>
+ unsupported(tr, "updated can only be applied to maps.")
}
- case ExArrayClone(t) => {
- val rt = rec(t)
- ArrayClone(rt)
+
+ case ExMapIsDefinedAt(m,k) =>
+ val rm = extractTree(m)
+ val rk = extractTree(k)
+ MapIsDefinedAt(rm, rk)
+
+ case ExPlusPlusPlus(t1,t2) =>
+ val rl = extractTree(t1)
+ val rr = extractTree(t2)
+ MultisetPlus(rl, rr).setType(rl.getType)
+
+ case app @ ExApply(lhs,args) =>
+ val rlhs = extractTree(lhs)
+ val rargs = args map extractTree
+
+ rlhs.getType match {
+ case MapType(_,tt) =>
+ assert(rargs.size == 1)
+ MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
+
+ case ArrayType(bt) =>
+ assert(rargs.size == 1)
+ ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
+
+ case _ =>
+ unsupported(tr, "apply on unexpected type")
}
- case ExArrayFill(baseType, length, defaultValue) => {
- val underlying = scalaType2PureScala(unit, silent)(baseType.tpe)
- val lengthRec = rec(length)
- val defaultValueRec = rec(defaultValue)
- ArrayFill(lengthRec, defaultValueRec).setType(ArrayType(underlying))
+
+ case ExArrayLength(t) =>
+ val rt = extractTree(t)
+ ArrayLength(rt)
+
+ case ExArrayClone(t) =>
+ val rt = extractTree(t)
+ ArrayClone(rt)
+
+ case ExArrayFill(baseType, length, defaultValue) =>
+ val underlying = extractType(baseType.tpe)
+ val lengthRec = extractTree(length)
+ val defaultValueRec = extractTree(defaultValue)
+ ArrayFill(lengthRec, defaultValueRec).setType(ArrayType(underlying))
+
+ case ExIfThenElse(t1,t2,t3) =>
+ val r1 = extractTree(t1)
+ if(containsLetDef(r1)) {
+ unsupported(t1, "Condition of if-then-else expression should not contain nested function definition")
}
- case ExIfThenElse(t1,t2,t3) => {
- val r1 = rec(t1)
- if(containsLetDef(r1)) {
- unit.error(t1.pos, "Condition of if-then-else expression should not contain nested function definition")
- throw ImpureCodeEncounteredException(t1)
- }
- val r2 = rec(t2)
- val r3 = rec(t3)
- val lub = leastUpperBound(r2.getType, r3.getType)
- lub match {
- case Some(lub) => IfExpr(r1, r2, r3).setType(lub)
- case None =>
- unit.error(nextExpr.pos, "Both branches of ifthenelse have incompatible types")
- throw ImpureCodeEncounteredException(t1)
- }
+ val r2 = extractTree(t2)
+ val r3 = extractTree(t3)
+ val lub = leastUpperBound(r2.getType, r3.getType)
+ lub match {
+ case Some(lub) =>
+ IfExpr(r1, r2, r3).setType(lub)
+
+ case None =>
+ unsupported(tr, "Both branches of ifthenelse have incompatible types")
}
- case ExIsInstanceOf(tt, cc) => {
- val ccRec = rec(cc)
- val checkType = scalaType2PureScala(unit, silent)(tt.tpe)
- checkType match {
- case CaseClassType(ccd) => {
- val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
- if(!ccRec.getType.isInstanceOf[ClassType]) {
- unit.error(tr.pos, "isInstanceOf can only be used with a case class")
+ case ExIsInstanceOf(tt, cc) => {
+ val ccRec = extractTree(cc)
+ val checkType = extractType(tt.tpe)
+ checkType match {
+ case CaseClassType(ccd) => {
+ val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
+ if(!ccRec.getType.isInstanceOf[ClassType]) {
+ reporter.error(tr.pos, "isInstanceOf can only be used with a case class")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
+ val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
+
+ if(rootType != testedExprRootType) {
+ reporter.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
throw ImpureCodeEncounteredException(tr)
} else {
- val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
- val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
-
- if(rootType != testedExprRootType) {
- unit.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
- throw ImpureCodeEncounteredException(tr)
- } else {
- CaseClassInstanceOf(ccd, ccRec)
- }
+ CaseClassInstanceOf(ccd, ccRec)
}
}
- case _ => {
- unit.error(tr.pos, "isInstanceOf can only be used with a case class")
- throw ImpureCodeEncounteredException(tr)
- }
}
- }
-
- case lc @ ExLocalCall(sy,nm,ar) => {
- if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
- if(!silent)
- unit.error(tr.pos, "Invoking an invalid function.")
+ case _ => {
+ reporter.error(tr.pos, "isInstanceOf can only be used with a case class")
throw ImpureCodeEncounteredException(tr)
}
- val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
}
+ }
- case pm @ ExPatternMatching(sel, cses) => {
- val rs = rec(sel)
- val rc = cses.map(rewriteCaseDef(_))
- val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_).get)
- MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
- }
-
-
- // default behaviour is to complain :)
- case _ => {
- if(!silent) {
- reporter.info(tr.pos, "Could not extract as PureScala.", true)
- }
- throw ImpureCodeEncounteredException(tree)
+ case lc @ ExLocalCall(sy,nm,ar) => {
+ if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
+ reporter.error(tr.pos, "Invoking an invalid function.")
+ throw ImpureCodeEncounteredException(tr)
}
+ val fd = defsToDefs(sy)
+ FunctionInvocation(fd, ar.map(extractTree(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
}
+
+ case pm @ ExPatternMatching(sel, cses) =>
+ val rs = extractTree(sel)
+ val rc = cses.map(extractMatchCase(_))
+ val rt: LeonType = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_).get)
+ MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
+
+
+ // default behaviour is to complain :)
+ case _ =>
+ unsupported(tr, "Could not extract as PureScala")
}
- val res = if(handleRest) {
- rest match {
- case Some(rst) => {
- val recRst = rec(rst)
- val block = PBlock(Seq(psExpr), recRst).setType(recRst.getType)
- block
- }
- case None => psExpr
- }
- } else {
- psExpr
+ rest match {
+ case Some(r) =>
+ LeonBlock(Seq(res), extractTree(r))
+ case None =>
+ res
}
+ }
+
+ private def extractType(tpt: Type): LeonType = tpt match {
+ case tpe if tpe == IntClass.tpe =>
+ Int32Type
+
+ case tpe if tpe == BooleanClass.tpe =>
+ BooleanType
+
+ case tpe if tpe == UnitClass.tpe =>
+ UnitType
+
+ case tpe if tpe == NothingClass.tpe =>
+ BottomType
- res
+ case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) =>
+ SetType(extractType(btt))
+
+ case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) =>
+ MultisetType(extractType(btt))
+
+ case TypeRef(_, sym, List(ftt,ttt)) if isMapTraitSym(sym) =>
+ MapType(extractType(ftt), extractType(ttt))
+
+ case TypeRef(_, sym, List(t1,t2)) if isTuple2(sym) =>
+ TupleType(Seq(extractType(t1),extractType(t2)))
+
+ case TypeRef(_, sym, List(t1,t2,t3)) if isTuple3(sym) =>
+ TupleType(Seq(extractType(t1),extractType(t2),extractType(t3)))
+
+ case TypeRef(_, sym, List(t1,t2,t3,t4)) if isTuple4(sym) =>
+ TupleType(Seq(extractType(t1),extractType(t2),extractType(t3),extractType(t4)))
+
+ case TypeRef(_, sym, List(t1,t2,t3,t4,t5)) if isTuple5(sym) =>
+ TupleType(Seq(extractType(t1),extractType(t2),extractType(t3),extractType(t4),extractType(t5)))
+
+ case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) =>
+ ArrayType(extractType(btt))
+
+ case TypeRef(_, sym, Nil) if classesToClasses contains sym =>
+ classDefToClassType(classesToClasses(sym))
+
+ case SingleType(_, sym) if classesToClasses contains sym.moduleClass=>
+ classDefToClassType(classesToClasses(sym.moduleClass))
+
+ case _ =>
+ unsupported("Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
}
- rec(tree)
- }
- private def scalaType2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Type): purescala.TypeTrees.TypeTree = {
-
- def rec(tr: Type): purescala.TypeTrees.TypeTree = tr match {
- case tpe if tpe == IntClass.tpe => Int32Type
- case tpe if tpe == BooleanClass.tpe => BooleanType
- case tpe if tpe == UnitClass.tpe => UnitType
- case tpe if tpe == NothingClass.tpe => BottomType
- case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
- case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
- case TypeRef(_, sym, List(ftt,ttt)) if isMapTraitSym(sym) => MapType(rec(ftt),rec(ttt))
- case TypeRef(_, sym, List(t1,t2)) if isTuple2(sym) => TupleType(Seq(rec(t1),rec(t2)))
- case TypeRef(_, sym, List(t1,t2,t3)) if isTuple3(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3)))
- case TypeRef(_, sym, List(t1,t2,t3,t4)) if isTuple4(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4)))
- case TypeRef(_, sym, List(t1,t2,t3,t4,t5)) if isTuple5(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3),rec(t4),rec(t5)))
- case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) => ArrayType(rec(btt))
- case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
- case _ => {
- if(!silent) {
- unit.error(NoPosition, "Could not extract type as PureScala. [" + tr + "]")
- throw new Exception("aouch")
- }
- throw ImpureCodeEncounteredException(null)
+ private def getReturnedExpr(expr: LeonExpr): Seq[LeonExpr] = expr match {
+ case Let(_, _, rest) => getReturnedExpr(rest)
+ case LetVar(_, _, rest) => getReturnedExpr(rest)
+ case LeonBlock(_, rest) => getReturnedExpr(rest)
+ case IfExpr(_, thenn, elze) => getReturnedExpr(thenn) ++ getReturnedExpr(elze)
+ case MatchExpr(_, cses) => cses.flatMap{
+ case SimpleCase(_, rhs) => getReturnedExpr(rhs)
+ case GuardedCase(_, _, rhs) => getReturnedExpr(rhs)
}
- // case tt => {
- // if(!silent) {
- // unit.error(tree.pos, "This does not appear to be a type tree: [" + tt + "]")
- // }
- // throw ImpureCodeEncounteredException(tree)
- // }
+ case _ => Seq(expr)
}
- rec(tree)
- }
+ def getOwner(exprs: Seq[LeonExpr]): Option[Option[FunDef]] = {
+ val exprOwners: Seq[Option[Option[FunDef]]] = exprs.map(owners.get(_))
+ if(exprOwners.exists(_ == None))
+ None
+ else if(exprOwners.exists(_ == Some(None)))
+ Some(None)
+ else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
+ Some(None)
+ else
+ exprOwners(0)
+ }
- def mkPosString(pos: scala.tools.nsc.util.Position) : String = {
- pos.line + "," + pos.column
- }
+ def getOwner(expr: LeonExpr): Option[Option[FunDef]] = getOwner(getReturnedExpr(expr))
- def getReturnedExpr(expr: Expr): Seq[Expr] = expr match {
- case Let(_, _, rest) => getReturnedExpr(rest)
- case LetVar(_, _, rest) => getReturnedExpr(rest)
- case PBlock(_, rest) => getReturnedExpr(rest)
- case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze)
- case MatchExpr(_, cses) => cses.flatMap{
- case SimpleCase(_, rhs) => getReturnedExpr(rhs)
- case GuardedCase(_, _, rhs) => getReturnedExpr(rhs)
- }
- case _ => Seq(expr)
- }
+ def extractProgram: Option[Program] = {
+ val topLevelObjDef = extractTopLevelDef
- def getOwner(exprs: Seq[Expr]): Option[Option[FunDef]] = {
- val exprOwners: Seq[Option[Option[FunDef]]] = exprs.map(owners.get(_))
- if(exprOwners.exists(_ == None))
- None
- else if(exprOwners.exists(_ == Some(None)))
- Some(None)
- else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
- Some(None)
- else
- exprOwners(0)
- }
+ val programName: Identifier = unit.body match {
+ case PackageDef(name, _) => FreshIdentifier(name.toString)
+ case _ => FreshIdentifier("<program>")
+ }
+
+ topLevelObjDef.map(obj => Program(programName, obj))
+ }
+ }
- def getOwner(expr: Expr): Option[Option[FunDef]] = getOwner(getReturnedExpr(expr))
}
diff --git a/src/main/scala/leon/plugin/ExtractionPhase.scala b/src/main/scala/leon/plugin/ExtractionPhase.scala
index 07f9f113fdc980599c28c24638682bd977fc0de0..b81c951303aadd4ae8be6ef0fdbe72a85cc6f8d6 100644
--- a/src/main/scala/leon/plugin/ExtractionPhase.scala
+++ b/src/main/scala/leon/plugin/ExtractionPhase.scala
@@ -4,7 +4,8 @@ package leon
package plugin
import purescala.Definitions.Program
-import scala.tools.nsc.{Global,Settings=>NSCSettings,SubComponent,CompilerCommand}
+
+import scala.tools.nsc.{Settings=>NSCSettings,CompilerCommand}
object ExtractionPhase extends LeonPhase[List[String], Program] {
@@ -16,6 +17,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val settings = new NSCSettings
settings.classpath.value = ctx.settings.classPath.mkString(":")
+ settings.skip.value = List("patmat")
val compilerOpts = args.filterNot(_.startsWith("--"))
@@ -31,13 +33,17 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
// )
// }
- val runner = new PluginRunner(settings, ctx, None)
- val run = new runner.Run
+ val compiler = new ScalaCompiler(settings, ctx)
+ val run = new compiler.Run
run.compile(command.files)
- runner.program match {
+ compiler.leonExtraction.program match {
case Some(p) =>
- p
+ if (ctx.reporter.errorCount > 0 && ctx.settings.strictCompilation) {
+ ctx.reporter.fatalError("Error while compiling.")
+ } else {
+ p
+ }
case None =>
ctx.reporter.fatalError("Error while compiling.")
}
@@ -46,30 +52,3 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
}
}
}
-
-/** This class is a compiler that will be used for running the plugin in
- * standalone mode. Original version courtesy of D. Zufferey. */
-class PluginRunner(settings : NSCSettings, ctx: LeonContext, var program: Option[Program]) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) {
- val leonPlugin = new LeonPlugin(this)
-
- protected def myAddToPhasesSet(sub : SubComponent, descr : String) : Unit = {
- phasesSet += sub
- }
-
- /** The phases to be run. */
- override protected def computeInternalPhases() : Unit = {
- val phs = List(
- syntaxAnalyzer -> "parse source into ASTs, perform simple desugaring",
- analyzer.namerFactory -> "resolve names, attach symbols to named trees",
- analyzer.packageObjects -> "load package objects",
- analyzer.typerFactory -> "the meat and potatoes: type the trees",
- superAccessors -> "add super accessors in traits and nested classes",
- pickler -> "serialize symbol tables",
- refchecks -> "reference and override checking, translate nested objects"
- ) ::: {
- val zipped = leonPlugin.components zip leonPlugin.descriptions
- zipped
- }
- phs foreach (myAddToPhasesSet _).tupled
- }
-}
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index e407a35086e62215869bcbfdeefd520b60f44d63..00da888f67181eecb21e62118b263e8ec326c6f3 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -8,24 +8,82 @@ import scala.tools.nsc._
/** Contains extractors to pull-out interesting parts of the Scala ASTs. */
trait Extractors {
val global: Global
- val pluginInstance: LeonPlugin
import global._
import global.definitions._
- protected lazy val tuple2Sym: Symbol = definitions.getClass("scala.Tuple2")
- protected lazy val tuple3Sym: Symbol = definitions.getClass("scala.Tuple3")
- protected lazy val tuple4Sym: Symbol = definitions.getClass("scala.Tuple4")
- protected lazy val tuple5Sym: Symbol = definitions.getClass("scala.Tuple5")
- private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
- private lazy val mapTraitSym = definitions.getClass("scala.collection.immutable.Map")
- private lazy val multisetTraitSym = definitions.getClass("scala.collection.immutable.Multiset")
- private lazy val optionClassSym = definitions.getClass("scala.Option")
+ def classFromName(str: String) = {
+ rootMirror.getClassByName(newTypeName(str))
+ }
+ def objectFromName(str: String) = {
+ rootMirror.getClassByName(newTermName(str))
+ }
+
+ protected lazy val tuple2Sym = classFromName("scala.Tuple2")
+ protected lazy val tuple3Sym = classFromName("scala.Tuple3")
+ protected lazy val tuple4Sym = classFromName("scala.Tuple4")
+ protected lazy val tuple5Sym = classFromName("scala.Tuple5")
+ protected lazy val mapSym = classFromName("scala.collection.immutable.Map")
+ protected lazy val setSym = classFromName("scala.collection.immutable.Set")
+ protected lazy val optionClassSym = classFromName("scala.Option")
+ protected lazy val arraySym = classFromName("scala.Array")
+ protected lazy val someClassSym = classFromName("scala.Some")
+ protected lazy val function1TraitSym = classFromName("scala.Function1")
+
+ def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
+ def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
+ def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
+ def isTuple5(sym : Symbol) : Boolean = sym == tuple5Sym
+
+
+ // Resolve type aliases
+ def getResolvedTypeSym(sym: Symbol): Symbol = {
+ if (sym.isAliasType) {
+ getResolvedTypeSym(sym.tpe.resultType.typeSymbol)
+ } else {
+ sym
+ }
+ }
+
+ def isSetTraitSym(sym : Symbol) : Boolean = {
+ getResolvedTypeSym(sym) == setSym
+ }
+
+ def isMapTraitSym(sym : Symbol) : Boolean = {
+ getResolvedTypeSym(sym) == mapSym
+ }
+
+ def isMultisetTraitSym(sym : Symbol) : Boolean = {
+ sym == multisetTraitSym
+ }
+
+ def isOptionClassSym(sym : Symbol) : Boolean = {
+ sym == optionClassSym || sym == someClassSym
+ }
+
+ def isFunction1TraitSym(sym : Symbol) : Boolean = {
+ sym == function1TraitSym
+ }
+
+
+ protected lazy val multisetTraitSym = try {
+ classFromName("scala.collection.immutable.Multiset")
+ } catch {
+ case e: Throwable =>
+ null
+ }
+
+ def isArrayClassSym(sym: Symbol): Boolean = sym == arraySym
object ExtractorHelpers {
object ExIdNamed {
def unapply(id: Ident): Option[String] = Some(id.toString)
}
+
+ object ExHasType {
+ def unapply(tr: Tree): Option[(Tree, Symbol)] = Some((tr, tr.tpe.typeSymbol))
+ }
+
object ExNamed {
def unapply(name: Name): Option[String] = Some(name.toString)
}
@@ -63,12 +121,10 @@ trait Extractors {
object ExHoldsExpression {
def unapply(tree: Select) : Option[Tree] = tree match {
- case Select(Apply(Select(Select(leonIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (
- utilsName.toString == "Utils" &&
- any2IsValidName.toString == "any2IsValid" &&
- holdsName.toString == "holds") => Some(realExpr)
+ case Select(Apply(ExSelected("leon", "Utils", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
+ Some(realExpr)
case _ => None
- }
+ }
}
object ExRequiredExpression {
@@ -137,7 +193,7 @@ trait Extractors {
object ExCaseClassSyntheticJunk {
def unapply(cd: ClassDef): Boolean = cd match {
- case ClassDef(_, _, _, _) if (cd.symbol.isSynthetic && cd.symbol.isFinal) => true
+ case ClassDef(_, _, _, _) if (cd.symbol.isSynthetic) => true
case _ => false
}
}
@@ -172,29 +228,12 @@ trait Extractors {
object ExpressionExtractors {
import ExtractorHelpers._
- //object ExLocalFunctionDef {
- // def unapply(tree: Block): Option[(DefDef,String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
- // case Block((dd @ DefDef(_, name, tparams, vparamss, tpt, rhs)) :: rest, expr) if(tparams.isEmpty && vparamss.size == 1 && name != nme.CONSTRUCTOR) => {
- // if(rest.isEmpty)
- // Some((dd,name.toString, vparamss(0), tpt, rhs, expr))
- // else
- // Some((dd,name.toString, vparamss(0), tpt, rhs, Block(rest, expr)))
- // }
- // case _ => None
- // }
- //}
-
-
object ExEpsilonExpression {
def unapply(tree: Apply) : Option[(Type, Symbol, Tree)] = tree match {
case Apply(
- TypeApply(Select(Select(funcheckIdent, utilsName), epsilonName), typeTree :: Nil),
- Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) => {
- if (utilsName.toString == "Utils" && epsilonName.toString == "epsilon")
+ TypeApply(ExSelected("leon", "Utils", "epsilon"), typeTree :: Nil),
+ Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) =>
Some((typeTree.tpe, vd.symbol, predicateBody))
- else
- None
- }
case _ => None
}
}
@@ -211,13 +250,9 @@ trait Extractors {
object ExChooseExpression {
def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree, Tree)] = tree match {
case a @ Apply(
- TypeApply(Select(s @ Select(funcheckIdent, utilsName), chooseName), types),
- Function(vds, predicateBody) :: Nil) => {
- if (utilsName.toString == "Utils" && chooseName.toString == "choose")
+ TypeApply(s @ ExSelected("leon", "Utils", "choose"), types),
+ Function(vds, predicateBody) :: Nil) =>
Some(((types.map(_.tpe) zip vds.map(_.symbol)).toList, a.tpe, predicateBody, s))
- else
- None
- }
case _ => None
}
}
@@ -225,13 +260,9 @@ trait Extractors {
object ExWaypointExpression {
def unapply(tree: Apply) : Option[(Type, Tree, Tree)] = tree match {
case Apply(
- TypeApply(Select(Select(funcheckIdent, utilsName), waypoint), typeTree :: Nil),
- List(i, expr)) => {
- if (utilsName.toString == "Utils" && waypoint.toString == "waypoint")
+ TypeApply(ExSelected("leon", "Utils", "waypoint"), typeTree :: Nil),
+ List(i, expr)) =>
Some((typeTree.tpe, i, expr))
- else
- None
- }
case _ => None
}
}
@@ -267,6 +298,7 @@ trait Extractors {
case _ => None
}
}
+
object ExWhileWithInvariant {
def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
case Apply(
@@ -277,6 +309,7 @@ trait Extractors {
case _ => None
}
}
+
object ExTuple {
def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
case Apply(
@@ -335,10 +368,11 @@ trait Extractors {
try {
val index = indexString.toInt
if(index > 0) {
- Some((lhs, index))
+ Some((lhs, index))
} else None
} catch {
- case _ => None
+ case t: Throwable =>
+ None
}
} else None
}
@@ -645,28 +679,20 @@ trait Extractors {
}
}
- // object ExFiniteMap {
- // def unapply(tree: Apply): Option[(Tree,Tree,List[Tree])] = tree match {
- // case Apply(TypeApply(Select(Select(Select(Select(Ident(s), collectionName), immutableName), mapName), applyName), List(fromTypeTree, toTypeTree)), args) if (collectionName.toString == "collection" && immutableName.toString == "immutable" && mapName.toString == "Map" && applyName.toString == "apply") => Some((fromTypeTree, toTypeTree, args))
- // case Apply(TypeApply(Select(Select(Select(This(scalaName), predefName), mapName), applyName), List(fromTypeTree, toTypeTree)), args) if (scalaName.toString == "scala" && predefName.toString == "Predef" && mapName.toString == "Map" && applyName.toString == "apply") => Some((fromTypeTree, toTypeTree, args))
- // case _ => None
- // }
- // }
-
object ExUnion {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
- case Apply(Select(lhs, n), List(rhs)) if (n == encode("++")/*nme.PLUSPLUS*/) => Some((lhs,rhs))
+ case Apply(Select(lhs, n), List(rhs)) if n == encode("++") => Some((lhs,rhs))
case _ => None
}
}
object ExPlusPlusPlus {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
- case Apply(Select(lhs, n), List(rhs)) if (n.toString == "$plus$plus$plus") => Some((lhs,rhs))
+ case Apply(Select(lhs, n), List(rhs)) if n.toString == encode("+++") => Some((lhs,rhs))
case _ => None
}
}
-
+
object ExIntersection {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
case Apply(Select(lhs, n), List(rhs)) if (n == encode("**") || n == encode("&")) => Some((lhs,rhs))
@@ -744,14 +770,14 @@ trait Extractors {
object ExArrayLength {
def unapply(tree: Select): Option[Tree] = tree match {
- case Select(t, n) if (n.toString == "length") => Some(t)
+ case Select(ExHasType(t, `arraySym`), n) if n.toString == "length" => Some(t)
case _ => None
}
}
object ExArrayClone {
def unapply(tree: Apply): Option[Tree] = tree match {
- case Apply(Select(t, n), List()) if (n.toString == "clone") => Some(t)
+ case Apply(Select(ExHasType(t, `arraySym`), n), List()) if n.toString == "clone" => Some(t)
case _ => None
}
}
@@ -762,18 +788,14 @@ trait Extractors {
case Apply(
Apply(
Apply(
- TypeApply(
- Select(Select(Ident(scala), arrayObject), fillMethod),
- baseType :: Nil
- ),
+ TypeApply(ExSelected("scala", "Array", "fill"), baseType :: Nil),
length :: Nil
),
defaultValue :: Nil
),
manifest
- ) if(scala.toString == "scala" &&
- arrayObject.toString == "Array" &&
- fillMethod.toString == "fill") => Some((baseType, length, defaultValue))
+ ) =>
+ Some((baseType, length, defaultValue))
case _ => None
}
}
diff --git a/src/main/scala/leon/plugin/LeonExtraction.scala b/src/main/scala/leon/plugin/LeonExtraction.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a2f00340e9026225e35b9e6d9f800ecd2563e735
--- /dev/null
+++ b/src/main/scala/leon/plugin/LeonExtraction.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package plugin
+
+import scala.tools.nsc._
+import scala.tools.nsc.plugins._
+
+import purescala.Definitions.Program
+
+trait LeonExtraction extends SubComponent with CodeExtraction {
+ import global._
+
+ val phaseName = "leon"
+
+ var program: Option[Program] = None
+
+ val ctx: LeonContext
+
+ def newPhase(prev: scala.tools.nsc.Phase): StdPhase = new Phase(prev)
+
+ class Phase(prev: scala.tools.nsc.Phase) extends StdPhase(prev) {
+ def apply(unit: CompilationUnit): Unit = {
+ program = new Extraction(unit).extractProgram
+ }
+ }
+}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
deleted file mode 100644
index badf32e8ef5d3333f937a6291d4fade2f8603aec..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ /dev/null
@@ -1,39 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-package plugin
-
-import scala.tools.nsc
-import scala.tools.nsc.{Global,Phase}
-import scala.tools.nsc.plugins.{Plugin,PluginComponent}
-import purescala.Definitions.Program
-
-/** This class is the entry point for the plugin. */
-class LeonPlugin(val global: PluginRunner) extends Plugin {
- import global._
-
- val name = "leon"
- val description = "The Leon static analyzer"
-
- /** The help message displaying the options for that plugin. */
- override val optionsHelp: Option[String] = Some(
- " --uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
- " --tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n"
- )
-
- /** Processes the command-line options. */
- private def splitList(lst: String) : Seq[String] = lst.split(':').map(_.trim).filter(!_.isEmpty)
- override def processOptions(options: List[String], error: String => Unit) {
- for(option <- options) {
- option match {
- case "uniqid" => leon.Settings.showIDs = true
- case "tolerant" => leon.Settings.silentlyTolerateNonPureBodies = true
-
- case _ => error("Invalid option: " + option + "\nValid options are:\n" + optionsHelp.get)
- }
- }
- }
-
- val components = List(new AnalysisComponent(global, this))
- val descriptions = List[String]("leon analyses")
-}
diff --git a/src/main/scala/leon/plugin/ScalaCompiler.scala b/src/main/scala/leon/plugin/ScalaCompiler.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f6052d60ac68b241a01235c5ff622927434cebe1
--- /dev/null
+++ b/src/main/scala/leon/plugin/ScalaCompiler.scala
@@ -0,0 +1,30 @@
+package leon
+package plugin
+
+import scala.tools.nsc.{Global,Settings=>NSCSettings}
+
+class ScalaCompiler(settings : NSCSettings, ctx: LeonContext) extends Global(settings, new SimpleReporter(settings, ctx.reporter)) {
+
+ object leonExtraction extends {
+ val global: ScalaCompiler.this.type = ScalaCompiler.this
+ val runsAfter = List[String]("refchecks")
+ val runsRightAfter = None
+ val ctx = ScalaCompiler.this.ctx
+ } with LeonExtraction
+
+ override protected def computeInternalPhases() : Unit = {
+ val phs = List(
+ syntaxAnalyzer -> "parse source into ASTs, perform simple desugaring",
+ analyzer.namerFactory -> "resolve names, attach symbols to named trees",
+ analyzer.packageObjects -> "load package objects",
+ analyzer.typerFactory -> "the meat and potatoes: type the trees",
+ patmat -> "translate match expressions",
+ superAccessors -> "add super accessors in traits and nested classes",
+ extensionMethods -> "add extension methods for inline classes",
+ pickler -> "serialize symbol tables",
+ refChecks -> "reference/override checking, translate nested objects",
+ leonExtraction -> "extracts leon trees out of scala trees"
+ )
+ phs foreach { phasesSet += _._1 }
+ }
+}
diff --git a/src/main/scala/leon/plugin/SimpleReporter.scala b/src/main/scala/leon/plugin/SimpleReporter.scala
index 549fb2589d47e5557b5ba1ebf415f7c37099f614..9057afeaf1ffa317b72c25292c58c9f56bf32260 100644
--- a/src/main/scala/leon/plugin/SimpleReporter.scala
+++ b/src/main/scala/leon/plugin/SimpleReporter.scala
@@ -5,8 +5,8 @@ package plugin
import scala.tools.nsc.Settings
import scala.tools.nsc.reporters.AbstractReporter
-import scala.tools.nsc.util._
-import scala.tools.util.StringOps
+
+import scala.reflect.internal.util.{Position, NoPosition, FakePos, StringOps}
/** This implements a reporter that calls the callback with every line that a
regular ConsoleReporter would display. */
@@ -28,40 +28,50 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
StringOps.countElementsAsString((severity).count, label(severity))
/** Prints the message. */
- def printMessage(msg: String) { reporter.info(msg) }
+ def printMessage(msg: String, severity: Severity) {
+ severity match {
+ case ERROR =>
+ reporter.error(msg)
+ case WARNING =>
+ reporter.warning(msg)
+ case INFO =>
+ reporter.info(msg)
+ }
+ }
/** Prints the message with the given position indication. */
- def printMessage(posIn: Position, msg: String) {
+ def printMessage(posIn: Position, msg: String, severity: Severity) {
val pos = if (posIn eq null) NoPosition
else if (posIn.isDefined) posIn.inUltimateSource(posIn.source)
else posIn
pos match {
case FakePos(fmsg) =>
- printMessage(fmsg+" "+msg)
+ printMessage(fmsg+" "+msg, severity)
case NoPosition =>
- printMessage(msg)
+ printMessage(msg, severity)
case _ =>
val buf = new StringBuilder(msg)
val file = pos.source.file
- printMessage(pos.line + ": " + msg)
- printSourceLine(pos)
+ printMessage(pos.line + ": " + msg+"\n"+getSourceLine(pos), severity)
}
}
def print(pos: Position, msg: String, severity: Severity) {
- printMessage(pos, clabel(severity) + msg)
+ printMessage(pos, clabel(severity) + msg, severity)
}
- def printSourceLine(pos: Position) {
- printMessage(pos.lineContent.stripLineEnd)
- printColumnMarker(pos)
+ def getSourceLine(pos: Position) = {
+ pos.lineContent.stripLineEnd+getColumnMarker(pos)
}
- def printColumnMarker(pos: Position) =
- if (pos.isDefined) { printMessage(" " * (pos.column - 1) + "^") }
+ def getColumnMarker(pos: Position) = if (pos.isDefined) {
+ "\n"+(" " * (pos.column - 1) + "^")
+ } else {
+ ""
+ }
def printSummary() {
- if (WARNING.count > 0) printMessage(getCountString(WARNING) + " found")
- if ( ERROR.count > 0) printMessage(getCountString(ERROR ) + " found")
+ if (WARNING.count > 0) printMessage(getCountString(WARNING) + " found", INFO)
+ if ( ERROR.count > 0) printMessage(getCountString(ERROR ) + " found", INFO)
}
def display(pos: Position, msg: String, severity: Severity) {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 704d6a7ae3d6f89a67af8b889ce1818d5ef83bf5..8837ee937c89adb0593d5a2ec0e208162dbcb2e3 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -105,7 +105,7 @@ object Extractors {
case FiniteArray(args) => Some((args, FiniteArray))
case Distinct(args) => Some((args, Distinct))
case Tuple(args) => Some((args, Tuple))
- case IfExpr(cond, then, elze) => Some((Seq(cond, then, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))))
+ case IfExpr(cond, thenn, elze) => Some((Seq(cond, thenn, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))))
case MatchExpr(scrut, cases) =>
Some((scrut +: cases.flatMap{ case SimpleCase(_, e) => Seq(e)
case GuardedCase(_, e1, e2) => Seq(e1, e2) }
@@ -207,7 +207,7 @@ object Extractors {
object TopLevelOrs { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case Or(exprs) =>
- Some(exprs.flatMap(unapply(_).flatten))
+ Some(exprs.flatMap(unapply(_)).flatten)
case e =>
Some(Seq(e))
}
@@ -215,7 +215,7 @@ object Extractors {
object TopLevelAnds { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case And(exprs) =>
- Some(exprs.flatMap(unapply(_).flatten))
+ Some(exprs.flatMap(unapply(_)).flatten)
case e =>
Some(Seq(e))
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 964d4d90559041c95086922d4c09fa9ae41fc9da..ebe8260c80372708a220ed55d8daa46c98ac39e5 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -56,7 +56,7 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
def pp(tree: Expr, lvl: Int): Unit = tree match {
case Variable(id) => sb.append(idToString(id))
case DeBruijnIndex(idx) => sb.append("_" + idx)
- case LetTuple(bs,d,e) => {
+ case LetTuple(bs,d,e) =>
//pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
sb.append("(let (" + bs.map(idToString _).mkString(",") + " := ");
pp(d, lvl)
@@ -64,9 +64,8 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
ind(lvl+1)
pp(e, lvl+1)
sb.append(")")
- sb
- }
- case Let(b,d,e) => {
+
+ case Let(b,d,e) =>
//pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
sb.append("(let (" + idToString(b) + " := ");
pp(d, lvl)
@@ -74,8 +73,7 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
ind(lvl+1)
pp(e, lvl+1)
sb.append(")")
- sb
- }
+
case And(exprs) => ppNary(exprs, "(", " \u2227 ", ")", lvl) // \land
case Or(exprs) => ppNary(exprs, "(", " \u2228 ", ")", lvl) // \lor
case Not(Equals(l, r)) => ppBinary(l, r, " \u2260 ", lvl) // \neq
@@ -88,41 +86,35 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
case StringLiteral(s) => sb.append("\"" + s + "\"")
case UnitLiteral => sb.append("()")
case t@Tuple(exprs) => ppNary(exprs, "(", ", ", ")", lvl)
- case s@TupleSelect(t, i) => {
+ case s@TupleSelect(t, i) =>
pp(t, lvl)
sb.append("._" + i)
- sb
- }
- case c@Choose(vars, pred) => {
+ case c@Choose(vars, pred) =>
sb.append("choose("+vars.map(idToString _).mkString(", ")+" => ")
pp(pred, lvl)
sb.append(")")
- }
- case CaseClass(cd, args) => {
+ case CaseClass(cd, args) =>
sb.append(idToString(cd.id))
if (cd.isCaseObject) {
ppNary(args, "", "", "", lvl)
} else {
ppNary(args, "(", ", ", ")", lvl)
}
- sb
- }
- case CaseClassInstanceOf(cd, e) => {
+
+ case CaseClassInstanceOf(cd, e) =>
pp(e, lvl)
sb.append(".isInstanceOf[" + idToString(cd.id) + "]")
- sb
- }
+
case CaseClassSelector(_, cc, id) =>
pp(cc, lvl)
sb.append("." + idToString(id))
- case FunctionInvocation(fd, args) => {
+ case FunctionInvocation(fd, args) =>
sb.append(idToString(fd.id))
ppNary(args, "(", ", ", ")", lvl)
- sb
- }
+
case Plus(l,r) => ppBinary(l, r, " + ", lvl)
case Minus(l,r) => ppBinary(l, r, " - ", lvl)
case Times(l,r) => ppBinary(l, r, " * ", lvl)
@@ -152,7 +144,7 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
case MultisetCardinality(t) => ppUnary(t, "|", "|", lvl)
case MultisetPlus(l,r) => ppBinary(l, r, " \u228E ", lvl) // U+
case MultisetToSet(e) => pp(e, lvl); sb.append(".toSet")
- case FiniteMap(rs) => {
+ case FiniteMap(rs) =>
sb.append("{")
val sz = rs.size
var c = 0
@@ -160,62 +152,58 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
pp(k, lvl); sb.append(" -> "); pp(v, lvl); c += 1 ; if(c < sz) sb.append(", ")
}}
sb.append("}")
- }
- case MapGet(m,k) => {
+
+ case MapGet(m,k) =>
pp(m, lvl)
ppNary(Seq(k), "(", ",", ")", lvl)
- sb
- }
- case MapIsDefinedAt(m,k) => {
+
+ case MapIsDefinedAt(m,k) =>
pp(m, lvl)
sb.append(".isDefinedAt")
ppNary(Seq(k), "(", ",", ")", lvl)
- sb
- }
- case ArrayLength(a) => {
+
+ case ArrayLength(a) =>
pp(a, lvl)
sb.append(".length")
- }
- case ArrayClone(a) => {
+
+ case ArrayClone(a) =>
pp(a, lvl)
sb.append(".clone")
- }
- case fill@ArrayFill(size, v) => {
+
+ case fill@ArrayFill(size, v) =>
sb.append("Array.fill(")
pp(size, lvl)
sb.append(")(")
pp(v, lvl)
sb.append(")")
- }
- case am@ArrayMake(v) => {
+
+ case am@ArrayMake(v) =>
sb.append("Array.make(")
pp(v, lvl)
sb.append(")")
- }
- case sel@ArraySelect(ar, i) => {
+
+ case sel@ArraySelect(ar, i) =>
pp(ar, lvl)
sb.append("(")
pp(i, lvl)
sb.append(")")
- }
- case up@ArrayUpdated(ar, i, v) => {
+
+ case up@ArrayUpdated(ar, i, v) =>
pp(ar, lvl)
sb.append(".updated(")
pp(i, lvl)
sb.append(", ")
pp(v, lvl)
sb.append(")")
- }
- case FiniteArray(exprs) => {
+
+ case FiniteArray(exprs) =>
ppNary(exprs, "Array(", ", ", ")", lvl)
- }
- case Distinct(exprs) => {
+ case Distinct(exprs) =>
sb.append("distinct")
ppNary(exprs, "(", ", ", ")", lvl)
- }
- case IfExpr(c, t, e) => {
+ case IfExpr(c, t, e) =>
sb.append("if (")
pp(c, lvl)
sb.append(")\n")
@@ -226,7 +214,6 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
sb.append("else\n")
ind(lvl+1)
pp(e, lvl+1)
- }
case mex @ MatchExpr(s, csc) => {
def ppc(p: Pattern): Unit = p match {
@@ -286,11 +273,10 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
case ResultVariable() => sb.append("#res")
case Not(expr) => ppUnary(expr, "\u00AC(", ")", lvl) // \neg
- case e @ Error(desc) => {
+ case e @ Error(desc) =>
sb.append("error(\"" + desc + "\")[")
pp(e.getType, lvl)
sb.append("]")
- }
case (expr: PrettyPrintable) => expr.printWith(lvl, this)
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index d7ab7e3a48dd140853f548bf38251fb92435d937..e2350d5037d430fe6e7ba48423a2e8f1c05ea791 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -415,15 +415,13 @@ object ScalaPrinter {
sb.append("}\n")
}
- case AbstractClassDef(id, parent) => {
+ case AbstractClassDef(id, parent) =>
ind(sb, lvl)
sb.append("sealed abstract class ")
sb.append(id)
parent.foreach(p => sb.append(" extends " + p.id))
- sb
- }
- case CaseClassDef(id, parent, varDecls) => {
+ case CaseClassDef(id, parent, varDecls) =>
ind(sb, lvl)
sb.append("case class ")
sb.append(id)
@@ -442,10 +440,8 @@ object ScalaPrinter {
})
sb.append(")")
parent.foreach(p => sb.append(" extends " + p.id))
- sb
- }
- case fd @ FunDef(id, rt, args, body, pre, post) => {
+ case fd @ FunDef(id, rt, args, body, pre, post) =>
//for(a <- fd.annotations) {
// ind(sb, lvl)
@@ -509,9 +505,6 @@ object ScalaPrinter {
}
}
- sb
- }
-
case _ => sb.append("Defn?")
}
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 818d125e4e2041add92b4888437608f0b5072229..d59e67b40aeb9e1944a18bd07d4031deb41ed1dc 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1015,12 +1015,12 @@ object TreeOps {
*/
def decomposeIfs(e: Expr): Expr = {
def pre(e: Expr): Expr = e match {
- case IfExpr(cond, then, elze) =>
+ case IfExpr(cond, thenn, elze) =>
val TopLevelOrs(orcases) = cond
if (orcases.exists{ case TopLevelAnds(ands) => ands.exists(_.isInstanceOf[CaseClassInstanceOf]) } ) {
if (!orcases.tail.isEmpty) {
- pre(IfExpr(orcases.head, then, IfExpr(Or(orcases.tail), then, elze)))
+ pre(IfExpr(orcases.head, thenn, IfExpr(Or(orcases.tail), thenn, elze)))
} else {
val TopLevelAnds(andcases) = orcases.head
@@ -1029,7 +1029,7 @@ object TreeOps {
if (andis.isEmpty || andnotis.isEmpty) {
e
} else {
- IfExpr(And(andis), IfExpr(And(andnotis), then, elze), elze)
+ IfExpr(And(andis), IfExpr(And(andnotis), thenn, elze), elze)
}
}
} else {
@@ -1045,7 +1045,7 @@ object TreeOps {
// This transformation assumes IfExpr of the form generated by decomposeIfs
def patternMatchReconstruction(e: Expr): Expr = {
def pre(e: Expr): Expr = e match {
- case IfExpr(cond, then, elze) =>
+ case IfExpr(cond, thenn, elze) =>
val TopLevelAnds(cases) = cond
if (cases.forall(_.isInstanceOf[CaseClassInstanceOf])) {
@@ -1107,7 +1107,7 @@ object TreeOps {
CaseClassPattern(Some(binder), cd, subconds)
}
- val (scrutinees, patterns) = scrutSet.toSeq.map(s => (s, computePatternFor(conditions(s), s))) unzip
+ val (scrutinees, patterns) = scrutSet.toSeq.map(s => (s, computePatternFor(conditions(s), s))).unzip
val (scrutinee, pattern) = if (scrutinees.size > 1) {
(Tuple(scrutinees), TuplePattern(None, patterns))
@@ -1119,7 +1119,7 @@ object TreeOps {
// (topdown).
// So replaceing using Map(a => b, CC(a) => d) will replace
// "CC(a)" by "d" and not by "CC(b)"
- val newThen = searchAndReplace(substMap.get)(then)
+ val newThen = searchAndReplace(substMap.get)(thenn)
// Remove unused binders
val vars = variablesOf(newThen)
@@ -1168,10 +1168,10 @@ object TreeOps {
e
- case IfExpr(cond, then, elze) =>
+ case IfExpr(cond, thenn, elze) =>
try {
solver.solve(cond) match {
- case Some(true) => then
+ case Some(true) => thenn
case Some(false) => solver.solve(Not(cond)) match {
case Some(true) => elze
case _ => e
@@ -1238,10 +1238,10 @@ object TreeOps {
val sb = rec(b, register(Equals(Tuple(is.map(Variable(_))), se), path))
LetTuple(is, se, sb)
- case IfExpr(cond, then, elze) =>
+ case IfExpr(cond, thenn, elze) =>
val rc = rec(cond, path)
- IfExpr(rc, rec(then, register(rc, path)), rec(elze, register(Not(rc), path)))
+ IfExpr(rc, rec(thenn, register(rc, path)), rec(elze, register(Not(rc), path)))
case And(es) => {
var soFar = path
@@ -1308,7 +1308,7 @@ object TreeOps {
}
protected override def rec(e: Expr, path: C) = e match {
- case IfExpr(cond, then, elze) =>
+ case IfExpr(cond, thenn, elze) =>
super.rec(e, path) match {
case IfExpr(BooleanLiteral(true) , t, _) => t
case IfExpr(BooleanLiteral(false), _, e) => e
@@ -1742,7 +1742,8 @@ object TreeOps {
if(t._1 == IntLiteral(0)) acc else Plus(acc, Times(t._1, t._2))
})
} catch {
- case _ => expr
+ case _: Throwable =>
+ expr
}
simplifyArithmetic(expr0)
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 21a23be82a8a50c20720404913f2a6c1d0cfb045..b0a7d3220196212b7b42f118b373fb73a489af7e 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -57,8 +57,8 @@ object Trees {
funDef.args.zip(args).foreach { case (a, c) => typeCheck(c, a.tpe) }
}
- case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr with FixedType {
- val fixedType = leastUpperBound(then.getType, elze.getType).getOrElse(AnyType)
+ case class IfExpr(cond: Expr, thenn: Expr, elze: Expr) extends Expr with FixedType {
+ val fixedType = leastUpperBound(thenn.getType, elze.getType).getOrElse(AnyType)
}
case class Tuple(exprs: Seq[Expr]) extends Expr with FixedType {
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
deleted file mode 100644
index b812f3b7e58b64ab38de723765ee2eb258f24870..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ /dev/null
@@ -1,169 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TypeTrees._
-
-import scala.actors.Actor
-import scala.actors.DaemonActor
-import scala.actors.Actor._
-
-import scala.concurrent.Lock
-
-@deprecated("Unused, Untested, Unmaintained", "")
-class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with NaiveIncrementalSolver {
- private val nbSolvers = solvers.size
- require(nbSolvers >= 2)
-
- private val reporter = context.reporter
-
- val description = "Solver running subsolvers in parallel " + solvers.map(_.description).mkString("(", ", ", ")")
- override val name = solvers.map(_.name).mkString("//")
- override val superseeds : Seq[String] = solvers.map(_.name).toSeq
-
- case class Solve(expr: Expr)
- case object Init
- case object Ready
- case class Result(res: Option[Boolean])
-
- private class SolverRunner(s: Solver) extends DaemonActor {
-
- /*
- val that = this
- val worker = new Actor {
- def act(): Unit = {
- while(true) {
- receive {
- case Solve(expr) => {
- reporter.info("Starting solver " + s.name)
- val res = s.solve(expr)
- that ! Result(res)
- reporter.info("Ending solver " + s.name)
- }
- }
- }
- }
- }
- */
-
- def act(): Unit = {
- while(true) {
- receive {
- case Init => {
- reporter.info("Init solver " + s.name)
- s.init
- coordinator ! Ready
- }
- case Solve(expr) => {
- reporter.info("Starting solver " + s.name)
- val res = s.solve(expr)
- coordinator ! Result(res)
- reporter.info("Ending solver " + s.name)
- }
- }
- }
- }
- }
-
- private class Coordinator extends DaemonActor {
-
- def act(): Unit = {
- while(true) {
- receive {
- case s@Solve(expr) => {
- var nbResponses = 0
-
- solverRunners.foreach(_ ! Init)
- while(nbResponses < nbSolvers) {
- receive {
- case Ready => nbResponses += 1
- }
- }
-
- nbResponses = 0
- solverRunners.foreach(_ ! s)
- var result: Option[Boolean] = None
-
- while(nbResponses < nbSolvers) {
- receive {
- case Result(Some(b)) => {
- solvers.foreach(_.halt)
- result = Some(b)
- nbResponses += 1
- }
- case Result(None) => {
- nbResponses += 1
- }
- }
- }
- reply(result)
- }
- }
- }
- }
- }
-
- private val solverRunners = solvers.map(s => new SolverRunner(s).start())
- solverRunners.foreach(_.start())
- private val coordinator = new Coordinator
- coordinator.start()
-
- def solve(expression: Expr) : Option[Boolean] = {
- val result = (coordinator !? Solve(expression)).asInstanceOf[Option[Boolean]]
- result
- }
-
- override def halt() {
- solvers.foreach(_.halt)
- }
-
- override def setProgram(prog: Program): Unit = {
- solvers.foreach(_.setProgram(prog))
- }
-
-}
-
-
-
-
-/*
- private val lock = new Lock
- private var nbResponses: Int = 0
- private var result: Option[Boolean] = None
- private var resultNotReady: Boolean = true
- private var foundSolution: Boolean = false
-
-
- class SolverRunner(s: Solver, expr: Expr) extends Actor {
- def act() {
- reporter.info("Starting solver " + s.name)
- s.solve(expr) match {
- case Some(b) => {
- lock.acquire
- nbResponses += 1
- if(!foundSolution) {
- solvers.foreach(_.halt)
- result = Some(b)
- foundSolution = true
- }
- lock.release
- }
- case None => {
- lock.acquire
- nbResponses += 1
- lock.release
- }
- }
- lock.acquire
- if(nbResponses >= nbSolvers)
- resultNotReady = false
- lock.release
- reporter.info("Ending solver " + s.name)
- }
- }
- */
-
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index e024b55460ed35db573a500ba517e92e9bcd1e98..f55c4956712b9ffbf976aefdc47378c90d41595e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -623,7 +623,7 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
case OpTrue => BooleanLiteral(true)
case OpFalse => BooleanLiteral(false)
case OpEq => Equals(rargs(0), rargs(1))
- case OpITE => {
+ case OpITE =>
assert(argsSize == 3)
val r0 = rargs(0)
val r1 = rargs(1)
@@ -631,15 +631,14 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
try {
IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType).get)
} catch {
- case e => {
+ case e: Throwable =>
println("I was asking for lub because of this.")
println(t)
println("which was translated as")
println(IfExpr(r0,r1,r2))
throw e
- }
}
- }
+
case OpAnd => And(rargs)
case OpOr => Or(rargs)
case OpIff => Iff(rargs(0), rargs(1))
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index aacc633764dd0df4dbee24b72d5aa3cb1f531b7d..32e919992f42c6978d843d8a5990ad27a79c0f87 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -263,8 +263,8 @@ object FunctionTemplate {
Or(parts.map(rec(pathVar, _)))
}
- case i @ IfExpr(cond, then, elze) => {
- if(!containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
+ case i @ IfExpr(cond, thenn, elze) => {
+ if(!containsFunctionCalls(cond) && !containsFunctionCalls(thenn) && !containsFunctionCalls(elze)) {
i
} else {
val newBool1 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
@@ -277,7 +277,7 @@ object FunctionTemplate {
exprVars += newExpr
val crec = rec(pathVar, cond)
- val trec = rec(newBool1, then)
+ val trec = rec(newBool1, thenn)
val erec = rec(newBool2, elze)
storeGuarded(pathVar, Or(Variable(newBool1), Variable(newBool2)))
diff --git a/src/main/scala/leon/synthesis/ManualSearch.scala b/src/main/scala/leon/synthesis/ManualSearch.scala
index 4e075254f217c5e5303b448a51d55acfa205e154..b64a8340326ce1d11454b05c859a7407c9325f82 100644
--- a/src/main/scala/leon/synthesis/ManualSearch.scala
+++ b/src/main/scala/leon/synthesis/ManualSearch.scala
@@ -157,7 +157,7 @@ class ManualSearch(synth: Synthesizer,
}
}
} catch {
- case e =>
+ case e: Throwable =>
error("Woops: "+e.getMessage())
e.printStackTrace()
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 5b6442206faf4dc71628fb30f25dd4bed9571f76..294a54f8f4e8caad453149410651fc3d36b492a2 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -233,12 +233,12 @@ case object CEGIS extends Rule("CEGIS") {
Error("No valid clause available").setType(c.getType)
} else {
cases.tail.foldLeft(cases.head._2) {
- case (elze, (b, then)) => IfExpr(Variable(b), then, elze)
+ case (elze, (b, thenn)) => IfExpr(Variable(b), thenn, elze)
}
}
c -> ifExpr
- } toMap
+ }.toMap
// Map each x generated by the program to fresh xs passed as argument
val newXs = p.xs.map(x => x -> FreshIdentifier(x.name, true).setType(x.getType))
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index 786d1970dd137eef4bd33e6971a5bcee1ff438e9..c2f08f1286f51489ecbeb974d4111aed85cc9f97 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -3,11 +3,11 @@
package leon.synthesis.search
import akka.actor._
-import akka.util.duration._
+import scala.concurrent.duration._
+import scala.concurrent.Await
import akka.util.Timeout
import akka.pattern.ask
import akka.pattern.AskTimeoutException
-import akka.dispatch.Await
abstract class AndOrGraphParallelSearch[WC,
AT <: AOAndTask[S],
diff --git a/src/main/scala/leon/testgen/CallGraph.scala b/src/main/scala/leon/testgen/CallGraph.scala
index a81a56ee213223187769fda525fd8d1aeb23fc69..62de1f42b6ef68b345d9b90641e8ca74889eaa8f 100644
--- a/src/main/scala/leon/testgen/CallGraph.scala
+++ b/src/main/scala/leon/testgen/CallGraph.scala
@@ -111,9 +111,9 @@ class CallGraph(val program: Program) {
// callGraph += (startingPoint -> (transitions + ((newPoint, newTransition))))
// rec(e, List(), newPoint)
//}
- case IfExpr(cond, then, elze) => {
+ case IfExpr(cond, thenn, elze) => {
rec(cond, path, startingPoint)
- rec(then, cond :: path, startingPoint)
+ rec(thenn, cond :: path, startingPoint)
rec(elze, Not(cond) :: path, startingPoint)
}
case n@NAryOperator(args, _) => {
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 7073f68f74a67e211b2061e9cf3f29d0bc10d4d8..d8a716ba59bf1af731acab5418bd86937fa0316f 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -139,7 +139,7 @@ class TestGeneration(context : LeonContext) {
// var allPaths: Seq[Expr] = Seq()
// def rec(expr: Expr, path: List[Expr]): Seq[Expr] = expr match {
- // case IfExpr(cond, then, elze) => rec(then, cond :: path) ++ rec(elze, Not(cond) :: path)
+ // case IfExpr(cond, thenn, elze) => rec(thenn, cond :: path) ++ rec(elze, Not(cond) :: path)
// case _ => Seq(And(path.toSeq))
// }
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index d866afdb4ac00650b4783dc519353d79a12fa3e9..94f4526f3ce7ea7b4f0af707f3cb774efc41a5a5 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -206,9 +206,9 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
rec(e, path)
rec(b, Equals(Variable(i), e) :: path)
}
- case IfExpr(cond, then, elze) => {
+ case IfExpr(cond, thenn, elze) => {
rec(cond, path)
- rec(then, cond :: path)
+ rec(thenn, cond :: path)
rec(elze, Not(cond) :: path)
}
case NAryOperator(args, _) => args.foreach(rec(_, path))
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index 0feb5476c83f3b6858c0b11d60837038eca2198d..8ade819e42e3bbe1eb1ba8f6e9f40cafd67b8039 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/src/main/scala/leon/xlang/FunctionClosure.scala
@@ -109,14 +109,14 @@ object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef],
//pathConstraints = pathConstraints.tail
Let(i, re, rb).setType(l.getType)
}
- case i @ IfExpr(cond,then,elze) => {
+ case i @ IfExpr(cond,thenn,elze) => {
/*
when acumulating path constraints, take the condition without closing it first, so this
might not work well with nested fundef in if then else condition
*/
val rCond = functionClosure(cond, bindedVars, id2freshId, fd2FreshFd)
pathConstraints ::= cond//rCond
- val rThen = functionClosure(then, bindedVars, id2freshId, fd2FreshFd)
+ val rThen = functionClosure(thenn, bindedVars, id2freshId, fd2FreshFd)
pathConstraints = pathConstraints.tail
pathConstraints ::= Not(cond)//Not(rCond)
val rElze = functionClosure(elze, bindedVars, id2freshId, fd2FreshFd)
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 97313acf18bcc977a8aa06481b732c1195b87446..5560f97f093609aafdd4d831963b176ce295d1df 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -18,11 +18,7 @@ object Trees {
sb
}
- case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable with ScalaPrintable {
- //val t = last.getType
- //if(t != Untyped)
- // setType(t)
-
+ case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable with ScalaPrintable with FixedType {
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
val Block(args, rest) = this
Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
@@ -54,6 +50,8 @@ object Trees {
sb.append("}\n")
sb
}
+
+ val fixedType = last.getType
}
case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType with UnaryExtractable with PrettyPrintable with ScalaPrintable {
diff --git a/src/main/scala/leon/z3plugins/bapa/AST.scala b/src/main/scala/leon/z3plugins/bapa/AST.scala
index 6169a9f741617c3b546d63e3c9c3855cbb98b16f..499550f199338016de19764cb20d9537eea99357 100644
--- a/src/main/scala/leon/z3plugins/bapa/AST.scala
+++ b/src/main/scala/leon/z3plugins/bapa/AST.scala
@@ -2,6 +2,8 @@
package purescala.z3plugins.bapa
+import scala.language.implicitConversions
+
import z3.scala._
object AST {
@@ -24,7 +26,7 @@ object AST {
def seteq(tree: Tree) = Op(SETEQ, Seq(this, tree))
def subseteq(tree: Tree) = Op(SUBSETEQ, Seq(this, tree))
def +(tree: Tree) = Op(ADD, Seq(this, tree))
-// def ifThenElse(then: Tree, elze: Tree) = Op(ITE, Seq(this, then, elze))
+// def ifThenElse(thenn: Tree, elze: Tree) = Op(ITE, Seq(this, thenn, elze))
def card = Op(CARD, Seq(this))
def ++(tree: Tree) = Op(UNION, Seq(this, tree))
def **(tree: Tree) = Op(INTER, Seq(this, tree))
diff --git a/src/main/scala/leon/z3plugins/bapa/Bubbles.scala b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
index a60c99016a1a7f9cc35cd19177e321cee049d12e..34d17040a3b56a75bf8e0f5b12dbd1c8f4bbd0a2 100644
--- a/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
+++ b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
@@ -421,11 +421,11 @@ trait Bubbles {
def showState {
println("------------")
println("Bubbles :")
- allBubbles.values foreach {x => println(x toLongString)}
+ allBubbles.values foreach {x => println(x.toLongString)}
println
println("Edges :")
- allEdges.values foreach {x => println(x toLongString)}
+ allEdges.values foreach {x => println(x.toLongString)}
println
}
// */
@@ -705,7 +705,7 @@ trait Bubbles {
// nodeOrder foreach println
toModel(singletons(reconstruct))
} catch {
- case ex =>
+ case ex: Throwable =>
var err = ex.toString
if (errorVennRegion != null) err += "\nPossible cause :\n " + errorVennRegion
BAPAModel(z3model, Map.empty[Z3AST,Set[Int]], Set.empty[Z3AST], err)
@@ -741,7 +741,7 @@ case class BAPAModel(z3model: Z3Model, setModel: Map[Z3AST,Set[Int]], blacklist:
}
*/
// TODO: HACK ! (scalaZ3 interface has no model navigation yet)
- val badstart = blacklist map {_ toString}
+ val badstart = blacklist map {_.toString}
val lines = (z3model.toString split '\n').toList filterNot {line =>
badstart exists {line startsWith _}
}
diff --git a/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
index 9330832d8d24d2c4fb2d090acad843a8b33fb9c1..3c825a2fcece0db4f0bdda068e762a0714af5f60 100644
--- a/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
+++ b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
@@ -3,6 +3,8 @@
package purescala.z3plugins.bapa
import scala.text.{Document, DocBreak}
+import scala.language.implicitConversions
+
import Document._
import AST._
diff --git a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
index b3b8a2f90ebbf941b9ef9b73ebb839e3df1cbf99..edf0e170e145458c3d606232be1242e096fa641f 100644
--- a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
@@ -50,7 +50,7 @@ object ListOperations {
def sizesAreEquiv(l: List) : Boolean = {
size(l) == sizeTailRec(l)
- } holds
+ }.holds
def content(l: List) : Set[Int] = l match {
case Nil() => Set.empty[Int]
@@ -59,7 +59,7 @@ object ListOperations {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
- } holds
+ }.holds
def drunk(l : List) : List = (l match {
case Nil() => Nil()
@@ -78,19 +78,19 @@ object ListOperations {
}) ensuring(content(_) == content(l1) ++ content(l2))
@induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
+ def nilAppend(l : List) : Boolean = (append(l, Nil()) == l).holds
@induct
def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))).holds
def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
(append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
- } holds
+ }.holds
@induct
def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
+ (size(append(l1, l2)) == size(l1) + size(l2)).holds
@induct
def concat(l1: List, l2: List) : List =
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index 3018379ccd3bbc179305459524689fdb06996dc8..ec14ad7bb900e9cfa63212832d4de4b18207c926 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -66,23 +66,23 @@ object PropositionalLogic {
// @induct
// def wrongCommutative(f: Formula) : Boolean = {
// nnf(simplify(f)) == simplify(nnf(f))
- // } holds
+ // }.holds
@induct
def simplifyBreaksNNF(f: Formula) : Boolean = {
require(isNNF(f))
isNNF(simplify(f))
- } holds
+ }.holds
@induct
def nnfIsStable(f: Formula) : Boolean = {
require(isNNF(f))
nnf(f) == f
- } holds
+ }.holds
@induct
def simplifyIsStable(f: Formula) : Boolean = {
require(isSimplified(f))
simplify(f) == f
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Unit1.scala b/src/test/resources/regression/verification/purescala/invalid/Unit1.scala
index ed3d6fcd394be796169577860de048e2395d6bfa..21ba0863c1199116a1d5f5226292b381c0db8e6f 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Unit1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Unit1.scala
@@ -4,6 +4,6 @@ object Unit1 {
def foo(u: Unit): Unit = ({
u
- }) ensuring(_ != ())
+ }) ensuring(res => false)
}
diff --git a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
index 81979fa4d18b20f0c957fad851bdce15971ee820..1b264b2e5ac7be4d0fba2b75695b2956665a3ece 100644
--- a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
@@ -78,7 +78,7 @@ object AmortizedQueue {
// asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
// } else
// true
- // } holds
+ // }.holds
@induct
def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
@@ -89,7 +89,7 @@ object AmortizedQueue {
}
} else
true
- } holds
+ }.holds
@induct
def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
@@ -100,14 +100,14 @@ object AmortizedQueue {
}
} else
true
- } // holds
+ } //.holds
def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
if (isEmpty(queue))
front(enqueue(queue, elem)) == elem
else
true
- } holds
+ }.holds
def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
if (isEmpty(queue)) {
@@ -122,5 +122,5 @@ object AmortizedQueue {
e1 == e1prime && e2 == e2prime && e3 == e3prime
} else
true
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
index ad450a93c81a006986ebd20b7f2a47cb761c0450..dd7516b20f9f11435bf047d7d58b4c4f9d0e692e 100644
--- a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
@@ -48,5 +48,5 @@ object AssociativeList {
@induct
def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala b/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
index c68eb99b23affb0a41537f38fd50460cb2ccdba6..449bba2f192833807566fe54784110aa71548868 100644
--- a/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
@@ -23,5 +23,5 @@ object BestRealTypes {
def somethingToProve(b : Boolean) : Boolean = {
val (z1,z2) = zipWrap(Wrapper(boolToNum(b)), Wrapper(boolToNum(!b)))
z1.num == Zero() || z2.num == Zero()
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
index 9f0b8da37fdab144679b9cce226a4a55b2784afd..178d9a523d71484b0e667e8c66f4ba06ab1152b2 100644
--- a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
@@ -50,7 +50,7 @@ object ListOperations {
def sizesAreEquiv(l: List) : Boolean = {
size(l) == sizeTailRec(l)
- } holds
+ }.holds
def content(l: List) : Set[Int] = l match {
case Nil() => Set.empty[Int]
@@ -59,7 +59,7 @@ object ListOperations {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
- } holds
+ }.holds
def drunk(l : List) : List = (l match {
case Nil() => Nil()
@@ -78,15 +78,15 @@ object ListOperations {
}) ensuring(content(_) == content(l1) ++ content(l2))
@induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
+ def nilAppend(l : List) : Boolean = (append(l, Nil()) == l).holds
@induct
def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))).holds
@induct
def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
+ (size(append(l1, l2)) == size(l1) + size(l2)).holds
@induct
def concat(l1: List, l2: List) : List =
diff --git a/src/test/resources/regression/verification/purescala/valid/MyMap.scala b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
index 5d039ff9463c7e01c107366820551098a7203ad3..7b75661126d4452b26387a009ba71236990ec378 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyMap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
@@ -13,6 +13,6 @@ object MyMap {
val m1 = Map[Int, Int]()
val m2 = Map.empty[Int, Int]
m1 == m2
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/MySet.scala b/src/test/resources/regression/verification/purescala/valid/MySet.scala
index 5be8bb6e76cdda433eae19d9bfca52969c62b17c..8f1b482ffbf28c0076f5265c016773140e73dbf8 100644
--- a/src/test/resources/regression/verification/purescala/valid/MySet.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MySet.scala
@@ -7,12 +7,12 @@ object MySet {
def set1(): Boolean = {
val s = Set(1, 2, 3, 4)
s.contains(3)
- } holds
+ }.holds
def set2(): Boolean = {
val s1 = Set[Int]()
val s2 = Set.empty[Int]
s1 == s2
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
index 60c1ef7a2fd62dd7e24c9c5c63a26e12820f813c..25b842f6c7ea194bfe8201d43384ca2690010917 100644
--- a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
@@ -67,11 +67,11 @@ object PropositionalLogic {
def nnfIsStable(f: Formula) : Boolean = {
require(isNNF(f))
nnf(f) == f
- } holds
+ }.holds
@induct
def simplifyIsStable(f: Formula) : Boolean = {
require(isSimplified(f))
simplify(f) == f
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
index 64230dbd7ca744bff5cf55c554c7f5ce698aaff1..44d5550c1a0286c63c0f7a5f38f597f985285166 100644
--- a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
@@ -46,5 +46,5 @@ object SearchLinkedList {
} else {
true
}
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
index 629dc6dba22584f8413b7b32ab0457713008f54d..555f80f0a7bf9814a65a3c6ce3f5d1f1433cfaea 100644
--- a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
@@ -37,12 +37,12 @@ object SumAndMax {
def prop0(list : List) : Boolean = {
require(list != Nil())
!allPos(list) || max(list) >= 0
- } holds
+ }.holds
@induct
def property(list : List) : Boolean = {
// This precondition was given in the problem but isn't actually useful :D
// require(allPos(list))
sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Unit1.scala b/src/test/resources/regression/verification/purescala/valid/Unit1.scala
index 0f4d78ae9d2d0e84ac5a3aa5f88089f921ded61a..cfcbba76ff8a6372a8bb6b839d3c8f6df76223f9 100644
--- a/src/test/resources/regression/verification/purescala/valid/Unit1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Unit1.scala
@@ -4,6 +4,6 @@ object Unit1 {
def foo(): Unit = ({
()
- }) ensuring(_ == ())
+ }) ensuring(r => true)
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Unit2.scala b/src/test/resources/regression/verification/purescala/valid/Unit2.scala
index 08c96fc22ef7b3c6bb731930d4cae179ed3db3cc..1f09609d04b65b3a38e32a673ff91c8cfb2d06cc 100644
--- a/src/test/resources/regression/verification/purescala/valid/Unit2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Unit2.scala
@@ -4,6 +4,6 @@ object Unit2 {
def foo(u: Unit): Unit = {
u
- } ensuring(_ == ())
+ } ensuring(res => true)
}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
index 51d72f9614baeea05681632fe43e57a214d0f594..48cc02793a635154563ba1546b2623f14b4f1ed2 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
@@ -9,6 +9,6 @@ object Epsilon1 {
//this should not hold
def property2(x: Int): Boolean = {
rand2(x) == rand2(x+1)
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
index 7ed458cefb9dbdc7f5909a9fe6e703c6556da9a4..f5f0d6be05a34af38f2d558489b34dc8b8b9ab71 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
@@ -9,5 +9,5 @@ object Epsilon1 {
//this should not hold
def property3(x: Int): Boolean = {
rand3(x) == rand3(x+1)
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
index 72cb25fc16f65bbe2aa7c2f485588e2a28b71f83..92cd1d75843217a1c026c0ca191ccf588fcb38ad 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
@@ -24,6 +24,6 @@ object Epsilon4 {
}
- def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
- //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+ def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)).holds
+ //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst).holds
}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
index 77315ca2f0ea326082a5b01feefb3cebce824f67..794c4f0708052adef0ffed9e34f1b5f0561dad15 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
@@ -9,7 +9,7 @@ object Epsilon1 {
//this should hold, that is the expected semantic of our epsilon
def property1(): Boolean = {
rand() == rand()
- } holds
+ }.holds
}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
index 14fabbeb2c81c6f9ff816649a2876944ea20fc91..cbe5498b4e89dc90c80bd7e716e0cd32abe621c6 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
@@ -24,11 +24,11 @@ object Epsilon4 {
}
//timeout, but this probably means that it is valid as expected
- //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+ //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)).holds
def propertyBase(lst: MyList): Boolean = ({
require(lst match { case MyNil() => true case _ => false})
size(toList(toSet(lst))) <= size(lst)
- }) holds
+ }).holds
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 27ba891159ebf47e3b0aacbdeddcd354fc9facc9..6cd6d9a88c96915eb1c2c7e90d1ef34209e5dd01 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -41,7 +41,7 @@ class EvaluatorsTests extends FunSuite {
val warningsBefore = leonContext.reporter.warningCount
val program = pipeline.run(leonContext)((str, Nil))
-
+
assert(leonContext.reporter.errorCount === errorsBefore)
assert(leonContext.reporter.warningCount === warningsBefore)
@@ -316,7 +316,7 @@ class EvaluatorsTests extends FunSuite {
| def finite() : Set[Int] = Set(1, 2, 3)
| def build(x : Int, y : Int, z : Int) : Set[Int] = Set(x, y, z)
| def union(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 ++ s2
- | def inter(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 ** s2
+ | def inter(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 & s2
| def diff(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 -- s2
|}""".stripMargin
diff --git a/unmanaged/32/cafebabe_2.10-1.2.jar b/unmanaged/32/cafebabe_2.10-1.2.jar
new file mode 120000
index 0000000000000000000000000000000000000000..37f428a8b2941987bdc522bac7e2fa90c0f37467
--- /dev/null
+++ b/unmanaged/32/cafebabe_2.10-1.2.jar
@@ -0,0 +1 @@
+../common/cafebabe_2.10-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/32/cafebabe_2.9.2-1.2.jar b/unmanaged/32/cafebabe_2.9.2-1.2.jar
deleted file mode 120000
index 2ccd5ee86a0781d0ad57ccc10ccafc9ef3b022bd..0000000000000000000000000000000000000000
--- a/unmanaged/32/cafebabe_2.9.2-1.2.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/cafebabe_2.9.2-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/64/cafebabe_2.10-1.2.jar b/unmanaged/64/cafebabe_2.10-1.2.jar
new file mode 120000
index 0000000000000000000000000000000000000000..37f428a8b2941987bdc522bac7e2fa90c0f37467
--- /dev/null
+++ b/unmanaged/64/cafebabe_2.10-1.2.jar
@@ -0,0 +1 @@
+../common/cafebabe_2.10-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/64/cafebabe_2.9.2-1.2.jar b/unmanaged/64/cafebabe_2.9.2-1.2.jar
deleted file mode 120000
index 2ccd5ee86a0781d0ad57ccc10ccafc9ef3b022bd..0000000000000000000000000000000000000000
--- a/unmanaged/64/cafebabe_2.9.2-1.2.jar
+++ /dev/null
@@ -1 +0,0 @@
-../common/cafebabe_2.9.2-1.2.jar
\ No newline at end of file
diff --git a/unmanaged/64/scalaz3.jar b/unmanaged/64/scalaz3.jar
deleted file mode 100644
index 1584e21c3ba8bc285dc862f63dafa6bee148642a..0000000000000000000000000000000000000000
Binary files a/unmanaged/64/scalaz3.jar and /dev/null differ
diff --git a/unmanaged/64/scalaz3_2.10-2.0.jar b/unmanaged/64/scalaz3_2.10-2.0.jar
new file mode 120000
index 0000000000000000000000000000000000000000..304102e51a192b3df47da9f705429736afc3c474
--- /dev/null
+++ b/unmanaged/64/scalaz3_2.10-2.0.jar
@@ -0,0 +1 @@
+/home/ekneuss/git/ScalaZ3/target/scala-2.10/scalaz3_2.10-2.0.jar
\ No newline at end of file
diff --git a/unmanaged/common/cafebabe_2.10-1.2.jar b/unmanaged/common/cafebabe_2.10-1.2.jar
new file mode 100644
index 0000000000000000000000000000000000000000..4dc1806689a5932ddc8097afe769df62f2d5ffbb
Binary files /dev/null and b/unmanaged/common/cafebabe_2.10-1.2.jar differ
diff --git a/unmanaged/common/cafebabe_2.9.2-1.2.jar b/unmanaged/common/cafebabe_2.9.2-1.2.jar
deleted file mode 100644
index 7fdd2eae06df631006abc992f29847c84198f9a4..0000000000000000000000000000000000000000
Binary files a/unmanaged/common/cafebabe_2.9.2-1.2.jar and /dev/null differ