SynthesisPhase.scala

package leon
package synthesis

import purescala.Definitions.Program

object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
  val name        = "Synthesis"
  val description = "Synthesis"

  def run(ctx: LeonContext)(p: Program): PipelineControl = {
    val quietReporter = new QuietReporter
    val solvers  = List(
      new TrivialSolver(quietReporter),
      new FairZ3Solver(quietReporter)
    )

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

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