From 64179f7983e16aabc5cc89da99e70c48607149d0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 23:49:30 +0200
Subject: [PATCH] Revert changes I no longer need

---
 src/main/scala/leon/ArrayTransformation.scala       |  5 -----
 src/main/scala/leon/ImperativeCodeElimination.scala |  2 +-
 src/main/scala/leon/Main.scala                      | 12 +++++-------
 src/main/scala/leon/synthesis/Synthesizer.scala     |  3 +--
 4 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 38f1fce44..7d0d94458 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -98,11 +98,6 @@ object ArrayTransformation extends Pass {
       IfExpr(rc, rt, re).setType(rt.getType)
     }
 
-    case c @ Choose(args, body) =>
-      val body2 = transform(body)
-
-      Choose(args, body2).setType(c.getType).setPosInfo(c)
-
     case m @ MatchExpr(scrut, cses) => {
       val scrutRec = transform(scrut)
       val csesRec = cses.map{
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index 127e862cf..d3cd29907 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -257,9 +257,9 @@ object ImperativeCodeElimination extends Pass {
         val (argVal, argScope, argFun) = toFunction(a)
         (recons(argVal).setType(u.getType), argScope, argFun)
       }
-
       case (t: Terminal) => (t, (body: Expr) => body, Map())
 
+
       case _ => sys.error("not supported: " + expr)
     }
     //val codeRepresentation = res._2(Block(res._3.map{ case (id1, id2) => Assignment(id1, id2.toVariable)}.toSeq, res._1))
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 584caaa6f..9af1b41e7 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -4,9 +4,6 @@ import scala.tools.nsc.{Global,Settings=>NSCSettings,SubComponent,CompilerComman
 
 import purescala.Definitions.Program
 
-import synthesis.Synthesizer
-import purescala.ScalaPrinter
-
 object Main {
   import leon.{Reporter,DefaultReporter,Analysis}
 
@@ -35,10 +32,11 @@ object Main {
 
   private def defaultAction(program: Program, reporter: Reporter) : Unit = {
     Logger.debug("Default action on program: " + program, 3, "main")
-    //val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
-    //val program2 = passManager.run(program)
-    assert(program.isPure)
-    val program2 = new Synthesizer().synthesizeAll(program)
+    val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
+    val program2 = passManager.run(program)
+    assert(program2.isPure)
+    val analysis = new Analysis(program2, reporter)
+    analysis.analyse
   }
 
   private def runWithSettings(args : Array[String], settings : NSCSettings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 3258b1062..a0783f8c3 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -60,7 +60,7 @@ class Synthesizer(rules: List[Rule]) {
     solution
   }
 
-  def test1 = {
+  def test() {
     import purescala.Common._
     import purescala.Trees._
     import purescala.TypeTrees._
@@ -73,7 +73,6 @@ class Synthesizer(rules: List[Rule]) {
   }
 
   def synthesizeAll(p: Program): Program = {
-    test1
     p
   }
 }
-- 
GitLab