From 002d96438792b877c0e903e19d95d5a3efa4e4a2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 2 Dec 2013 16:00:28 +0100
Subject: [PATCH] Remove confusing plugin package, move to frontends.scalac
---
src/main/scala/leon/Main.scala | 4 +-
.../scalac/ASTExtractors.scala} | 4 +-
.../scalac}/CodeExtraction.scala | 18 ++-
.../scalac}/ExtractionPhase.scala | 4 +-
.../scalac}/LeonExtraction.scala | 2 +-
.../scalac}/ScalaCompiler.scala | 2 +-
.../scalac}/SimpleReporter.scala | 2 +-
.../leon/synthesis/utils/Benchmarks.scala | 149 ------------------
.../TemporaryInputPhase.scala | 4 +-
9 files changed, 23 insertions(+), 166 deletions(-)
rename src/main/scala/leon/{plugin/Extractors.scala => frontends/scalac/ASTExtractors.scala} (99%)
rename src/main/scala/leon/{plugin => frontends/scalac}/CodeExtraction.scala (98%)
rename src/main/scala/leon/{plugin => frontends/scalac}/ExtractionPhase.scala (96%)
rename src/main/scala/leon/{plugin => frontends/scalac}/LeonExtraction.scala (95%)
rename src/main/scala/leon/{plugin => frontends/scalac}/ScalaCompiler.scala (98%)
rename src/main/scala/leon/{plugin => frontends/scalac}/SimpleReporter.scala (99%)
delete mode 100644 src/main/scala/leon/synthesis/utils/Benchmarks.scala
rename src/main/scala/leon/{plugin => utils}/TemporaryInputPhase.scala (86%)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3a23a33e4..58386b849 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 8735654d7..2083d0e36 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 0bb34ac38..2fe5da3f4 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 b81c95130..9822ef4db 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 a2f00340e..f6574fa99 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 489404d02..2eea72237 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 9057afeaf..b31cd91bb 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 55756ad45..000000000
--- 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 88717785c..216f46dd2 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
--
GitLab