Trait for Scala code generation

src/funcheck/CPComponent.scala

@@ -28,15 +28,15 @@ class CPComponent(val global: Global, val pluginInstance: FunCheckPlugin)
       fresh = unit.fresh
 
       val prog: purescala.Definitions.Program = extractCode(unit)
-      val fileName = writeProgram(prog)
-      println("Program extracted and written into: " + fileName)
+      val filename = writeProgram(prog)
+      println("Program extracted and written into: " + filename)
 
-      transformCalls(unit, prog)
+      transformCalls(unit, prog, filename)
       println("Finished transformation")
 
       /*
       try {
-        val recovered = readProgram(fileName)
+        val recovered = readProgram(filename)
         println
         println("Recovered: " + recovered)
       } catch {

src/funcheck/CallTransformation.scala

@@ -4,24 +4,23 @@ import scala.tools.nsc.transform.TypingTransformers
 import purescala.FairZ3Solver
 import purescala.DefaultReporter
 import purescala.Definitions._
+import purescala.Trees._
 
 trait CallTransformation 
   extends TypingTransformers
-  with CodeExtraction
+  with CodeGeneration
 {
+  self: CPComponent =>
   import global._
 
   private lazy val funcheckPackage = definitions.getModule("funcheck")
   private lazy val cpDefinitionsModule = definitions.getModule("funcheck.CP")
 
-  private lazy val purescalaPackage = definitions.getModule("purescala")
-  private lazy val fairZ3Solver = definitions.getClass("purescala.FairZ3Solver")
-  private lazy val defaultReporter = definitions.getClass("purescala.DefaultReporter")
 
-  def transformCalls(unit: CompilationUnit, prog: Program) : Unit =
-    unit.body = new CallTransformer(unit, prog).transform(unit.body)
+  def transformCalls(unit: CompilationUnit, prog: Program, filename: String) : Unit =
+    unit.body = new CallTransformer(unit, prog, filename).transform(unit.body)
   
-  class CallTransformer(unit: CompilationUnit, prog: Program) extends TypingTransformer(unit) {
+  class CallTransformer(unit: CompilationUnit, prog: Program, filename: String) extends TypingTransformer(unit) {
     override def transform(tree: Tree) : Tree = {
       tree match {
         case a @ Apply(TypeApply(Select(s: Select, n), _), rhs @ List(predicate: Function)) if (cpDefinitionsModule == s.symbol && n.toString == "choose") => {
@@ -34,35 +33,17 @@ trait CallTransformation
           println("Here is the extracted FunDef:") 
           println(fd)
 
-          val solverSymbol = currentOwner.newValue(NoPosition, unit.fresh.newName(NoPosition, "s")).setInfo(fairZ3Solver.tpe)
-          
-          val code = Block(
-            ValDef(
-              solverSymbol,
-              New(
-                Ident(fairZ3Solver),
-                List(
-                  List(
-                    New(
-                      Ident(defaultReporter),
-                      List(Nil)
-                    )
-                  )
-                )
-              )
-            ) :: Nil,
-            Literal(Constant(0))
-          )
-
+          /*
           typer.typed(atOwner(currentOwner) {
             code
           })
+          */
+          super.transform(tree)
 
           /*
           val solver = new FairZ3Solver(new DefaultReporter)
           solver.setProgram(prog)
           println(solver.decide(fd.body.get, false))
-          super.transform(tree)
           */
         }
 

src/funcheck/CodeGeneration.scala

+package funcheck
+
+import purescala.Trees._
+
+trait CodeGeneration {
+  self: CallTransformation =>
+  import global._
+
+  private lazy val serializationModule = definitions.getClass("funcheck.Serialization")
+  private lazy val readProgramFunction = definitions.getMember(serializationModule, "readProgram")
+  private lazy val purescalaPackage = definitions.getModule("purescala")
+  private lazy val definitionsModule = definitions.getModule("purescala.Definitions")
+  private lazy val programClass = definitions.getClass("purescala.Definitions.Program")
+  private lazy val fairZ3SolverClass = definitions.getClass("purescala.FairZ3Solver")
+  private lazy val decideWithModelFunction = definitions.getMember(fairZ3SolverClass, "decideWithModel")
+  private lazy val setProgramFunction = definitions.getMember(fairZ3SolverClass, "setProgram")
+
+  private lazy val defaultReporter = definitions.getClass("purescala.DefaultReporter")
+
+  class CodeGenerator(unit: CompilationUnit, owner: Symbol) {
+    /*
+    def exprToTree(expr: Expr) : Tree = expr match {
+      case Variable(id) => 
+    }
+    */
+
+    def generateProgramRead(filename: String) : (Tree, Symbol) = {
+      val progSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "prog")).setInfo(programClass.tpe)
+      val readStatement =
+        ValDef(
+          progSymbol,
+          Apply(
+            Select(
+              Ident(serializationModule),
+              readProgramFunction
+            ),
+            List(Literal(Constant(filename)))
+          )
+        )
+      (readStatement, progSymbol)
+    }
+
+    def generateSolverInvocation(formula: Expr) : Tree = {
+      val solverSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "solver")).setInfo(fairZ3SolverClass.tpe)
+      val solverDeclaration = 
+        ValDef(
+          solverSymbol,
+          New(
+            Ident(fairZ3SolverClass),
+            List(
+              List(
+                New(
+                  Ident(defaultReporter),
+                  List(Nil)
+                )
+              )
+            )
+          )
+        )
+      val setProgram =
+        Apply(
+          Select(
+            Ident(solverSymbol),
+            setProgramFunction
+          ),
+          List(/* read program into a var and plug its symbol here */)
+        )
+
+      val invocation =
+        Apply(
+          Select(
+            Ident(solverSymbol),
+            decideWithModelFunction
+          ),
+          List(/* convert pred into scala AST and plug it here */)
+        )
+
+      Block(
+            solverDeclaration :: setProgram :: invocation :: Nil,
+            Literal(Constant(0))
+          )
+    }
+  }
+}

src/funcheck/Serialization.scala

@@ -37,3 +37,5 @@ trait Serialization {
     recovered
   }
 }
+
+object Serialization extends Serialization