From b2360e549c31d9d0fa7aa97af259c69e47be54c9 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 16 Mar 2015 16:33:08 +0100
Subject: [PATCH] Remove unused imports
---
src/main/scala/leon/LeonContext.scala | 1 -
src/main/scala/leon/Reporter.scala | 5 ----
.../scala/leon/codegen/CodeGenPhase.scala | 5 ----
.../leon/codegen/CompiledExpression.scala | 6 -----
.../leon/codegen/runtime/GenericValues.scala | 10 +------
.../scala/leon/datagen/NaiveDataGen.scala | 1 -
.../leon/evaluators/CodeGenEvaluator.scala | 2 --
.../frontends/scalac/AddTypeAnnotations.scala | 2 --
.../frontends/scalac/LeonExtraction.scala | 4 ---
.../leon/frontends/scalac/SaveImports.scala | 1 -
.../CompleteAbstractDefinitions.scala | 3 ---
.../scala/leon/purescala/Constructors.scala | 2 --
.../scala/leon/purescala/Definitions.scala | 2 --
.../leon/purescala/FunctionMapping.scala | 2 --
.../scala/leon/purescala/PrettyPrinter.scala | 27 ++++++++-----------
.../scala/leon/purescala/ScalaPrinter.scala | 4 ---
.../leon/purescala/ScopeSimplifier.scala | 3 ---
.../leon/purescala/TreeNormalizations.scala | 2 --
src/main/scala/leon/purescala/Trees.scala | 1 -
.../scala/leon/repair/RepairCostModel.scala | 7 -----
src/main/scala/leon/repair/RepairPhase.scala | 7 -----
.../leon/repair/RepairTrackingEvaluator.scala | 1 -
.../leon/solvers/combinators/DNFSolver.scala | 2 --
.../solvers/combinators/PortfolioSolver.scala | 5 ----
.../solvers/combinators/RewritingSolver.scala | 3 ---
.../solvers/combinators/UnrollingSolver.scala | 1 -
.../leon/solvers/smtlib/SMTLIBTarget.scala | 1 -
.../scala/leon/synthesis/ChooseInfo.scala | 2 --
.../leon/synthesis/ConvertWithOracles.scala | 1 -
.../scala/leon/synthesis/FileInterface.scala | 2 +-
.../leon/synthesis/PartialSolution.scala | 3 ---
src/main/scala/leon/synthesis/Problem.scala | 1 -
src/main/scala/leon/synthesis/Rules.scala | 1 -
.../scala/leon/synthesis/SearchContext.scala | 1 -
src/main/scala/leon/synthesis/Solution.scala | 3 ---
.../scala/leon/synthesis/SynthesisPhase.scala | 3 ---
.../leon/synthesis/graph/DotGenerator.scala | 2 --
.../scala/leon/synthesis/graph/Search.scala | 3 ---
.../scala/leon/synthesis/rules/Assert.scala | 1 -
.../leon/synthesis/rules/BottomUpTegis.scala | 12 ---------
.../leon/synthesis/rules/CaseSplit.scala | 2 --
.../scala/leon/synthesis/rules/Cegis.scala | 16 -----------
.../scala/leon/synthesis/rules/Cegless.scala | 3 ---
.../leon/synthesis/rules/DetupleOutput.scala | 2 --
.../leon/synthesis/rules/Disunification.scala | 2 --
.../leon/synthesis/rules/EqualitySplit.scala | 4 ---
.../scala/leon/synthesis/rules/Ground.scala | 2 --
.../scala/leon/synthesis/rules/IfSplit.scala | 1 -
.../synthesis/rules/InequalitySplit.scala | 4 ---
.../leon/synthesis/rules/InlineHoles.scala | 4 ---
.../leon/synthesis/rules/InnerCaseSplit.scala | 2 --
.../synthesis/rules/OptimisticGround.scala | 2 --
.../synthesis/rules/OptimisticInjection.scala | 4 ---
.../synthesis/rules/SelectiveInlining.scala | 4 ---
.../scala/leon/synthesis/rules/Tegis.scala | 8 ------
.../leon/synthesis/rules/TegisLike.scala | 5 ----
.../scala/leon/synthesis/rules/Tegless.scala | 4 ---
.../synthesis/rules/UnconstrainedOutput.scala | 1 -
.../leon/synthesis/rules/Unification.scala | 1 -
.../leon/synthesis/rules/UnusedInput.scala | 2 --
.../scala/leon/synthesis/utils/Helpers.scala | 1 -
.../SynthesisProblemExtractionPhase.scala | 4 ---
.../leon/termination/ComponentProcessor.scala | 1 -
.../leon/termination/RecursionProcessor.scala | 1 -
.../leon/termination/RelationBuilder.scala | 2 --
.../leon/termination/RelationComparator.scala | 4 ---
.../scala/leon/utils/OracleTraverser.scala | 1 -
.../leon/verification/DefaultTactic.scala | 2 --
.../leon/verification/InjectAsserts.scala | 1 -
.../verification/VerificationContext.scala | 2 --
.../leon/xlang/ArrayTransformation.scala | 1 -
.../scala/leon/xlang/EpsilonElimination.scala | 1 -
.../leon/xlang/NoXLangFeaturesChecking.scala | 4 ---
src/main/scala/leon/xlang/TreeOps.scala | 4 ---
src/main/scala/leon/xlang/Trees.scala | 3 +--
75 files changed, 14 insertions(+), 236 deletions(-)
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 8eea31aa7..adeb162f4 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -4,7 +4,6 @@ package leon
import leon.utils._
-import purescala.Definitions.Program
import java.io.File
/** Everything that is part of a compilation unit, except the actual program tree.
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index cc39c108e..9bd1a983f 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -4,11 +4,6 @@ package leon
import utils._
-import purescala.Definitions.Definition
-import purescala.Trees.Expr
-import purescala.PrettyPrinter
-import scala.annotation.implicitNotFound
-
abstract class Reporter(settings: Settings) {
abstract class Severity
diff --git a/src/main/scala/leon/codegen/CodeGenPhase.scala b/src/main/scala/leon/codegen/CodeGenPhase.scala
index 2d9abd0b2..8acf1fa61 100644
--- a/src/main/scala/leon/codegen/CodeGenPhase.scala
+++ b/src/main/scala/leon/codegen/CodeGenPhase.scala
@@ -5,13 +5,8 @@ package codegen
import scala.util.control.NonFatal
-import purescala.Common._
import purescala.Definitions._
-import cafebabe._
-import cafebabe.ClassFileTypes.U2
-import cafebabe.Flags._
-
object CodeGenPhase extends LeonPhase[Program,CompilationResult] {
val name = "CodeGen"
val description = "Compiles a Leon program into Java methods"
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index dc2f9767a..78cca61d1 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -4,15 +4,9 @@ package leon
package codegen
import purescala.Common._
-import purescala.Definitions._
import purescala.Trees._
-import purescala.TypeTrees._
import cafebabe._
-import cafebabe.AbstractByteCodes._
-import cafebabe.ByteCodes._
-import cafebabe.ClassFileTypes._
-import cafebabe.Flags._
import runtime.{LeonCodeGenRuntimeMonitor => LM }
diff --git a/src/main/scala/leon/codegen/runtime/GenericValues.scala b/src/main/scala/leon/codegen/runtime/GenericValues.scala
index 790f35a5c..dee6b1850 100644
--- a/src/main/scala/leon/codegen/runtime/GenericValues.scala
+++ b/src/main/scala/leon/codegen/runtime/GenericValues.scala
@@ -3,17 +3,9 @@
package leon
package codegen.runtime
-import utils._
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees.{Tuple => LeonTuple, _}
-import purescala.TreeOps.valuateWithModel
-import purescala.TypeTrees._
-
+import purescala.Trees.GenericValue
import scala.collection.immutable.{Map => ScalaMap}
-import synthesis._
-
object GenericValues {
private[this] var counter = 0;
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 212b3ba22..b44777872 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -5,7 +5,6 @@ package datagen
import purescala.Common._
import purescala.Trees._
-import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
import utils.StreamUtils._
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index e13a0d216..c21315468 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -5,9 +5,7 @@ package evaluators
import purescala.Common._
import purescala.Definitions._
-import purescala.TreeOps._
import purescala.Trees._
-import purescala.TypeTrees._
import codegen.CompilationUnit
import codegen.CodeGenParams
diff --git a/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala b/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala
index 3bfe34f49..98f616034 100644
--- a/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala
+++ b/src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala
@@ -4,11 +4,9 @@ package leon
package frontends.scalac
import scala.tools.nsc._
-import scala.tools.nsc.plugins._
trait AddTypeAnnotations extends SubComponent with ASTExtractors {
import global._
- import global.definitions._
import ExtractorHelpers._
val phaseName = "addtypeannotations"
diff --git a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
index 36ba8587d..acb427180 100644
--- a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
@@ -4,10 +4,6 @@ package leon
package frontends.scalac
import scala.tools.nsc._
-import scala.tools.nsc.plugins._
-
-import purescala.Definitions.Program
-import purescala.Definitions.{ModuleDef => LeonModuleDef, _}
trait LeonExtraction extends SubComponent with CodeExtraction {
import global._
diff --git a/src/main/scala/leon/frontends/scalac/SaveImports.scala b/src/main/scala/leon/frontends/scalac/SaveImports.scala
index dc941d197..fddabd521 100644
--- a/src/main/scala/leon/frontends/scalac/SaveImports.scala
+++ b/src/main/scala/leon/frontends/scalac/SaveImports.scala
@@ -12,7 +12,6 @@ import utils.{Position => LeonPosition, RangePosition => LeonRangePosition, Offs
trait SaveImports extends SubComponent {
import global._
- import global.definitions._
val phaseName = "imports"
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
index 5d67a2286..c3e2ba46c 100644
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
@@ -6,9 +6,6 @@ package purescala
import Common._
import Definitions._
import Trees._
-import Extractors._
-import TreeOps._
-import TypeTrees._
object CompleteAbstractDefinitions extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 34e634e12..8f1b5f57f 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -3,8 +3,6 @@
package leon
package purescala
-import utils._
-
object Constructors {
import Trees._
import TreeOps._
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index f056671da..95942afe5 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -10,8 +10,6 @@ object Definitions {
import Common._
import Trees._
import TreeOps._
- import DefOps._
- import Extractors._
import TypeTrees._
import TypeTreeOps._
diff --git a/src/main/scala/leon/purescala/FunctionMapping.scala b/src/main/scala/leon/purescala/FunctionMapping.scala
index 8efa25c86..c11c80a39 100644
--- a/src/main/scala/leon/purescala/FunctionMapping.scala
+++ b/src/main/scala/leon/purescala/FunctionMapping.scala
@@ -3,10 +3,8 @@
package leon
package purescala
-import Common._
import Definitions._
import Trees._
-import Extractors._
import TreeOps._
import TypeTrees._
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index f43546154..b82f1e71e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -3,21 +3,16 @@
package leon
package purescala
-import Common._
-import Trees._
-import TypeTrees._
-import Definitions._
-import DefOps._
-
-import utils._
-
-import java.lang.StringBuffer
-import PrinterHelpers._
-import TreeOps.{isListLiteral, simplestValue, variablesOf}
-import TypeTreeOps.leastUpperBound
-import Extractors._
-
-import synthesis.Witnesses._
+import leon.purescala.Common._
+import leon.purescala.DefOps._
+import leon.purescala.Definitions._
+import leon.purescala.Extractors._
+import leon.purescala.PrinterHelpers._
+import leon.purescala.TreeOps.{isListLiteral, simplestValue}
+import leon.purescala.Trees._
+import leon.purescala.TypeTreeOps.leastUpperBound
+import leon.purescala.TypeTrees._
+import leon.synthesis.Witnesses._
case class PrinterContext(
current: Tree,
@@ -556,7 +551,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
|"""
case PackageImport(pack) =>
- import DefOps._
+ import leon.purescala.DefOps._
val newPack = ( for (
scope <- ctx.scope;
unit <- unitOf(scope);
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 666f728d6..e38418c0a 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -3,10 +3,6 @@
package leon
package purescala
-import Common._
-import Trees._
-import TypeTrees._
-import Definitions._
import Constructors._
import Extractors._
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 525c5f26d..74cb530c7 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -6,10 +6,7 @@ package purescala
import Common._
import Definitions._
import Trees._
-import TypeTrees._
-import TreeOps._
import Extractors._
-import Constructors._
class ScopeSimplifier extends Transformer {
case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 3558ad598..73bc15aef 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -6,10 +6,8 @@ package purescala
object TreeNormalizations {
import Common._
import TypeTrees._
- import Definitions._
import Trees._
import TreeOps._
- import Extractors._
/* TODO: we should add CNF and DNF at least */
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 5773f1716..57e85d91f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -8,7 +8,6 @@ import utils._
/** AST definitions for Pure Scala. */
object Trees {
import Common._
- import TreeOps.variablesOf
import TypeTrees._
import TypeTreeOps._
import Definitions._
diff --git a/src/main/scala/leon/repair/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
index 25c19cc2a..43e25dcb0 100644
--- a/src/main/scala/leon/repair/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -3,17 +3,10 @@
package leon
package repair
import synthesis._
-import Witnesses._
import synthesis.rules._
import repair.rules._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.DefOps._
-import purescala.TreeOps._
-import purescala.Extractors._
-
case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("+cm.name+")") {
import graph._
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index c6e1e4466..d030327b5 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -3,16 +3,9 @@
package leon
package repair
-import purescala.Common._
import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Constructors._
import purescala.DefOps._
-import java.io.FileWriter
-
object RepairPhase extends LeonPhase[Program, Program] {
val name = "Repair"
val description = "Repairing"
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 22c4cb271..4446f786c 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -8,7 +8,6 @@ import leon.purescala.TypeTrees._
import leon.purescala.Definitions._
import leon.LeonContext
import leon.evaluators.RecursiveEvaluator
-import leon.synthesis._
/**
* This evaluator tracks all dependencies between function calls (.fullCallGraph)
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 755e9a6e2..1fc16886f 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -5,11 +5,9 @@ package solvers
package combinators
import purescala.Common._
-import purescala.Definitions._
import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.TypeTrees._
class DNFSolver(val context: LeonContext,
underlyings: SolverFactory[Solver]) extends Solver {
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index f9fd8a7d4..942f75191 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -5,17 +5,12 @@ package solvers
package combinators
import purescala.Common._
-import purescala.Definitions._
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
import utils.Interruptible
import scala.concurrent._
import scala.concurrent.duration._
-import scala.collection.mutable.{Map=>MutableMap}
-
import ExecutionContext.Implicits.global
class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, solvers: Seq[SolverFactory[S]])
diff --git a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
index c7579ef3b..5b089883b 100644
--- a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
@@ -5,10 +5,7 @@ package solvers
package combinators
import purescala.Common._
-import purescala.Definitions._
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
abstract class RewritingSolver[+S <: Solver, T](underlying: S) {
val context = underlying.context
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 6ff60b5de..3239bdd97 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -9,7 +9,6 @@ import purescala.Definitions._
import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.TypeTrees._
import solvers.templates._
import utils.Interruptible
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 91a074d5e..74cf6d031 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -2,7 +2,6 @@ package leon
package solvers
package smtlib
-import utils.Interruptible
import purescala._
import Common._
import Trees.{Assert => _, _}
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 841247dd2..72ac87a52 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -3,12 +3,10 @@
package leon
package synthesis
-import purescala.Common._
import purescala.Definitions._
import purescala.Constructors._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.DefOps._
import Witnesses._
case class ChooseInfo(fd: FunDef,
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
index 8b130c7ad..e35c6e581 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracles.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
@@ -3,7 +3,6 @@
package leon
package synthesis
-import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
import purescala.Definitions._
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index cdabf6eb6..0e81f6f6c 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -5,7 +5,7 @@ package synthesis
import purescala.Trees._
import purescala.Common.Tree
-import purescala.Definitions.{Definition,FunDef}
+import purescala.Definitions.Definition
import purescala.ScalaPrinter
import purescala.PrinterOptions
import purescala.PrinterContext
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index f76355b78..2f05eb1a7 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -4,9 +4,6 @@ package leon
package synthesis
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.DefOps._
-import purescala.Common._
import graph._
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 71c12af51..297b3210f 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -4,7 +4,6 @@ package leon
package synthesis
import leon.purescala.Trees._
-import leon.purescala.Definitions._
import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
import leon.purescala.Common._
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 3ae642fc3..a4a0686c1 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -7,7 +7,6 @@ import purescala.Common._
import purescala.Trees._
import purescala.TypeTrees._
import purescala.TreeOps._
-import purescala.Constructors._
import rules._
abstract class Rule(val name: String) extends RuleDSL {
diff --git a/src/main/scala/leon/synthesis/SearchContext.scala b/src/main/scala/leon/synthesis/SearchContext.scala
index 853314f08..531ae4514 100644
--- a/src/main/scala/leon/synthesis/SearchContext.scala
+++ b/src/main/scala/leon/synthesis/SearchContext.scala
@@ -3,7 +3,6 @@
package leon
package synthesis
-import purescala.Trees.Choose
import graph._
/**
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index bc93ce0c7..2eb1e73f1 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -8,10 +8,7 @@ import purescala.Trees._
import purescala.TypeTrees.{TypeTree,TupleType}
import purescala.Definitions._
import purescala.TreeOps._
-import purescala.ScopeSimplifier
import purescala.Constructors._
-import solvers.z3._
-import solvers._
import leon.utils.Simplifiers
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 0944851f5..a6f794ca7 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,10 +3,7 @@ package leon
package synthesis
import purescala.TreeOps._
-import solvers.z3._
-import purescala.Trees._
-import purescala.Common._
import purescala.ScalaPrinter
import purescala.Definitions.{Program, FunDef}
import leon.utils.ASCIIHelpers
diff --git a/src/main/scala/leon/synthesis/graph/DotGenerator.scala b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
index 4694044cc..c4ee0d758 100644
--- a/src/main/scala/leon/synthesis/graph/DotGenerator.scala
+++ b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
@@ -2,8 +2,6 @@ package leon.synthesis.graph
import java.io.{File, FileWriter, BufferedWriter}
-import leon.synthesis.Histogram
-
class DotGenerator(g: Graph) {
private[this] var _nextID = 0
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index 82e3e1175..b5f37629f 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -4,9 +4,6 @@ package graph
import scala.annotation.tailrec
-import purescala.Trees.Choose
-import leon.utils.StreamUtils.cartesianProduct
-
import scala.collection.mutable.ArrayBuffer
import leon.utils.Interruptible
import java.util.concurrent.atomic.AtomicBoolean
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 3e11b4d65..eff8465aa 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -4,7 +4,6 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 1259a50a7..d08a1e077 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -4,23 +4,11 @@ package leon
package synthesis
package rules
-import solvers._
-import solvers.z3._
-
import purescala.Trees._
import purescala.Common._
-import purescala.Definitions._
import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.TypeTreeOps._
-import purescala.Extractors._
-import purescala.ScalaPrinter
import purescala.Constructors._
-
-import scala.collection.mutable.{Map=>MutableMap, ArrayBuffer}
-
import evaluators._
-import datagen._
import codegen.CodeGenParams
import utils._
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index b09dbd703..203a35b7d 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -5,8 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object CaseSplit extends Rule("Case-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 6d989c4ef..4cf48c204 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -4,23 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.Definitions._
-import utils.Helpers._
-import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.DefOps._
-import purescala.TypeTreeOps._
-import purescala.Extractors._
-import purescala.ScalaPrinter
-
-import scala.collection.mutable.{Map=>MutableMap}
-
-import evaluators._
-import datagen._
-import codegen.CodeGenParams
import utils._
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala
index 914003fec..893657d4c 100644
--- a/src/main/scala/leon/synthesis/rules/Cegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegless.scala
@@ -4,11 +4,8 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index 4cb861624..1ec3858fc 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -8,8 +8,6 @@ import purescala.Trees._
import purescala.Definitions._
import purescala.Common._
import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object DetupleOutput extends Rule("Detuple Out") {
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 53c69e252..812a0c119 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -5,8 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 0a3be81d4..087c9d9d1 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -5,10 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 43d2ead62..a2a6f9955 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -6,9 +6,7 @@ package rules
import solvers._
import purescala.Trees._
-import purescala.TypeTrees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object Ground extends Rule("Ground") {
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index dff14901a..ea115e42c 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -6,7 +6,6 @@ package rules
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object IfSplit extends Rule("If-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index a71574fda..f6edb6bb2 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -6,10 +6,6 @@ package rules
import purescala.Trees._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index 7e1cd1611..de4c61916 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -6,16 +6,12 @@ package rules
import scala.annotation.tailrec
-import leon.utils._
-
import solvers._
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Extractors._
import purescala.Constructors._
case object InlineHoles extends Rule("Inline-Holes") {
diff --git a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
index 637bdeeb9..f87751e0d 100644
--- a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
@@ -5,8 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object InnerCaseSplit extends Rule("Inner-Case-Split"){
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index bc46805ae..13d79428e 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -5,9 +5,7 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TypeTrees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
index d6ccc416f..299bdeb0f 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
@@ -4,13 +4,9 @@ package leon
package synthesis
package rules
-import purescala.Common._
import purescala.Trees._
import purescala.Extractors._
import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
case object OptimisticInjection extends Rule("Opt. Injection") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
index e79d857d4..b8877d783 100644
--- a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
@@ -4,13 +4,9 @@ package leon
package synthesis
package rules
-import purescala.Common._
import purescala.Trees._
import purescala.Extractors._
import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
case object SelectiveInlining extends Rule("Sel. Inlining") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index 273e170ec..06bf87c60 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -4,15 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.TypeTrees._
-import purescala.Constructors._
-
-import evaluators._
-import datagen._
-
import utils._
case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
diff --git a/src/main/scala/leon/synthesis/rules/TegisLike.scala b/src/main/scala/leon/synthesis/rules/TegisLike.scala
index 51bbf8a6e..864f5302b 100644
--- a/src/main/scala/leon/synthesis/rules/TegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TegisLike.scala
@@ -5,19 +5,14 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.TypeTrees._
-import purescala.Extractors._
import purescala.Constructors._
import evaluators._
-import datagen._
import codegen.CodeGenParams
import utils._
-import bonsai._
import bonsai.enumerators._
abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
diff --git a/src/main/scala/leon/synthesis/rules/Tegless.scala b/src/main/scala/leon/synthesis/rules/Tegless.scala
index e1880752a..f182305ac 100644
--- a/src/main/scala/leon/synthesis/rules/Tegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegless.scala
@@ -4,11 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
-import purescala.TreeOps._
import purescala.TypeTrees._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index e41d3f64b..3b42bf379 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -6,7 +6,6 @@ package rules
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Constructors._
case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index c0e865b57..db2e8b6d1 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -5,7 +5,6 @@ package synthesis
package rules
import purescala.Trees._
-import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
import purescala.Constructors._
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index b463a2725..467a10643 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -4,9 +4,7 @@ package leon
package synthesis
package rules
-import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
case object UnusedInput extends NormalizingRule("UnusedInput") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 88b154c5b..617ae9462 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -9,7 +9,6 @@ import purescala.TypeTrees._
import purescala.Extractors._
import purescala.TypeTreeOps._
import purescala.Trees._
-import purescala.TreeOps._
import purescala.DefOps._
import purescala.Common._
import Witnesses._
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index 0034e0588..658a4b532 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -4,11 +4,7 @@ package leon
package synthesis
package utils
-import purescala.Trees._
-import purescala.TreeOps._
import purescala.Definitions._
-import solvers.z3._
-import solvers.Solver
object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
val name = "Synthesis Problem Extraction"
diff --git a/src/main/scala/leon/termination/ComponentProcessor.scala b/src/main/scala/leon/termination/ComponentProcessor.scala
index b541a7477..6fd32320c 100644
--- a/src/main/scala/leon/termination/ComponentProcessor.scala
+++ b/src/main/scala/leon/termination/ComponentProcessor.scala
@@ -3,7 +3,6 @@
package leon
package termination
-import purescala.TreeOps._
import purescala.Definitions._
import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 0238612e4..89824297a 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -5,7 +5,6 @@ package termination
import purescala.Trees._
import purescala.Common._
-import purescala.Definitions._
import scala.annotation.tailrec
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index 3f62a4a55..c14a56a58 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -5,8 +5,6 @@ package termination
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
-import purescala.Common._
import purescala.Definitions._
import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala
index eb886d5ea..d50458d32 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -4,10 +4,6 @@ package leon
package termination
import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Definitions._
-import purescala.Common._
trait RelationComparator { self : StructuralSize =>
diff --git a/src/main/scala/leon/utils/OracleTraverser.scala b/src/main/scala/leon/utils/OracleTraverser.scala
index d70d1fb5d..8c40f5f9e 100644
--- a/src/main/scala/leon/utils/OracleTraverser.scala
+++ b/src/main/scala/leon/utils/OracleTraverser.scala
@@ -6,7 +6,6 @@ package utils
import purescala.Trees._
import purescala.TypeTrees._
import purescala.Definitions._
-import utils._
case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
private def call(name: String) = {
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 6ecd9f720..e297bcd16 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -3,10 +3,8 @@
package leon
package verification
-import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
import purescala.Definitions._
import purescala.Constructors._
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index b50bb4212..6844f776e 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -3,7 +3,6 @@
package leon
package utils
-import purescala.Common._
import purescala.Trees._
import xlang.Trees._
import purescala.TreeOps._
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index c28f2ca39..f2837ee11 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -6,8 +6,6 @@ package verification
import purescala.Definitions.Program
import solvers._
-import java.util.concurrent.atomic.AtomicBoolean
-
case class VerificationContext (
context: LeonContext,
program: Program,
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 5c4b314ea..2f03dbaa4 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -9,7 +9,6 @@ import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.xlang.Trees._
import leon.purescala.Extractors._
-import leon.purescala.Constructors._
import leon.purescala.TypeTrees._
object ArrayTransformation extends TransformationPhase {
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index e90c53707..9828e45f0 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -8,7 +8,6 @@ import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
import leon.xlang.Trees._
object EpsilonElimination extends TransformationPhase {
diff --git a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 0c6f11a8d..8484b9840 100644
--- a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -3,12 +3,8 @@
package leon
package xlang
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.Trees._
import purescala.TreeOps.collect
import purescala.Definitions._
-import purescala.Constructors._
import utils.Position
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index ce2944a8f..b76186d29 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -3,13 +3,9 @@
package leon
package xlang
-import purescala.Common._
-import purescala.TypeTrees._
-import purescala.Definitions._
import purescala.Trees._
import xlang.Trees._
import purescala.TreeOps._
-import purescala.Extractors._
object TreeOps {
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 6c3864204..e3d23d2cc 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -6,9 +6,8 @@ package xlang
import purescala.Common._
import purescala.TypeTrees._
import purescala.Trees._
-import purescala.Definitions._
import purescala.Extractors._
-import purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter, PrinterContext}
+import purescala.{PrettyPrintable, PrinterContext}
import utils._
object Trees {
--
GitLab