diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3a23a33e4557e9dbebba578bdfc689342c589abb..58386b84906b5371fe09e455f3cb1a0f60292d16 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -8,7 +8,7 @@ object Main {
lazy val allPhases: List[LeonPhase[_, _]] = {
List(
- plugin.ExtractionPhase,
+ frontends.scalac.ExtractionPhase,
SubtypingPhase,
xlang.ArrayTransformation,
xlang.EpsilonElimination,
@@ -187,7 +187,7 @@ object Main {
def computePipeline(settings: Settings): Pipeline[List[String], Any] = {
import purescala.Definitions.Program
- val pipeBegin : Pipeline[List[String],Program] = plugin.ExtractionPhase andThen SubtypingPhase
+ val pipeBegin : Pipeline[List[String],Program] = frontends.scalac.ExtractionPhase andThen SubtypingPhase
val pipeProcess: Pipeline[Program, Any] =
if (settings.synthesis) {
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
similarity index 99%
rename from src/main/scala/leon/plugin/Extractors.scala
rename to src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 8735654d7813bf2e86777a5964400638977a4f1c..2083d0e36e7eb1eedad58b544c6fcdfbac4dfc45 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -1,12 +1,12 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package frontends.scalac
import scala.tools.nsc._
/** Contains extractors to pull-out interesting parts of the Scala ASTs. */
-trait Extractors {
+trait ASTExtractors {
val global: Global
import global._
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
similarity index 98%
rename from src/main/scala/leon/plugin/CodeExtraction.scala
rename to src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0bb34ac382ac4c30127e924e50547fe18a96b09c..2fe5da3f4220a8d785621edc98dc88989c70480d 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package frontends.scalac
import scala.tools.nsc._
import scala.tools.nsc.plugins._
@@ -11,15 +11,15 @@ import scala.language.implicitConversions
import purescala._
import purescala.Definitions._
import purescala.Trees.{Expr => LeonExpr, _}
-import xlang.Trees.{Block => LeonBlock, _}
-import xlang.TreeOps._
import purescala.TypeTrees.{TypeTree => LeonType, _}
import purescala.Common._
import purescala.TreeOps._
+import xlang.Trees.{Block => LeonBlock, _}
+import xlang.TreeOps._
-import utils.{Position => LeonPosition, OffsetPosition => LeonOffsetPosition}
+import utils.{Position => LeonPosition, OffsetPosition => LeonOffsetPosition, RangePosition => LeonRangePosition}
-trait CodeExtraction extends Extractors {
+trait CodeExtraction extends ASTExtractors {
self: LeonExtraction =>
import global._
@@ -29,7 +29,13 @@ trait CodeExtraction extends Extractors {
import ExtractorHelpers._
implicit def scalaPosToLeonPos(p: global.Position): LeonPosition = {
- LeonOffsetPosition(p.line, p.column, null)
+ if (p.isRange) {
+ val start = p.focusStart
+ val end = p.focusEnd
+ LeonRangePosition(start.line, start.column, end.line, end.column, p.source.file.file)
+ } else {
+ LeonOffsetPosition(p.line, p.column, p.source.file.file)
+ }
}
private val mutableVarSubsts: scala.collection.mutable.Map[Symbol,Function0[LeonExpr]] =
diff --git a/src/main/scala/leon/plugin/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
similarity index 96%
rename from src/main/scala/leon/plugin/ExtractionPhase.scala
rename to src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index b81c951303aadd4ae8be6ef0fdbe72a85cc6f8d6..9822ef4db1fe2e31cdc257a7de8d19f7db161db7 100644
--- a/src/main/scala/leon/plugin/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package frontends.scalac
import purescala.Definitions.Program
@@ -9,7 +9,7 @@ import scala.tools.nsc.{Settings=>NSCSettings,CompilerCommand}
object ExtractionPhase extends LeonPhase[List[String], Program] {
- val name = "Extraction"
+ val name = "Scalc Extraction"
val description = "Extraction of trees from the Scala Compiler"
def run(ctx: LeonContext)(args: List[String]): Program = {
diff --git a/src/main/scala/leon/plugin/LeonExtraction.scala b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
similarity index 95%
rename from src/main/scala/leon/plugin/LeonExtraction.scala
rename to src/main/scala/leon/frontends/scalac/LeonExtraction.scala
index a2f00340e9026225e35b9e6d9f800ecd2563e735..f6574fa998a80ce08565fad23a2a4c0f3f5adcb3 100644
--- a/src/main/scala/leon/plugin/LeonExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package frontends.scalac
import scala.tools.nsc._
import scala.tools.nsc.plugins._
diff --git a/src/main/scala/leon/plugin/ScalaCompiler.scala b/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
similarity index 98%
rename from src/main/scala/leon/plugin/ScalaCompiler.scala
rename to src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
index 489404d02ec5a1e3428b4e68907bc9623e9cf64b..2eea722374ffd0804903fcaed7fd9511eac6062f 100644
--- a/src/main/scala/leon/plugin/ScalaCompiler.scala
+++ b/src/main/scala/leon/frontends/scalac/ScalaCompiler.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package frontends.scalac
import scala.tools.nsc.{Global,Settings=>NSCSettings}
diff --git a/src/main/scala/leon/plugin/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
similarity index 99%
rename from src/main/scala/leon/plugin/SimpleReporter.scala
rename to src/main/scala/leon/frontends/scalac/SimpleReporter.scala
index 9057afeaf1ffa317b72c25292c58c9f56bf32260..b31cd91bb2063bfe1a34f9c88bff007faa9cbe38 100644
--- a/src/main/scala/leon/plugin/SimpleReporter.scala
+++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package frontends.scalac
import scala.tools.nsc.Settings
import scala.tools.nsc.reporters.AbstractReporter
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
deleted file mode 100644
index 55756ad45fcb69cee43293b5719bb056853ec4ac..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ /dev/null
@@ -1,149 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon.synthesis.utils
-
-import leon._
-import leon.utils._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.synthesis._
-
-import java.util.Date
-import java.text.SimpleDateFormat
-
-import sys.process._
-
-import java.io.File
-
-object Benchmarks extends App {
-
- val allRules = Rules.all ++ Heuristics.all
-
- var rule: Rule = rules.CEGIS
-
- // Parse arguments
- val (options, others) = args.partition(_.startsWith("--"))
-
- val newOptions = options flatMap {
- case setting if setting.startsWith("--rule=") =>
- val name = setting.drop(7)
-
- allRules.find(_.name.toLowerCase == name.toLowerCase) match {
- case Some(r) =>
- rule = r
- case None =>
- println("Could not find rule: "+name)
- println("Available rules: ")
- for (r <- allRules) {
- println(" - "+r.name)
- }
- sys.exit(1);
- }
-
- None
-
- case setting =>
- Some(setting)
- }
-
- println("# Date: "+new SimpleDateFormat("dd.MM.yyyy HH:mm:ss").format(new Date()))
- println("# Git tree: "+("git log -1 --format=\"%H\"".!!).trim)
- println("# Using rule: "+rule.name)
-
-
- val infoSep : String = "╟" + ("┄" * 100) + "╢"
- val infoFooter : String = "â•š" + ("â•" * 100) + "â•"
- val infoHeader : String = " ┌────────────â”\n" +
- "â•”â•â•¡ Benchmarks â•ž" + ("â•" * 85) + "â•—\n" +
- "║ └────────────┘" + (" " * 85) + "║"
-
- val runtime = Runtime.getRuntime()
-
- def infoLine(file: String, f: String, ts: Long, nAlt: Int, nSuccess: Int, nInnap: Int, nDecomp: Int) : String = {
- "â•‘ %-30s %-24s %3d %10s %10s ms %10d Mb â•‘".format(
- file,
- f,
- nAlt,
- nSuccess+"/"+nInnap+"/"+nDecomp,
- ts,
- (runtime.totalMemory()-runtime.freeMemory())/(1024*1024))
- }
-
- println(infoHeader)
-
- var nSuccessTotal, nInnapTotal, nDecompTotal, nAltTotal = 0
- var tTotal: Long = 0
-
- val ctx = leon.Main.processOptions(others ++ newOptions)
-
- for (file <- ctx.files) {
- Thread.sleep(10*1000);
-
- val innerCtx = ctx.copy(files = List(file))
-
- val opts = SynthesisOptions()
-
- val pipeline = leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
-
- val (program, results) = pipeline.run(innerCtx)(file.getPath :: Nil)
-
-
- for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
- val sctx = SynthesisContext(
- context = ctx,
- options = opts,
- functionContext = Some(f),
- program = program,
- reporter = ctx.reporter
- )
-
- val ts = System.currentTimeMillis
-
- val rr = rule.instantiateOn(sctx, p)
-
- val nAlt = rr.size
- var nSuccess, nInnap, nDecomp = 0
-
- for (alt <- rr) {
- alt.apply(sctx) match {
- case RuleApplicationImpossible =>
- nInnap += 1
- case s: RuleDecomposed =>
- nDecomp += 1
- case s: RuleSuccess =>
- nSuccess += 1
- }
- }
-
- val t = System.currentTimeMillis - ts
-
- nAltTotal += nAlt
- tTotal += t
- nSuccessTotal += nSuccess
- nInnapTotal += nInnap
- nDecompTotal += nDecomp
-
- println(infoLine(file.getName().toString, f.id.toString, t, nAlt, nSuccess, nInnap, nDecomp))
- }
-
- println(infoSep)
-
- }
-
- println(infoLine("TOTAL", "", tTotal, nAltTotal, nSuccessTotal, nInnapTotal, nDecompTotal))
-
- println(infoFooter)
-
- println
-
- //val infoHeader2 : String = " ┌────────────â”\n" +
- // "â•”â•â•¡ Timers â•ž" + ("â•" * 71) + "â•—\n" +
- // "║ └────────────┘" + (" " * 71) + "║"
-
- //println(infoHeader2)
- //for ((name, sw) <- TimerCollections.getAll.toSeq.sortBy(_._1)) {
- // println("â•‘ %-70s %10s ms â•‘".format(name, sw.getMillis))
- //}
- //println(infoFooter)
-}
diff --git a/src/main/scala/leon/plugin/TemporaryInputPhase.scala b/src/main/scala/leon/utils/TemporaryInputPhase.scala
similarity index 86%
rename from src/main/scala/leon/plugin/TemporaryInputPhase.scala
rename to src/main/scala/leon/utils/TemporaryInputPhase.scala
index 88717785c466aec2d3505130a4c8e5ca323941b4..216f46dd223937b4feca247a8806eba7267a6b72 100644
--- a/src/main/scala/leon/plugin/TemporaryInputPhase.scala
+++ b/src/main/scala/leon/utils/TemporaryInputPhase.scala
@@ -1,14 +1,14 @@
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
-package plugin
+package utils
import java.io.{File, BufferedWriter, FileWriter}
object TemporaryInputPhase extends LeonPhase[(String, List[String]), List[String]] {
val name = "Temporary Input"
- val description = "Feed the compiler with a temporary input file"
+ val description = "Create source files from string content"
def run(ctx: LeonContext)(data: (String, List[String])): List[String] = {
val (content, opts) = data