diff --git a/PERMISSIONS b/PERMISSIONS
index cfb16377c7bc961ddb3d8d433ab9e746c44b8772..b7955144e43d584b2d7b9812e5f8c76a935c3ce7 100755
--- a/PERMISSIONS
+++ b/PERMISSIONS
@@ -12,5 +12,5 @@ tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}
exit $_
# **Do not** add new lines after the following two!
-WRITERS kuncak psuter rblanc edarulov hojjat ekneuss kandhada
+WRITERS kuncak psuter rblanc edarulov hojjat ekneuss kandhada kuraj gvero
READERS @lara mazimmer hardy amin
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 2ba7a69ad7aa69be4b49d0cdd7b395dfa2bf6c34..ce98c70aaa2552f4506fd94610668c082aa56c71 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -328,11 +328,11 @@ object Analysis {
}
}
-object AnalysisPhase extends plugin.UnitPhase {
+object AnalysisPhase extends UnitPhase[Program] {
val name = "Analysis"
val description = "Leon Analyses"
- def apply(program: Program) {
+ def apply(ctx: LeonContext, program: Program) {
new Analysis(program).analyse
}
}
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 0dab758176b2b3381eaed88c67415d95d5cd8df3..9d0403039b767571a4ae23a6d9ffc0c29ef7e28b 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -5,12 +5,12 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object ArrayTransformation extends plugin.TransformationPhase {
+object ArrayTransformation extends TransformationPhase {
val name = "Array Transformation"
val description = "Add bound checking for array access and remove array update with side effect"
- def apply(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
diff --git a/src/main/scala/leon/EpsilonElimination.scala b/src/main/scala/leon/EpsilonElimination.scala
index 5cc7645d54e99c6480f09dcfd16b46e01e4a0713..a785ddf9e6710ec7c6ace7dda0c2f223c9a88eb1 100644
--- a/src/main/scala/leon/EpsilonElimination.scala
+++ b/src/main/scala/leon/EpsilonElimination.scala
@@ -5,12 +5,12 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object EpsilonElimination extends plugin.TransformationPhase {
+object EpsilonElimination extends TransformationPhase {
val name = "Epsilon Elimination"
val description = "Remove all epsilons from the program"
- def apply(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 64c0c123f7d1c289e6b59a0bbe13ddd6390f5ae4..ed5920185c0940375fc0a270e9f13204830bebc3 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object FunctionClosure extends plugin.TransformationPhase{
+object FunctionClosure extends TransformationPhase{
val name = "Function Closure"
val description = "Closing function with its scoping variables"
@@ -15,7 +15,7 @@ object FunctionClosure extends plugin.TransformationPhase{
private var newFunDefs: Map[FunDef, FunDef] = Map()
private var topLevelFuns: Set[FunDef] = Set()
- def apply(program: Program): Program = {
+ def apply(ctx: LeonContext, program: Program): Program = {
newFunDefs = Map()
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
index e467f3f20eb0c414936a3584001285fdc24d9eba..d0fd3f83f80499b4986a986ff1fcfeee60ee2378 100644
--- a/src/main/scala/leon/FunctionHoisting.scala
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -5,12 +5,12 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object FunctionHoisting extends plugin.TransformationPhase {
+object FunctionHoisting extends TransformationPhase {
val name = "Function Hoisting"
val description = "Hoist function at the top level"
- def apply(program: Program): Program = {
+ def apply(ctx: LeonContext, program: Program): Program = {
val funDefs = program.definedFunctions
var topLevelFuns: Set[FunDef] = Set()
funDefs.foreach(fd => {
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index bb770ba8e15eede296321707f58bcf4460404a98..18243ea6ba735ec73b402003ac0fefbfa63c061e 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object ImperativeCodeElimination extends plugin.TransformationPhase {
+object ImperativeCodeElimination extends TransformationPhase {
val name = "Imperative Code Elimination"
val description = "Transform imperative constructs into purely functional code"
@@ -13,7 +13,7 @@ object ImperativeCodeElimination extends plugin.TransformationPhase {
private var varInScope = Set[Identifier]()
private var parent: FunDef = null //the enclosing fundef
- def apply(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
parent = fd
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9037c5f9e7da0f7d2e9fbb97e1cc6df11bde2195
--- /dev/null
+++ b/src/main/scala/leon/LeonContext.scala
@@ -0,0 +1,9 @@
+package leon
+
+import purescala.Definitions.Program
+
+case class LeonContext(
+ val settings: Settings = Settings(),
+ val reporter: Reporter = new DefaultReporter
+)
+
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2579e5aff59113c1a1ae0d3484278532bc9fd18
--- /dev/null
+++ b/src/main/scala/leon/LeonOption.scala
@@ -0,0 +1,13 @@
+package leon
+
+sealed abstract class LeonOption {
+ val name: String
+}
+
+case class LeonFlagOption(name: String) extends LeonOption
+case class LeonValueOption(name: String, value: String) extends LeonOption {
+
+ def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
+}
+
+case class LeonOptionDef(name: String, isFlag: Boolean, description: String)
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d81b8eea718d40639c0ff5edce6bdc57c0837f83
--- /dev/null
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -0,0 +1,41 @@
+package leon
+
+import purescala.Definitions.Program
+
+abstract class LeonPhase[F, T] {
+ val name: String
+ val description: String
+
+ def definedOptions: Set[LeonOptionDef] = Set()
+
+ def run(ac: LeonContext)(v: F): T
+}
+
+abstract class TransformationPhase extends LeonPhase[Program, Program] {
+ def apply(ctx: LeonContext, p: Program): Program
+
+ override def run(ctx: LeonContext)(p: Program) = {
+ apply(ctx, p)
+ }
+}
+
+abstract class UnitPhase[Program] extends LeonPhase[Program, Program] {
+ def apply(ctx: LeonContext, p: Program): Unit
+
+ override def run(ctx: LeonContext)(p: Program) = {
+ apply(ctx, p)
+ p
+ }
+}
+
+case class NoopPhase[T]() extends LeonPhase[T, T] {
+ val name = "noop";
+ val description = "no-op"
+ override def run(ctx: LeonContext)(v: T) = v
+}
+
+case class ExitPhase[T]() extends LeonPhase[T, Unit] {
+ val name = "end";
+ val description = "end"
+ override def run(ctx: LeonContext)(v: T) = ()
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 760e5c5de0a994f450c2d6190e9ce89624d79fac..013ae1cf5ce21156271ad66f6482a2716c125e88 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -1,75 +1,119 @@
package leon
-import scala.tools.nsc.{Global,Settings=>NSCSettings,SubComponent,CompilerCommand}
+object Main {
+
+ def allPhases: List[LeonPhase[_, _]] = {
+ List(
+ plugin.ExtractionPhase,
+ ArrayTransformation,
+ EpsilonElimination,
+ ImperativeCodeElimination,
+ /*UnitElimination,*/
+ FunctionClosure,
+ /*FunctionHoisting,*/
+ Simplificator,
+ synthesis.SynthesisPhase,
+ AnalysisPhase
+ )
+ }
-import purescala.Definitions.Program
+ def processOptions(reporter: Reporter, args: List[String]) = {
+ val phases = allPhases
-object Main {
- import leon.{Reporter,DefaultReporter,Analysis}
-
- def main(args : Array[String]) : Unit = run(args)
-
- def runFromString(program : String, args : Array[String], reporter : Reporter = new DefaultReporter, classPath : Option[Seq[String]] = None) : Unit = {
- import java.io.{BufferedWriter,File,FileWriter,IOException}
-
- try {
- val file : File = File.createTempFile("leon", ".scala")
- file.deleteOnExit
- val out = new BufferedWriter(new FileWriter(file))
- out.write(program)
- out.close
- run(file.getPath.toString +: args, reporter, classPath)
- } catch {
- case e : IOException => reporter.error(e.getMessage)
+ val allOptions = allPhases.flatMap(_.definedOptions) ++ Set(
+ LeonOptionDef("synthesis", true, "--synthesis Magic!"),
+ LeonOptionDef("xlang", true, "--xlang Preprocessing and transformation from extended programs")
+ )
+
+ val allOptionsMap = allOptions.map(o => o.name -> o).toMap
+
+ // Detect unknown options:
+ val options = args.filter(_.startsWith("--"))
+
+ val leonOptions = options.flatMap { opt =>
+ val leonOpt: LeonOption = opt.substring(2, opt.length).split("=", 2).toList match {
+ case List(name, value) =>
+ LeonValueOption(name, value)
+ case List(name) => name
+ LeonFlagOption(name)
+ case _ =>
+ reporter.fatalError("Woot?")
+ }
+
+ if (allOptionsMap contains leonOpt.name) {
+ (allOptionsMap(leonOpt.name).isFlag, leonOpt) match {
+ case (true, LeonFlagOption(name)) =>
+ Some(leonOpt)
+ case (false, LeonValueOption(name, value)) =>
+ Some(leonOpt)
+ case _ =>
+ reporter.fatalError("Invalid option usage")
+ None
+ }
+ } else {
+ None
+ }
}
- }
- def run(args: Array[String], reporter: Reporter = new DefaultReporter, classPath : Option[Seq[String]] = None) : Unit = {
- val settings = new NSCSettings
- classPath.foreach(s => settings.classpath.tryToSet(s.toList))
+ var settings = Settings()
- val (leonOptions, nonLeonOptions) = args.toList.partition(_.startsWith("--"))
- val command = new CompilerCommand(nonLeonOptions, settings) {
- override val cmdName = "leon"
+ // Process options we understand:
+ for(opt <- leonOptions) opt match {
+ case LeonFlagOption("synthesis") =>
+ settings = settings.copy(synthesis = true, xlang = false, analyze = false)
+ case LeonFlagOption("xlang") =>
+ settings = settings.copy(synthesis = false, xlang = true)
+ case _ =>
}
- if(command.ok) {
- if(settings.version.value) {
- println(command.cmdName + " beta.")
+ LeonContext(settings = settings, reporter = reporter)
+ }
+
+ implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
+
+ def computePipeLine(settings: Settings): Pipeline[List[String], Unit] = {
+ import purescala.Definitions.Program
+
+ val pipeBegin = phaseToPipeline(plugin.ExtractionPhase)
+
+ val pipeTransforms: Pipeline[Program, Program] =
+ if (settings.xlang) {
+ ArrayTransformation andThen
+ EpsilonElimination andThen
+ ImperativeCodeElimination
} else {
- val runner = new PluginRunner(settings, reporter)
- runner.leonPlugin.processOptions(leonOptions.map(_.substring(2)), reporter.error(_))
+ NoopPhase[Program]()
+ }
- val run = new runner.Run
- run.compile(command.files)
+ val pipeSynthesis: Pipeline[Program, Program] =
+ if (settings.synthesis) {
+ synthesis.SynthesisPhase
+ } else {
+ NoopPhase[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, reporter : Reporter) extends Global(settings, new plugin.SimpleReporter(settings, reporter)) {
- val leonPlugin = new plugin.LeonPlugin(this, reporter)
+ val pipeAnalysis: Pipeline[Program, Program] =
+ if (settings.analyze) {
+ AnalysisPhase
+ } else {
+ NoopPhase[Program]()
+ }
- protected def myAddToPhasesSet(sub : SubComponent, descr : String) : Unit = {
- phasesSet += sub
+ pipeBegin followedBy
+ pipeTransforms followedBy
+ pipeSynthesis followedBy
+ pipeAnalysis andThen
+ ExitPhase()
}
- /** 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
+ def main(args : Array[String]) : Unit = {
+ val reporter = new DefaultReporter()
+
+ // Process options
+ val ctx = processOptions(reporter, args.toList)
+
+ val pipeline = computePipeLine(ctx.settings)
+
+ pipeline.run(ctx)(args.toList)
}
}
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
new file mode 100644
index 0000000000000000000000000000000000000000..477a08c31250ba1996ddccd59262631fe75499c1
--- /dev/null
+++ b/src/main/scala/leon/Pipeline.scala
@@ -0,0 +1,26 @@
+package leon
+
+abstract class Pipeline[F, T] {
+ def andThen[G](then: LeonPhase[T, G]): Pipeline[F, G];
+ def followedBy[G](pipe: Pipeline[T, G]): Pipeline[F, G];
+ def run(ctx: LeonContext)(v: F): T;
+}
+
+class PipeCons[F, V, T](phase: LeonPhase[F, V], then: Pipeline[V, T]) extends Pipeline[F, T] {
+ def andThen[G](last: LeonPhase[T, G]) = new PipeCons(phase, then andThen last)
+ def followedBy[G](pipe: Pipeline[T, G]) = new PipeCons(phase, then followedBy pipe);
+ def run(ctx: LeonContext)(v: F): T = then.run(ctx)(phase.run(ctx)(v))
+
+ override def toString = {
+ phase.toString + " -> " + then.toString
+ }
+}
+
+class PipeNil[T]() extends Pipeline[T,T] {
+ def andThen[G](last: LeonPhase[T, G]) = new PipeCons(last, new PipeNil)
+ def run(ctx: LeonContext)(v: T): T = v
+ def followedBy[G](pipe: Pipeline[T, G]) = pipe;
+ override def toString = {
+ "|"
+ }
+}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 4c15d2cbea3ad72442aca4a42b12c39eebaa285d..c57a1e4514b00372033c7e19242b7782e40b8c56 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -34,3 +34,9 @@ object Settings {
var stopAfterAnalysis: Boolean = true
var silentlyTolerateNonPureBodies: Boolean = false
}
+
+case class Settings(
+ val synthesis: Boolean = false,
+ val xlang: Boolean = false,
+ val analyze: Boolean = true
+)
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
index c9de13922b3a93ee8e9055046dfcf020bd64c74e..92b54072a1d89e176f64225225789161a25870af 100644
--- a/src/main/scala/leon/Simplificator.scala
+++ b/src/main/scala/leon/Simplificator.scala
@@ -5,12 +5,12 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object Simplificator extends plugin.TransformationPhase {
+object Simplificator extends TransformationPhase {
val name = "Simplificator"
val description = "Some safe and minimal simplification"
- def apply(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
index 67a2e1bafb7e9d2e9f7f4c169ee77918b45d73d1..08291badcd2dca0f6945bdf7c330493bef53c2fe 100644
--- a/src/main/scala/leon/TypeChecking.scala
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -5,12 +5,12 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object TypeChecking extends plugin.UnitPhase {
+object TypeChecking extends UnitPhase[Program] {
val name = "Type Checking"
val description = "Type check the AST"
- def apply(pgm: Program): Unit = {
+ def apply(ctx: LeonContext, pgm: Program): Unit = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index f653b8b7c8d9cd75e1dc60b400410316d1dcb6b3..d30ac296f3206780e743c56bc54364a0c60e766e 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
-object UnitElimination extends plugin.TransformationPhase {
+object UnitElimination extends TransformationPhase {
val name = "Unit Elimination"
val description = "Remove all usage of the Unit type and value"
@@ -13,7 +13,7 @@ object UnitElimination extends plugin.TransformationPhase {
private var fun2FreshFun: Map[FunDef, FunDef] = Map()
private var id2FreshId: Map[Identifier, Identifier] = Map()
- def apply(pgm: Program): Program = {
+ def apply(ctx: LeonContext, pgm: Program): Program = {
fun2FreshFun = Map()
val allFuns = pgm.definedFunctions
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index 2d2ea4143433a0d99b311dfff41e17dfb8a95294..77c058a6fa5335cbc5092b545c453d9ef0396cf0 100644
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -7,7 +7,7 @@ import scala.tools.nsc.plugins._
import purescala.Definitions.Program
import synthesis.SynthesisPhase
-class AnalysisComponent(val global: Global, val leonReporter: Reporter, val pluginInstance: LeonPlugin)
+class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
extends PluginComponent
with CodeExtraction
{
@@ -34,59 +34,12 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
def newPhase(prev: Phase) = new AnalysisPhase(prev)
class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
- def computeLeonPhases: List[LeonPhase] = {
- List(
- if (Settings.transformProgram) {
- List(
- ArrayTransformation,
- EpsilonElimination,
- ImperativeCodeElimination,
- /*UnitElimination,*/
- FunctionClosure,
- /*FunctionHoisting,*/
- Simplificator
- )
- } else {
- Nil
- }
- ,
- if (Settings.synthesis)
- List(
- SynthesisPhase
- )
- else
- Nil
- ,
- if (!Settings.stopAfterTransformation) {
- List(
- AnalysisPhase
- )
- } else {
- Nil
- }
- ).flatten
- }
-
def apply(unit: CompilationUnit): Unit = {
//global ref to freshName creator
fresh = unit.fresh
- var ac = LeonContext(program = extractCode(unit),
- reporter = leonReporter)
-
- if(Settings.stopAfterExtraction) {
- leonReporter.info("Extracted program for " + unit + ": ")
- leonReporter.info(ac.program)
- sys.exit(0)
- }
-
- val phases = computeLeonPhases
-
- for ((phase, i) <- phases.zipWithIndex) {
- leonReporter.info("%2d".format(i)+": "+phase.name)
- ac = phase.run(ac)
- }
-
+
+ pluginInstance.global.program = Some(extractCode(unit))
}
}
}
diff --git a/src/main/scala/leon/plugin/ExtractorPhase.scala b/src/main/scala/leon/plugin/ExtractorPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ef94d03e53d357b4837173ff49cdf2d082fc3d97
--- /dev/null
+++ b/src/main/scala/leon/plugin/ExtractorPhase.scala
@@ -0,0 +1,63 @@
+package leon
+package plugin
+
+import purescala.Definitions.Program
+import scala.tools.nsc.{Global,Settings=>NSCSettings,SubComponent,CompilerCommand}
+
+object ExtractionPhase extends LeonPhase[List[String], Program] {
+
+ val name = "Extraction"
+ val description = "Extraction of trees from the Scala Compiler"
+
+ def run(ctx: LeonContext)(args: List[String]): Program = {
+
+ val settings = new NSCSettings
+ val compilerOpts = args.filterNot(_.startsWith("--"))
+
+ val command = new CompilerCommand(compilerOpts, settings) {
+ override val cmdName = "leon"
+ }
+
+ if(command.ok) {
+ val runner = new PluginRunner(settings, ctx, None)
+ val run = new runner.Run
+ run.compile(command.files)
+
+ runner.program match {
+ case Some(p) =>
+ p
+ case None =>
+ ctx.reporter.fatalError("Error while compiling.")
+ }
+ } else {
+ ctx.reporter.fatalError("No input 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/LeonContext.scala b/src/main/scala/leon/plugin/LeonContext.scala
deleted file mode 100644
index 0c6ebabdd2d4eafc77607a8591e3852149038353..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/plugin/LeonContext.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-package leon
-package plugin
-
-import purescala.Definitions.Program
-
-case class LeonContext(
- val program: Program,
- val reporter: Reporter
-)
-
diff --git a/src/main/scala/leon/plugin/LeonPhase.scala b/src/main/scala/leon/plugin/LeonPhase.scala
deleted file mode 100644
index 13f437ea4b0f1e9eb0846cb6921980320723f62d..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/plugin/LeonPhase.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-package leon
-package plugin
-
-import purescala.Definitions.Program
-
-abstract class LeonPhase {
- val name: String
- val description: String
-
- def run(ac: LeonContext): LeonContext
-}
-
-abstract class TransformationPhase extends LeonPhase {
- def apply(p: Program): Program
-
- override def run(ac: LeonContext) = ac.copy(program = apply(ac.program))
-}
-
-abstract class UnitPhase extends LeonPhase {
- def apply(p: Program): Unit
-
- override def run(ac: LeonContext) = { apply(ac.program); ac }
-}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index a45711871146ca1fb1092a8e1fed5c2a7d3edca9..13542da332745a4db94d34e09bb107a5f4d75e3b 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -7,7 +7,7 @@ import scala.tools.nsc.plugins.{Plugin,PluginComponent}
import purescala.Definitions.Program
/** This class is the entry point for the plugin. */
-class LeonPlugin(val global: Global, val reporter: Reporter) extends Plugin {
+class LeonPlugin(val global: PluginRunner) extends Plugin {
import global._
val name = "leon"
@@ -85,6 +85,6 @@ class LeonPlugin(val global: Global, val reporter: Reporter) extends Plugin {
}
}
- val components = List(new AnalysisComponent(global, reporter, this))
+ val components = List(new AnalysisComponent(global, this))
val descriptions = List[String]("leon analyses")
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 5666d15c896210d24a2c48ca64082e96fec5b318..f887def32d1bce83dfe59f99cda889eea298ac67 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,22 +1,19 @@
package leon
package synthesis
-import plugin.LeonContext
import purescala.Definitions.Program
-object SynthesisPhase extends plugin.LeonPhase {
+object SynthesisPhase extends TransformationPhase {
val name = "Synthesis"
val description = "Synthesis"
- def run(ctx: LeonContext): LeonContext = {
+ def apply(ctx: LeonContext, p: Program): Program = {
val quietReporter = new QuietReporter
val solvers = List(
new TrivialSolver(quietReporter),
new FairZ3Solver(quietReporter)
)
- val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(ctx.program)
-
- ctx.copy(program = newProgram)
+ new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
}
}