diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index e2350d5037d430fe6e7ba48423a2e8f1c05ea791..75f5e37f359bed8edd225fb9e27b60ae33f9f682 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -1,9 +1,14 @@
/* Copyright 2009-2013 EPFL, Lausanne */
+package leon
+package purescala
-package leon.purescala
+import Common._
+import Trees._
+import TypeTrees._
+import Definitions._
/** This pretty-printer only print valid scala syntax */
-object ScalaPrinter {
+class ScalaPrinter(sb: StringBuffer = new StringBuffer) extends PrettyPrinter(sb) {
import Common._
import Trees._
import TypeTrees._
@@ -11,263 +16,205 @@ object ScalaPrinter {
import java.lang.StringBuffer
- def apply(tree: Expr): String = {
- val retSB = new StringBuffer
- pp(tree, retSB, 0)
- retSB.toString
- }
-
- def apply(tree: Expr, lvl: Int): String = {
- val retSB = new StringBuffer
- pp(tree, retSB, lvl)
- retSB.toString
- }
-
- def apply(tpe: TypeTree): String = {
- val retSB = new StringBuffer
- pp(tpe, retSB, 0)
- retSB.toString
- }
-
- def apply(defn: Definition): String = {
- val retSB = new StringBuffer
- pp(defn, retSB, 0)
- retSB.toString
- }
-
- private def ind(sb: StringBuffer, lvl: Int) {
- sb.append(" " * lvl)
- }
-
// EXPRESSIONS
// all expressions are printed in-line
- private def ppUnary(sb: StringBuffer, expr: Expr, op1: String, op2: String, lvl: Int) {
- sb.append(op1)
- pp(expr, sb, lvl)
- sb.append(op2)
- }
-
- private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String, lvl: Int) {
- sb.append("(")
- pp(left, sb, lvl)
- sb.append(op)
- pp(right, sb, lvl)
- sb.append(")")
- }
-
- private def ppNary(sb: StringBuffer, exprs: Seq[Expr], pre: String, op: String, post: String, lvl: Int) {
- sb.append(pre)
- val sz = exprs.size
- var c = 0
-
- exprs.foreach(ex => {
- pp(ex, sb, lvl) ; c += 1 ; if(c < sz) sb.append(op)
- })
-
- sb.append(post)
- }
-
- private def pp(tree: Expr, sb: StringBuffer, lvl: Int): Unit = tree match {
+ override def pp(tree: Expr, lvl: Int): Unit = tree match {
case Variable(id) => sb.append(id)
case DeBruijnIndex(idx) => sys.error("Not Valid Scala")
- case LetTuple(ids,d,e) => {
+ case LetTuple(ids,d,e) =>
sb.append("locally {\n")
- ind(sb, lvl+1)
+ ind(lvl+1)
sb.append("val (" )
for (((id, tpe), i) <- ids.map(id => (id, id.getType)).zipWithIndex) {
sb.append(id.toString+": ")
- pp(tpe, sb, lvl)
+ pp(tpe, lvl)
if (i != ids.size-1) {
sb.append(", ")
}
}
sb.append(") = ")
- pp(d, sb, lvl+1)
+ pp(d, lvl+1)
sb.append("\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
+ ind(lvl+1)
+ pp(e, lvl+1)
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("}\n")
- ind(sb, lvl)
- }
- case Let(b,d,e) => {
+ ind(lvl)
+
+ case Let(b,d,e) =>
sb.append("locally {\n")
- ind(sb, lvl+1)
+ ind(lvl+1)
sb.append("val " + b + " = ")
- pp(d, sb, lvl+1)
+ pp(d, lvl+1)
sb.append("\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
+ ind(lvl+1)
+ pp(e, lvl+1)
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("}\n")
- ind(sb, lvl)
- }
- case And(exprs) => ppNary(sb, exprs, "(", " && ", ")", lvl) // \land
- case Or(exprs) => ppNary(sb, exprs, "(", " || ", ")", lvl) // \lor
- case Not(Equals(l, r)) => ppBinary(sb, l, r, " != ", lvl) // \neq
- case UMinus(expr) => ppUnary(sb, expr, "-(", ")", lvl)
- case Equals(l,r) => ppBinary(sb, l, r, " == ", lvl)
+ ind(lvl)
+
+ case And(exprs) => ppNary(exprs, "(", " && ", ")", lvl) // \land
+ case Or(exprs) => ppNary(exprs, "(", " || ", ")", lvl) // \lor
+ case Not(Equals(l, r)) => ppBinary(l, r, " != ", lvl) // \neq
+ case UMinus(expr) => ppUnary(expr, "-(", ")", lvl)
+ case Equals(l,r) => ppBinary(l, r, " == ", lvl)
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
case UnitLiteral => sb.append("()")
/* These two aren't really supported in Scala, but we know how to encode them. */
- case Implies(l,r) => pp(Or(Not(l), r), sb, lvl)
- case Iff(l,r) => ppBinary(sb, l, r, " == ", lvl)
+ case Implies(l,r) => pp(Or(Not(l), r), lvl)
+ case Iff(l,r) => ppBinary(l, r, " == ", lvl)
- case Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
- case TupleSelect(t, i) => {
- pp(t, sb, lvl)
+ case Tuple(exprs) => ppNary(exprs, "(", ", ", ")", lvl)
+ case TupleSelect(t, i) =>
+ pp(t, lvl)
sb.append("._" + i)
- }
- case CaseClass(cd, args) => {
+ case CaseClass(cd, args) =>
sb.append(cd.id)
if (cd.isCaseObject) {
- ppNary(sb, args, "", "", "", lvl)
+ ppNary(args, "", "", "", lvl)
} else {
- ppNary(sb, args, "(", ", ", ")", lvl)
+ ppNary(args, "(", ", ", ")", lvl)
}
- }
- case CaseClassInstanceOf(cd, e) => {
- pp(e, sb, lvl)
+
+ case CaseClassInstanceOf(cd, e) =>
+ pp(e, lvl)
sb.append(".isInstanceOf[" + cd.id + "]")
- }
+
case CaseClassSelector(_, cc, id) =>
- pp(cc, sb, lvl)
+ pp(cc, lvl)
sb.append("." + id)
- case FunctionInvocation(fd, args) => {
+
+ case FunctionInvocation(fd, args) =>
sb.append(fd.id)
- ppNary(sb, args, "(", ", ", ")", lvl)
- }
- case Plus(l,r) => ppBinary(sb, l, r, " + ", lvl)
- case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
- case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
- case Division(l,r) => ppBinary(sb, l, r, " / ", lvl)
- case Modulo(l,r) => ppBinary(sb, l, r, " % ", lvl)
- case LessThan(l,r) => ppBinary(sb, l, r, " < ", lvl)
- case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
- case LessEquals(l,r) => ppBinary(sb, l, r, " <= ", lvl) // \leq
- case GreaterEquals(l,r) => ppBinary(sb, l, r, " >= ", lvl) // \geq
- case FiniteSet(rs) => ppNary(sb, rs, "Set(", ", ", ")", lvl)
- case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl)
+ ppNary(args, "(", ", ", ")", lvl)
+
+ case Plus(l,r) => ppBinary(l, r, " + ", lvl)
+ case Minus(l,r) => ppBinary(l, r, " - ", lvl)
+ case Times(l,r) => ppBinary(l, r, " * ", lvl)
+ case Division(l,r) => ppBinary(l, r, " / ", lvl)
+ case Modulo(l,r) => ppBinary(l, r, " % ", lvl)
+ case LessThan(l,r) => ppBinary(l, r, " < ", lvl)
+ case GreaterThan(l,r) => ppBinary(l, r, " > ", lvl)
+ case LessEquals(l,r) => ppBinary(l, r, " <= ", lvl) // \leq
+ case GreaterEquals(l,r) => ppBinary(l, r, " >= ", lvl) // \geq
+ case FiniteSet(rs) => ppNary(rs, "Set(", ", ", ")", lvl)
+ case FiniteMultiset(rs) => ppNary(rs, "{|", ", ", "|}", lvl)
case EmptyMultiset(_) => sys.error("Not Valid Scala")
- case ElementOfSet(e, s) => ppBinary(sb, s, e, " contains ", lvl)
- //case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in
- //case SubsetOf(l,r) => ppBinary(sb, l, r, " \u2286 ", lvl) // \subseteq
- //case Not(SubsetOf(l,r)) => ppBinary(sb, l, r, " \u2288 ", lvl) // \notsubseteq
+ case ElementOfSet(e, s) => ppBinary(s, e, " contains ", lvl)
+ //case ElementOfSet(s,e) => ppBinary(s, e, " \u2208 ", lvl) // \in
+ //case SubsetOf(l,r) => ppBinary(l, r, " \u2286 ", lvl) // \subseteq
+ //case Not(SubsetOf(l,r)) => ppBinary(l, r, " \u2288 ", lvl) // \notsubseteq
case SetMin(s) =>
- pp(s, sb, lvl)
+ pp(s, lvl)
sb.append(".min")
case SetMax(s) =>
- pp(s, sb, lvl)
+ pp(s, lvl)
sb.append(".max")
- case SetUnion(l,r) => ppBinary(sb, l, r, " ++ ", lvl) // \cup
- // case MultisetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
- // case MapUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl) // \cup
- case SetDifference(l,r) => ppBinary(sb, l, r, " -- ", lvl)
- // case MultisetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)
- case SetIntersection(l,r) => ppBinary(sb, l, r, " & ", lvl) // \cap
- // case MultisetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap
- case SetCardinality(t) => ppUnary(sb, t, "", ".size", lvl)
- // case MultisetCardinality(t) => ppUnary(sb, t, "|", "|", lvl)
- // case MultisetPlus(l,r) => ppBinary(sb, l, r, " \u228E ", lvl) // U+
- // case MultisetToSet(e) => pp(e, sb, lvl).append(".toSet")
- case FiniteMap(rs) => {
+ case SetUnion(l,r) => ppBinary(l, r, " ++ ", lvl) // \cup
+ // case MultisetUnion(l,r) => ppBinary(l, r, " \u222A ", lvl) // \cup
+ // case MapUnion(l,r) => ppBinary(l, r, " \u222A ", lvl) // \cup
+ case SetDifference(l,r) => ppBinary(l, r, " -- ", lvl)
+ // case MultisetDifference(l,r) => ppBinary(l, r, " \\ ", lvl)
+ case SetIntersection(l,r) => ppBinary(l, r, " & ", lvl) // \cap
+ // case MultisetIntersection(l,r) => ppBinary(l, r, " \u2229 ", lvl) // \cap
+ case SetCardinality(t) => ppUnary(t, "", ".size", lvl)
+ // case MultisetCardinality(t) => ppUnary(t, "|", "|", lvl)
+ // case MultisetPlus(l,r) => ppBinary(l, r, " \u228E ", lvl) // U+
+ // case MultisetToSet(e) => pp(e, lvl).append(".toSet")
+ case FiniteMap(rs) =>
sb.append("{")
val sz = rs.size
var c = 0
rs.foreach{case (k, v) => {
- pp(k, sb, lvl); sb.append(" -> "); pp(v, sb, lvl); c += 1 ; if(c < sz) sb.append(", ")
+ pp(k, lvl); sb.append(" -> "); pp(v, lvl); c += 1 ; if(c < sz) sb.append(", ")
}}
sb.append("}")
- }
- case MapGet(m,k) => {
- pp(m, sb, lvl)
- ppNary(sb, Seq(k), "(", ",", ")", lvl)
- }
+
+ case MapGet(m,k) =>
+ pp(m, lvl)
+ ppNary(Seq(k), "(", ",", ")", lvl)
+
case MapIsDefinedAt(m,k) => {
- pp(m, sb, lvl)
+ pp(m, lvl)
sb.append(".isDefinedAt")
- ppNary(sb, Seq(k), "(", ",", ")", lvl)
+ ppNary(Seq(k), "(", ",", ")", lvl)
}
- case ArrayLength(a) => {
- pp(a, sb, lvl)
+ case ArrayLength(a) =>
+ pp(a, lvl)
sb.append(".length")
- }
- case ArrayClone(a) => {
- pp(a, sb, lvl)
+
+ case ArrayClone(a) =>
+ pp(a, lvl)
sb.append(".clone")
- }
- case ArrayFill(size, v) => {
+
+ case ArrayFill(size, v) =>
sb.append("Array.fill(")
- pp(size, sb, lvl)
+ pp(size, lvl)
sb.append(")(")
- pp(v, sb, lvl)
+ pp(v, lvl)
sb.append(")")
- }
+
case ArrayMake(v) => sys.error("Not Scala Code")
- case ArraySelect(ar, i) => {
- pp(ar, sb, lvl)
+ case ArraySelect(ar, i) =>
+ pp(ar, lvl)
sb.append("(")
- pp(i, sb, lvl)
+ pp(i, lvl)
sb.append(")")
- }
- case ArrayUpdated(ar, i, v) => {
- pp(ar, sb, lvl)
+
+ case ArrayUpdated(ar, i, v) =>
+ pp(ar, lvl)
sb.append(".updated(")
- pp(i, sb, lvl)
+ pp(i, lvl)
sb.append(", ")
- pp(v, sb, lvl)
+ pp(v, lvl)
sb.append(")")
- }
- case FiniteArray(exprs) => {
- ppNary(sb, exprs, "Array(", ", ", ")", lvl)
- }
- case Distinct(exprs) => {
+ case FiniteArray(exprs) =>
+ ppNary(exprs, "Array(", ", ", ")", lvl)
+
+ case Distinct(exprs) =>
sb.append("distinct")
- ppNary(sb, exprs, "(", ", ", ")", lvl)
- }
+ ppNary(exprs, "(", ", ", ")", lvl)
- case IfExpr(c, t, e) => {
+ case IfExpr(c, t, e) =>
sb.append("if (")
- pp(c, sb, lvl)
+ pp(c, lvl)
sb.append(") {\n")
- ind(sb, lvl+1)
- pp(t, sb, lvl+1)
+ ind(lvl+1)
+ pp(t, lvl+1)
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("} else {\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
+ ind(lvl+1)
+ pp(e, lvl+1)
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("}")
- }
- case Choose(ids, pred) => {
+ case Choose(ids, pred) =>
sb.append("(choose { (")
for (((id, tpe), i) <- ids.map(id => (id, id.getType)).zipWithIndex) {
sb.append(id.toString+": ")
- pp(tpe, sb, lvl)
+ pp(tpe, lvl)
if (i != ids.size-1) {
sb.append(", ")
}
}
sb.append(") =>\n")
- ind(sb, lvl+1)
- pp(pred, sb, lvl+1)
+ ind(lvl+1)
+ pp(pred, lvl+1)
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("})")
- }
case mex @ MatchExpr(s, csc) => {
- def ppc(sb: StringBuffer, p: Pattern): Unit = p match {
+ def ppc(p: Pattern): Unit = p match {
//case InstanceOfPattern(None, ctd) =>
//case InstanceOfPattern(Some(id), ctd) =>
case CaseClassPattern(bndr, ccd, subps) => {
@@ -276,7 +223,7 @@ object ScalaPrinter {
var c = 0
val sz = subps.size
subps.foreach(sp => {
- ppc(sb, sp)
+ ppc(sp)
if(c < sz - 1)
sb.append(", ")
c = c + 1
@@ -293,17 +240,17 @@ object ScalaPrinter {
bndr.foreach(b => sb.append(b + " @ "))
sb.append("(")
subPatterns.init.foreach(p => {
- ppc(sb, p)
+ ppc(p)
sb.append(", ")
})
- ppc(sb, subPatterns.last)
+ ppc(subPatterns.last)
sb.append(")")
}
case _ => sb.append("Pattern?")
}
sb.append("(")
- pp(s, sb, lvl)
+ pp(s, lvl)
// if(mex.posInfo != "") {
// sb.append(" match@(" + mex.posInfo + ") {\n")
// } else {
@@ -311,33 +258,34 @@ object ScalaPrinter {
// }
csc.foreach(cs => {
- ind(sb, lvl+1)
+ ind(lvl+1)
sb.append("case ")
- ppc(sb, cs.pattern)
+ ppc(cs.pattern)
cs.theGuard.foreach(g => {
sb.append(" if ")
- pp(g, sb, lvl+1)
+ pp(g, lvl+1)
})
sb.append(" =>\n")
- ind(sb, lvl+2)
- pp(cs.rhs, sb, lvl+2)
+ ind(lvl+2)
+ pp(cs.rhs, lvl+2)
sb.append("\n")
})
- ind(sb, lvl)
+ ind(lvl)
sb.append("}")
sb.append(")")
}
case ResultVariable() => sb.append("res")
- case Not(expr) => ppUnary(sb, expr, "!(", ")", lvl) // \neg
+ case Not(expr) => ppUnary(expr, "!(", ")", lvl) // \neg
case e @ Error(desc) => {
sb.append("leon.Utils.error[")
- pp(e.getType, sb, lvl)
+ pp(e.getType, lvl)
sb.append("](\"" + desc + "\")")
}
- case (expr: ScalaPrintable) => expr.ppScala(sb, lvl, pp, pp, pp)
+ case (expr: PrettyPrintable) => expr.printWith(lvl, this)
+
case _ => sb.append("Expr?")
}
@@ -349,7 +297,7 @@ object ScalaPrinter {
var c = 0
tpes.foreach(t => {
- pp(t, sb, lvl) ; c += 1 ; if(c < sz) sb.append(op)
+ pp(t, lvl) ; c += 1 ; if(c < sz) sb.append(op)
})
sb.append(post)
@@ -362,23 +310,23 @@ object ScalaPrinter {
case BooleanType => sb.append("Boolean")
case ArrayType(bt) =>
sb.append("Array[")
- pp(bt, sb, lvl)
+ pp(bt, lvl)
sb.append("]")
case SetType(bt) =>
sb.append("Set[")
- pp(bt, sb, lvl)
+ pp(bt, lvl)
sb.append("]")
case MapType(ft,tt) =>
sb.append("Map[")
- pp(ft, sb, lvl)
+ pp(ft, lvl)
sb.append(",")
- pp(tt, sb, lvl)
+ pp(tt, lvl)
sb.append("]")
case MultisetType(bt) =>
sb.append("Multiset[")
- pp(bt, sb, lvl)
+ pp(bt, lvl)
sb.append("]")
- case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
+ case TupleType(tpes) => ppNaryType(tpes, "(", ", ", ")", lvl)
case c: ClassType => sb.append(c.classDef.id)
case _ => sb.append("Type?")
}
@@ -390,11 +338,11 @@ object ScalaPrinter {
defn match {
case Program(id, mainObj) => {
assert(lvl == 0)
- pp(mainObj, sb, lvl)
+ pp(mainObj, lvl)
}
case ObjectDef(id, defs, invs) => {
- ind(sb, lvl)
+ ind(lvl)
sb.append("object ")
sb.append(id)
sb.append(" {\n")
@@ -403,7 +351,7 @@ object ScalaPrinter {
val sz = defs.size
defs.foreach(df => {
- pp(df, sb, lvl+1)
+ pp(df, lvl+1)
if(c < sz - 1) {
sb.append("\n\n")
}
@@ -411,18 +359,18 @@ object ScalaPrinter {
})
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("}\n")
}
case AbstractClassDef(id, parent) =>
- ind(sb, lvl)
+ ind(lvl)
sb.append("sealed abstract class ")
sb.append(id)
parent.foreach(p => sb.append(" extends " + p.id))
case CaseClassDef(id, parent, varDecls) =>
- ind(sb, lvl)
+ ind(lvl)
sb.append("case class ")
sb.append(id)
sb.append("(")
@@ -432,7 +380,7 @@ object ScalaPrinter {
varDecls.foreach(vd => {
sb.append(vd.id)
sb.append(": ")
- pp(vd.tpe, sb, lvl)
+ pp(vd.tpe, lvl)
if(c < sz - 1) {
sb.append(", ")
}
@@ -444,11 +392,11 @@ object ScalaPrinter {
case fd @ FunDef(id, rt, args, body, pre, post) =>
//for(a <- fd.annotations) {
- // ind(sb, lvl)
+ // ind(lvl)
// sb.append("@" + a + "\n")
//}
- ind(sb, lvl)
+ ind(lvl)
sb.append("def ")
sb.append(id)
sb.append("(")
@@ -459,7 +407,7 @@ object ScalaPrinter {
args.foreach(arg => {
sb.append(arg.id)
sb.append(" : ")
- pp(arg.tpe, sb, lvl)
+ pp(arg.tpe, lvl)
if(c < sz - 1) {
sb.append(", ")
@@ -468,20 +416,20 @@ object ScalaPrinter {
})
sb.append(") : ")
- pp(rt, sb, lvl)
+ pp(rt, lvl)
sb.append(" = (")
if(body.isDefined) {
pre match {
- case None => pp(body.get, sb, lvl)
+ case None => pp(body.get, lvl)
case Some(prec) => {
sb.append("{\n")
- ind(sb, lvl+1)
+ ind(lvl+1)
sb.append("require(")
- pp(prec, sb, lvl+1)
+ pp(prec, lvl+1)
sb.append(")\n")
- pp(body.get, sb, lvl)
+ pp(body.get, lvl)
sb.append("\n")
- ind(sb, lvl)
+ ind(lvl)
sb.append("}")
}
}
@@ -498,9 +446,9 @@ object ScalaPrinter {
val newPost = TreeOps.replace(Map(ResultVariable() -> res), postc)
sb.append(" ensuring(")
- pp(res, sb, lvl)
+ pp(res, lvl)
sb.append(" => ") //TODO, not very general solution...
- pp(newPost, sb, lvl)
+ pp(newPost, lvl)
sb.append("))")
}
}
@@ -508,12 +456,30 @@ object ScalaPrinter {
case _ => sb.append("Defn?")
}
}
+}
+
+object ScalaPrinter {
+ def apply(tree: Expr, indent: Int): String = {
+ val printer = new ScalaPrinter()
+ printer.pp(tree, indent)
+ printer.toString
+ }
+
+ def apply(tree: Expr): String = {
+ val printer = new ScalaPrinter()
+ printer.pp(tree, 0)
+ printer.toString
+ }
- trait ScalaPrintable {
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer
+ def apply(tpe: TypeTree): String = {
+ val printer = new ScalaPrinter()
+ printer.pp(tpe, 0)
+ printer.toString
+ }
+
+ def apply(defn: Definition): String = {
+ val printer = new ScalaPrinter()
+ printer.pp(defn, 0)
+ printer.toString
}
}
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 5560f97f093609aafdd4d831963b176ce295d1df..22cb9e639948ed04624da20436816e06815b3c22 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -8,8 +8,7 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import leon.purescala.Definitions._
import leon.purescala.Extractors._
-import leon.purescala.{PrettyPrinter, PrettyPrintable}
-import leon.purescala.ScalaPrinter._
+import leon.purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter}
object Trees {
@@ -18,7 +17,7 @@ object Trees {
sb
}
- case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable with ScalaPrintable with FixedType {
+ case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable with FixedType {
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
val Block(args, rest) = this
Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
@@ -35,26 +34,10 @@ object Trees {
printer.append("}\n")
}
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- sb.append("{\n")
- (exprs :+ last).foreach(e => {
- ind(sb, lvl+1)
- ep(e, sb, lvl+1)
- sb.append("\n")
- })
- ind(sb, lvl)
- sb.append("}\n")
- sb
- }
-
val fixedType = last.getType
}
- case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType with UnaryExtractable with PrettyPrintable with ScalaPrintable {
+ case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType with UnaryExtractable with PrettyPrintable {
val fixedType = UnitType
def extract: Option[(Expr, (Expr)=>Expr)] = {
@@ -68,22 +51,9 @@ object Trees {
printer.pp(expr,lvl)
printer.append(")")
}
-
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- var nsb: StringBuffer = sb
- nsb.append("(")
- nsb.append(varId.name)
- nsb.append(" = ")
- ep(expr, nsb, lvl)
- nsb.append(")")
- nsb
- }
}
- case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional with BinaryExtractable with PrettyPrintable with ScalaPrintable {
+
+ 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
@@ -114,72 +84,36 @@ object Trees {
printer.pp(body, lvl+1)
printer.append("\n")
}
-
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- invariant match {
- case Some(inv) => {
- sb.append("\n")
- ind(sb, lvl)
- sb.append("@invariant: ")
- ep(inv, sb, lvl)
- sb.append("\n")
- ind(sb, lvl)
- }
- case None =>
- }
- sb.append("while(")
- ep(cond, sb, lvl)
- sb.append(")\n")
- ind(sb, lvl+1)
- ep(body, sb, lvl+1)
- sb.append("\n")
- }
-
}
- case class Epsilon(pred: Expr) extends Expr with ScalacPositional with UnaryExtractable with PrettyPrintable with ScalaPrintable {
+ 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 printWith(lvl: Int, printer: PrettyPrinter) {
- printer.append("epsilon(x" + this.posIntInfo._1 + "_" + this.posIntInfo._2 + ". ")
- printer.pp(pred, lvl)
- printer.append(")")
- }
-
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- sys.error("Not Scala Code")
+ printer match {
+ case _: ScalaPrinter =>
+ sys.error("Not Scala Code")
+
+ case _ =>
+ printer.append("epsilon(x" + this.posIntInfo._1 + "_" + this.posIntInfo._2 + ". ")
+ printer.pp(pred, lvl)
+ printer.append(")")
+ }
}
-
}
- case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal with PrettyPrintable with ScalaPrintable {
+
+ case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal with PrettyPrintable{
def printWith(lvl: Int, printer: PrettyPrinter) {
val (row, col) = pos
printer.append("x" + row + "_" + col)
}
-
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- val (row, col) = pos
- sb.append("x" + row + "_" + col)
- }
}
//same as let, buf for mutable variable declaration
- case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable with PrettyPrintable with ScalaPrintable {
+ case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable with PrettyPrintable {
binder.markAsLetBinder
val et = body.getType
if(et != Untyped)
@@ -191,36 +125,34 @@ object Trees {
}
def printWith(lvl: Int, printer: PrettyPrinter) {
- val LetVar(b,d,e) = this
- printer.append("(letvar (" + b + " := ");
- printer.pp(d, lvl)
- printer.append(") in\n")
- printer.ind(lvl+1)
- printer.pp(e, lvl+1)
- printer.append(")")
- }
+ printer match {
+ case _: ScalaPrinter =>
+ val LetVar(b,d,e) = this
+ printer.append("locally {\n")
+ printer.ind(lvl+1)
+ printer.append("var " + b + " = ")
+ printer.pp(d, lvl+1)
+ printer.append("\n")
+ printer.ind(lvl+1)
+ printer.pp(e, lvl+1)
+ printer.append("\n")
+ printer.ind(lvl)
+ printer.append("}\n")
+ printer.ind(lvl)
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- val LetVar(b,d,e) = this
- sb.append("locally {\n")
- ind(sb, lvl+1)
- sb.append("var " + b + " = ")
- ep(d, sb, lvl+1)
- sb.append("\n")
- ind(sb, lvl+1)
- ep(e, sb, lvl+1)
- sb.append("\n")
- ind(sb, lvl)
- sb.append("}\n")
- ind(sb, lvl)
+ case _ =>
+ val LetVar(b,d,e) = this
+ printer.append("(letvar (" + b + " := ");
+ printer.pp(d, lvl)
+ printer.append(") in\n")
+ printer.ind(lvl+1)
+ printer.pp(e, lvl+1)
+ printer.append(")")
+ }
}
}
- case class LetDef(fd: FunDef, body: Expr) extends Expr with NAryExtractable with PrettyPrintable with ScalaPrintable {
+ case class LetDef(fd: FunDef, body: Expr) extends Expr with NAryExtractable with PrettyPrintable {
val et = body.getType
if(et != Untyped)
setType(et)
@@ -310,48 +242,41 @@ object Trees {
}
def printWith(lvl: Int, printer: PrettyPrinter) {
- printer.append("\n")
- printer.pp(fd, lvl+1)
- printer.append("\n")
- printer.append("\n")
- printer.ind(lvl)
- printer.pp(body, lvl)
- }
-
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- sb.append("{\n")
- dp(fd, sb, lvl+1)
- sb.append("\n")
- sb.append("\n")
- ind(sb, lvl)
- ep(body, sb, lvl)
- sb.append("}\n")
- sb
+ printer match {
+ case _: ScalaPrinter =>
+ printer.append("{\n")
+ printer.pp(fd, lvl+1)
+ printer.append("\n")
+ printer.append("\n")
+ printer.ind(lvl)
+ printer.pp(body, lvl)
+ printer.append("}\n")
+ case _ =>
+ printer.append("\n")
+ printer.pp(fd, lvl+1)
+ printer.append("\n")
+ printer.append("\n")
+ printer.ind(lvl)
+ printer.pp(body, lvl)
+ }
}
-
}
- case class Waypoint(i: Int, expr: Expr) extends Expr with UnaryExtractable with PrettyPrintable with ScalaPrintable {
+ 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 printWith(lvl: Int, printer: PrettyPrinter) {
- printer.append("waypoint_" + i + "(")
- printer.pp(expr, lvl)
- printer.append(")")
- }
-
- def ppScala(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => Unit,
- tp: (TypeTree, StringBuffer, Int) => Unit,
- dp: (Definition, StringBuffer, Int) => Unit
- ): StringBuffer = {
- sys.error("Not Scala Code")
+ printer match {
+ case _: ScalaPrinter =>
+ sys.error("Not Scala Code")
+
+ case _ =>
+ printer.append("waypoint_" + i + "(")
+ printer.pp(expr, lvl)
+ printer.append(")")
+ }
}
}