no xlang in PrettyPrinter

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 = {

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)
+    }
   }
 }