From 902b1adbc9a52d9eaab1b84bda690fb78294b0dd Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 6 May 2014 14:25:53 +0200
Subject: [PATCH] Fix printing bugs, add synthesis->print tests
---
.../scala/leon/purescala/PrettyPrinter.scala | 26 +++-
.../scala/leon/purescala/ScalaPrinter.scala | 12 +-
src/main/scala/leon/purescala/TreeOps.scala | 6 +-
.../scala/leon/synthesis/FileInterface.scala | 2 +-
.../scala/leon/synthesis/Heuristics.scala | 2 +-
src/main/scala/leon/synthesis/Solution.scala | 2 +-
.../test/synthesis/StablePrintingSuite.scala | 118 ++++++++++++++++++
7 files changed, 156 insertions(+), 12 deletions(-)
create mode 100644 src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index fb8831f64..85be66b6b 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -191,8 +191,14 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case Tuple(exprs) => p"($exprs)"
case TupleSelect(t, i) => p"${t}._$i"
case h @ Hole(o) => p"???[${h.getType}]($o)"
- case Choose(vars, pred) => p"choose($vars => $pred)"
- case CaseClassInstanceOf(cct, e) => p"$e.isInstanceOf[$cct]"
+ case Choose(vars, pred) => p"choose(($vars) => $pred)"
+ case e @ Error(err) => p"""error[${e.getType}]("$err")"""
+ case CaseClassInstanceOf(cct, e) =>
+ if (cct.classDef.isCaseObject) {
+ p"($e == ${cct.id})"
+ } else {
+ p"$e.isInstanceOf[$cct]"
+ }
case CaseClassSelector(_, e, id) => p"$e.$id"
case MethodInvocation(rec, _, tfd, args) =>
p"$rec.${tfd.id}"
@@ -293,11 +299,20 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case CaseClassPattern(ob, cct, subps) =>
ob.foreach { b => p"$b @ " }
- p"${cct.id}($subps)"
+ if (cct.classDef.isCaseObject) {
+ p"${cct.id}"
+ } else {
+ p"${cct.id}($subps)"
+ }
case InstanceOfPattern(ob, cct) =>
- ob.foreach { b => p"$b : " }
- p"$cct"
+ if (cct.classDef.isCaseObject) {
+ ob.foreach { b => p"$b @ " }
+ p"${cct.id}"
+ } else {
+ ob.foreach { b => p"$b : " }
+ p"$cct"
+ }
case TuplePattern(ob, subps) =>
ob.foreach { b => p"$b @ " }
@@ -420,6 +435,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (_: Assert, Some(_: Definition)) => true
case (_, Some(_: Definition)) => false
case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef)) => false
+ case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef)) => false
case (_, _) => true
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 755e48af7..87090a80d 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -16,9 +16,17 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
case Not(Equals(l, r)) => p"$l != $r"
- case Iff(l,r) => p"$l == $r"
+ case Iff(l,r) => pp(Equals(l, r))
case Implies(l,r) => pp(Or(Not(l), r))
- case Choose(vars, pred) => p"choose(${typed(vars)} => $pred)" // TODO
+ case Choose(vars, pred) => p"choose((${typed(vars)}) => $pred)"
+ case s @ FiniteSet(rs) => {
+ s.getType match {
+ case SetType(ut) =>
+ p"Set[$ut]($rs)"
+ case _ =>
+ p"Set($rs)"
+ }
+ }
case ElementOfSet(e,s) => p"$s.contains(e)"
case SetUnion(l,r) => p"$l ++ $r"
case MapUnion(l,r) => p"$l ++ $r"
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 68e940449..9bd1b04ed 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -216,11 +216,13 @@ object TreeOps {
/*
* Apply 'f' on 'e' as long as until it stays the same (value equality)
*/
- def fixpoint[T](f: T => T)(e: T): T = {
+ def fixpoint[T](f: T => T, limit: Int = -1)(e: T): T = {
var v1 = e
var v2 = f(v1)
- while(v2 != v1) {
+ var lim = limit
+ while(v2 != v1 && lim != 0) {
v1 = v2
+ lim -= 1
v2 = f(v2)
}
v2
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 4936b748c..4874fa838 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -64,7 +64,7 @@ class FileInterface(reporter: Reporter) {
val p = new ScalaPrinter(PrinterOptions())
p.pp(toTree)(PrinterContext(toTree, Some(fromTree), indent/2, p))
- before + p.toString + after
+ before + "{" + p.toString + "}" + after
case p =>
sys.error("Substitution requires RangePos on the input tree: "+fromTree +": "+fromTree.getClass+" GOT" +p)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 5c3fe9a07..378b0018e 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -14,7 +14,7 @@ object Heuristics {
InnerCaseSplit,
//new OptimisticInjection(_),
//new SelectiveInlining(_),
- ADTLongInduction,
+ //ADTLongInduction,
ADTInduction
)
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index c504eadac..00a007661 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -68,7 +68,7 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
}
// Simplify first using stable simplifiers
- val s = fixpoint(simple)(toExpr)
+ val s = fixpoint(simple, 5)(toExpr)
// Clean up ids/names
(new ScopeSimplifier).transform(s)
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
new file mode 100644
index 000000000..000977b68
--- /dev/null
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -0,0 +1,118 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package test
+package synthesis
+
+import leon._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.ScalaPrinter
+import leon.purescala.TreeOps._
+import leon.solvers.z3._
+import leon.solvers.Solver
+import leon.synthesis._
+import leon.synthesis.utils._
+
+import scala.collection.mutable.Stack
+import scala.io.Source
+
+import java.io.{File, BufferedWriter, FileWriter}
+
+class StablePrintingSuite extends LeonTestSuite {
+ private def forEachFileIn(path : String)(block : File => Unit) {
+ val fs = filesInResourceDir(path, _.endsWith(".scala"))
+
+ for(f <- fs) {
+ block(f)
+ }
+ }
+
+
+ private def testIterativeSynthesis(cat: String, f: File, depth: Int) {
+
+ def getChooses(ctx: LeonContext, content: String): (Program, Seq[ChooseInfo]) = {
+ val opts = SynthesisOptions()
+ val pipeline = leon.utils.TemporaryInputPhase andThen
+ frontends.scalac.ExtractionPhase andThen
+ leon.utils.PreprocessingPhase andThen
+ purescala.FunctionClosure
+
+ val program = pipeline.run(ctx)((content, Nil))
+
+ (program, ChooseInfo.extractFromProgram(ctx, program, opts))
+ }
+
+ case class Job(content: String, choosesToProcess: Set[Int], rules: List[String]) {
+ def info(task: String): String = {
+ val r = if (rules.isEmpty) "<init>" else "after "+rules.head
+
+ val indent = " "*(rules.size)+" "
+
+ f"${indent+r}%-40s [$task%s]"
+ }
+ }
+
+
+ test(cat+": "+f.getName+" - Synthesis <-> Print (depth="+depth+")") {
+ val res = Source.fromFile(f).mkString
+
+ val workList = Stack[Job](Job(res, Set(), Nil))
+
+ while(!workList.isEmpty) {
+ val reporter = new TestSilentReporter
+ val ctx = createLeonContext("--synthesis").copy(reporter = reporter)
+ val j = workList.pop()
+
+ info(j.info("compilation"))
+
+ val (pgm, chooses) = try {
+ getChooses(ctx, j.content)
+ } catch {
+ case e: Throwable =>
+ val contentWithLines = j.content.split("\n").zipWithIndex.map{ case (l, i) => f"${i+1}%4d: $l"}.mkString("\n")
+ info("Error while compiling:\n"+contentWithLines)
+ for (e <- reporter.lastErrors) {
+ info(e)
+ }
+ fail("Compilation failed")
+ }
+
+ if (j.rules.size < depth) {
+ for ((ci, i) <- chooses.zipWithIndex if j.choosesToProcess(i) || j.choosesToProcess.isEmpty) {
+ val sctx = SynthesisContext.fromSynthesizer(ci.synthesizer)
+ val problem = ci.problem
+ info(j.info("synthesis "+problem))
+ val apps = Rules.getInstantiations(sctx, problem)
+
+ for (a <- apps) {
+ a.apply(sctx) match {
+ case RuleSuccess(sol, isTrusted) =>
+ case RuleDecomposed(sub) =>
+ a.onSuccess(sub.map(Solution.choose(_))) match {
+ case Some(sol) =>
+ val result = sol.toSimplifiedExpr(ctx, pgm)
+ val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.ch, result)
+ workList push Job(newContent, (i to i+sub.size).toSet, a.toString :: j.rules)
+ case None =>
+ }
+
+ case RuleApplicationImpossible =>
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+
+ forEachFileIn("regression/synthesis/Church/") { f =>
+ testIterativeSynthesis("Church", f, 1)
+ }
+
+ forEachFileIn("regression/synthesis/List/") { f =>
+ testIterativeSynthesis("List", f, 1)
+ }
+}
--
GitLab