File output, and noop option to do only that

src/main/scala/leon/Main.scala

@@ -10,6 +10,7 @@ object Main {
     List(
       frontends.scalac.ExtractionPhase,
       utils.TypingPhase,
+      FileOutputPhase,
       xlang.ArrayTransformation,
       xlang.EpsilonElimination,
       xlang.ImperativeCodeElimination,
@@ -32,6 +33,7 @@ object Main {
       LeonFlagOptionDef ("xlang",       "--xlang",              "Support for extra program constructs (imperative,...)"),
       LeonFlagOptionDef ("library",     "--library",            "Inject Leon standard library"),
       LeonValueOptionDef("debug",       "--debug=<sections..>", "Enables specific messages"),
+      LeonFlagOptionDef ("noop",        "--noop",               "No operation performed, just output program"),
       LeonFlagOptionDef ("help",        "--help",               "Show help")
     )
 
@@ -156,6 +158,8 @@ object Main {
           }
         }
         settings = settings.copy(debugSections = debugSections.toSet)
+      case LeonFlagOption("noop", true) =>
+        settings = settings.copy(verify = false)
       case LeonFlagOption("help", true) =>
         displayHelp(initReporter)
       case _ =>
@@ -207,7 +211,7 @@ object Main {
       } else if (settings.verify) {
         AnalysisPhase
       } else {
-        NoopPhase()
+        utils.FileOutputPhase
       }
     }
 

src/main/scala/leon/purescala/Definitions.scala

@@ -58,6 +58,15 @@ object Definitions {
         case d => d
       })))
     }
+    
+    def writeScalaFile(filename: String) {
+      import java.io.FileWriter
+      import java.io.BufferedWriter
+      val fstream = new FileWriter(filename)
+      val out = new BufferedWriter(fstream)
+      out.write(ScalaPrinter(this))
+      out.close
+    }
   }
 
   object Program {

src/main/scala/leon/utils/FileOutputPhase.scala

+package leon.utils
+
+import leon._
+import purescala.Definitions.Program
+import java.io.File
+
+object FileOutputPhase extends UnitPhase[Program] {
+  
+  val name = "File output"
+  val description = "Output parsed/generated program into a file (default: memo.out.scala)"
+    
+  override val definedOptions : Set[LeonOptionDef] = Set( 
+     LeonValueOptionDef("o", "--o=<file>",  "Output file")
+  )
+
+  def apply(ctx:LeonContext, p : Program) {
+    // Get the output file name from command line, or use default
+    val outputFile = ( for (LeonValueOption("o", file) <- ctx.options) yield file ).lastOption.getOrElse("memo.out.scala")
+    try {
+      p.writeScalaFile(outputFile)
+    } catch {
+      case _ : java.io.IOException => ctx.reporter.fatalError("Could not write on " + outputFile)
+    }
+    ctx.reporter.info("Output written on " + outputFile)
+  }
+  
+}