Pipeline.when optionally applies a pipeline

src/main/scala/leon/LeonPhase.scala

@@ -5,7 +5,6 @@ package leon
 import purescala.Definitions.Program
 
 trait LeonPhase[-F, +T] extends Pipeline[F, T] with LeonComponent {
-
   // def run(ac: LeonContext)(v: F): T
 }
 
@@ -22,6 +21,7 @@ abstract class TransformationPhase extends LeonPhase[Program, Program] {
     ctx.reporter.debug("Running transformation phase: " + name)(utils.DebugSectionLeon)
     (ctx, apply(ctx, p))
   }
+
 }
 
 abstract class UnitPhase[T] extends LeonPhase[T, T] {

src/main/scala/leon/Main.scala

@@ -195,7 +195,7 @@ object Main {
 
       val verification =
         VerificationPhase andThen
-        (if (xlangF) FixReportLabels else NoopPhase[VerificationReport]()) andThen
+        FixReportLabels.when(xlangF) andThen
         PrintReportPhase
       val termination  = TerminationPhase andThen PrintReportPhase
 

src/main/scala/leon/Pipeline.scala

@@ -13,6 +13,12 @@ abstract class Pipeline[-F, +T] {
     }
   }
 
+  def when[F2 <: F, T2 >: T](cond: Boolean)(implicit tps: F2 =:= T2): Pipeline[F2, T2] = {
+    if (cond) this else new Pipeline[F2, T2] {
+      def run(ctx: LeonContext, v: F2): (LeonContext, T2) = (ctx, v)
+    }
+  }
+
   def run(ctx: LeonContext, v: F): (LeonContext, T)
 }
 

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

@@ -16,44 +16,28 @@ class PreprocessingPhase(desugarXLang: Boolean = false, genc: Boolean = false) e
 
   override def run(ctx: LeonContext, p: Program): (LeonContext, Program) = {
 
-    def debugTrees(title: String): LeonPhase[Program, Program] = {
-      if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
-        PrintTreePhase(title)
-      } else {
-        NoopPhase[Program]()
-      }
-    }
-
-    val checkX = if (desugarXLang) {
-      NoopPhase[Program]()
-    } else {
-      NoXLangFeaturesChecking
-    }
+    def debugTrees(title: String) =
+      PrintTreePhase(title).when(ctx.reporter.isDebugEnabled(DebugSectionTrees))
 
     val pipeBegin =
-      debugTrees("Program after extraction") andThen
-      checkX                                 andThen
-      MethodLifting                          andThen
-      TypingPhase                            andThen
-      synthesis.ConversionPhase              andThen
+      debugTrees("Program after extraction")      andThen
+      NoXLangFeaturesChecking.when(!desugarXLang) andThen
+      MethodLifting                               andThen
+      TypingPhase                                 andThen
+      synthesis.ConversionPhase                   andThen
       InliningPhase
 
-    val pipeX = if (!genc && desugarXLang) {
-      // Do not desugar when generating C code
+    // Do not desugar xlang when generating C code
+    val pipeX = (
       XLangDesugaringPhase andThen
       debugTrees("Program after xlang desugaring")
-    } else {
-      NoopPhase[Program]()
-    }
+    ) when (!genc && desugarXLang)
 
-    def pipeEnd = if (genc) {
-      // No InjectAsserts, FunctionClosure and AdaptationPhase phases
-      NoopPhase[Program]()
-    } else {
+    def pipeEnd = (
       InjectAsserts  andThen
       FunctionClosure andThen
       AdaptationPhase
-    }
+    ) when (!genc)
 
     val phases =
       pipeBegin andThen

src/test/scala/leon/regression/verification/VerificationSuite.scala

@@ -37,9 +37,9 @@ trait VerificationSuite extends LeonRegressionSuite {
       new PreprocessingPhase(desugarXLang)
 
     val analysis =
-      (if (isabelle) AdaptationPhase else NoopPhase[Program]) andThen
+      AdaptationPhase.when(isabelle) andThen
       VerificationPhase andThen
-      (if (desugarXLang) FixReportLabels else NoopPhase[VerificationReport])
+      FixReportLabels.when(desugarXLang)
 
     val ctx = createLeonContext(files:_*).copy(reporter = new TestErrorReporter)