diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 57ed71b5d99e44a579d120255a0de8da873d5865..ceaac05a72e988d33ace2e7a88f3473543c51cb7 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 9df66e65f8a5b28e9e737a8ca0c7a6dc6121b1b2..b647188e922f592ab0606387ac316fadcb311465 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 8fd2f86360c5cf6cb17c76bf3ff1afefc60acfaf..36ba8587dae30245af64b3e561bd088beee21cac 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 e6b02b7afe45b794278f454d313c2446494de2ed..ec75d2f994cbdba4f7593219af71d4c6b5d7c872 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) } }