diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 796c1aabed3dfd46281fb844404ba2191c1afd82..360b1306193074649e2b38a2e1b46ba2d3bcefd2 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -6,7 +6,6 @@ package purescala
object PrettyPrinter {
import Common._
import Trees._
- import xlang.Trees._
import TypeTrees._
import Definitions._
@@ -28,8 +27,8 @@ object PrettyPrinter {
}
private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
- sb.append(" " * lvl)
- sb
+ sb.append(" " * lvl)
+ sb
}
// EXPRESSIONS
@@ -89,15 +88,6 @@ object PrettyPrinter {
sb.append(")")
sb
}
- case LetVar(b,d,e) => {
- sb.append("(letvar (" + b + " := ");
- pp(d, sb, lvl)
- sb.append(") in\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
- sb.append(")")
- sb
- }
case LetDef(fd,e) => {
sb.append("\n")
pp(fd, sb, lvl+1)
@@ -118,38 +108,6 @@ object PrettyPrinter {
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
case UnitLiteral => sb.append("()")
- case Block(exprs, last) => {
- sb.append("{\n")
- (exprs :+ last).foreach(e => {
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
- sb.append("\n")
- })
- ind(sb, lvl)
- sb.append("}\n")
- sb
- }
- case Assignment(lhs, rhs) => ppBinary(sb, lhs.toVariable, rhs, " = ", lvl)
- case wh@While(cond, body) => {
- wh.invariant match {
- case Some(inv) => {
- sb.append("\n")
- ind(sb, lvl)
- sb.append("@invariant: ")
- pp(inv, sb, lvl)
- sb.append("\n")
- ind(sb, lvl)
- }
- case None =>
- }
- sb.append("while(")
- pp(cond, sb, lvl)
- sb.append(")\n")
- ind(sb, lvl+1)
- pp(body, sb, lvl+1)
- sb.append("\n")
- }
-
case t@Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
case s@TupleSelect(t, i) => {
pp(t, sb, lvl)
@@ -157,14 +115,6 @@ object PrettyPrinter {
sb
}
- case e@Epsilon(pred) => {
- var nsb = sb
- nsb.append("epsilon(x" + e.posIntInfo._1 + "_" + e.posIntInfo._2 + ". ")
- nsb = pp(pred, nsb, lvl)
- nsb.append(")")
- nsb
- }
-
case c@Choose(vars, pred) => {
var nsb = sb
nsb.append("choose("+vars.mkString(", ")+" => ")
@@ -173,12 +123,6 @@ object PrettyPrinter {
nsb
}
- case Waypoint(i, expr) => {
- sb.append("waypoint_" + i + "(")
- pp(expr, sb, lvl)
- sb.append(")")
- }
-
case OptionSome(a) => {
var nsb = sb
nsb.append("Some(")
@@ -300,13 +244,6 @@ object PrettyPrinter {
pp(i, sb, lvl)
sb.append(")")
}
- case up@ArrayUpdate(ar, i, v) => {
- pp(ar, sb, lvl)
- sb.append("(")
- pp(i, sb, lvl)
- sb.append(") = ")
- pp(v, sb, lvl)
- }
case up@ArrayUpdated(ar, i, v) => {
pp(ar, sb, lvl)
sb.append(".updated(")
@@ -411,7 +348,6 @@ object PrettyPrinter {
}
case ResultVariable() => sb.append("#res")
- case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col)
case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
case e @ Error(desc) => {
@@ -422,9 +358,15 @@ object PrettyPrinter {
nsb
}
+ case (expr: PrettyPrintable) => expr.pp(sb, lvl, pp)
+
case _ => sb.append("Expr?")
}
+ trait PrettyPrintable {
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer
+ }
+
// TYPE TREES
// all type trees are printed in-line
private def ppNaryType(sb: StringBuffer, tpes: Seq[TypeTree], pre: String, op: String, post: String, lvl: Int): StringBuffer = {
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index b1b7fffe1bdd28f7f817f6ff4332e47d3646c740..e04fcbb7ecb7067df6e90c5e99b306359912f6a4 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -6,10 +6,16 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import leon.purescala.Definitions._
import leon.purescala.Extractors._
+import leon.purescala.PrettyPrinter._
object Trees {
- case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable {
+ private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
+ sb.append(" " * lvl)
+ sb
+ }
+
+ case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable {
//val t = last.getType
//if(t != Untyped)
// setType(t)
@@ -18,16 +24,38 @@ object Trees {
val Block(args, rest) = this
Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
}
+
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ sb.append("{\n")
+ (exprs :+ last).foreach(e => {
+ ind(sb, lvl+1)
+ rp(e, sb, lvl+1)
+ sb.append("\n")
+ })
+ ind(sb, lvl)
+ sb.append("}\n")
+ sb
+ }
+
}
- case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType with UnaryExtractable {
+ case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType with UnaryExtractable with PrettyPrintable {
val fixedType = UnitType
def extract: Option[(Expr, (Expr)=>Expr)] = {
Some((expr, Assignment(varId, _)))
}
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ var nsb: StringBuffer = sb
+ nsb.append("(")
+ nsb.append(varId.name)
+ nsb.append(" = ")
+ nsb = rp(expr, nsb, lvl)
+ nsb.append(")")
+ nsb
+ }
}
- case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional with BinaryExtractable {
+ case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional with BinaryExtractable with PrettyPrintable {
val fixedType = UnitType
var invariant: Option[Expr] = None
@@ -38,17 +66,52 @@ object Trees {
def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)] = {
Some((cond, body, (t1, t2) => While(t1, t2).setInvariant(this.invariant).setPosInfo(this)))
}
+
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ invariant match {
+ case Some(inv) => {
+ sb.append("\n")
+ ind(sb, lvl)
+ sb.append("@invariant: ")
+ rp(inv, sb, lvl)
+ sb.append("\n")
+ ind(sb, lvl)
+ }
+ case None =>
+ }
+ sb.append("while(")
+ rp(cond, sb, lvl)
+ sb.append(")\n")
+ ind(sb, lvl+1)
+ rp(body, sb, lvl+1)
+ sb.append("\n")
+ }
+
}
- case class Epsilon(pred: Expr) extends Expr with ScalacPositional with UnaryExtractable {
+ case class Epsilon(pred: Expr) extends Expr with ScalacPositional with UnaryExtractable with PrettyPrintable {
def extract: Option[(Expr, (Expr)=>Expr)] = {
Some((pred, (expr: Expr) => Epsilon(expr).setType(this.getType).setPosInfo(this)))
}
+
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ var nsb = sb
+ nsb.append("epsilon(x" + this.posIntInfo._1 + "_" + this.posIntInfo._2 + ". ")
+ nsb = rp(pred, nsb, lvl)
+ nsb.append(")")
+ nsb
+ }
+
+ }
+ case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal with PrettyPrintable {
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ val (row, col) = pos
+ sb.append("x" + row + "_" + col)
+ }
}
- case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal
//same as let, buf for mutable variable declaration
- case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable {
+ case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable with PrettyPrintable {
binder.markAsLetBinder
val et = body.getType
if(et != Untyped)
@@ -58,22 +121,47 @@ object Trees {
val LetVar(binders, expr, body) = this
Some((expr, body, (e: Expr, b: Expr) => LetVar(binders, e, b)))
}
+
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ val LetVar(b,d,e) = this
+ sb.append("(letvar (" + b + " := ");
+ rp(d, sb, lvl)
+ sb.append(") in\n")
+ ind(sb, lvl+1)
+ rp(e, sb, lvl+1)
+ sb.append(")")
+ sb
+ }
}
- case class Waypoint(i: Int, expr: Expr) extends Expr with UnaryExtractable {
+ case class Waypoint(i: Int, expr: Expr) extends Expr with UnaryExtractable with PrettyPrintable {
def extract: Option[(Expr, (Expr)=>Expr)] = {
Some((expr, (e: Expr) => Waypoint(i, e)))
}
+
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ sb.append("waypoint_" + i + "(")
+ rp(expr, sb, lvl)
+ sb.append(")")
+ }
}
//the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the functional version
//ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is kept all the way to the backend
- case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType with NAryExtractable {
+ case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType with NAryExtractable with PrettyPrintable {
val fixedType = UnitType
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
val ArrayUpdate(t1, t2, t3) = this
Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2))))
}
+
+ def pp(sb: StringBuffer, lvl: Int, rp: (Expr, StringBuffer, Int) => StringBuffer): StringBuffer = {
+ rp(array, sb, lvl)
+ sb.append("(")
+ rp(index, sb, lvl)
+ sb.append(") = ")
+ rp(newValue, sb, lvl)
+ }
}
}