--debug=trees actually debug trees

src/main/scala/leon/Main.scala

@@ -153,6 +153,14 @@ object Main {
     val verifyF      = ctx.findOptionOrDefault(optVerify)
     val evalF        = ctx.findOptionOrDefault(optEval)
 
+    def debugTrees(title: String): LeonPhase[Program, Program] = {
+      if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
+        PrintTreePhase(title)
+      } else {
+        NoopPhase[Program]
+      }
+    }
+
     if (helpF) {
       displayVersion(ctx.reporter)
       displayHelp(ctx.reporter, error = false)
@@ -160,11 +168,15 @@ object Main {
       val pipeBegin: Pipeline[List[String], Program] =
         if (xlangF)
           ExtractionPhase andThen
-            PreprocessingPhase
+          debugTrees("Program after extraction") andThen
+          PreprocessingPhase andThen
+          debugTrees("Program after pre-processing")
         else
           ExtractionPhase andThen
-            PreprocessingPhase andThen
-            xlang.NoXLangFeaturesChecking
+          debugTrees("Program after extraction") andThen
+          PreprocessingPhase andThen
+          debugTrees("Program after pre-processing")
+          xlang.NoXLangFeaturesChecking
 
       val pipeProcess: Pipeline[Program, Any] = {
         if (noopF) RestoreMethods andThen FileOutputPhase

src/main/scala/leon/Reporter.scala

@@ -69,14 +69,18 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
   // Debugging
   private val debugMask = debugSections.foldLeft(0){ _ | _.mask }
 
+  def isDebugEnabled(implicit section: DebugSection): Boolean = {
+    (debugMask & section.mask) == section.mask
+  }
+
   def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection) = {
-    if ((debugMask & section.mask) == section.mask) {
+    if (isDebugEnabled) {
       body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
     }
   }
 
   def whenDebug(section: DebugSection)(body: (Any => Unit) => Any) {
-    if ((debugMask & section.mask) == section.mask) {
+    if (isDebugEnabled(section)) {
       body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
     }
   }

src/main/scala/leon/frontends/scalac/ExtractionPhase.scala

@@ -6,6 +6,8 @@ package frontends.scalac
 import purescala.Definitions.Program
 import purescala.Common.FreshIdentifier
 
+import purescala.ScalaPrinter
+
 import utils._
 
 import scala.tools.nsc.{Settings,CompilerCommand}

src/main/scala/leon/utils/PreprocessingPhase.scala

@@ -4,6 +4,7 @@ package leon
 package utils
 
 import purescala.Definitions.Program
+import purescala.ScalaPrinter
 
 import purescala.{MethodLifting, CompleteAbstractDefinitions}
 import synthesis.{ConvertWithOracle, ConvertHoles}
@@ -25,6 +26,7 @@ object PreprocessingPhase extends TransformationPhase {
       CompleteAbstractDefinitions   andThen
       InjectAsserts
 
+
     phases.run(ctx)(p)
   }
 }

src/main/scala/leon/utils/PrintTreePhase.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package utils
+
+
+import purescala.Definitions.Program
+
+case class PrintTreePhase(title: String) extends UnitPhase[Program] {
+
+  val name = "Print program"
+  val description = "Display: "+title
+
+  def apply(ctx: LeonContext, p: Program) {
+    ctx.reporter.info(ASCIIHelpers.title(title))
+    ctx.reporter.info(p.asString(ctx))
+  }
+}