diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala index 9130639d52a147389144825125051e604e93e2fb..d81b8eea718d40639c0ff5edce6bdc57c0837f83 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, PipelineControl] { +case class ExitPhase[T]() extends LeonPhase[T, Unit] { val name = "end"; val description = "end" - override def run(ctx: LeonContext)(v: T) = PipelineControl(restart = false) + override def run(ctx: LeonContext)(v: T) = () } diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala index c2ea3d878434e9f976e6dd465c7c2740b1d01e61..e52ea1ccf6cebb8a9ccd3b85de1a3d4d89474ec0 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], PipelineControl] = { + def computePipeline(settings: Settings): Pipeline[List[String], Unit] = { import purescala.Definitions.Program val pipeBegin = phaseToPipeline(plugin.ExtractionPhase) @@ -107,10 +107,15 @@ object Main { NoopPhase[Program]() } - val pipeAction: Pipeline[Program, PipelineControl]= + val pipeSynthesis: Pipeline[Program, Program]= if (settings.synthesis) { synthesis.SynthesisPhase - } else if (settings.analyze) { + } else { + NoopPhase[Program]() + } + + val pipeAnalysis: Pipeline[Program, Unit] = + if (settings.analyze) { AnalysisPhase andThen ExitPhase[Program]() } else { @@ -119,7 +124,8 @@ object Main { pipeBegin followedBy pipeTransforms followedBy - pipeAction + pipeSynthesis followedBy + pipeAnalysis } def main(args : Array[String]) { @@ -131,11 +137,7 @@ object Main { // Compute leon pipeline val pipeline = computePipeline(ctx.settings) - var exec = PipelineControl() - do { - exec = pipeline.run(ctx)(args.toList) - } while(exec.restart) - - sys.exit(exec.exitcode) + // Run pipeline + pipeline.run(ctx)(args.toList) } } diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala index ce2677d41eafe2a5aa397d159e0556a287bf373c..477a08c31250ba1996ddccd59262631fe75499c1 100644 --- a/src/main/scala/leon/Pipeline.scala +++ b/src/main/scala/leon/Pipeline.scala @@ -24,5 +24,3 @@ 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 b21f87ae304e5b58fd03290fe63d68bb93f60cd7..62e004d22cea004b5e45eab1ee956bc2b49790a4 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -3,11 +3,11 @@ package synthesis import purescala.Definitions.Program -object SynthesisPhase extends LeonPhase[Program, PipelineControl] { +object SynthesisPhase extends LeonPhase[Program, Program] { val name = "Synthesis" val description = "Synthesis" - def run(ctx: LeonContext)(p: Program): PipelineControl = { + def run(ctx: LeonContext)(p: Program): Program = { val quietReporter = new QuietReporter val solvers = List( new TrivialSolver(quietReporter), @@ -17,46 +17,7 @@ object SynthesisPhase extends LeonPhase[Program, PipelineControl] { val synth = new Synthesizer(ctx.reporter, solvers) val solutions = synth.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) - } + p } - def detectEditor: Option[String] = { - Option(System.getenv("EDITOR")) orElse Option(System.getenv("VISUAL")) - } - - def openEditor(program: String, path: String) { - val proc = Runtime.getRuntime().exec(program+" "+path) - - val errGobbler = new StreamGobbler(proc.getErrorStream(), System.err) - val outGobbler = new StreamGobbler(proc.getInputStream(), System.out) - val inGobbler = new StreamGobbler(System.in, proc.getOutputStream()) - - errGobbler.start() - outGobbler.start() - inGobbler.start() - - proc.waitFor() - errGobbler.join() - outGobbler.join() - } - - import java.io.{InputStream, OutputStream} - class StreamGobbler(is: InputStream, os: OutputStream) extends Thread { - override def run() { - var c: Int = is.read() - while(c != 1) { - os.write(c); - os.flush(); - - c = is.read() - } - } - } }