diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index fd8fa2ed0e404b7004ff14373e5495b75322e4c7..11e98e534e5f5f15b6b8e51ee322373469404ae5 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -1,494 +1,470 @@
package leon
package purescala
-/** This pretty-printer uses Unicode for some operators, to make sure we
- * distinguish PureScala from "real" Scala (and also because it's cute). */
-object PrettyPrinter {
- import Common._
- import Trees._
- import TypeTrees._
- import Definitions._
+import Common._
+import Trees._
+import TypeTrees._
+import Definitions._
- import java.lang.StringBuffer
-
- def apply(tree: Expr): String = {
- val retSB = pp(tree, new StringBuffer, 0)
- retSB.toString
- }
+import java.lang.StringBuffer
- def apply(tpe: TypeTree): String = {
- val retSB = pp(tpe, new StringBuffer, 0)
- retSB.toString
- }
+/** This pretty-printer uses Unicode for some operators, to make sure we
+ * distinguish PureScala from "real" Scala (and also because it's cute). */
+class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
+ override def toString = sb.toString
- def apply(defn: Definition): String = {
- val retSB = pp(defn, new StringBuffer, 0)
- retSB.toString
+ def append(str: String) {
+ sb.append(str)
}
- private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
+ def ind(lvl: Int) {
sb.append(" " * lvl)
- sb
}
// EXPRESSIONS
// all expressions are printed in-line
- private def ppUnary(sb: StringBuffer, expr: Expr, op1: String, op2: String, lvl: Int): StringBuffer = {
- var nsb: StringBuffer = sb
- nsb.append(op1)
- nsb = pp(expr, nsb, lvl)
- nsb.append(op2)
- nsb
+ def ppUnary(expr: Expr, op1: String, op2: String, lvl: Int) {
+ sb.append(op1)
+ pp(expr, lvl)
+ sb.append(op2)
}
- private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String, lvl: Int): StringBuffer = {
- var nsb: StringBuffer = sb
- nsb.append("(")
- nsb = pp(left, nsb, lvl)
- nsb.append(op)
- nsb = pp(right, nsb, lvl)
- nsb.append(")")
- nsb
+ def ppBinary(left: Expr, right: Expr, op: String, lvl: Int) {
+ sb.append("(")
+ pp(left, lvl)
+ sb.append(op)
+ pp(right, lvl)
+ sb.append(")")
}
- private def ppNary(sb: StringBuffer, exprs: Seq[Expr], pre: String, op: String, post: String, lvl: Int): StringBuffer = {
- var nsb = sb
- nsb.append(pre)
+ def ppNary(exprs: Seq[Expr], pre: String, op: String, post: String, lvl: Int) {
+ sb.append(pre)
val sz = exprs.size
var c = 0
exprs.foreach(ex => {
- nsb = pp(ex, nsb, lvl) ; c += 1 ; if(c < sz) nsb.append(op)
+ pp(ex, lvl) ; c += 1 ; if(c < sz) sb.append(op)
})
- nsb.append(post)
- nsb
+ sb.append(post)
}
- private def pp(tree: Expr, sb: StringBuffer, lvl: Int): StringBuffer = tree match {
- case Variable(id) => sb.append(id)
+ def idToString(id: Identifier): String = id.toString
+
+ def pp(tree: Expr, lvl: Int): Unit = tree match {
+ case Variable(id) => sb.append(idToString(id))
case DeBruijnIndex(idx) => sb.append("_" + idx)
case LetTuple(bs,d,e) => {
//pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
- sb.append("(let (" + bs.mkString(",") + " := ");
- pp(d, sb, lvl)
+ sb.append("(let (" + bs.map(idToString _).mkString(",") + " := ");
+ pp(d, lvl)
sb.append(") in\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
+ ind(lvl+1)
+ pp(e, lvl+1)
sb.append(")")
sb
}
case Let(b,d,e) => {
//pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
- sb.append("(let (" + b + " := ");
- pp(d, sb, lvl)
+ sb.append("(let (" + idToString(b) + " := ");
+ pp(d, lvl)
sb.append(") in\n")
- ind(sb, lvl+1)
- pp(e, sb, lvl+1)
+ ind(lvl+1)
+ pp(e, lvl+1)
sb.append(")")
sb
}
- case And(exprs) => ppNary(sb, exprs, "(", " \u2227 ", ")", lvl) // \land
- case Or(exprs) => ppNary(sb, exprs, "(", " \u2228 ", ")", lvl) // \lor
- case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl) // \neq
- case Iff(l,r) => ppBinary(sb, l, r, " <=> ", lvl)
- case Implies(l,r) => ppBinary(sb, l, r, " ==> ", lvl)
- case UMinus(expr) => ppUnary(sb, expr, "-(", ")", lvl)
- case Equals(l,r) => ppBinary(sb, l, r, " == ", lvl)
+ case And(exprs) => ppNary(exprs, "(", " \u2227 ", ")", lvl) // \land
+ case Or(exprs) => ppNary(exprs, "(", " \u2228 ", ")", lvl) // \lor
+ case Not(Equals(l, r)) => ppBinary(l, r, " \u2260 ", lvl) // \neq
+ case Iff(l,r) => ppBinary(l, r, " <=> ", lvl)
+ case Implies(l,r) => ppBinary(l, r, " ==> ", lvl)
+ 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("()")
- case t@Tuple(exprs) => ppNary(sb, exprs, "(", ", ", ")", lvl)
+ case t@Tuple(exprs) => ppNary(exprs, "(", ", ", ")", lvl)
case s@TupleSelect(t, i) => {
- pp(t, sb, lvl)
+ pp(t, lvl)
sb.append("._" + i)
sb
}
case c@Choose(vars, pred) => {
- var nsb = sb
- nsb.append("choose("+vars.mkString(", ")+" => ")
- nsb = pp(pred, nsb, lvl)
- nsb.append(")")
- nsb
+ sb.append("choose("+vars.map(idToString _).mkString(", ")+" => ")
+ pp(pred, lvl)
+ sb.append(")")
}
case CaseClass(cd, args) => {
- var nsb = sb
- nsb.append(cd.id)
+ sb.append(idToString(cd.id))
if (cd.isCaseObject) {
- nsb = ppNary(nsb, args, "", "", "", lvl)
+ ppNary(args, "", "", "", lvl)
} else {
- nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
+ ppNary(args, "(", ", ", ")", lvl)
}
- nsb
+ sb
}
case CaseClassInstanceOf(cd, e) => {
- var nsb = sb
- nsb = pp(e, nsb, lvl)
- nsb.append(".isInstanceOf[" + cd.id + "]")
- nsb
+ pp(e, lvl)
+ sb.append(".isInstanceOf[" + idToString(cd.id) + "]")
+ sb
}
- case CaseClassSelector(_, cc, id) => pp(cc, sb, lvl).append("." + id)
+ case CaseClassSelector(_, cc, id) =>
+ pp(cc, lvl)
+ sb.append("." + idToString(id))
+
case FunctionInvocation(fd, args) => {
- var nsb = sb
- nsb.append(fd.id)
- nsb = ppNary(nsb, args, "(", ", ", ")", lvl)
- nsb
+ sb.append(idToString(fd.id))
+ ppNary(args, "(", ", ", ")", lvl)
+ sb
}
- 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, " \u2264 ", lvl) // \leq
- case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl) // \geq
- case FiniteSet(rs) => if(rs.isEmpty) sb.append("\u2205") /* Ø */ else ppNary(sb, rs, "{", ", ", "}", lvl)
- case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", 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, " \u2264 ", lvl) // \leq
+ case GreaterEquals(l,r) => ppBinary(l, r, " \u2265 ", lvl) // \geq
+ case FiniteSet(rs) => if(rs.isEmpty) sb.append("\u2205") /* Ø */ else ppNary(rs, "{", ", ", "}", lvl)
+ case FiniteMultiset(rs) => ppNary(rs, "{|", ", ", "|}", lvl)
case EmptyMultiset(_) => sb.append("\u2205") // Ø
- case Not(ElementOfSet(s,e)) => ppBinary(sb, s, e, " \u2209 ", lvl) // \notin
- 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 SetMin(s) => pp(s, sb, lvl).append(".min")
- case SetMax(s) => pp(s, sb, lvl).append(".max")
- case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", 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, " \u2229 ", lvl) // \cap
- case MultisetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap
- case SetCardinality(t) => ppUnary(sb, t, "|", "|", 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 Not(ElementOfSet(s,e)) => ppBinary(s, e, " \u2209 ", lvl) // \notin
+ 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, lvl); sb.append(".min")
+ case SetMax(s) => pp(s, lvl); sb.append(".max")
+ case SetUnion(l,r) => ppBinary(l, r, " \u222A ", 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, " \u2229 ", lvl) // \cap
+ case MultisetIntersection(l,r) => ppBinary(l, r, " \u2229 ", lvl) // \cap
+ case SetCardinality(t) => ppUnary(t, "|", "|", lvl)
+ case MultisetCardinality(t) => ppUnary(t, "|", "|", lvl)
+ case MultisetPlus(l,r) => ppBinary(l, r, " \u228E ", lvl) // U+
+ case MultisetToSet(e) => pp(e, lvl); sb.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) => {
- var nsb = sb
- pp(m, nsb, lvl)
- nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
- nsb
+ pp(m, lvl)
+ ppNary(Seq(k), "(", ",", ")", lvl)
+ sb
}
case MapIsDefinedAt(m,k) => {
- var nsb = sb
- pp(m, nsb, lvl)
- nsb.append(".isDefinedAt")
- nsb = ppNary(nsb, Seq(k), "(", ",", ")", lvl)
- nsb
+ pp(m, lvl)
+ sb.append(".isDefinedAt")
+ ppNary(Seq(k), "(", ",", ")", lvl)
+ sb
}
case ArrayLength(a) => {
- pp(a, sb, lvl)
+ pp(a, lvl)
sb.append(".length")
}
case ArrayClone(a) => {
- pp(a, sb, lvl)
+ pp(a, lvl)
sb.append(".clone")
}
case fill@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 am@ArrayMake(v) => {
sb.append("Array.make(")
- pp(v, sb, lvl)
+ pp(v, lvl)
sb.append(")")
}
case sel@ArraySelect(ar, i) => {
- pp(ar, sb, lvl)
+ pp(ar, lvl)
sb.append("(")
- pp(i, sb, lvl)
+ pp(i, lvl)
sb.append(")")
}
case up@ArrayUpdated(ar, i, v) => {
- pp(ar, sb, lvl)
+ 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)
+ ppNary(exprs, "Array(", ", ", ")", lvl)
}
case Distinct(exprs) => {
- var nsb = sb
- nsb.append("distinct")
- nsb = ppNary(nsb, exprs, "(", ", ", ")", lvl)
- nsb
+ sb.append("distinct")
+ ppNary(exprs, "(", ", ", ")", lvl)
}
case IfExpr(c, t, e) => {
- var nsb = sb
- nsb.append("if (")
- nsb = pp(c, nsb, lvl)
- nsb.append(")\n")
- ind(nsb, lvl+1)
- nsb = pp(t, nsb, lvl+1)
- nsb.append("\n")
- ind(nsb, lvl)
- nsb.append("else\n")
- ind(nsb, lvl+1)
- nsb = pp(e, nsb, lvl+1)
- nsb
- //nsb.append(") {\n")
- //ind(nsb, lvl+1)
- //nsb = pp(t, nsb, lvl+1)
- //nsb.append("\n")
- //ind(nsb, lvl)
- //nsb.append("} else {\n")
- //ind(nsb, lvl+1)
- //nsb = pp(e, nsb, lvl+1)
- //nsb.append("\n")
- //ind(nsb, lvl)
- //nsb.append("}")
- //nsb
+ sb.append("if (")
+ pp(c, lvl)
+ sb.append(")\n")
+ ind(lvl+1)
+ pp(t, lvl+1)
+ sb.append("\n")
+ ind(lvl)
+ sb.append("else\n")
+ ind(lvl+1)
+ pp(e, lvl+1)
}
case mex @ MatchExpr(s, csc) => {
- def ppc(sb: StringBuffer, p: Pattern): StringBuffer = p match {
+ def ppc(p: Pattern): Unit = p match {
//case InstanceOfPattern(None, ctd) =>
//case InstanceOfPattern(Some(id), ctd) =>
case CaseClassPattern(bndr, ccd, subps) => {
- var nsb = sb
- bndr.foreach(b => nsb.append(b + " @ "))
- nsb.append(ccd.id).append("(")
+ bndr.foreach(b => sb.append(idToString(b) + " @ "))
+ sb.append(idToString(ccd.id)).append("(")
var c = 0
val sz = subps.size
subps.foreach(sp => {
- nsb = ppc(nsb, sp)
+ ppc(sp)
if(c < sz - 1)
- nsb.append(", ")
+ sb.append(", ")
c = c + 1
})
- nsb.append(")")
+ sb.append(")")
}
case WildcardPattern(None) => sb.append("_")
- case WildcardPattern(Some(id)) => sb.append(id)
+ case WildcardPattern(Some(id)) => sb.append(idToString(id))
case TuplePattern(bndr, subPatterns) => {
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?")
}
- var nsb = sb
- nsb == pp(s, nsb, lvl)
+ pp(s, lvl)
// if(mex.posInfo != "") {
- // nsb.append(" match@(" + mex.posInfo + ") {\n")
+ // sb.append(" match@(" + mex.posInfo + ") {\n")
// } else {
- nsb.append(" match {\n")
+ sb.append(" match {\n")
// }
csc.foreach(cs => {
- ind(nsb, lvl+1)
- nsb.append("case ")
- nsb = ppc(nsb, cs.pattern)
+ ind(lvl+1)
+ sb.append("case ")
+ ppc(cs.pattern)
cs.theGuard.foreach(g => {
- nsb.append(" if ")
- nsb = pp(g, nsb, lvl+1)
+ sb.append(" if ")
+ pp(g, lvl+1)
})
- nsb.append(" => ")
- nsb = pp(cs.rhs, nsb, lvl+1)
- nsb.append("\n")
+ sb.append(" => ")
+ pp(cs.rhs, lvl+1)
+ sb.append("\n")
})
- ind(nsb, lvl).append("}")
- nsb
+ ind(lvl)
+ sb.append("}")
}
case ResultVariable() => sb.append("#res")
- case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
+ case Not(expr) => ppUnary(expr, "\u00AC(", ")", lvl) // \neg
case e @ Error(desc) => {
- var nsb = sb
- nsb.append("error(\"" + desc + "\")[")
- nsb = pp(e.getType, nsb, lvl)
- nsb.append("]")
- nsb
+ sb.append("error(\"" + desc + "\")[")
+ pp(e.getType, lvl)
+ sb.append("]")
}
- case (expr: PrettyPrintable) => expr.pp(sb, lvl, pp, pp, pp)
+ case (expr: PrettyPrintable) => expr.printWith(lvl, this)
case _ => sb.append("Expr?")
}
- trait PrettyPrintable {
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, 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 = {
- var nsb = sb
- nsb.append(pre)
+ def ppNaryType(tpes: Seq[TypeTree], pre: String, op: String, post: String, lvl: Int): StringBuffer = {
+ sb.append(pre)
val sz = tpes.size
var c = 0
tpes.foreach(t => {
- nsb = pp(t, nsb, lvl) ; c += 1 ; if(c < sz) nsb.append(op)
+ pp(t, lvl) ; c += 1 ; if(c < sz) sb.append(op)
})
- nsb.append(post)
- nsb
+ sb.append(post)
+ sb
}
- private def pp(tpe: TypeTree, sb: StringBuffer, lvl: Int): StringBuffer = tpe match {
+ def pp(tpe: TypeTree, lvl: Int): StringBuffer = tpe match {
case Untyped => sb.append("???")
case UnitType => sb.append("Unit")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
- case ArrayType(bt) => pp(bt, sb.append("Array["), lvl).append("]")
- case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
- case MapType(ft,tt) => pp(tt, pp(ft, sb.append("Map["), lvl).append(","), lvl).append("]")
- case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
- case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
+ case ArrayType(bt) => sb.append("Array["); pp(bt, lvl); sb.append("]")
+ case SetType(bt) => sb.append("Set["); pp(bt, lvl); sb.append("]")
+ case MapType(ft,tt) => sb.append("Map["); pp(ft, lvl); sb.append(","); pp(tt, lvl); sb.append("]")
+ case MultisetType(bt) => sb.append("Multiset["); pp(bt, lvl); sb.append("]")
+ case TupleType(tpes) => ppNaryType(tpes, "(", ", ", ")", lvl)
case c: ClassType => sb.append(c.classDef.id)
case _ => sb.append("Type?")
}
// DEFINITIONS
// all definitions are printed with an end-of-line
- private def pp(defn: Definition, sb: StringBuffer, lvl: Int): StringBuffer = {
-
+ def pp(defn: Definition, lvl: Int) {
defn match {
case Program(id, mainObj) => {
assert(lvl == 0)
sb.append("package ")
- sb.append(id)
+ sb.append(idToString(id))
sb.append(" {\n")
- pp(mainObj, sb, lvl+1).append("}\n")
+ pp(mainObj, lvl+1)
+ sb.append("}\n")
}
case ObjectDef(id, defs, invs) => {
- var nsb = sb
- ind(nsb, lvl)
- nsb.append("object ")
- nsb.append(id)
- nsb.append(" {\n")
+ ind(lvl)
+ sb.append("object ")
+ sb.append(idToString(id))
+ sb.append(" {\n")
var c = 0
val sz = defs.size
defs.foreach(df => {
- nsb = pp(df, nsb, lvl+1)
+ pp(df, lvl+1)
if(c < sz - 1) {
- nsb.append("\n\n")
+ sb.append("\n\n")
}
c = c + 1
})
- nsb.append("\n")
- ind(nsb, lvl).append("}\n")
+ sb.append("\n")
+ ind(lvl)
+ sb.append("}\n")
}
case AbstractClassDef(id, parent) => {
- var nsb = sb
- ind(nsb, lvl)
- nsb.append("sealed abstract class ")
- nsb.append(id)
- parent.foreach(p => nsb.append(" extends " + p.id))
- nsb
+ ind(lvl)
+ sb.append("sealed abstract class ")
+ sb.append(idToString(id))
+ parent.foreach(p => sb.append(" extends " + idToString(p.id)))
}
case CaseClassDef(id, parent, varDecls) => {
- var nsb = sb
- ind(nsb, lvl)
- nsb.append("case class ")
- nsb.append(id)
- nsb.append("(")
+ ind(lvl)
+ sb.append("case class ")
+ sb.append(idToString(id))
+ sb.append("(")
var c = 0
val sz = varDecls.size
varDecls.foreach(vd => {
- nsb.append(vd.id)
- nsb.append(": ")
- nsb = pp(vd.tpe, nsb, lvl)
+ sb.append(idToString(vd.id))
+ sb.append(": ")
+ pp(vd.tpe, lvl)
if(c < sz - 1) {
- nsb.append(", ")
+ sb.append(", ")
}
c = c + 1
})
- nsb.append(")")
- parent.foreach(p => nsb.append(" extends " + p.id))
- nsb
+ sb.append(")")
+ parent.foreach(p => sb.append(" extends " + idToString(p.id)))
}
case fd @ FunDef(id, rt, args, body, pre, post) => {
- var nsb = sb
-
for(a <- fd.annotations) {
- ind(nsb, lvl)
- nsb.append("@" + a + "\n")
+ ind(lvl)
+ sb.append("@" + a + "\n")
}
pre.foreach(prec => {
- ind(nsb, lvl)
- nsb.append("@pre : ")
- nsb = pp(prec, nsb, lvl)
- nsb.append("\n")
+ ind(lvl)
+ sb.append("@pre : ")
+ pp(prec, lvl)
+ sb.append("\n")
})
post.foreach(postc => {
- ind(nsb, lvl)
- nsb.append("@post: ")
- nsb = pp(postc, nsb, lvl)
- nsb.append("\n")
+ ind(lvl)
+ sb.append("@post: ")
+ pp(postc, lvl)
+ sb.append("\n")
})
- ind(nsb, lvl)
- nsb.append("def ")
- nsb.append(id)
- nsb.append("(")
+ ind(lvl)
+ sb.append("def ")
+ sb.append(idToString(id))
+ sb.append("(")
val sz = args.size
var c = 0
args.foreach(arg => {
- nsb.append(arg.id)
- nsb.append(" : ")
- nsb = pp(arg.tpe, nsb, lvl)
+ sb.append(arg.id)
+ sb.append(" : ")
+ pp(arg.tpe, lvl)
if(c < sz - 1) {
- nsb.append(", ")
+ sb.append(", ")
}
c = c + 1
})
- nsb.append(") : ")
- nsb = pp(rt, nsb, lvl)
- nsb.append(" = ")
+ sb.append(") : ")
+ pp(rt, lvl)
+ sb.append(" = ")
if(body.isDefined)
- pp(body.get, nsb, lvl)
+ pp(body.get, lvl)
else
- nsb.append("[unknown function implementation]")
+ sb.append("[unknown function implementation]")
}
case _ => sb.append("Defn?")
}
}
}
+
+class EquivalencePrettyPrinter() extends PrettyPrinter() {
+ override def idToString(id: Identifier) = id.name
+}
+
+object PrettyPrinter {
+ def apply(tree: Expr): String = {
+ val printer = new PrettyPrinter()
+ printer.pp(tree, 0)
+ printer.toString
+ }
+
+ def apply(tpe: TypeTree): String = {
+ val printer = new PrettyPrinter()
+ printer.pp(tpe, 0)
+ printer.toString
+ }
+
+ def apply(defn: Definition): String = {
+ val printer = new PrettyPrinter()
+ printer.pp(defn, 0)
+ printer.toString
+ }
+}
+
+trait PrettyPrintable {
+ def printWith(lvl: Int, printer: PrettyPrinter): Unit
+}
+
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 3809069403d45e2921a98969604f0d5ff31ef0c0..fe953a272b53085bc0c15935b32026b6854aa4f3 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -88,9 +88,11 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
solverResult match {
case _ if vctx.shouldStop.get() =>
reporter.info("=== CANCELLED ===")
+ vcInfo.time = Some(dt)
false
case None =>
+ vcInfo.time = Some(dt)
false
case Some(true) =>
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 0517d7ee3ae04aab8c889f4877410f87ae365b92..2773078e7faa0dadc8dd31f6579b4cf57aae5805 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -6,7 +6,7 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import leon.purescala.Definitions._
import leon.purescala.Extractors._
-import leon.purescala.PrettyPrinter._
+import leon.purescala.{PrettyPrinter, PrettyPrintable}
import leon.purescala.ScalaPrinter._
object Trees {
@@ -26,20 +26,15 @@ object Trees {
Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
- sb.append("{\n")
+ def printWith(lvl: Int, printer: PrettyPrinter) {
+ printer.append("{\n")
(exprs :+ last).foreach(e => {
- ind(sb, lvl+1)
- ep(e, sb, lvl+1)
- sb.append("\n")
+ printer.ind(lvl+1)
+ printer.pp(e, lvl+1)
+ printer.append("\n")
})
- ind(sb, lvl)
- sb.append("}\n")
- sb
+ printer.ind(lvl)
+ printer.append("}\n")
}
def ppScala(sb: StringBuffer, lvl: Int,
@@ -65,18 +60,13 @@ object Trees {
def extract: Option[(Expr, (Expr)=>Expr)] = {
Some((expr, Assignment(varId, _)))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
- var nsb: StringBuffer = sb
- nsb.append("(")
- nsb.append(varId.name)
- nsb.append(" = ")
- nsb = ep(expr, nsb, lvl)
- nsb.append(")")
- nsb
+
+ def printWith(lvl: Int, printer: PrettyPrinter) {
+ printer.append("(")
+ printer.append(varId.name)
+ printer.append(" = ")
+ printer.pp(expr,lvl)
+ printer.append(")")
}
def ppScala(sb: StringBuffer, lvl: Int,
@@ -105,28 +95,24 @@ object Trees {
Some((cond, body, (t1, t2) => While(t1, t2).setInvariant(this.invariant).setPosInfo(this)))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
+ def printWith(lvl: Int, printer: PrettyPrinter) {
invariant match {
case Some(inv) => {
- sb.append("\n")
- ind(sb, lvl)
- sb.append("@invariant: ")
- ep(inv, sb, lvl)
- sb.append("\n")
- ind(sb, lvl)
+ printer.append("\n")
+ printer.ind(lvl)
+ printer.append("@invariant: ")
+ printer.pp(inv, lvl)
+ printer.append("\n")
+ printer.ind(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")
+ printer.append("while(")
+ printer.pp(cond, lvl)
+ printer.append(")\n")
+ printer.ind(lvl+1)
+ printer.pp(body, lvl+1)
+ printer.append("\n")
}
def ppScala(sb: StringBuffer, lvl: Int,
@@ -160,16 +146,10 @@ object Trees {
Some((pred, (expr: Expr) => Epsilon(expr).setType(this.getType).setPosInfo(this)))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
- var nsb = sb
- nsb.append("epsilon(x" + this.posIntInfo._1 + "_" + this.posIntInfo._2 + ". ")
- nsb = ep(pred, nsb, lvl)
- nsb.append(")")
- nsb
+ 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,
@@ -183,13 +163,9 @@ object Trees {
}
case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal with PrettyPrintable with ScalaPrintable {
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
+ def printWith(lvl: Int, printer: PrettyPrinter) {
val (row, col) = pos
- sb.append("x" + row + "_" + col)
+ printer.append("x" + row + "_" + col)
}
def ppScala(sb: StringBuffer, lvl: Int,
@@ -214,19 +190,14 @@ object Trees {
Some((expr, body, (e: Expr, b: Expr) => LetVar(binders, e, b)))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
+ def printWith(lvl: Int, printer: PrettyPrinter) {
val LetVar(b,d,e) = this
- sb.append("(letvar (" + b + " := ");
- ep(d, sb, lvl)
- sb.append(") in\n")
- ind(sb, lvl+1)
- ep(e, sb, lvl+1)
- sb.append(")")
- sb
+ printer.append("(letvar (" + b + " := ");
+ printer.pp(d, lvl)
+ printer.append(") in\n")
+ printer.ind(lvl+1)
+ printer.pp(e, lvl+1)
+ printer.append(")")
}
def ppScala(sb: StringBuffer, lvl: Int,
@@ -338,18 +309,13 @@ object Trees {
}
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
- sb.append("\n")
- dp(fd, sb, lvl+1)
- sb.append("\n")
- sb.append("\n")
- ind(sb, lvl)
- ep(body, sb, lvl)
- sb
+ 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,
@@ -374,14 +340,10 @@ object Trees {
Some((expr, (e: Expr) => Waypoint(i, e)))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
- sb.append("waypoint_" + i + "(")
- ep(expr, sb, lvl)
- sb.append(")")
+ def printWith(lvl: Int, printer: PrettyPrinter) {
+ printer.append("waypoint_" + i + "(")
+ printer.pp(expr, lvl)
+ printer.append(")")
}
def ppScala(sb: StringBuffer, lvl: Int,
@@ -403,16 +365,12 @@ object Trees {
Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2))))
}
- def pp(sb: StringBuffer, lvl: Int,
- ep: (Expr, StringBuffer, Int) => StringBuffer,
- tp: (TypeTree, StringBuffer, Int) => StringBuffer,
- dp: (Definition, StringBuffer, Int) => StringBuffer
- ): StringBuffer = {
- ep(array, sb, lvl)
- sb.append("(")
- ep(index, sb, lvl)
- sb.append(") = ")
- ep(newValue, sb, lvl)
+ def printWith(lvl: Int, printer: PrettyPrinter) {
+ printer.pp(array, lvl)
+ printer.append("(")
+ printer.pp(index, lvl)
+ printer.append(") = ")
+ printer.pp(newValue, lvl)
}
}