From dc91b649923ded877a4c045fd776d223ecbc6f90 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Apr 2014 20:47:01 +0200
Subject: [PATCH] File output, and noop option to do only that
---
src/main/scala/leon/Main.scala | 6 ++++-
.../scala/leon/purescala/Definitions.scala | 9 +++++++
.../scala/leon/utils/FileOutputPhase.scala | 27 +++++++++++++++++++
3 files changed, 41 insertions(+), 1 deletion(-)
create mode 100644 src/main/scala/leon/utils/FileOutputPhase.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3cac21a4d..325ba92de 100644
--- a/src/main/scala/leon/Main.scala
+++ b/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
}
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 54b43592e..32f21b0e7 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/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 {
diff --git a/src/main/scala/leon/utils/FileOutputPhase.scala b/src/main/scala/leon/utils/FileOutputPhase.scala
new file mode 100644
index 000000000..e6b02b7af
--- /dev/null
+++ b/src/main/scala/leon/utils/FileOutputPhase.scala
@@ -0,0 +1,27 @@
+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)
+ }
+
+}
--
GitLab