Fix ugly mess with reports in Main

src/main/scala/leon/Main.scala

@@ -3,6 +3,7 @@
 package leon
 
 import leon.utils._
+import leon.verification.VerificationReport
 
 object Main {
 
@@ -11,7 +12,7 @@ object Main {
       frontends.scalac.ExtractionPhase,
       frontends.scalac.ClassgenPhase,
       utils.TypingPhase,
-      FileOutputPhase,
+      utils.FileOutputPhase,
       purescala.RestoreMethods,
       xlang.ArrayTransformation,
       xlang.EpsilonElimination,
@@ -192,14 +193,18 @@ object Main {
           ExtractionPhase andThen
           new PreprocessingPhase(xlangF)
 
-      val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
+      val verification =
+        VerificationPhase andThen
+        (if (xlangF) FixReportLabels else NoopPhase[VerificationReport]()) andThen
+        PrintReportPhase
+      val termination  = TerminationPhase andThen PrintReportPhase
 
       val pipeProcess: Pipeline[Program, Any] = {
         if (noopF) RestoreMethods andThen FileOutputPhase
         else if (synthesisF) SynthesisPhase
         else if (repairF) RepairPhase
-        else if (analysisF) Pipeline.both(verification, TerminationPhase)
-        else if (terminationF) TerminationPhase
+        else if (analysisF) Pipeline.both(verification, termination)
+        else if (terminationF) termination
         else if (isabelleF) IsabellePhase
         else if (evalF) EvaluationPhase
         else if (inferInvF) InferInvariantsPhase
@@ -264,23 +269,7 @@ object Main {
       val timer = ctx.timers.total.start()
 
       // Run pipeline
-      val ctx2 = pipeline.run(ctx, args.toList) match {
-        case (ctx2, (vReport: verification.VerificationReport, tReport: termination.TerminationReport)) =>
-          ctx2.reporter.info(vReport.summaryString)
-          ctx2.reporter.info(tReport.summaryString)
-          ctx2
-
-        case (ctx2, report: verification.VerificationReport) =>
-          ctx2.reporter.info(report.summaryString)
-          ctx2
-
-        case (ctx2, report: termination.TerminationReport) =>
-          ctx2.reporter.info(report.summaryString)
-          ctx2
-
-        case (ctx2, _) =>
-          ctx2
-      }
+      val (ctx2, _) = pipeline.run(ctx, args.toList)
 
       timer.stop()
 

src/main/scala/leon/termination/TerminationReport.scala

@@ -4,9 +4,10 @@ package leon
 package termination
 
 import purescala.Definitions._
+import utils.Report
 import utils.ASCIIHelpers._
 
-case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
+case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
 
   def summaryString : String = {
     var t = Table("Termination summary")

src/main/scala/leon/utils/PrintReportPhase.scala

+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package utils
+
+/** Pretty-prints a [[Report]] */
+case object PrintReportPhase extends UnitPhase[Report] {
+
+  override val description: String = "Print a Leon report"
+  override val name: String = "PrintReport"
+
+  override def apply(ctx: LeonContext, rep: Report): Unit = {
+    ctx.reporter.info(rep.summaryString)
+  }
+
+}

src/main/scala/leon/utils/Report.scala

+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.utils
+
+/** Represents a pretty-printable report */
+abstract class Report {
+  def summaryString: String
+}

src/main/scala/leon/verification/VerificationReport.scala

@@ -4,8 +4,9 @@ package leon
 package verification
 
 import purescala.Definitions.Program
+import utils.Report
 
-case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
+case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) extends Report {
   val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
     case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
   }