From 4d88b0c92541bbaaa097ca82f78efafb86980efb Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Mar 2016 13:55:43 +0100
Subject: [PATCH] Pipeline.when optionally applies a pipeline
---
src/main/scala/leon/LeonPhase.scala | 2 +-
src/main/scala/leon/Main.scala | 2 +-
src/main/scala/leon/Pipeline.scala | 6 +++
.../scala/leon/utils/PreprocessingPhase.scala | 40 ++++++-------------
.../verification/VerificationSuite.scala | 4 +-
5 files changed, 22 insertions(+), 32 deletions(-)
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index db04f677e..8fb530795 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 db23f2a6a..b1e898b7d 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 de3800ca7..48f4192e3 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 3a0eaab30..1d4fed4bc 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 becde94bf..d1b252e64 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)
--
GitLab