From daeb0818386e8bfe1c414f1c9c2769b28d536d5e Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 1 Sep 2014 16:54:58 +0200
Subject: [PATCH] Print units in separate files
---
.../frontends/scalac/CodeExtraction.scala | 19 +++++++++++++------
.../frontends/scalac/ExtractionPhase.scala | 3 +--
.../frontends/scalac/LeonExtraction.scala | 4 ++--
.../scala/leon/utils/FileOutputPhase.scala | 18 +++++++++++++-----
4 files changed, 29 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 57ed71b5d..ceaac05a7 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -115,7 +115,13 @@ trait CodeExtraction extends ASTExtractors {
// Simple case classes to capture the representation of units/modules after discovering them.
case class TempModule(name : Identifier, trees : List[Tree])
- case class TempUnit(name : String, pack : PackageRef, modules : List[TempModule], imports : List[Import])
+ case class TempUnit(
+ name : String,
+ pack : PackageRef,
+ modules : List[TempModule],
+ imports : List[Import],
+ isPrintable : Boolean
+ )
class Extraction(units: List[CompilationUnit]) {
@@ -187,6 +193,8 @@ trait CodeExtraction extends ASTExtractors {
def extractUnits: List[UnitDef] = {
try {
+ def isLib(u : CompilationUnit) = Build.libFiles contains u.source.file.absolute.path
+
val templates: List[TempUnit] = units.reverse.map { u => u.body match {
case pd @ PackageDef(refTree, lst) =>
@@ -227,12 +235,11 @@ trait CodeExtraction extends ASTExtractors {
extractPackageRef(refTree),
if (standaloneDefs.isEmpty) modules
else ( TempModule(FreshIdentifier(unitName+ "$standalone"), standaloneDefs) ) :: modules,
- imports.getOrElse(refTree, Nil)
+ imports.getOrElse(refTree, Nil),
+ !isLib(u)
)
}
-
-
}
// Phase 1, we detect objects/classes/types
@@ -254,11 +261,11 @@ trait CodeExtraction extends ASTExtractors {
for (temp <- templates; mod <- temp.modules) extractObjectDef(mod.name, mod.trees)
// Phase 7, we wrap modules in units
- val withoutImports = for (TempUnit(name,pack,mods,imps) <- templates) yield {
+ val withoutImports = for (TempUnit(name,pack,mods,imps,isPrintable) <- templates) yield {
( UnitDef(
FreshIdentifier(name),
for( TempModule(nm,_) <- mods) yield objects2Objects(nm),
- pack, Nil, true
+ pack, Nil, isPrintable
)
, imps
)
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 9df66e65f..b647188e9 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -36,7 +36,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
settings.skip.value = List("patmat")
val libFiles = Build.libFiles
-
+
val injected = if (ctx.settings.injectLibrary) {
libFiles
} else {
@@ -67,7 +67,6 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
compiler.leonExtraction.setImports(compiler.saveImports.imports )
val pgm = Program(FreshIdentifier("__program"), compiler.leonExtraction.compiledUnits)
- ctx.reporter.debug(pgm.asString(ctx))
pgm
} else {
ctx.reporter.fatalError("No input program.")
diff --git a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
index 8fd2f8636..36ba8587d 100644
--- a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
@@ -15,11 +15,11 @@ trait LeonExtraction extends SubComponent with CodeExtraction {
val phaseName = "leon"
var units: List[CompilationUnit] = Nil
-
+
val ctx: LeonContext
var imports : Map[RefTree,List[Import]] = Map()
-
+
def setImports( imports : Map[RefTree,List[Import]] ) {
this.imports = imports
}
diff --git a/src/main/scala/leon/utils/FileOutputPhase.scala b/src/main/scala/leon/utils/FileOutputPhase.scala
index e6b02b7af..ec75d2f99 100644
--- a/src/main/scala/leon/utils/FileOutputPhase.scala
+++ b/src/main/scala/leon/utils/FileOutputPhase.scala
@@ -7,7 +7,7 @@ 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)"
+ val description = "Output parsed/generated program into files under the specified directory (default: leon.out)"
override val definedOptions : Set[LeonOptionDef] = Set(
LeonValueOptionDef("o", "--o=<file>", "Output file")
@@ -15,13 +15,21 @@ object FileOutputPhase extends UnitPhase[Program] {
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")
+ val outputFolder = ( for (LeonValueOption("o", file) <- ctx.options) yield file ).lastOption.getOrElse("leon.out")
try {
- p.writeScalaFile(outputFile)
+ new File(outputFolder).mkdir()
} catch {
- case _ : java.io.IOException => ctx.reporter.fatalError("Could not write on " + outputFile)
+ case _ : java.io.IOException => ctx.reporter.fatalError("Could not create directory " + outputFolder)
}
- ctx.reporter.info("Output written on " + outputFile)
+
+ for (u <- p.units if u.isMainUnit) {
+ val outputFile = s"$outputFolder${File.separator}${u.id.toString}.scala"
+ try { u.writeScalaFile(outputFile) }
+ catch {
+ case _ : java.io.IOException => ctx.reporter.fatalError("Could not write on " + outputFile)
+ }
+ }
+ ctx.reporter.info("Output written on " + outputFolder)
}
}
--
GitLab