From 92fd83a40cfbe150fbbb4ea916eba50b8171eedf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Thu, 17 May 2012 16:37:02 +0200 Subject: [PATCH] add a method to write a program to a file in valid scala syntax --- src/main/scala/leon/TestGeneration.scala | 2 +- src/main/scala/leon/purescala/Definitions.scala | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala index 5b2f86946..14269dccc 100644 --- a/src/main/scala/leon/TestGeneration.scala +++ b/src/main/scala/leon/TestGeneration.scala @@ -43,7 +43,7 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { val Program(id, ObjectDef(objId, defs, invariants)) = program val testProgram = Program(id, ObjectDef(objId, testFun +: defs , invariants)) - println("New program:\n" + ScalaPrinter(testProgram)) + testProgram.writeScalaFile("TestGen.scala") reporter.info("Running from waypoint with the following testcases:\n") reporter.info(testcases.mkString("\n")) diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala index bc497dcdd..3c18e858f 100644 --- a/src/main/scala/leon/purescala/Definitions.scala +++ b/src/main/scala/leon/purescala/Definitions.scala @@ -54,6 +54,15 @@ object Definitions { def caseClassDef(name: String) = mainObject.caseClassDef(name) def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(Trees.isPure) && fd.precondition.forall(Trees.isPure) && fd.postcondition.forall(Trees.isPure)) + + 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 + } } /** Objects work as containers for class definitions, functions (def's) and -- GitLab