reorganize call transformation a little.

src/funcheck/CallTransformation.scala

@@ -32,19 +32,20 @@ trait CallTransformation
 
           println("Here is the extracted FunDef:") 
           println(fd)
-
-          /*
-          typer.typed(atOwner(currentOwner) {
-            code
-          })
-          */
-          super.transform(tree)
-
-          /*
-          val solver = new FairZ3Solver(new DefaultReporter)
-          solver.setProgram(prog)
-          println(solver.decide(fd.body.get, false))
-          */
+          
+          val codeGen = new CodeGenerator(unit, currentOwner)
+
+          fd.body match {
+            case None => println("Could not extract choose predicate: " + funBody); super.transform(tree)
+            case Some(b) =>
+              val (readProgram, progSym) = codeGen.generateProgramRead(filename)
+              val solverInvocation = codeGen.generateSolverInvocation(b, progSym)
+              val code = Block(readProgram :: Nil, solverInvocation)
+
+              typer.typed(atOwner(currentOwner) {
+                code
+              })
+          }
         }
 
         case _ => super.transform(tree)

src/funcheck/CodeGeneration.scala

@@ -40,7 +40,7 @@ trait CodeGeneration {
       (readStatement, progSymbol)
     }
 
-    def generateSolverInvocation(formula: Expr) : Tree = {
+    def generateSolverInvocation(formula: Expr, progSymbol: Symbol) : Tree = {
       val solverSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "solver")).setInfo(fairZ3SolverClass.tpe)
       val solverDeclaration = 
         ValDef(
@@ -63,7 +63,7 @@ trait CodeGeneration {
             Ident(solverSymbol),
             setProgramFunction
           ),
-          List(/* read program into a var and plug its symbol here */)
+          List(Ident(progSymbol))
         )
 
       val invocation =
@@ -72,7 +72,7 @@ trait CodeGeneration {
             Ident(solverSymbol),
             decideWithModelFunction
           ),
-          List(/* convert pred into scala AST and plug it here */)
+          List(/* convert pred into scala AST of funcheck expression and plug it here */)
         )
 
       Block(