From 16c5eabe30990473834cd21ff77db76c7c18da1e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 31 Aug 2015 13:35:06 +0200
Subject: [PATCH] Pretty print Raw Array
---
src/main/scala/leon/solvers/RawArray.scala | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/RawArray.scala b/src/main/scala/leon/solvers/RawArray.scala
index e63dbad12..05ec28a86 100644
--- a/src/main/scala/leon/solvers/RawArray.scala
+++ b/src/main/scala/leon/solvers/RawArray.scala
@@ -3,13 +3,23 @@
package leon
package solvers
+import leon.purescala.{PrinterContext, PrettyPrintable}
+import leon.purescala.PrinterHelpers._
import purescala.Types._
import purescala.Expressions._
// Corresponds to a smt map, not a leon/scala array
-private[solvers] case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree
+private[solvers] case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree with PrettyPrintable {
+ override def printWith(implicit pctx: PrinterContext): Unit = {
+ p"RawArrayType[$from, $to]"
+ }
+}
// Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array)
-private[solvers] case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr {
+private[solvers] case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr with PrettyPrintable{
val getType = RawArrayType(keyTpe, default.getType)
+
+ override def printWith(implicit pctx: PrinterContext): Unit = {
+ p"RawArrayValue[$keyTpe](${nary(elems.toSeq, ", ")}, default = $default)"
+ }
}
--
GitLab