Process management, try #2

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -14,7 +14,8 @@ object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
       new FairZ3Solver(quietReporter)
     )
 
-    val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
+    val synth = new Synthesizer(ctx.reporter, solvers)
+    val solutions = synth.synthesizeAll(p)
 
     detectEditor match {
       case Some(program) => 
@@ -31,7 +32,31 @@ object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
   }
 
   def openEditor(program: String, path: String) {
-    val p = sys.process.Process(program+" "+path)
-    p !<
+    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()
+      }
+    }
   }
 }

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -86,8 +86,8 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
     (None, Map())
   }
 
-  def synthesizeAll(program: Program) = {
-    import purescala.Trees._
+  import purescala.Trees._
+  def synthesizeAll(program: Program): List[(Choose, Solution)] = {
 
     solvers.foreach(_.setProgram(program))
 
@@ -95,8 +95,10 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
 
     def noop(u:Expr, u2: Expr) = u
 
+    var solutions = List[(Choose, Solution)]()
+
     def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
-      case Choose(vars, pred) =>
+      case ch @ Choose(vars, pred) =>
         val xs = vars
         val as = (variablesOf(pred)--xs).toList
         val phi = pred
@@ -105,8 +107,11 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
         info("")
         info("In Function "+f.id+":")
         info("-"*80)
+
         val sol = synthesize(Problem(as, phi, xs), rules)
 
+        solutions = (ch, sol) :: solutions
+
         info("Scala code:")
         info(ScalaPrinter(simplifyLets(sol.toExpr)))
 
@@ -120,6 +125,13 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
       treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
     }
 
-    program
+    solutions
+  }
+
+  def substitueChooses(file: String, sols: List[(Choose, Solution)]) = {
+    import scala.io.Source
+
+    val src = Source.fromFile(file)
+
   }
 }