diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c8a1f666b4f462a05a61498d29151b9cf5038a78..fb8831f64e929c4755fdf551dc28bd75a5b4702c 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -11,566 +11,463 @@ import Definitions._
import utils._
import java.lang.StringBuffer
+import PrinterHelpers._
+
+case class PrinterContext(
+ current: Tree,
+ parent: Option[Tree],
+ lvl: Int,
+ printer: PrettyPrinter
+)
+
+object PrinterHelpers {
+ implicit class Printable(val f: PrinterContext => Any) extends AnyVal {
+ def print(ctx: PrinterContext) = f(ctx)
+ }
-/** 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(opts: PrinterOptions, val sb: StringBuffer = new StringBuffer) {
- override def toString = sb.toString
+ implicit class PrintingHelper(val sc: StringContext) extends AnyVal {
- def append(str: String) {
- sb.append(str)
- }
+ def p(args: Any*)(implicit ctx: PrinterContext): Unit = {
+ val printer = ctx.printer
+ val sb = printer.sb
+
+ var strings = sc.parts.iterator
+ var expressions = args.iterator
+
+ var extraInd = 0;
+ var firstElem = true;
+
+ while(strings.hasNext) {
+ val s = strings.next.stripMargin
+
+ // Compute indentation
+ var start = s.lastIndexOf('\n')
+ if(start >= 0 || firstElem) {
+ var i = start+1;
+ while(i < s.length && s(i) == ' ') {
+ i += 1
+ }
+ extraInd = (i-start-1)/2
+ }
+
+ firstElem = false
+
+ // Make sure new lines are also indented
+ sb.append(s.replaceAll("\n", "\n"+(" "*ctx.lvl)))
+
+ var nctx = ctx.copy(lvl = ctx.lvl + extraInd)
+
+ if (expressions.hasNext) {
+ val e = expressions.next
+
+ e match {
+ case (t1, t2) =>
+ nary(Seq(t1, t2), " -> ").print(nctx)
+
+ case ts: Seq[Any] =>
+ nary(ts).print(nctx)
+
+ case t: Tree =>
+ nctx = nctx.copy(current = t, parent = Some(nctx.current))
+ printer.pp(t)(nctx)
- def ind(implicit lvl: Int) {
- sb.append(" " * lvl)
+ case p: Printable =>
+ p.print(nctx)
+
+ case e =>
+ sb.append(e.toString)
+ }
+ }
+ }
+ }
}
- def nl(implicit lvl: Int) {
- sb.append("\n")
- ind(lvl)
+
+ def nary(ls: Seq[Any], sep: String = ", "): Printable = {
+ val strs = List("") ::: List.fill(ls.size-1)(sep)
+
+ implicit pctx: PrinterContext =>
+ new StringContext(strs: _*).p(ls: _*)
}
- // EXPRESSIONS
- // all expressions are printed in-line
- def ppUnary(expr: Tree, op1: String, op2: String)(implicit parent: Option[Tree], lvl: Int) {
- sb.append(op1)
- pp(expr, parent)
- sb.append(op2)
+ def typed(t: Tree with Typed): Printable = {
+ implicit pctx: PrinterContext =>
+ p"$t: ${t.getType}"
}
- def ppBinary(left: Tree, right: Tree, op: String)(implicit parent: Option[Tree], lvl: Int) {
- sb.append("(")
- pp(left, parent)
- sb.append(op)
- pp(right, parent)
- sb.append(")")
+ def typed(ts: Seq[Tree with Typed]): Printable = {
+ nary(ts.map(typed))
}
+}
+
+/** 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(opts: PrinterOptions, val sb: StringBuffer = new StringBuffer) {
- def ppNary(exprs: Seq[Tree], pre: String, op: String, post: String)(implicit parent: Option[Tree], lvl: Int) {
- sb.append(pre)
- val sz = exprs.size
- var c = 0
+ override def toString = sb.toString
- exprs.foreach(ex => {
- pp(ex, parent) ; c += 1 ; if(c < sz) sb.append(op)
- })
+ protected def optP(body: => Any)(implicit ctx: PrinterContext) = {
+ if (requiresParentheses(ctx.current, ctx.parent)) {
+ sb.append("(")
+ body
+ sb.append(")")
+ } else {
+ body
+ }
+ }
- sb.append(post)
+ protected def optB(body: => Any)(implicit ctx: PrinterContext) = {
+ if (requiresBraces(ctx.current, ctx.parent)) {
+ sb.append("{")
+ body
+ sb.append("}")
+ } else {
+ body
+ }
}
- def pp(tree: Tree, parent: Option[Tree])(implicit lvl: Int): Unit = {
- implicit val p = Some(tree)
+ def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
case id: Identifier =>
if (opts.printUniqueIds) {
- sb.append(id.uniqueName)
+ p"${id.uniqueName}"
} else {
- sb.append(id.toString)
+ p"${id.toString}"
}
case Variable(id) =>
- if (opts.printTypes) {
- sb.append("(")
- pp(id, p)
- sb.append(": ")
- pp(id.getType, p)
- sb.append(")")
- } else {
- pp(id, p)
- }
+ p"$id"
case LetTuple(bs,d,e) =>
- sb.append("(let ")
- ppNary(bs, "(", ",", " :=");
- pp(d, p)
- sb.append(") in")
- nl(lvl+1)
- pp(e, p)(lvl+1)
- sb.append(")")
+ p"""|val ($bs) = $d;
+ |$e"""
case Let(b,d,e) =>
- sb.append("(let (")
- pp(b, p)
- sb.append(" := ");
- pp(d, p)
- sb.append(") in")
- nl(lvl+1)
- pp(e, p)(lvl+1)
- sb.append(")")
+ p"""|val $b = $d;
+ |$e"""
case LetDef(fd,body) =>
- sb.append("\n")
- pp(fd, p)(lvl+1)
- sb.append("\n")
- sb.append("\n")
- nl
- pp(body, p)
-
- case And(exprs) => ppNary(exprs, "(", " \u2227 ", ")") // \land
- case Or(exprs) => ppNary(exprs, "(", " \u2228 ", ")") // \lor
- case Not(Equals(l, r)) => ppBinary(l, r, " \u2260 ") // \neq
- case Iff(l,r) => ppBinary(l, r, " <=> ")
- case Implies(l,r) => ppBinary(l, r, " ==> ")
- case UMinus(expr) => ppUnary(expr, "-(", ")")
- case Equals(l,r) => ppBinary(l, r, " == ")
- case IntLiteral(v) => sb.append(v)
- case BooleanLiteral(v) => sb.append(v)
- case StringLiteral(s) => sb.append("\"" + s + "\"")
- case UnitLiteral() => sb.append("()")
- case GenericValue(tp, id) =>
- pp(tp, p)
- sb.append("#"+id)
-
- case t@Tuple(exprs) => ppNary(exprs, "(", ", ", ")")
- case s@TupleSelect(t, i) =>
- pp(t, p)
- sb.append("._" + i)
-
- case h @ Hole(o) =>
- sb.append("???[")
- pp(h.getType, p)
- sb.append("](")
- pp(o, p)
- sb.append(")")
-
- case c@Choose(vars, pred) =>
- sb.append("choose(")
- ppNary(vars, "", ", ", "")
- sb.append(" => ")
- pp(pred, p)
- sb.append(")")
+ p"""|$fd
+ |$body"""
+
+ case Require(pre, body) =>
+ p"""|require($pre)
+ |$body"""
+
+ case Assert(const, Some(err), body) =>
+ p"""|assert($const, "$err")
+ |$body"""
+
+ case Assert(const, None, body) =>
+ p"""|assert($const)
+ |$body"""
+
+ case Ensuring(body, id, post) =>
+ p"""|{
+ | $body
+ |} ensuring {
+ | (${typed(id)}) => $post
+ |}"""
case CaseClass(cct, args) =>
- pp(cct, p)
if (cct.classDef.isCaseObject) {
- ppNary(args, "", "", "")
+ p"$cct"
} else {
- ppNary(args, "(", ", ", ")")
+ p"$cct($args)"
}
- case CaseClassInstanceOf(cct, e) =>
- pp(e, p)
- sb.append(".isInstanceOf[")
- pp(cct, p)
- sb.append("]")
-
- case CaseClassSelector(_, cc, id) =>
- pp(cc, p)
- sb.append(".")
- pp(id, p)
-
+ case And(exprs) => optP { p"${nary(exprs, " && ")}" }
+ case Or(exprs) => optP { p"${nary(exprs, "| || ")}" }
+ case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
+ case Iff(l,r) => optP { p"$l <=> $r" }
+ case Implies(l,r) => optP { p"$l ==> $r" }
+ case UMinus(expr) => p"-$expr"
+ case Equals(l,r) => optP { p"$l == $r" }
+ case IntLiteral(v) => p"$v"
+ case BooleanLiteral(v) => p"$v"
+ case StringLiteral(s) => p""""$s""""
+ case UnitLiteral() => p"()"
+ case GenericValue(tp, id) => p"$tp#$id"
+ 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 CaseClassSelector(_, e, id) => p"$e.$id"
case MethodInvocation(rec, _, tfd, args) =>
- pp(rec, p)
- sb.append(".")
- pp(tfd.id, p)
+ p"$rec.${tfd.id}"
if (tfd.tps.nonEmpty) {
- ppNary(tfd.tps, "[", ",", "]")
+ p"[${tfd.tps}]"
}
- ppNary(args, "(", ", ", ")")
+ p"($args)"
case FunctionInvocation(tfd, args) =>
- pp(tfd.id, p)
+ p"${tfd.id}"
if (tfd.tps.nonEmpty) {
- ppNary(tfd.tps, "[", ",", "]")
+ p"[${tfd.tps}]"
}
- ppNary(args, "(", ", ", ")")
-
- case Plus(l,r) => ppBinary(l, r, " + ")
- case Minus(l,r) => ppBinary(l, r, " - ")
- case Times(l,r) => ppBinary(l, r, " * ")
- case Division(l,r) => ppBinary(l, r, " / ")
- case Modulo(l,r) => ppBinary(l, r, " % ")
- case LessThan(l,r) => ppBinary(l, r, " < ")
- case GreaterThan(l,r) => ppBinary(l, r, " > ")
- case LessEquals(l,r) => ppBinary(l, r, " \u2264 ") // \leq
- case GreaterEquals(l,r) => ppBinary(l, r, " \u2265 ") // \geq
- case FiniteSet(rs) => if(rs.isEmpty) sb.append("\u2205") /* Ø */ else ppNary(rs, "{", ", ", "}")
- case FiniteMultiset(rs) => ppNary(rs, "{|", ", ", "|}")
- case EmptyMultiset(_) => sb.append("\u2205") // Ø
- case Not(ElementOfSet(s,e)) => ppBinary(s, e, " \u2209 ") // \notin
- case ElementOfSet(s,e) => ppBinary(s, e, " \u2208 ") // \in
- case SubsetOf(l,r) => ppBinary(l, r, " \u2286 ") // \subseteq
- case Not(SubsetOf(l,r)) => ppBinary(l, r, " \u2288 ") // \notsubseteq
- case SetMin(s) => pp(s, p); sb.append(".min")
- case SetMax(s) => pp(s, p); sb.append(".max")
- case SetUnion(l,r) => ppBinary(l, r, " \u222A ") // \cup
- case MultisetUnion(l,r) => ppBinary(l, r, " \u222A ") // \cup
- case MapUnion(l,r) => ppBinary(l, r, " \u222A ") // \cup
- case SetDifference(l,r) => ppBinary(l, r, " \\ ")
- case MultisetDifference(l,r) => ppBinary(l, r, " \\ ")
- case SetIntersection(l,r) => ppBinary(l, r, " \u2229 ") // \cap
- case MultisetIntersection(l,r) => ppBinary(l, r, " \u2229 ") // \cap
- case SetCardinality(t) => ppUnary(t, "|", "|")
- case MultisetCardinality(t) => ppUnary(t, "|", "|")
- case MultisetPlus(l,r) => ppBinary(l, r, " \u228E ") // U+
- case MultisetToSet(e) => pp(e, p); sb.append(".toSet")
+ p"($args)"
+
+ case Plus(l,r) => optP { p"$l + $r" }
+ case Minus(l,r) => optP { p"$l - $r" }
+ case Times(l,r) => optP { p"$l * $r" }
+ case Division(l,r) => optP { p"$l / $r" }
+ case Modulo(l,r) => optP { p"$l % $r" }
+ case LessThan(l,r) => optP { p"$l < $r" }
+ case GreaterThan(l,r) => optP { p"$l > $r" }
+ case LessEquals(l,r) => optP { p"$l <= $r" }
+ case GreaterEquals(l,r) => optP { p"$l >= $r" }
+ case FiniteSet(rs) => p"{$rs}"
+ case FiniteMultiset(rs) => p"{|$rs|)"
+ case EmptyMultiset(_) => p"\u2205"
+ case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
+ case ElementOfSet(e,s) => p"$e \u2208 $s"
+ case SubsetOf(l,r) => p"$l \u2286 $r"
+ case Not(SubsetOf(l,r)) => p"$l \u2288 $r"
+ case SetMin(s) => p"$s.min"
+ case SetMax(s) => p"$s.max"
+ case SetUnion(l,r) => p"$l \u222A $r"
+ case MultisetUnion(l,r) => p"$l \u222A $r"
+ case MapUnion(l,r) => p"$l \u222A $r"
+ case SetDifference(l,r) => p"$l \\ $r"
+ case MultisetDifference(l,r) => p"$l \\ $r"
+ case SetIntersection(l,r) => p"$l \u2229 $r"
+ case MultisetIntersection(l,r) => p"$l \u2229 $r"
+ case SetCardinality(s) => p"|$s|"
+ case MultisetCardinality(s) => p"|$s|"
+ case MultisetPlus(l,r) => p"$l \u228E $r"
+ case MultisetToSet(e) => p"$e.toSet"
+ case MapGet(m,k) => p"$m($k)"
+ case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
+ case ArrayLength(a) => p"$a.length"
+ case ArrayClone(a) => p"$a.clone"
+ case ArrayFill(size, v) => p"Array.fill($size)($v)"
+ case ArrayMake(v) => p"Array.make($v)"
+ case ArraySelect(a, i) => p"$a($i)"
+ case ArrayUpdated(a, i, v) => p"$a.updated($i, $v)"
+ case FiniteArray(exprs) => p"Array($exprs)"
+ case Distinct(exprs) => p"distinct($exprs)"
+ case Not(expr) => p"\u00AC$expr"
+ case ValDef(id, tpe) => p"${typed(id)}"
+ case This(_) => p"this"
+ case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
+ case TypeParameterDef(tp) => p"$tp"
+ case TypeParameter(id) => p"$id"
+
case FiniteMap(rs) =>
- sb.append("{")
- val sz = rs.size
- var c = 0
- rs.foreach{case (k, v) => {
- pp(k, p); sb.append(" -> "); pp(v, p); c += 1 ; if(c < sz) sb.append(", ")
- }}
- sb.append("}")
-
- case MapGet(m,k) =>
- pp(m, p)
- ppNary(Seq(k), "(", ",", ")")
-
- case MapIsDefinedAt(m,k) =>
- pp(m, p)
- sb.append(".isDefinedAt")
- ppNary(Seq(k), "(", ",", ")")
-
- case ArrayLength(a) =>
- pp(a, p)
- sb.append(".length")
-
- case ArrayClone(a) =>
- pp(a, p)
- sb.append(".clone")
-
- case fill@ArrayFill(size, v) =>
- sb.append("Array.fill(")
- pp(size, p)
- sb.append(")(")
- pp(v, p)
- sb.append(")")
-
- case am@ArrayMake(v) =>
- sb.append("Array.make(")
- pp(v, p)
- sb.append(")")
-
- case sel@ArraySelect(ar, i) =>
- pp(ar, p)
- sb.append("(")
- pp(i, p)
- sb.append(")")
-
- case up@ArrayUpdated(ar, i, v) =>
- pp(ar, p)
- sb.append(".updated(")
- pp(i, p)
- sb.append(", ")
- pp(v, p)
- sb.append(")")
-
- case FiniteArray(exprs) =>
- ppNary(exprs, "Array(", ", ", ")")
-
- case Distinct(exprs) =>
- sb.append("distinct")
- ppNary(exprs, "(", ", ", ")")
-
+ p"{$rs}"
+
+
case IfExpr(c, t, e) =>
- sb.append("if (")
- pp(c, p)
- sb.append(")")
- nl(lvl+1)
- pp(t, p)(lvl+1)
- nl
- sb.append("else")
- nl(lvl+1)
- pp(e, p)(lvl+1)
-
- case mex @ MatchExpr(s, csc) =>
- pp(s, p)
- sb.append(" match {\n")
-
- csc.foreach(cs => {
- nl(lvl+1)
- pp(cs, p)
- sb.append("\n")
- })
- nl(lvl)
- sb.append("}")
-
- case Not(expr) => ppUnary(expr, "\u00AC(", ")") // \neg
-
- case e @ Error(desc) =>
- sb.append("error(\"" + desc + "\")[")
- pp(e.getType, p)
- sb.append("]")
-
- case (tree: PrettyPrintable) => tree.printWith(this)
+ optP {
+ p"""|if ($c) {
+ | $t
+ |} else {
+ | $e
+ |}"""
+ }
+
+ case MatchExpr(s, csc) =>
+ optP {
+ p"""|$s match {
+ | ${nary(csc, "\n")}
+ |}"""
+ }
// Cases
case SimpleCase(pat, rhs) =>
- sb.append("case ")
- pp(pat, p)
- sb.append(" =>\n")
- ind(lvl+1)
- pp(rhs, p)(lvl+1)
+ p"""|case $pat =>
+ | $rhs"""
+
case GuardedCase(pat, guard, rhs) =>
- sb.append("case ")
- pp(pat, p)
- sb.append(" if ")
- pp(guard, p)
- sb.append(" =>\n")
- ind(lvl+1)
- pp(rhs, p)(lvl+1)
+ p"""|case $pat if $guard =>
+ | $rhs"""
// Patterns
- case CaseClassPattern(bndr, cct, subps) =>
- bndr.foreach(b => sb.append(b + " @ "))
- pp(cct, p)
- sb.append("(")
- var c = 0
- val sz = subps.size
- subps.foreach(sp => {
- pp(sp, p)
- if(c < sz - 1)
- sb.append(", ")
- c = c + 1
- })
- sb.append(")")
-
- case WildcardPattern(None) => sb.append("_")
- case WildcardPattern(Some(id)) => pp(id.toVariable, p)
- case InstanceOfPattern(bndr, cct) =>
- bndr.foreach(b => sb.append(b + " : "))
- pp(cct, p)
-
- case TuplePattern(bndr, subPatterns) =>
- bndr.foreach(b => sb.append(b + " @ "))
- sb.append("(")
- subPatterns.init.foreach(pat => {
- pp(pat, p)
- sb.append(", ")
- })
- pp(subPatterns.last, p)
- sb.append(")")
+ case WildcardPattern(None) => p"_"
+ case WildcardPattern(Some(id)) => p"$id"
+ case CaseClassPattern(ob, cct, subps) =>
+ ob.foreach { b => p"$b @ " }
+ p"${cct.id}($subps)"
- // Types
- case Untyped => sb.append("<untyped>")
- case UnitType => sb.append("Unit")
- case Int32Type => sb.append("Int")
- case BooleanType => sb.append("Boolean")
- case ArrayType(bt) =>
- sb.append("Array[")
- pp(bt, p)
- sb.append("]")
- case SetType(bt) =>
- sb.append("Set[")
- pp(bt, p)
- sb.append("]")
- case MapType(ft,tt) =>
- sb.append("Map[")
- pp(ft, p)
- sb.append(",")
- pp(tt, p)
- sb.append("]")
- case MultisetType(bt) =>
- sb.append("Multiset[")
- pp(bt, p)
- sb.append("]")
- case TupleType(tpes) => ppNary(tpes, "(", ", ", ")")
- case FunctionType(fts, tt) =>
- if (fts.size > 1) {
- ppNary(fts, "(", ", ", ")")
- } else if (fts.size == 1) {
- pp(fts.head, p)
- }
- sb.append(" => ")
- pp(tt, p)
+ case InstanceOfPattern(ob, cct) =>
+ ob.foreach { b => p"$b : " }
+ p"$cct"
+ case TuplePattern(ob, subps) =>
+ ob.foreach { b => p"$b @ " }
+ p"($subps)"
+
+ // Types
+ case Untyped => p"<untyped>"
+ case UnitType => p"Unit"
+ case Int32Type => p"Int"
+ case BooleanType => p"Boolean"
+ case ArrayType(bt) => p"Array[$bt]"
+ case SetType(bt) => p"Set[$bt]"
+ case MapType(ft,tt) => p"Map[$ft, $tt]"
+ case MultisetType(bt) => p"Multiset[$bt]"
+ case TupleType(tpes) => p"($tpes)"
+ case FunctionType(fts, tt) => p"($fts) => $tt"
case c: ClassType =>
- pp(c.classDef.id, p)
+ p"${c.classDef.id}"
if (c.tps.nonEmpty) {
- ppNary(c.tps, "[", ",", "]")
+ p"[${c.tps}]"
}
// Definitions
case Program(id, modules) =>
- assert(lvl == 0)
- sb.append("package ")
- pp(id, p)
- sb.append(" {\n")
- modules.foreach {
- m => pp(m, p)(lvl+1)
- }
- sb.append("}\n")
+ p"""|package $id {
+ | ${nary(modules, "\n\n")}
+ |}"""
case ModuleDef(id, defs) =>
- nl
- sb.append("object ")
- pp(id, p)
- sb.append(" {")
-
- var c = 0
- val sz = defs.size
-
- defs.foreach(df => {
- pp(df, p)(lvl+1)
- if(c < sz - 1) {
- sb.append("\n\n")
- }
- c = c + 1
- })
-
- nl
- sb.append("}\n")
+ p"""|object $id {
+ | ${nary(defs, "\n\n")}
+ |}"""
case acd @ AbstractClassDef(id, tparams, parent) =>
- sb.append("sealed abstract class ")
- pp(id, p)
+ p"abstract class $id"
if (tparams.nonEmpty) {
- ppNary(tparams, "[", ",", "]")
+ p"[$tparams]"
}
parent.foreach{ par =>
- sb.append(" extends ")
- pp(par.id, p)
+ p" extends ${par.id}"
}
if (acd.methods.nonEmpty) {
- sb.append(" {\n")
- for (md <- acd.methods) {
- ind(lvl+1)
- pp(md, p)(lvl+1)
- sb.append("\n\n")
- }
- ind
- sb.append("}")
+ p"""| {
+ | ${nary(acd.methods, "\n\n")}
+ |}"""
}
case ccd @ CaseClassDef(id, tparams, parent, isObj) =>
if (isObj) {
- sb.append("case object ")
+ p"case object $id"
} else {
- sb.append("case class ")
+ p"case class $id"
}
- pp(id, p)
-
if (tparams.nonEmpty) {
- ppNary(tparams, "[", ", ", "]")
+ p"[$tparams]"
}
if (!isObj) {
- ppNary(ccd.fields, "(", ", ", ")")
+ p"(${ccd.fields})"
}
parent.foreach{ par =>
- sb.append(" extends ")
- pp(par.id, p)
+ p" extends ${par.id}"
}
if (ccd.methods.nonEmpty) {
- sb.append(" {\n")
- for (md <- ccd.methods) {
- ind(lvl+1)
- pp(md, p)(lvl+1)
- sb.append("\n\n")
- }
- ind
- sb.append("}")
+ p"""| {
+ | ${nary(ccd.methods, "\n\n")}
+ |}"""
}
- case th: This =>
- sb.append("this")
-
- case tfd: TypedFunDef =>
- sb.append("typed def ")
- pp(tfd.id, p)
- ppNary(tfd.tps, "[", ", ", "]")
-
case fd: FunDef =>
for(a <- fd.annotations) {
- ind
- sb.append("@" + a + "\n")
+ p"""|@$a
+ |"""
}
- fd.precondition.foreach(prec => {
- ind
- sb.append("@pre : ")
- pp(prec, p)(lvl)
- sb.append("\n")
- })
-
- fd.postcondition.foreach{ case (id, postc) => {
- ind
- sb.append("@post: ")
- pp(id, p)
- sb.append(" => ")
- pp(postc, p)(lvl)
- sb.append("\n")
- }}
-
- ind
- sb.append("def ")
- pp(fd.id, p)
- sb.append("(")
-
- val sz = fd.params.size
- var c = 0
-
- fd.params.foreach(arg => {
- sb.append(arg.id)
- sb.append(" : ")
- pp(arg.tpe, p)
-
- if(c < sz - 1) {
- sb.append(", ")
- }
- c = c + 1
- })
- sb.append(") : ")
- pp(fd.returnType, p)
- sb.append(" = ")
+ p"""|def ${fd.id}(${fd.params}): ${fd.returnType} = {
+ |"""
+
+ fd.precondition.foreach { case pre =>
+ p"""| require($pre)
+ |"""
+ }
+
fd.body match {
- case Some(body) =>
- pp(body, p)(lvl)
+ case Some(b) =>
+ p" $b"
case None =>
- sb.append("[unknown function implementation]")
+ p"???"
}
- case TypeParameterDef(tp) =>
- pp(tp, p)
+ p"""|
+ |}"""
+
+ fd.postcondition.foreach { case (id, post) =>
+ p"""| ensuring {
+ | (${typed(id)}) => $post
+ |}"""
+ }
- case TypeParameter(id) =>
- pp(id, p)
+ case (tree: PrettyPrintable) => tree.printWith(ctx)
case _ => sb.append("Tree? (" + tree.getClass + ")")
}
- if (opts.printPositions) {
- ppos(tree.getPos)
- }
}
- def ppos(p: Position) = p match {
- case op: OffsetPosition =>
- sb.append("@"+op.toString)
- case rp: RangePosition =>
- sb.append("@"+rp.focusBegin.toString+"--"+rp.focusEnd.toString)
- case _ =>
+ def requiresBraces(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
+ case (pa: PrettyPrintable, _) => pa.printRequiresBraces(within)
+ case (_, None) => false
+ case (_: Require, Some(_: Ensuring)) => false
+ case (_: Require, _) => true
+ case (_: Assert, Some(_: Definition)) => true
+ case (_, Some(_: Definition)) => false
+ case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef)) => false
+ case (_, _) => true
+ }
+
+ def precedence(ex: Expr): Int = ex match {
+ case (pa: PrettyPrintable) => pa.printPrecedence
+ case (_: ElementOfSet) => 0
+ case (_: Or) => 1
+ case (_: And) => 3
+ case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
+ case (_: Equals | _: Iff | _: Not) => 5
+ case (_: Plus | _: Minus | _: SetUnion| _: SetDifference) => 6
+ case (_: Times | _: Division | _: Modulo) => 7
+ case _ => 7
+ }
+
+ def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
+ case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
+ case (_, None) => false
+ case (_, Some(_: Ensuring)) => false
+ case (_, Some(_: Assert)) => false
+ case (_, Some(_: Require)) => false
+ case (_, Some(_: Definition)) => false
+ case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef | _: IfExpr)) => false
+ case (_, Some(_: FunctionInvocation)) => false
+ case (ie: IfExpr, _) => true
+ case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
+ case (_, _) => true
}
}
trait PrettyPrintable {
self: Tree =>
- def printWith(printer: PrettyPrinter)(implicit lvl: Int): Unit
+ def printWith(implicit pctx: PrinterContext): Unit
+
+ def printPrecedence: Int = 1000
+ def printRequiresParentheses(within: Option[Tree]): Boolean = false
+ def printRequiresBraces(within: Option[Tree]): Boolean = false
}
class EquivalencePrettyPrinter(opts: PrinterOptions) extends PrettyPrinter(opts) {
- override def pp(tree: Tree, parent: Option[Tree])(implicit lvl: Int): Unit = {
+ override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
case id: Identifier =>
- sb.append(id.name)
+ p"""${id.name}"""
case _ =>
- super.pp(tree, parent)
+ super.pp(tree)
}
}
}
@@ -580,7 +477,8 @@ abstract class PrettyPrinterFactory {
def apply(tree: Tree, opts: PrinterOptions = PrinterOptions()): String = {
val printer = create(opts)
- printer.pp(tree, None)(opts.baseIndent)
+ val ctx = PrinterContext(tree, None, opts.baseIndent, printer)
+ printer.pp(tree)(ctx)
printer.toString
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 2d1202d73b6248efebf4ad13061f3933f3b9a35d..755e48af7f9034dfe12814256bc25326c7130c41 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -8,375 +8,31 @@ import Trees._
import TypeTrees._
import Definitions._
+import PrinterHelpers._
+
/** This pretty-printer only print valid scala syntax */
class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, sb) {
- import Common._
- import Trees._
- import TypeTrees._
- import Definitions._
-
- import java.lang.StringBuffer
-
- override def ppBinary(left: Tree, right: Tree, op: String)(implicit parent: Option[Tree], lvl: Int) {
- pp(left, parent)
- sb.append(op)
- pp(right, parent)
- }
-
- // EXPRESSIONS
- // all expressions are printed in-line
- override def pp(tree: Tree, parent: Option[Tree])(implicit lvl: Int): Unit = {
- implicit val p = Some(tree)
-
- def optParentheses(body: => Unit) {
- val rp = requiresParentheses(tree, parent)
- if (rp) sb.append("(")
- body
- if (rp) sb.append(")")
- }
-
- def optBraces(body: Int => Unit) {
- val rp = requiresBraces(tree, parent)
- if (rp) {
- sb.append("{\n")
- ind(lvl+1)
-
- body(lvl+1)
-
- sb.append("\n")
- ind(lvl)
- sb.append("}\n")
- } else {
- body(lvl)
- }
- }
-
- var printPos = opts.printPositions
+ override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
- case LetTuple(ids,d,e) =>
- optBraces { implicit lvl =>
- sb.append("val (" )
- for (((id, tpe), i) <- ids.map(id => (id, id.getType)).zipWithIndex) {
- pp(id, p)
- sb.append(": ")
- pp(tpe, p)
- if (i != ids.size-1) {
- sb.append(", ")
- }
- }
- sb.append(") = ")
- pp(d, p)
- sb.append("\n")
- ind
- pp(e, p)
- sb.append("\n")
- }
-
- case Let(b,d,e) =>
- optBraces { implicit lvl =>
- sb.append("val " + b + " = ")
- pp(d, p)
- sb.append("\n")
- ind
- pp(e, p)
- sb.append("\n")
- }
-
- case LetDef(fd, body) =>
- optBraces { implicit lvl =>
- pp(fd, p)
- sb.append("\n")
- sb.append("\n")
- ind
- pp(body, p)
- }
-
- case And(exprs) => optParentheses { ppNary(exprs, "", " && ", "") }
- case Or(exprs) => optParentheses { ppNary(exprs, "", " || ", "") }
- case Not(Equals(l, r)) => optParentheses { ppBinary(l, r, " != ") }
- case UMinus(expr) => ppUnary(expr, "-(", ")")
- case Equals(l,r) => optParentheses { ppBinary(l, r, " == ") }
-
- 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), p)
- case Iff(l,r) => optParentheses { ppBinary(l, r, " == ") }
-
- case Tuple(exprs) => ppNary(exprs, "(", ", ", ")")
- case TupleSelect(t, i) =>
- pp(t, p)
- sb.append("._" + i)
-
- case Plus(l,r) => optParentheses { ppBinary(l, r, " + ") }
- case Minus(l,r) => optParentheses { ppBinary(l, r, " - ") }
- case Times(l,r) => optParentheses { ppBinary(l, r, " * ") }
- case Division(l,r) => optParentheses { ppBinary(l, r, " / ") }
- case Modulo(l,r) => optParentheses { ppBinary(l, r, " % ") }
- case LessThan(l,r) => optParentheses { ppBinary(l, r, " < ") }
- case GreaterThan(l,r) => optParentheses { ppBinary(l, r, " > ") }
- case LessEquals(l,r) => optParentheses { ppBinary(l, r, " <= ") }
- case GreaterEquals(l,r) => optParentheses { ppBinary(l, r, " >= ") }
- case fs @ FiniteSet(rs) =>
- if (rs.isEmpty) {
- fs.getType match {
- case SetType(b) =>
- sb.append("Set[")
- pp(b, p)
- sb.append("]()")
- case _ =>
- sb.append("Set()")
- }
- } else {
- ppNary(rs, "Set(", ", ", ")")
- }
- case FiniteMultiset(rs) => ppNary(rs, "{|", ", ", "|}")
- case EmptyMultiset(_) => sys.error("Not Valid Scala")
- case ElementOfSet(e, s) => optParentheses { ppBinary(s, e, " contains ") }
- case SetUnion(l,r) => optParentheses { ppBinary(l, r, " ++ ") }
- case SetDifference(l,r) => optParentheses { ppBinary(l, r, " -- ") }
- case SetIntersection(l,r) => optParentheses { ppBinary(l, r, " & ") }
- case SetMin(s) =>
- pp(s, p)
- sb.append(".min")
- case SetMax(s) =>
- pp(s, p)
- sb.append(".max")
- case SetCardinality(t) => ppUnary(t, "", ".size")
- case FiniteMap(rs) =>
- sb.append("{")
- val sz = rs.size
- var c = 0
- rs.foreach{case (k, v) => {
- pp(k, p); sb.append(" -> "); pp(v, p); c += 1 ; if(c < sz) sb.append(", ")
- }}
- sb.append("}")
-
- case MapGet(m,k) =>
- pp(m, p)
- ppNary(Seq(k), "(", ",", ")")
-
- case MapIsDefinedAt(m,k) => {
- pp(m, p)
- sb.append(".isDefinedAt")
- ppNary(Seq(k), "(", ",", ")")
- }
- case ArrayLength(a) =>
- pp(a, p)
- sb.append(".length")
-
- case ArrayClone(a) =>
- pp(a, p)
- sb.append(".clone")
-
- case ArrayFill(size, v) =>
- sb.append("Array.fill(")
- pp(size, p)
- sb.append(")(")
- pp(v, p)
- sb.append(")")
-
- case ArraySelect(ar, i) =>
- pp(ar, p)
- sb.append("(")
- pp(i, p)
- sb.append(")")
-
- case ArrayUpdated(ar, i, v) =>
- pp(ar, p)
- sb.append(".updated(")
- pp(i, p)
- sb.append(", ")
- pp(v, p)
- sb.append(")")
-
- case FiniteArray(exprs) =>
- ppNary(exprs, "Array(", ", ", ")")
-
- case Distinct(exprs) =>
- sb.append("distinct")
- ppNary(exprs, "(", ", ", ")")
-
- case IfExpr(c, t, e) =>
- optParentheses {
- sb.append("if (")
- pp(c, p)
- sb.append(") {\n")
- ind(lvl+1)
- pp(t, p)(lvl+1)
- sb.append("\n")
- ind(lvl)
- sb.append("} else {\n")
- ind(lvl+1)
- pp(e, p)(lvl+1)
- sb.append("\n")
- ind(lvl)
- sb.append("}")
- }
-
- case Choose(ids, pred) =>
- optParentheses {
- sb.append("choose { (")
- for (((id, tpe), i) <- ids.map(id => (id, id.getType)).zipWithIndex) {
- pp(id, p)
- sb.append(": ")
- pp(tpe, p)
- if (i != ids.size-1) {
- sb.append(", ")
- }
- }
- sb.append(") =>\n")
- ind(lvl+1)
- pp(pred, p)(lvl+1)
- sb.append("\n")
- ind(lvl)
- sb.append("}")
- }
-
- case mex @ MatchExpr(s, csc) => {
- optParentheses {
- pp(s, p)
- sb.append(" match {\n")
-
- csc.foreach { cs =>
- ind(lvl+1)
- pp(cs, p)(lvl+1)
- sb.append("\n")
- }
-
- ind(lvl)
- sb.append("}")
- }
- }
-
- case Not(expr) => sb.append("!"); optParentheses { pp(expr, p) }
-
- case e @ Error(desc) => {
- sb.append("leon.lang.error[")
- pp(e.getType, p)
- sb.append("](\"" + desc + "\")")
- }
-
- case (expr: PrettyPrintable) => expr.printWith(this)
-
- // Definitions
- case Program(id, modules) =>
- ppNary(modules, "", "\n", "")
-
- case ModuleDef(id, defs) =>
- sb.append("object ")
- pp(id, p)
- sb.append(" {\n")
-
- var c = 0
- val sz = defs.size
-
- defs.foreach(df => {
- ind(lvl+1)
- pp(df, p)(lvl+1)
- if(c < sz - 1) {
- sb.append("\n\n")
- }
- c = c + 1
- })
-
- sb.append("\n")
- ind(lvl)
- sb.append("}\n")
-
- case vd: ValDef =>
- pp(vd.id, p)
- sb.append(": ")
- pp(vd.tpe, p)
-
- case fd: FunDef =>
- sb.append("def ")
- pp(fd.id, p)
-
- if (fd.tparams.nonEmpty) {
- ppNary(fd.tparams, "[", ", ", "]")
- }
-
- ppNary(fd.params, "(", ", ", ")")
-
- sb.append(": ")
- pp(fd.returnType, p)
- sb.append(" = {\n")
- ind(lvl+1)
-
- fd.precondition match {
- case None =>
- case Some(prec) =>
- sb.append("require(")
- pp(prec, p)(lvl+1)
- sb.append(");\n")
- ind(lvl+1)
- }
-
- fd.body match {
- case Some(body) =>
- pp(body, p)(lvl+1)
- case None =>
- sb.append("???")
- }
-
- sb.append("\n")
- ind
-
- fd.postcondition match {
- case None =>
- sb.append("}")
-
- case Some((id, postc)) =>
- sb.append("} ensuring { ")
- pp(Variable(id), p)
- sb.append(" => ")
- pp(postc, p)
- sb.append(" }")
- }
+ case Not(Equals(l, r)) => p"$l != $r"
+ case Iff(l,r) => p"$l == $r"
+ case Implies(l,r) => pp(Or(Not(l), r))
+ case Choose(vars, pred) => p"choose(${typed(vars)} => $pred)" // TODO
+ case ElementOfSet(e,s) => p"$s.contains(e)"
+ case SetUnion(l,r) => p"$l ++ $r"
+ case MapUnion(l,r) => p"$l ++ $r"
+ case SetDifference(l,r) => p"$l -- $r"
+ case SetIntersection(l,r) => p"$l & $r"
+ case SetCardinality(s) => p"$s.size"
+ case FiniteArray(exprs) => p"Array($exprs)"
+ case Distinct(exprs) => p"distinct($exprs)"
+ case Not(expr) => p"!$expr"
case _ =>
- super.pp(tree, parent)(lvl)
- // Parent will already print
- printPos = false
- }
-
- if (printPos) {
- ppos(tree.getPos)
+ super.pp(tree)
}
}
-
- private def requiresBraces(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
- case (_, None) => false
- case (_, Some(_: Definition)) => false
- case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef)) => false
- case (_, _) => true
- }
-
- private def precedence(ex: Expr): Int = ex match {
- case (_: ElementOfSet) => 0
- case (_: Or) => 1
- case (_: And) => 3
- case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
- case (_: Equals | _: Iff | _: Not) => 5
- case (_: Plus | _: Minus | _: SetUnion| _: SetDifference) => 6
- case (_: Times | _: Division | _: Modulo) => 7
- case _ => 7
- }
-
- private def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
- case (_, None) => false
- case (_, Some(_: Definition)) => false
- case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef | _: IfExpr)) => false
- case (_, Some(_: FunctionInvocation)) => false
- case (ie: IfExpr, _) => true
- case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
- case (_, _) => true
- }
}
object ScalaPrinter extends PrettyPrinterFactory {
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 899ce89edddad73f17c035f08fe65ade78485b49..4936b748c5fae3315bedc3288b7da440def0d43f 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -8,6 +8,7 @@ import purescala.Common.Tree
import purescala.Definitions.FunDef
import purescala.ScalaPrinter
import purescala.PrinterOptions
+import purescala.PrinterContext
import leon.utils.RangePosition
@@ -61,7 +62,7 @@ class FileInterface(reporter: Reporter) {
val indent = lineChars.takeWhile(_ == ' ').size
val p = new ScalaPrinter(PrinterOptions())
- p.pp(toTree, Some(fromTree))(indent/2)
+ p.pp(toTree)(PrinterContext(toTree, Some(fromTree), indent/2, p))
before + p.toString + after
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 3532030ae7ab8860157b3d040cfa6187c75225a3..6da2d30f7d87b032de6e8ef1ed16849302baca3d 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -8,10 +8,11 @@ import purescala.TypeTrees._
import purescala.Trees._
import purescala.Definitions._
import purescala.Extractors._
-import purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter}
+import purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter, PrinterContext}
import utils._
object Trees {
+ import purescala.PrinterHelpers._
private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
sb.append(" " * lvl)
@@ -24,15 +25,10 @@ object Trees {
Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- printer.append("{\n")
- (exprs :+ last).foreach(e => {
- printer.ind(lvl+1)
- printer.pp(e, Some(this))(lvl+1)
- printer.append("\n")
- })
- printer.ind(lvl)
- printer.append("}\n")
+ def printWith(implicit pctx: PrinterContext) {
+ p"""|{
+ | ${nary(exprs :+ last, "\n")}
+ |}"""
}
val fixedType = last.getType
@@ -45,12 +41,8 @@ object Trees {
Some((expr, Assignment(varId, _)))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- printer.append("(")
- printer.append(varId.name)
- printer.append(" = ")
- printer.pp(expr, Some(this))
- printer.append(")")
+ def printWith(implicit pctx: PrinterContext) {
+ p"$varId = $expr;"
}
}
@@ -66,24 +58,17 @@ object Trees {
Some((cond, body, (t1, t2) => While(t1, t2).setInvariant(this.invariant).setPos(this)))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
+ def printWith(implicit pctx: PrinterContext) {
invariant match {
- case Some(inv) => {
- printer.append("\n")
- printer.ind
- printer.append("@invariant: ")
- printer.pp(inv, Some(this))
- printer.append("\n")
- printer.ind
- }
+ case Some(inv) =>
+ p"""|@invariant($inv)
+ |"""
case None =>
}
- printer.append("while(")
- printer.pp(cond, Some(this))
- printer.append(")\n")
- printer.ind(lvl+1)
- printer.pp(body, Some(this))(lvl+1)
- printer.append("\n")
+
+ p"""|while($cond) {
+ | $body
+ |}"""
}
}
@@ -92,20 +77,15 @@ object Trees {
Some((pred, (expr: Expr) => Epsilon(expr).setType(this.getType).setPos(this)))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- printer match {
- case _ =>
- printer.append("epsilon(x" + this.getPos.line + "_" + this.getPos.col + ". ")
- printer.pp(pred, Some(this))
- printer.append(")")
- }
+ def printWith(implicit pctx: PrinterContext) {
+ p"epsilon(x${getPos.line}_${getPos.col}. $pred)"
}
}
case class EpsilonVariable(pos: Position) extends Expr with Terminal with PrettyPrintable{
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- printer.append("x" + pos.line + "_" + pos.col)
+ def printWith(implicit pctx: PrinterContext) {
+ p"x${pos.line}_${pos.col}"
}
}
@@ -120,30 +100,11 @@ object Trees {
Some((expr, body, (e: Expr, b: Expr) => LetVar(binders, e, b)))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- 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, Some(this))(lvl+1)
- printer.append("\n")
- printer.ind(lvl+1)
- printer.pp(e, Some(this))(lvl+1)
- printer.nl
- printer.append("}")
- printer.nl
-
- case _ =>
- val LetVar(b,d,e) = this
- printer.append("(letvar (" + b + " := ");
- printer.pp(d, Some(this))
- printer.append(") in\n")
- printer.ind(lvl+1)
- printer.pp(e, Some(this))(lvl+1)
- printer.append(")")
- }
+ def printWith(implicit pctx: PrinterContext) {
+ p"""|locally {
+ | var $binder = $value
+ | $body
+ |}"""
}
}
@@ -152,18 +113,11 @@ object Trees {
Some((expr, (e: Expr) => Waypoint(i, e)))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- printer match {
- case _ =>
- printer.append("waypoint_" + i + "(")
- printer.pp(expr, Some(this))
- printer.append(")")
- }
+ def printWith(implicit pctx: PrinterContext) {
+ p"waypoint_$i($expr)"
}
}
- //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 FixedType with NAryExtractable with PrettyPrintable {
val fixedType = UnitType
@@ -172,12 +126,8 @@ object Trees {
Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2))))
}
- def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- printer.pp(array, Some(this))
- printer.append("(")
- printer.pp(index, Some(this))
- printer.append(") = ")
- printer.pp(newValue, Some(this))
+ def printWith(implicit pctx: PrinterContext) {
+ p"$array($index) = $newValue"
}
}