diff --git a/cp-demo/ChooseCalls.scala b/cp-demo/ChooseCalls.scala index c0d4ab277c07fc8dcd83ae50f5c046f693b203a1..2e4480db2f80bb64d9bc8dcf50cc8ea5e7f5f63b 100644 --- a/cp-demo/ChooseCalls.scala +++ b/cp-demo/ChooseCalls.scala @@ -1,7 +1,4 @@ -import scala.collection.immutable.Set -import funcheck.Annotations._ -import funcheck.Utils._ -import cp.CP._ +import cp.Definitions._ object ChooseCalls { sealed abstract class Color diff --git a/src/cp/CPComponent.scala b/src/cp/CPComponent.scala index 8a0e56aa90c129225b7bb54e094c5d63f6af990e..0ce12c08fcdda1383430d9a27e394a54bdbfe900 100644 --- a/src/cp/CPComponent.scala +++ b/src/cp/CPComponent.scala @@ -30,13 +30,15 @@ class CPComponent(val global: Global, val pluginInstance: CPPlugin) println("Starting CP phase") + /* def plop(tr: Tree) = tr match { case a: Apply => println(a) println(a.fun.getClass) case _ => } - // new ForeachTreeTraverser(plop).traverse(unit.body) + new ForeachTreeTraverser(plop).traverse(unit.body) + */ val prog: purescala.Definitions.Program = extractCode(unit, true) val (progString, progId) = serialize(prog) diff --git a/src/cp/CallTransformation.scala b/src/cp/CallTransformation.scala index ff2fa31e80ea684ab014efa95530e818e72d0088..5715bcde8d9862537a4d94c767c6e04c588b72a6 100644 --- a/src/cp/CallTransformation.scala +++ b/src/cp/CallTransformation.scala @@ -18,7 +18,9 @@ trait CallTransformation import CODE._ private lazy val cpPackage = definitions.getModule("cp") - private lazy val cpDefinitionsModule = definitions.getModule("cp.CP") + private lazy val cpDefinitionsModule = definitions.getModule("cp.Definitions") + + val reporter = purescala.Settings.reporter def transformCalls(unit: CompilationUnit, prog: Program, serializedProgString : String, serializedProgId : Int) : Unit = unit.body = new CallTransformer(unit, prog, serializedProgString, serializedProgId).transform(unit.body) @@ -36,16 +38,15 @@ trait CallTransformation val fd = extractPredicate(unit, funValDefs, funBody) val outputVarList = funValDefs.map(_.name.toString) - println("Output variables: " + outputVarList.mkString(", ")) + reporter.info("Considering predicate:") + reporter.info(fd) - println("Extracted function definition:") - println(fd) val codeGen = new CodeGenerator(unit, currentOwner, tree.pos) fd.body match { - case None => println("Could not extract choose predicate: " + funBody); super.transform(tree) + case None => reporter.error("Could not extract choose predicate: " + funBody); super.transform(tree) case Some(b) => - // write expression into a file + // serialize expression val (exprString, exprId) = serialize(b) // retrieve program, expression @@ -54,7 +55,10 @@ trait CallTransformation // compute input variables and assert equalities val inputVars = variablesOf(b).filter{ v => !outputVarList.contains(v.name) }.toList - println("Input variables: " + inputVars.mkString(", ")) + + reporter.info("Input variables : " + inputVars.mkString(", ")) + reporter.info("Output variables: " + outputVarList.mkString(", ")) + val (inputVarListString, inputVarListId) = serialize(inputVars map (iv => Variable(iv))) val equalities : List[Tree] = (for (iv <- inputVars) yield { codeGen.inputEquality(inputVarListString, inputVarListId, iv, scalaToExprSym) @@ -66,11 +70,9 @@ trait CallTransformation val (solverInvocation, outcomeTupleSym) = codeGen.invokeSolver(progSym, if (inputVars.isEmpty) exprSym else andExprSym) val (modelAssignment, modelSym) = codeGen.assignModel(outcomeTupleSym) - // TODO generate all correct e2s invocations + // retrieving interpretations and converting to Scala val tripleList = (for ((ov, tt) <- (outputVarList zip typeTreeList)) yield { - // declare modelValue : Expr val (modelValueAssignment, modelValueSym) = codeGen.assignModelValue(ov, modelSym) - // declare castedValue : type of argument ov val (scalaValueAssignment, scalaValueSym) = codeGen.assignScalaValue(exprToScalaCastSym, tt, modelValueSym) (modelValueAssignment, scalaValueAssignment, scalaValueSym) }) diff --git a/src/cp/CP.scala b/src/cp/Definitions.scala similarity index 94% rename from src/cp/CP.scala rename to src/cp/Definitions.scala index 9d4599da826c5df3ef2d70362e9ff4949fcd2c01..cc5266bd010dc9cf78802f58d195b64c4f359c70 100644 --- a/src/cp/CP.scala +++ b/src/cp/Definitions.scala @@ -1,6 +1,6 @@ package cp -object CP { +object Definitions { final class NotImplementedException extends Exception def choose[A](pred : A => Boolean) : A = {