diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala index db04f677eff7e1916892ca1f47bc1ce2b524e828..8fb5307955305fb6612cd7b3933fcda553cd0fe7 100644 --- a/src/main/scala/leon/LeonPhase.scala +++ b/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] { diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala index db23f2a6ace4ca8d9e0a3bbc5e85dc2a4e6377f0..b1e898b7d8b0f3e7a3230a3deebfe5f8fe58aa03 100644 --- a/src/main/scala/leon/Main.scala +++ b/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 diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala index de3800ca780376a641bb5e843d067d57bdb0c6a8..48f4192e3058548af64ddab922e84c4149299b61 100644 --- a/src/main/scala/leon/Pipeline.scala +++ b/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) } diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala index 3a0eaab30abd16f107f13decdccc3f335914a604..1d4fed4bc3d1a0d439e336603a2f5b2e9c5af50c 100644 --- a/src/main/scala/leon/utils/PreprocessingPhase.scala +++ b/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 diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala index becde94bf2072a37fa7ddc643d20da800a3c2970..d1b252e64e48fe03dd2e82759a08df3d896a2bb7 100644 --- a/src/test/scala/leon/regression/verification/VerificationSuite.scala +++ b/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)