From ff2a3de247a7761b9f5d2882d2a2804f07cb8374 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 7 Mar 2016 16:46:16 +0100
Subject: [PATCH] Move Printable to core leon package. More classes implement
it
---
src/main/scala/leon/Printable.scala | 8 ++++++++
src/main/scala/leon/purescala/Printable.scala | 7 -------
src/main/scala/leon/solvers/ADTManager.scala | 4 ++--
src/main/scala/leon/solvers/Model.scala | 3 ++-
src/main/scala/leon/solvers/templates/UnrollingBank.scala | 1 -
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 1 -
src/main/scala/leon/synthesis/CostModel.scala | 2 +-
src/main/scala/leon/synthesis/InOutExample.scala | 3 +--
src/main/scala/leon/synthesis/Problem.scala | 4 ++--
src/main/scala/leon/synthesis/Rules.scala | 4 ++--
src/main/scala/leon/synthesis/Solution.scala | 2 +-
src/main/scala/leon/synthesis/graph/Graph.scala | 2 +-
.../leon/synthesis/strategies/CostBasedStrategy.scala | 2 +-
src/main/scala/leon/utils/FreeableIterator.scala | 2 ++
14 files changed, 23 insertions(+), 22 deletions(-)
create mode 100644 src/main/scala/leon/Printable.scala
delete mode 100644 src/main/scala/leon/purescala/Printable.scala
diff --git a/src/main/scala/leon/Printable.scala b/src/main/scala/leon/Printable.scala
new file mode 100644
index 000000000..cbe2e8ed9
--- /dev/null
+++ b/src/main/scala/leon/Printable.scala
@@ -0,0 +1,8 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+/** A trait for objects that can be pretty-printed given a [[leon.LeonContext]] */
+trait Printable {
+ def asString(implicit ctx: LeonContext): String
+}
diff --git a/src/main/scala/leon/purescala/Printable.scala b/src/main/scala/leon/purescala/Printable.scala
deleted file mode 100644
index 27be03538..000000000
--- a/src/main/scala/leon/purescala/Printable.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-package leon
-package purescala
-
-
-trait Printable {
- def asString(implicit ctx: LeonContext): String
-}
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index e811feaa1..fada59c17 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -6,12 +6,12 @@ package solvers
import purescala.Types._
import purescala.Common._
-case class DataType(sym: Identifier, cases: Seq[Constructor]) {
+case class DataType(sym: Identifier, cases: Seq[Constructor]) extends Printable {
def asString(implicit ctx: LeonContext) = {
"Datatype: "+sym.asString+"\n"+cases.map(c => " - "+c.asString(ctx)).mkString("\n")
}
}
-case class Constructor(sym: Identifier, tpe: TypeTree, fields: Seq[(Identifier, TypeTree)]) {
+case class Constructor(sym: Identifier, tpe: TypeTree, fields: Seq[(Identifier, TypeTree)]) extends Printable {
def asString(implicit ctx: LeonContext) = {
sym.asString(ctx)+" ["+tpe.asString(ctx)+"] "+fields.map(f => f._1.asString(ctx)+": "+f._2.asString(ctx)).mkString("(", ", ", ")")
}
diff --git a/src/main/scala/leon/solvers/Model.scala b/src/main/scala/leon/solvers/Model.scala
index 57f93655f..59b6c9064 100644
--- a/src/main/scala/leon/solvers/Model.scala
+++ b/src/main/scala/leon/solvers/Model.scala
@@ -9,7 +9,8 @@ import purescala.Quantification.Domains
import purescala.ExprOps._
trait AbstractModel[+This <: Model with AbstractModel[This]]
- extends scala.collection.IterableLike[(Identifier, Expr), This] {
+ extends scala.collection.IterableLike[(Identifier, Expr), This]
+ with Printable {
protected val mapping: Map[Identifier, Expr]
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index cb7fe90d2..1866fc72b 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package templates
-import purescala.Printable
import purescala.Common._
import purescala.Expressions._
import purescala.Types._
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 5c12fd386..ee6197774 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -7,7 +7,6 @@ package z3
import utils._
import _root_.z3.scala._
-import purescala.Printable
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index bc5873392..8449d37a5 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -23,7 +23,7 @@ case class Cost(minSize: Int) extends AnyVal with Ordered[Cost] {
this.minSize-that.minSize
}
- def asString: String = {
+ override def toString: String = {
f"$minSize%3d"
}
}
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index ae6e24bbc..3340816aa 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -4,9 +4,8 @@ package leon
package synthesis
import purescala.Expressions._
-import leon.utils.ASCIIHelpers._
-sealed abstract class Example {
+sealed abstract class Example extends Printable {
def ins: Seq[Expr]
def asString(implicit ctx: LeonContext) = {
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index f51fe3dd5..d59d956e9 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -21,7 +21,7 @@ import Witnesses._
* @param phi The formula on `as` and `xs` to satisfy
* @param xs The list of output identifiers for which we want to compute a function
*/
-case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) {
+case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) extends Printable {
def inType = tupleTypeWrap(as.map(_.getType))
def outType = tupleTypeWrap(xs.map(_.getType))
@@ -35,7 +35,7 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
| ${pcws.asString} ≺
| ⟨ ${phi.asString} ⟩
| ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"}
- |⟧ """.stripMargin + ebInfo
+ |⟧ $ebInfo""".stripMargin
}
def withWs(es: Seq[Expr]) = {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 6f8b3781d..f3019de65 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -11,7 +11,7 @@ import purescala.Constructors._
import rules._
/** A Rule can be applied on a synthesis problem */
-abstract class Rule(val name: String) extends RuleDSL {
+abstract class Rule(val name: String) extends RuleDSL with Printable {
def instantiateOn(implicit hctx: SearchContext, problem: Problem): Traversable[RuleInstantiation]
val priority: RulePriority = RulePriorityDefault
@@ -78,7 +78,7 @@ object Rules {
/** When applying this to a [SearchContext] it returns a wrapped stream of solutions or a new list of problems. */
abstract class RuleInstantiation(val description: String,
val onSuccess: SolutionBuilder = SolutionBuilderCloser())
- (implicit val problem: Problem, val rule: Rule) {
+ (implicit val problem: Problem, val rule: Rule) extends Printable {
def apply(hctx: SearchContext): RuleApplication
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 24a518fa9..428df1ee6 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -14,7 +14,7 @@ import leon.utils.Simplifiers
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
-class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrusted: Boolean = true) {
+class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrusted: Boolean = true) extends Printable {
def asString(implicit ctx: LeonContext) = {
"⟨ "+pre.asString+" | "+defs.map(_.asString).mkString(" ")+" "+term.asString+" ⟩"
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 3bb9fbff9..2af026aaa 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -27,7 +27,7 @@ sealed class Graph(problem: Problem) {
}
}
-sealed abstract class Node(val parent: Option[Node]) {
+sealed abstract class Node(val parent: Option[Node]) extends Printable {
def asString(implicit ctx: LeonContext): String
diff --git a/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala b/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala
index 70ccc90ab..e309593fe 100644
--- a/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala
+++ b/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala
@@ -90,5 +90,5 @@ class CostBasedStrategy(ctx: LeonContext, cm: CostModel) extends Strategy {
recomputeCost(n)
}
- def debugInfoFor(n: Node) = bestCosts.get(n).map(_.asString).getOrElse("?")
+ def debugInfoFor(n: Node) = bestCosts.get(n).map(_.toString).getOrElse("?")
}
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
index a790b2dbf..b288dcae4 100644
--- a/src/main/scala/leon/utils/FreeableIterator.scala
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
package leon
package utils
--
GitLab