From c8997c5be792c8a7a5c3786746191b6cccac1854 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 6 May 2015 17:44:33 +0200
Subject: [PATCH] Print types in pretty printer when asked to
---
.../scala/leon/purescala/PrettyPrinter.scala | 22 ++++++++++++++++---
.../scala/leon/purescala/PrinterOptions.scala | 9 ++++----
src/main/scala/leon/utils/DebugSections.scala | 4 +++-
3 files changed, 27 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c312ad18f..41f469eae 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -148,8 +148,16 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
- def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = tree match {
-
+ def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+ if (opts.printTypes) {
+ tree match {
+ case t: Expr =>
+ p"⟨"
+
+ case _ =>
+ }
+ }
+ tree match {
case id: Identifier =>
val name = if (opts.printUniqueIds) {
@@ -657,7 +665,15 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (tree: PrettyPrintable) => tree.printWith(ctx)
case _ => sb.append("Tree? (" + tree.getClass + ")")
-
+ }
+ if (opts.printTypes) {
+ tree match {
+ case t: Expr=>
+ p" : ${t.getType} ⟩"
+
+ case _ =>
+ }
+ }
}
object FcallMethodInvocation {
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 0a9cb6d77..6a95b265d 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -8,20 +8,21 @@ import utils._
case class PrinterOptions (
baseIndent: Int = 0,
printPositions: Boolean = false,
- printTypes: Boolean = false,
- printUniqueIds: Boolean = false
+ printUniqueIds: Boolean = false,
+ printTypes: Boolean = false
)
object PrinterOptions {
def fromContext(ctx: LeonContext): PrinterOptions = {
val debugTrees = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTrees
+ val debugTypes = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTypes
val debugPositions = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionPositions
PrinterOptions(
baseIndent = 0,
printPositions = debugPositions,
- printTypes = debugTrees,
- printUniqueIds = debugTrees
+ printUniqueIds = debugTrees,
+ printTypes = debugTypes
)
}
}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 7562edf59..9ccabc241 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -21,6 +21,7 @@ case object DebugSectionEvaluation extends DebugSection("eval", 1 << 9
case object DebugSectionRepair extends DebugSection("repair", 1 << 10)
case object DebugSectionLeon extends DebugSection("leon", 1 << 11)
case object DebugSectionXLang extends DebugSection("xlang", 1 << 12)
+case object DebugSectionTypes extends DebugSection("types", 1 << 13)
object DebugSections {
val all = Set[DebugSection](
@@ -36,6 +37,7 @@ object DebugSections {
DebugSectionEvaluation,
DebugSectionRepair,
DebugSectionLeon,
- DebugSectionXLang
+ DebugSectionXLang,
+ DebugSectionTypes
)
}
--
GitLab