TransformationPhase -> UnitPhase, when possible

src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala

@@ -7,20 +7,18 @@ import Common._
 import Definitions._
 import Expressions._
 
-object CompleteAbstractDefinitions extends TransformationPhase {
+object CompleteAbstractDefinitions extends UnitPhase[Program] {
 
   val name = "Materialize abstract functions"
   val description = "Inject fake choose-like body in abstract definitions"
 
-  def apply(ctx: LeonContext, program: Program): Program = {
+  def apply(ctx: LeonContext, program: Program) = {
     for (u <- program.units; m <- u.modules; fd <- m.definedFunctions; if fd.body.isEmpty) {
       val post = fd.postcondition getOrElse (
         Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType))), BooleanLiteral(true))
       )
       fd.body = Some(Choose(post))
     }
-    // Translation is in-place
-    program
   }
 
 }

src/main/scala/leon/xlang/ArrayTransformation.scala

@@ -2,7 +2,7 @@
 
 package leon.xlang
 
-import leon.TransformationPhase
+import leon.UnitPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
@@ -11,16 +11,15 @@ import leon.xlang.Expressions._
 import leon.purescala.Extractors._
 import leon.purescala.Types._
 
-object ArrayTransformation extends TransformationPhase {
+object ArrayTransformation extends UnitPhase[Program] {
 
   val name = "Array Transformation"
   val description = "Add bound checking for array access and remove array update with side effect"
 
-  def apply(ctx: LeonContext, pgm: Program): Program = {
+  def apply(ctx: LeonContext, pgm: Program) = {
     pgm.definedFunctions.foreach(fd => {
       fd.fullBody = transform(fd.fullBody)(Map())
     })
-    pgm
   }
 
   def transform(expr: Expr)(implicit env: Map[Identifier, Identifier]): Expr = (expr match {

src/main/scala/leon/xlang/EpsilonElimination.scala

@@ -2,24 +2,22 @@
 
 package leon.xlang
 
-import leon.TransformationPhase
-import leon.LeonContext
+import leon.{UnitPhase, TransformationPhase, LeonContext}
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Expressions._
 import leon.purescala.ExprOps._
 import leon.xlang.Expressions._
 
-object EpsilonElimination extends TransformationPhase {
+object EpsilonElimination extends UnitPhase[Program] {
 
   val name = "Epsilon Elimination"
   val description = "Remove all epsilons from the program"
 
-  def apply(ctx: LeonContext, pgm: Program): Program = {
+  def apply(ctx: LeonContext, pgm: Program) = {
 
-    val allFuns = pgm.definedFunctions
     for {
-      fd <- allFuns
+      fd <- pgm.definedFunctions
       body <- fd.body
     } {
       val newBody = postMap{
@@ -37,7 +35,6 @@ object EpsilonElimination extends TransformationPhase {
       }(body)
       fd.body = Some(newBody)
     }
-    pgm
   }
 
 }

src/main/scala/leon/xlang/XLangAnalysisPhase.scala

@@ -16,10 +16,10 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
 
   def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
 
-    val pgm1 = ArrayTransformation(ctx, pgm)
-    val pgm2 = EpsilonElimination(ctx, pgm1)
-    val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
-    val pgm4 = purescala.FunctionClosure.run(ctx)(pgm3)
+    ArrayTransformation(ctx, pgm) // In-place
+    EpsilonElimination(ctx, pgm)  // In-place
+    val (pgm1, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm)
+    val pgm2 = purescala.FunctionClosure.run(ctx)(pgm1)
 
     def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
       case Some(nested) => // could have been a LetDef originally
@@ -28,7 +28,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
     }
 
     var subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
-    pgm4.definedFunctions.foreach { fd => fd.owner match {
+    pgm2.definedFunctions.foreach { fd => fd.owner match {
       case Some(p : FunDef) =>
         subFunctionsOf += p -> (subFunctionsOf(p) + fd)
       case _ =>
@@ -54,7 +54,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
       case opt => opt
     }
 
-    val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
+    val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm2)
     completeVerificationReport(vr, functionWasLoop)
   }