From c095c926a12ae810d523be2ffdf6b47cb736eb35 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 25 Oct 2012 16:22:40 +0200
Subject: [PATCH] Some changes regarding pipeline control
---
src/main/scala/leon/LeonPhase.scala | 4 +--
src/main/scala/leon/Main.scala | 30 +++++++++----------
src/main/scala/leon/Pipeline.scala | 2 ++
.../scala/leon/synthesis/SynthesisPhase.scala | 24 +++++++++++++--
testcases/synthesis/Spt.scala | 3 +-
5 files changed, 41 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index d81b8eea7..9130639d5 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -34,8 +34,8 @@ case class NoopPhase[T]() extends LeonPhase[T, T] {
override def run(ctx: LeonContext)(v: T) = v
}
-case class ExitPhase[T]() extends LeonPhase[T, Unit] {
+case class ExitPhase[T]() extends LeonPhase[T, PipelineControl] {
val name = "end";
val description = "end"
- override def run(ctx: LeonContext)(v: T) = ()
+ override def run(ctx: LeonContext)(v: T) = PipelineControl(restart = false)
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 0f44ffb74..d67270144 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -92,7 +92,7 @@ object Main {
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] = {
+ def computePipeLine(settings: Settings): Pipeline[List[String], PipelineControl] = {
import purescala.Definitions.Program
val pipeBegin = phaseToPipeline(plugin.ExtractionPhase)
@@ -107,28 +107,22 @@ object Main {
NoopPhase[Program]()
}
- val pipeSynthesis: Pipeline[Program, Program] =
+ val pipeAction: Pipeline[Program, PipelineControl]=
if (settings.synthesis) {
synthesis.SynthesisPhase
+ } else if (settings.analyze) {
+ AnalysisPhase andThen
+ ExitPhase[Program]()
} else {
- NoopPhase[Program]()
- }
-
- val pipeAnalysis: Pipeline[Program, Program] =
- if (settings.analyze) {
- AnalysisPhase
- } else {
- NoopPhase[Program]()
+ ExitPhase[Program]()
}
pipeBegin followedBy
pipeTransforms followedBy
- pipeSynthesis followedBy
- pipeAnalysis andThen
- ExitPhase()
+ pipeAction
}
- def main(args : Array[String]) : Unit = {
+ def main(args : Array[String]) {
val reporter = new DefaultReporter()
// Process options
@@ -137,7 +131,11 @@ object Main {
// Compute leon pipeline
val pipeline = computePipeLine(ctx.settings)
- // Run phases
- pipeline.run(ctx)(args.toList)
+ var exec = PipelineControl()
+ do {
+ exec = pipeline.run(ctx)(args.toList)
+ } while(exec.restart)
+
+ sys.exit(exec.exitcode)
}
}
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 477a08c31..ce2677d41 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -24,3 +24,5 @@ class PipeNil[T]() extends Pipeline[T,T] {
"|"
}
}
+
+case class PipelineControl(exitcode: Int = 0, restart: Boolean = false)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index f887def32..bf7a62e7e 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,17 +3,35 @@ package synthesis
import purescala.Definitions.Program
-object SynthesisPhase extends TransformationPhase {
+object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
val name = "Synthesis"
val description = "Synthesis"
- def apply(ctx: LeonContext, p: Program): Program = {
+ def run(ctx: LeonContext)(p: Program): PipelineControl = {
val quietReporter = new QuietReporter
val solvers = List(
new TrivialSolver(quietReporter),
new FairZ3Solver(quietReporter)
)
- new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
+ val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
+
+ detectEditor match {
+ case Some(program) =>
+ openEditor(program, "/home/ekneuss/plop")
+ PipelineControl(restart = false)
+ case None =>
+ ctx.reporter.fatalError("Cannot open editor, $EDITOR / $VISUAL missing")
+ PipelineControl(restart = false)
+ }
+ }
+
+ def detectEditor: Option[String] = {
+ Option(System.getenv("EDITOR")) orElse Option(System.getenv("VISUAL"))
+ }
+
+ def openEditor(program: String, path: String) {
+ val p = sys.process.Process(program+" "+path)
+ p !<
}
}
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 99cc01287..729ef9336 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -15,7 +15,8 @@ object SynthesisProceduresToolkit {
def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
- def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4)) || (a1 == a3 && x1 == x3))
+ def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) =>
+ Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4)) || (a1 == a3 && x1 == x3))
abstract class Nat
case class Z() extends Nat
--
GitLab