Some changes regarding pipeline control

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)
 }

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)
   }
 }

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)

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 !<
   }
 }

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