From ddd6e8c3fe451940b93db992a85d42c33a22bf2b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 26 Oct 2012 16:29:51 +0200
Subject: [PATCH] Define inplace option
---
src/main/scala/leon/LeonContext.scala | 1 +
src/main/scala/leon/LeonOption.scala | 14 +++++++++++++-
src/main/scala/leon/Main.scala | 14 +++++++-------
.../scala/leon/purescala/ScalaPrinter.scala | 4 +---
.../scala/leon/synthesis/SynthesisPhase.scala | 17 +++++++++++++++--
5 files changed, 37 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 29cc186e2..7aa76a971 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -4,6 +4,7 @@ import purescala.Definitions.Program
case class LeonContext(
val settings: Settings = Settings(),
+ val options: List[LeonOption] = Nil,
val files: List[String] = Nil,
val reporter: Reporter = new DefaultReporter
)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index f2579e5af..0340e7461 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -10,4 +10,16 @@ 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)
+sealed abstract class LeonOptionDef {
+ val name: String
+ val usageOption: String
+ val usageDesc: String
+ val isFlag: Boolean
+}
+case class LeonFlagOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
+ val isFlag = true
+}
+
+case class LeonValueOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
+ val isFlag = false
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b815f5cb9..ace9c2d29 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -18,11 +18,11 @@ object Main {
}
lazy val allOptions = allPhases.flatMap(_.definedOptions) ++ Set(
- LeonOptionDef("synthesis", true, "--synthesis Partial synthesis or choose() constructs"),
- LeonOptionDef("xlang", true, "--xlang Support for extra program constructs (imperative,...)"),
- LeonOptionDef("parse", true, "--parse Checks only whether the program is valid PureScala"),
- LeonOptionDef("debug", false, "--debug=[1-5] Debug level"),
- LeonOptionDef("help", true, "--help This help")
+ LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis or choose() constructs"),
+ LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
+ LeonFlagOptionDef ("parse", "--parse", "Checks only whether the program is valid PureScala"),
+ LeonValueOptionDef("debug", "--debug=[1-5]", "Debug level"),
+ LeonFlagOptionDef ("help", "--help", "This help")
)
def displayHelp(reporter: Reporter) {
@@ -30,7 +30,7 @@ object Main {
reporter.info("")
reporter.info("Leon options are:")
for (opt <- allOptions.toSeq.sortBy(_.name)) {
- reporter.info(" "+opt.description)
+ reporter.info(" %-20s %s".format(opt.usageOption, opt.usageDesc))
}
sys.exit(1)
}
@@ -89,7 +89,7 @@ object Main {
case _ =>
}
- LeonContext(settings = settings, reporter = reporter, files = files)
+ LeonContext(settings = settings, reporter = reporter, files = files, options = leonOptions)
}
implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 2967ea34a..269f612b8 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -421,9 +421,7 @@ object ScalaPrinter {
case e @ Error(desc) => {
var nsb = sb
- nsb.append("error(\"" + desc + "\")[")
- nsb = pp(e.getType, nsb, lvl)
- nsb.append("]")
+ nsb.append("error(\"" + desc + "\")")
nsb
}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ac10811eb..898891307 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -7,6 +7,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val name = "Synthesis"
val description = "Synthesis"
+ override def definedOptions = Set(
+ LeonFlagOptionDef("inplace", "--inplace", "Debug level")
+ )
+
def run(ctx: LeonContext)(p: Program): Program = {
val quietReporter = new QuietReporter
val solvers = List(
@@ -14,11 +18,20 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
new FairZ3Solver(quietReporter)
)
+ var inPlace = false
+ for(opt <- ctx.options) opt match {
+ case LeonFlagOption("inplace") =>
+ inPlace = true
+ case _ =>
+ }
+
val synth = new Synthesizer(ctx.reporter, solvers)
val solutions = synth.synthesizeAll(p)
- for (file <- ctx.files) {
- synth.updateFile(new java.io.File(file), solutions)
+ if (inPlace) {
+ for (file <- ctx.files) {
+ synth.updateFile(new java.io.File(file), solutions)
+ }
}
p
--
GitLab