From 73fd074190dce0714e08ac330276a2af513df47b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 17 Mar 2015 12:26:05 +0100
Subject: [PATCH] The name changes you all wanted but were afraid to ask

---
 src/main/scala/leon/codegen/CodeGeneration.scala       | 10 +++++-----
 src/main/scala/leon/codegen/CompilationUnit.scala      |  4 ++--
 src/main/scala/leon/codegen/CompiledExpression.scala   |  2 +-
 .../scala/leon/codegen/runtime/ChooseEntryPoint.scala  |  6 +++---
 .../scala/leon/codegen/runtime/GenericValues.scala     |  2 +-
 src/main/scala/leon/datagen/DataGenerator.scala        |  2 +-
 src/main/scala/leon/datagen/NaiveDataGen.scala         |  4 ++--
 src/main/scala/leon/datagen/VanuatooDataGen.scala      |  6 +++---
 src/main/scala/leon/evaluators/CodeGenEvaluator.scala  |  2 +-
 src/main/scala/leon/evaluators/DefaultEvaluator.scala  |  2 +-
 src/main/scala/leon/evaluators/DualEvaluator.scala     |  4 ++--
 src/main/scala/leon/evaluators/EvaluationResults.scala |  2 +-
 src/main/scala/leon/evaluators/Evaluator.scala         |  2 +-
 .../scala/leon/evaluators/RecursiveEvaluator.scala     | 10 +++++-----
 src/main/scala/leon/evaluators/TracingEvaluator.scala  |  6 +++---
 .../scala/leon/frontends/scalac/CodeExtraction.scala   |  8 ++++----
 src/main/scala/leon/purescala/CallGraph.scala          |  4 ++--
 src/main/scala/leon/purescala/Common.scala             |  4 ++--
 .../leon/purescala/CompleteAbstractDefinitions.scala   |  2 +-
 src/main/scala/leon/purescala/Constructors.scala       |  8 ++++----
 src/main/scala/leon/purescala/DefOps.scala             |  6 +++---
 src/main/scala/leon/purescala/Definitions.scala        |  8 ++++----
 .../leon/purescala/{TreeOps.scala => ExprOps.scala}    |  8 ++++----
 .../leon/purescala/{Trees.scala => Expressions.scala}  |  6 +++---
 src/main/scala/leon/purescala/Extractors.scala         |  8 ++++----
 src/main/scala/leon/purescala/FunctionClosure.scala    |  6 +++---
 src/main/scala/leon/purescala/FunctionMapping.scala    |  6 +++---
 src/main/scala/leon/purescala/MethodLifting.scala      |  8 ++++----
 src/main/scala/leon/purescala/PrettyPrinter.scala      |  8 ++++----
 src/main/scala/leon/purescala/RestoreMethods.scala     |  6 +++---
 src/main/scala/leon/purescala/ScalaPrinter.scala       |  6 +++---
 src/main/scala/leon/purescala/ScopeSimplifier.scala    |  2 +-
 .../scala/leon/purescala/SimplifierWithPaths.scala     |  6 +++---
 src/main/scala/leon/purescala/Transformer.scala        |  2 +-
 src/main/scala/leon/purescala/TransformerWithPC.scala  |  4 ++--
 src/main/scala/leon/purescala/TreeNormalizations.scala |  6 +++---
 .../purescala/{TypeTreeOps.scala => TypeOps.scala}     |  8 ++++----
 .../leon/purescala/{TypeTrees.scala => Types.scala}    |  6 +++---
 src/main/scala/leon/repair/RepairNDEvaluator.scala     |  6 +++---
 .../scala/leon/repair/RepairTrackingEvaluator.scala    |  4 ++--
 src/main/scala/leon/repair/Repairman.scala             |  6 +++---
 src/main/scala/leon/repair/rules/GuidedCloser.scala    |  6 +++---
 src/main/scala/leon/repair/rules/GuidedDecomp.scala    |  6 +++---
 src/main/scala/leon/solvers/AssumptionSolver.scala     |  2 +-
 src/main/scala/leon/solvers/EnumerationSolver.scala    |  6 +++---
 .../scala/leon/solvers/NaiveAssumptionSolver.scala     |  6 +++---
 .../scala/leon/solvers/SimpleAssumptionSolverAPI.scala |  2 +-
 src/main/scala/leon/solvers/SimpleSolverAPI.scala      |  2 +-
 src/main/scala/leon/solvers/Solver.scala               |  2 +-
 .../scala/leon/solvers/TimeoutAssumptionSolver.scala   |  2 +-
 .../scala/leon/solvers/combinators/DNFSolver.scala     |  4 ++--
 .../leon/solvers/combinators/PortfolioSolver.scala     |  2 +-
 .../leon/solvers/combinators/RewritingSolver.scala     |  2 +-
 .../leon/solvers/combinators/UnrollingSolver.scala     |  4 ++--
 .../scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala   |  6 +++---
 src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala  |  6 +++---
 src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala  |  6 +++---
 .../scala/leon/solvers/smtlib/SMTLIBZ3Target.scala     |  6 +++---
 .../scala/leon/solvers/templates/LambdaManager.scala   |  6 +++---
 .../scala/leon/solvers/templates/TemplateEncoder.scala |  2 +-
 .../leon/solvers/templates/TemplateGenerator.scala     |  6 +++---
 .../scala/leon/solvers/templates/TemplateInfo.scala    |  2 +-
 src/main/scala/leon/solvers/templates/Templates.scala  |  6 +++---
 .../scala/leon/solvers/templates/UnrollingBank.scala   |  6 +++---
 src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala  |  8 ++++----
 src/main/scala/leon/solvers/z3/FairZ3Solver.scala      |  6 +++---
 .../scala/leon/solvers/z3/UninterpretedZ3Solver.scala  |  6 +++---
 .../scala/leon/solvers/z3/Z3ModelReconstruction.scala  |  6 +++---
 src/main/scala/leon/synthesis/ChooseInfo.scala         |  4 ++--
 src/main/scala/leon/synthesis/ConvertHoles.scala       |  6 +++---
 src/main/scala/leon/synthesis/ConvertWithOracle.scala  |  4 ++--
 src/main/scala/leon/synthesis/CostModel.scala          |  4 ++--
 src/main/scala/leon/synthesis/ExamplesFinder.scala     |  6 +++---
 src/main/scala/leon/synthesis/FileInterface.scala      |  2 +-
 src/main/scala/leon/synthesis/InOutExample.scala       |  2 +-
 src/main/scala/leon/synthesis/LinearEquations.scala    |  4 ++--
 src/main/scala/leon/synthesis/PartialSolution.scala    |  2 +-
 src/main/scala/leon/synthesis/Problem.scala            |  6 +++---
 src/main/scala/leon/synthesis/Rules.scala              |  6 +++---
 src/main/scala/leon/synthesis/Solution.scala           |  6 +++---
 src/main/scala/leon/synthesis/SynthesisContext.scala   |  2 +-
 src/main/scala/leon/synthesis/SynthesisPhase.scala     |  2 +-
 src/main/scala/leon/synthesis/Synthesizer.scala        |  6 +++---
 src/main/scala/leon/synthesis/Witnesses.scala          |  4 ++--
 src/main/scala/leon/synthesis/rules/ADTDual.scala      |  4 ++--
 src/main/scala/leon/synthesis/rules/ADTInduction.scala |  6 +++---
 .../scala/leon/synthesis/rules/ADTLongInduction.scala  |  6 +++---
 src/main/scala/leon/synthesis/rules/ADTSplit.scala     |  6 +++---
 src/main/scala/leon/synthesis/rules/Assert.scala       |  2 +-
 .../scala/leon/synthesis/rules/BottomUpTegis.scala     |  4 ++--
 src/main/scala/leon/synthesis/rules/CEGIS.scala        |  2 +-
 src/main/scala/leon/synthesis/rules/CEGISLike.scala    |  8 ++++----
 src/main/scala/leon/synthesis/rules/CaseSplit.scala    |  2 +-
 src/main/scala/leon/synthesis/rules/DetupleInput.scala |  6 +++---
 .../scala/leon/synthesis/rules/DetupleOutput.scala     |  4 ++--
 .../scala/leon/synthesis/rules/Disunification.scala    |  2 +-
 .../scala/leon/synthesis/rules/EqualitySplit.scala     |  2 +-
 .../scala/leon/synthesis/rules/EquivalentInputs.scala  |  4 ++--
 src/main/scala/leon/synthesis/rules/Ground.scala       |  4 ++--
 src/main/scala/leon/synthesis/rules/IfSplit.scala      |  4 ++--
 .../scala/leon/synthesis/rules/InequalitySplit.scala   |  4 ++--
 src/main/scala/leon/synthesis/rules/InlineHoles.scala  |  4 ++--
 .../scala/leon/synthesis/rules/InnerCaseSplit.scala    |  2 +-
 src/main/scala/leon/synthesis/rules/IntInduction.scala |  6 +++---
 .../scala/leon/synthesis/rules/IntegerEquation.scala   |  6 +++---
 .../leon/synthesis/rules/IntegerInequalities.scala     |  6 +++---
 src/main/scala/leon/synthesis/rules/OnePoint.scala     |  4 ++--
 .../scala/leon/synthesis/rules/OptimisticGround.scala  |  4 ++--
 .../leon/synthesis/rules/OptimisticInjection.scala     |  2 +-
 .../scala/leon/synthesis/rules/SelectiveInlining.scala |  2 +-
 src/main/scala/leon/synthesis/rules/TEGIS.scala        |  2 +-
 src/main/scala/leon/synthesis/rules/TEGISLike.scala    |  4 ++--
 .../leon/synthesis/rules/UnconstrainedOutput.scala     |  4 ++--
 src/main/scala/leon/synthesis/rules/Unification.scala  |  4 ++--
 src/main/scala/leon/synthesis/rules/UnusedInput.scala  |  2 +-
 .../scala/leon/synthesis/utils/ExpressionGrammar.scala |  8 ++++----
 src/main/scala/leon/synthesis/utils/Helpers.scala      |  6 +++---
 src/main/scala/leon/termination/ChainBuilder.scala     |  8 ++++----
 src/main/scala/leon/termination/ChainComparator.scala  |  8 ++++----
 src/main/scala/leon/termination/ChainProcessor.scala   |  6 +++---
 .../leon/termination/ComplexTerminationChecker.scala   |  2 +-
 src/main/scala/leon/termination/LoopProcessor.scala    |  4 ++--
 src/main/scala/leon/termination/Processor.scala        |  4 ++--
 .../scala/leon/termination/RecursionProcessor.scala    |  2 +-
 src/main/scala/leon/termination/RelationBuilder.scala  |  4 ++--
 .../scala/leon/termination/RelationComparator.scala    |  2 +-
 .../scala/leon/termination/RelationProcessor.scala     |  6 +++---
 .../leon/termination/SimpleTerminationChecker.scala    |  4 ++--
 src/main/scala/leon/termination/Strengthener.scala     |  6 +++---
 src/main/scala/leon/termination/StructuralSize.scala   |  6 +++---
 .../scala/leon/termination/TerminationChecker.scala    |  2 +-
 src/main/scala/leon/utils/GraphOps.scala               |  2 +-
 src/main/scala/leon/utils/OracleTraverser.scala        |  4 ++--
 src/main/scala/leon/utils/Simplifiers.scala            |  4 ++--
 src/main/scala/leon/utils/TypingPhase.scala            |  6 +++---
 src/main/scala/leon/utils/UnitElimination.scala        |  4 ++--
 src/main/scala/leon/verification/AnalysisPhase.scala   |  6 +++---
 src/main/scala/leon/verification/DefaultTactic.scala   |  4 ++--
 src/main/scala/leon/verification/InductionTactic.scala |  6 +++---
 src/main/scala/leon/verification/InjectAsserts.scala   |  4 ++--
 src/main/scala/leon/verification/Tactic.scala          |  4 ++--
 .../leon/verification/VerificationCondition.scala      |  2 +-
 src/main/scala/leon/xlang/ArrayTransformation.scala    |  4 ++--
 src/main/scala/leon/xlang/EpsilonElimination.scala     |  4 ++--
 .../scala/leon/xlang/ImperativeCodeElimination.scala   |  8 ++++----
 .../scala/leon/xlang/NoXLangFeaturesChecking.scala     |  2 +-
 src/main/scala/leon/xlang/TreeOps.scala                |  4 ++--
 src/main/scala/leon/xlang/Trees.scala                  |  4 ++--
 src/test/scala/leon/test/codegen/CodeGenTests.scala    |  4 ++--
 .../leon/test/evaluators/DefaultEvaluatorTests.scala   |  4 ++--
 .../scala/leon/test/evaluators/EvaluatorsTests.scala   |  4 ++--
 src/test/scala/leon/test/purescala/DataGen.scala       |  4 ++--
 src/test/scala/leon/test/purescala/LikelyEqSuite.scala |  4 ++--
 .../leon/test/purescala/TransformationTests.scala      |  6 +++---
 .../leon/test/purescala/TreeNormalizationsTests.scala  |  6 +++---
 src/test/scala/leon/test/purescala/TreeOpsTests.scala  |  6 +++---
 src/test/scala/leon/test/purescala/TreeTests.scala     |  4 ++--
 .../leon/test/solvers/EnumerationSolverTests.scala     |  4 ++--
 .../scala/leon/test/solvers/TimeoutSolverTests.scala   |  4 ++--
 .../scala/leon/test/solvers/UnrollingSolverTests.scala |  4 ++--
 .../scala/leon/test/solvers/z3/FairZ3SolverTests.scala |  6 +++---
 .../leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala |  6 +++---
 .../test/solvers/z3/UninterpretedZ3SolverTests.scala   |  6 +++---
 .../leon/test/synthesis/LinearEquationsSuite.scala     |  6 +++---
 .../leon/test/synthesis/SynthesisRegressionSuite.scala |  4 ++--
 src/test/scala/leon/test/utils/Streams.scala           |  4 ++--
 166 files changed, 382 insertions(+), 382 deletions(-)
 rename src/main/scala/leon/purescala/{TreeOps.scala => ExprOps.scala} (99%)
 rename src/main/scala/leon/purescala/{Trees.scala => Expressions.scala} (99%)
 rename src/main/scala/leon/purescala/{TypeTreeOps.scala => TypeOps.scala} (99%)
 rename src/main/scala/leon/purescala/{TypeTrees.scala => Types.scala} (98%)

diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 7dd3d3dd4..9cfc6170a 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -5,11 +5,11 @@ package codegen
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps.{simplestValue, matchToIfThenElse}
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps.{simplestValue, matchToIfThenElse}
+import purescala.Types._
 import purescala.Constructors._
-import purescala.TypeTreeOps.instantiateType
+import purescala.TypeOps.instantiateType
 import purescala.Extractors._
 import utils._
 
@@ -555,7 +555,7 @@ trait CodeGeneration {
           CLASS_ACC_FINAL
         ).asInstanceOf[U2])
 
-        val closures = purescala.TreeOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
+        val closures = purescala.ExprOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
         val closureTypes = closures.map(id => id.name -> typeToJVM(id.getType))
 
         if (closureTypes.isEmpty) {
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 70f9342dd..6fcdbc00f 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -5,8 +5,8 @@ package codegen
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Extractors._
 import purescala.Constructors._
 import codegen.runtime.LeonCodeGenRuntimeMonitor
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index e75c9b0bb..cdc6413ef 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -4,7 +4,7 @@ package leon
 package codegen
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 import cafebabe._
 
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 0f8762d4e..d91b6e18d 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -6,9 +6,9 @@ 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.Expressions.{Tuple => LeonTuple, _}
+import purescala.ExprOps.valuateWithModel
+import purescala.Types._
 import purescala.Constructors._
 import solvers.TimeoutSolver
 import solvers.z3._
diff --git a/src/main/scala/leon/codegen/runtime/GenericValues.scala b/src/main/scala/leon/codegen/runtime/GenericValues.scala
index 0bf7b27ae..685253d9e 100644
--- a/src/main/scala/leon/codegen/runtime/GenericValues.scala
+++ b/src/main/scala/leon/codegen/runtime/GenericValues.scala
@@ -3,7 +3,7 @@
 package leon
 package codegen.runtime
 
-import purescala.Trees.GenericValue
+import purescala.Expressions.GenericValue
 import scala.collection.immutable.{Map => ScalaMap}
 
 object GenericValues {
diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala
index 3a34af97f..555ed428e 100644
--- a/src/main/scala/leon/datagen/DataGenerator.scala
+++ b/src/main/scala/leon/datagen/DataGenerator.scala
@@ -3,7 +3,7 @@
 package leon
 package datagen
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
 import utils._
 
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 91238109a..70caf95cb 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -4,8 +4,8 @@ package leon
 package datagen
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Definitions._
 import utils.StreamUtils._
 
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index daec365e4..fac16d509 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -5,9 +5,9 @@ package datagen
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index c21315468..e097e75c1 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -5,7 +5,7 @@ package evaluators
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 
 import codegen.CompilationUnit
 import codegen.CodeGenParams
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index bf27ce8bd..66857a4f8 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -4,7 +4,7 @@ package leon
 package evaluators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 
 class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index bef203c06..f6f6a3cb0 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -4,9 +4,9 @@ package leon
 package evaluators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
-import purescala.TypeTrees._
+import purescala.Types._
 
 import codegen._
 
diff --git a/src/main/scala/leon/evaluators/EvaluationResults.scala b/src/main/scala/leon/evaluators/EvaluationResults.scala
index caabd5f4c..8e6957f3f 100644
--- a/src/main/scala/leon/evaluators/EvaluationResults.scala
+++ b/src/main/scala/leon/evaluators/EvaluationResults.scala
@@ -3,7 +3,7 @@
 package leon
 package evaluators
 
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 object EvaluationResults {
   /** Possible results of expression evaluation. */
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 93c7129c4..9c4403b10 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -5,7 +5,7 @@ package evaluators
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 
 abstract class Evaluator(val context : LeonContext, val program : Program) extends LeonComponent {
 
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index e52d12904..e6e516c67 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -5,9 +5,9 @@ package evaluators
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Constructors._
 import purescala.Extractors._
 
@@ -504,7 +504,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       e(impl)
 
     case choose @ Choose(_, None) =>
-      import purescala.TreeOps.simplestValue
+      import purescala.ExprOps.simplestValue
 
       implicit val debugSection = utils.DebugSectionSynthesis
 
@@ -571,7 +571,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
   }
 
   def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[Identifier, Expr])] = {
-    import purescala.TypeTreeOps.isSubtypeOf
+    import purescala.TypeOps.isSubtypeOf
 
     def matchesPattern(pat: Pattern, e: Expr): Option[Map[Identifier, Expr]] = (pat, e) match {
       case (InstanceOfPattern(ob, pct), CaseClass(ct, _)) =>
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index 80757d88a..39885c185 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -4,11 +4,11 @@ package leon
 package evaluators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog, maxSteps) {
   type RC = TracingRecContext
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index cfcf667c5..379413fea 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -17,13 +17,13 @@ import purescala.Definitions.{
   Import    => LeonImport,
   _
 }
-import purescala.Trees.{Expr => LeonExpr, This => LeonThis, _}
-import purescala.TypeTrees.{TypeTree => LeonType, _}
+import purescala.Expressions.{Expr => LeonExpr, This => LeonThis, _}
+import purescala.Types.{TypeTree => LeonType, _}
 import purescala.Common._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTreeOps._
+import purescala.ExprOps._
+import purescala.TypeOps._
 import purescala.DefOps.packageOf
 import xlang.Trees.{Block => LeonBlock, _}
 import xlang.TreeOps._
diff --git a/src/main/scala/leon/purescala/CallGraph.scala b/src/main/scala/leon/purescala/CallGraph.scala
index 77fa4cfa8..38c690020 100644
--- a/src/main/scala/leon/purescala/CallGraph.scala
+++ b/src/main/scala/leon/purescala/CallGraph.scala
@@ -4,8 +4,8 @@ package leon
 package purescala
 
 import Definitions._
-import Trees._
-import TreeOps._
+import Expressions._
+import ExprOps._
 
 class CallGraph(p: Program) {
 
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 7c6d32e04..6da84692b 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -7,8 +7,8 @@ import utils._
 import Definitions.Definition
 
 object Common {
-  import Trees.Variable
-  import TypeTrees._
+  import Expressions.Variable
+  import Types._
 
   abstract class Tree extends Positioned with Serializable {
     def copiedFrom(o: Tree): this.type = {
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
index c3e2ba46c..482bd06cf 100644
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
@@ -5,7 +5,7 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 
 object CompleteAbstractDefinitions extends TransformationPhase {
 
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 3d316f8d8..dcca26675 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -4,12 +4,12 @@ package leon
 package purescala
 
 object Constructors {
-  import Trees._
-  import TreeOps._
+  import Expressions._
+  import ExprOps._
   import Definitions._
-  import TypeTreeOps._
+  import TypeOps._
   import Common._
-  import TypeTrees._
+  import Types._
 
   // If isTuple, the whole expression is returned. This is to avoid a situation
   // like tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x, which is not expected.
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 96acd8f22..25f5fb384 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -2,7 +2,7 @@ package leon.purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 
 object DefOps {
 
@@ -265,8 +265,8 @@ object DefOps {
   
   
   
-  import Trees.Expr
-  import TreeOps.{preMap, postMap}
+  import Expressions.Expr
+  import ExprOps.{preMap, postMap}
   
   /*
    * Apply an expression operation on all expressions contained in a FunDef
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 201835745..680e7c099 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -8,10 +8,10 @@ import utils.Library
 
 object Definitions {
   import Common._
-  import Trees._
-  import TreeOps._
-  import TypeTrees._
-  import TypeTreeOps._
+  import Expressions._
+  import ExprOps._
+  import Types._
+  import TypeOps._
 
   sealed abstract class Definition extends Tree {
     
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
similarity index 99%
rename from src/main/scala/leon/purescala/TreeOps.scala
rename to src/main/scala/leon/purescala/ExprOps.scala
index fe0a0c6ce..2f7f2ab35 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -9,12 +9,12 @@ import leon.solvers._
 
 import scala.collection.concurrent.TrieMap
 
-object TreeOps {
+object ExprOps {
   import Common._
-  import TypeTrees._
+  import Types._
   import Definitions._
-  import Trees._
-  import TypeTreeOps._
+  import Expressions._
+  import TypeOps._
   import Extractors._
   import Constructors._
   import DefOps._
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Expressions.scala
similarity index 99%
rename from src/main/scala/leon/purescala/Trees.scala
rename to src/main/scala/leon/purescala/Expressions.scala
index 197fc891f..32e56f1da 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -6,10 +6,10 @@ package purescala
 import utils._
 
 /** AST definitions for Pure Scala. */
-object Trees {
+object Expressions {
   import Common._
-  import TypeTrees._
-  import TypeTreeOps._
+  import Types._
+  import TypeOps._
   import Definitions._
   import Extractors._
   import Constructors._
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 7077cf9f8..9f705f388 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -3,16 +3,16 @@
 package leon
 package purescala
 
-import Trees._
+import Expressions._
 
 object Extractors {
   import Common._
-  import TypeTrees._
-  import TypeTreeOps._
+  import Types._
+  import TypeOps._
   import Definitions._
   import Extractors._
   import Constructors._
-  import TreeOps._
+  import ExprOps._
 
   object UnaryOperator {
     def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 7fcfb683e..a9c443c49 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -5,10 +5,10 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 import Extractors._
-import TreeOps._
-import TypeTrees._
+import ExprOps._
+import Types._
 import Constructors._
 
 object FunctionClosure extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/FunctionMapping.scala b/src/main/scala/leon/purescala/FunctionMapping.scala
index c11c80a39..a82b84f83 100644
--- a/src/main/scala/leon/purescala/FunctionMapping.scala
+++ b/src/main/scala/leon/purescala/FunctionMapping.scala
@@ -4,9 +4,9 @@ package leon
 package purescala
 
 import Definitions._
-import Trees._
-import TreeOps._
-import TypeTrees._
+import Expressions._
+import ExprOps._
+import Types._
 
 abstract class FunctionMapping extends TransformationPhase {
   
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index dc6ce8aea..6d970b65d 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -5,11 +5,11 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 import Extractors._
-import TreeOps._
-import TypeTrees._
-import TypeTreeOps.instantiateType
+import ExprOps._
+import Types._
+import TypeOps.instantiateType
 
 object MethodLifting extends TransformationPhase {
 
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index fd881faa5..a54084b5f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -8,10 +8,10 @@ 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.purescala.ExprOps.{isListLiteral, simplestValue}
+import leon.purescala.Expressions._
+import leon.purescala.TypeOps.leastUpperBound
+import leon.purescala.Types._
 import leon.synthesis.Witnesses._
 
 case class PrinterContext(
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index e65add9c2..353bb8697 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -3,10 +3,10 @@ package leon.purescala
 import leon._
 import leon.purescala.Definitions._
 import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps.{replaceFromIDs,functionCallsOf}
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps.{replaceFromIDs,functionCallsOf}
 import leon.purescala.DefOps.{applyOnFunDef,preMapOnFunDef}
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import utils.GraphOps._
 
 object RestoreMethods extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index e38418c0a..45a3db6fa 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -11,8 +11,8 @@ import PrinterHelpers._
 /** This pretty-printer only print valid scala syntax */
 class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, sb) {
   import Common._
-  import Trees._
-  import TypeTrees._
+  import Expressions._
+  import Types._
   import Definitions._
 
   import java.lang.StringBuffer
@@ -54,7 +54,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
       case SetCardinality(s)    => p"$s.size"
 
       case a@FiniteArray(elems, oDef, size) => {
-        import TreeOps._
+        import ExprOps._
         val ArrayType(underlying) = a.getType
         val default = oDef.getOrElse(simplestValue(underlying))
         size match {
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 74cb530c7..7a1299d68 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -5,7 +5,7 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 import Extractors._
 
 class ScopeSimplifier extends Transformer {
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index 8cd319d89..a3e1e02ec 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -3,9 +3,9 @@
 package leon
 package purescala
 
-import Trees._
-import TypeTrees._
-import TreeOps._
+import Expressions._
+import Types._
+import ExprOps._
 import Extractors._
 import Constructors._
 import solvers._
diff --git a/src/main/scala/leon/purescala/Transformer.scala b/src/main/scala/leon/purescala/Transformer.scala
index c623aa1dd..46314714f 100644
--- a/src/main/scala/leon/purescala/Transformer.scala
+++ b/src/main/scala/leon/purescala/Transformer.scala
@@ -3,7 +3,7 @@
 package leon
 package purescala
 
-import purescala.Trees._
+import purescala.Expressions._
 
 
 trait Transformer {
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index 10cc17dfe..821f4c9ef 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -3,8 +3,8 @@
 package leon
 package purescala
 
-import Trees._
-import TreeOps._
+import Expressions._
+import ExprOps._
 import Extractors._
 import Constructors._
 
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 554d3268e..7b80083e4 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -5,9 +5,9 @@ package purescala
 
 object TreeNormalizations {
   import Common._
-  import TypeTrees._
-  import Trees._
-  import TreeOps._
+  import Types._
+  import Expressions._
+  import ExprOps._
 
   /* TODO: we should add CNF and DNF at least */
 
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
similarity index 99%
rename from src/main/scala/leon/purescala/TypeTreeOps.scala
rename to src/main/scala/leon/purescala/TypeOps.scala
index dd6597e8f..14eba4fe9 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -3,15 +3,15 @@
 package leon
 package purescala
 
-import TreeOps.postMap
-import TypeTrees._
+import ExprOps.postMap
+import Types._
 import Definitions._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
 import Constructors._
 
-object TypeTreeOps {
+object TypeOps {
   def typeDepth(t: TypeTree): Int = t match {
     case NAryType(tps, builder) => 1+tps.foldLeft(0) { case (d, t) => d max typeDepth(t) }
   }
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/Types.scala
similarity index 98%
rename from src/main/scala/leon/purescala/TypeTrees.scala
rename to src/main/scala/leon/purescala/Types.scala
index 511958245..091914350 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -5,11 +5,11 @@ package purescala
 
 import scala.language.implicitConversions
 
-object TypeTrees {
+object Types {
   import Common._
-  import Trees._
+  import Expressions._
   import Definitions._
-  import TypeTreeOps._
+  import TypeOps._
 
   trait Typed {
     def getType: TypeTree
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index da65e5c1f..b521e8717 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -2,9 +2,9 @@ package leon.repair
 
 import leon.purescala._
 import Definitions._
-import Trees._
-import TypeTrees._
-import TreeOps.postMap
+import Expressions._
+import Types._
+import ExprOps.postMap
 import Constructors.not
 import leon.LeonContext
 import leon.evaluators.DefaultEvaluator
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 4446f786c..75fe9e853 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -3,8 +3,8 @@ package leon.repair
 import scala.collection.immutable.Map
 import scala.collection.mutable.{Map => MMap}
 import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 import leon.purescala.Definitions._
 import leon.LeonContext
 import leon.evaluators.RecursiveEvaluator
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 9e234643c..0c2f298ee 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -5,9 +5,9 @@ package repair
   
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.DefOps._
 import purescala.Constructors._
 import purescala.Extractors.unwrapTuple
diff --git a/src/main/scala/leon/repair/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala
index 50b255755..06f250821 100644
--- a/src/main/scala/leon/repair/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/repair/rules/GuidedCloser.scala
@@ -7,11 +7,11 @@ package rules
 import synthesis._
 
 import leon.utils.Simplifiers
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
index 2546dd4e5..bbac7dd0b 100644
--- a/src/main/scala/leon/repair/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
@@ -8,11 +8,11 @@ import synthesis._
 
 import leon.utils.Simplifiers
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/solvers/AssumptionSolver.scala b/src/main/scala/leon/solvers/AssumptionSolver.scala
index 73084bf6d..f180eaf42 100644
--- a/src/main/scala/leon/solvers/AssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/AssumptionSolver.scala
@@ -3,7 +3,7 @@
 package leon
 package solvers
 
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 trait AssumptionSolver extends Solver {
   def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 9ec495e88..5f158c79f 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -7,10 +7,10 @@ import utils._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 import datagen._
 
diff --git a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
index c888f38df..fb73f5f29 100644
--- a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
@@ -6,11 +6,11 @@ package solvers
 import utils._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 trait NaiveAssumptionSolver extends AssumptionSolver {
   self: IncrementalSolver =>
diff --git a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
index b8053b765..e38c63e7f 100644
--- a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
@@ -4,7 +4,7 @@ package leon
 package solvers
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends SimpleSolverAPI(sf) {
 
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index eafd3fbd3..325d5e102 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -4,7 +4,7 @@ package leon
 package solvers
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 class SimpleSolverAPI(sf: SolverFactory[Solver]) {
   def solveVALID(expression: Expr): Option[Boolean] = {
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index e1b430346..9b278aeb6 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -4,7 +4,7 @@ package leon
 package solvers
 
 import utils._
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 import purescala.Common.Identifier
 
 
diff --git a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
index 7fae46a9c..b6bcdc1f1 100644
--- a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
@@ -3,7 +3,7 @@
 package leon
 package solvers
 
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 trait TimeoutAssumptionSolver extends TimeoutSolver with AssumptionSolver {
 
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 0b06aeb96..d67b2094c 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -6,8 +6,8 @@ package combinators
 
 import purescala.Common._
 import purescala.Constructors._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 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 4e9a28045..b24617a4e 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -5,7 +5,7 @@ package solvers
 package combinators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 import utils.Interruptible
 import scala.concurrent._
diff --git a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
index 5b089883b..1230ac3c5 100644
--- a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
@@ -5,7 +5,7 @@ package solvers
 package combinators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 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 59ac92e7a..c2e9d7cfb 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -7,8 +7,8 @@ package combinators
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 import solvers.templates._
 import utils.Interruptible
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 2f9e44233..366f977d2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -7,11 +7,11 @@ package smtlib
 import utils._
 import purescala._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
 import Constructors._
-import TypeTrees._
-import TreeOps.simplestValue
+import Types._
+import ExprOps.simplestValue
 
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands._
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 4da09b251..30c1a967c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -7,10 +7,10 @@ package smtlib
 import utils._
 import purescala._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
-import TreeOps._
-import TypeTrees._
+import ExprOps._
+import Types._
 import Definitions._
 
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index fca07352c..6cb34c94b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -4,10 +4,10 @@ package smtlib
 
 import purescala._
 import Common._
-import Trees.{Assert => _, _}
+import Expressions.{Assert => _, _}
 import Extractors._
-import TreeOps._
-import TypeTrees._
+import ExprOps._
+import Types._
 import Constructors._
 import Definitions._
 import utils.IncrementalBijection
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 6c0e9cfbf..376e99b6b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -7,10 +7,10 @@ package smtlib
 import utils._
 import purescala._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
-import TypeTrees._
-import TreeOps.simplestValue
+import Types._
+import ExprOps.simplestValue
 
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands.{DefineSort, GetModel, DefineFun}
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index d8aa9026f..6c69b458d 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -5,9 +5,9 @@ package solvers
 package templates
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 
 class LambdaManager[T](encoder: TemplateEncoder[T]) {
   private type IdMap = Map[T, LambdaTemplate[T]]
diff --git a/src/main/scala/leon/solvers/templates/TemplateEncoder.scala b/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
index 7460ae0cf..829a40326 100644
--- a/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
@@ -5,7 +5,7 @@ package solvers
 package templates
 
 import purescala.Common.Identifier
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 trait TemplateEncoder[T] {
   def encodeId(id: Identifier): T
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 8a35871f4..1ee5d303d 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -6,10 +6,10 @@ package templates
 
 import utils._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 110e658a3..0dce3f324 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -5,7 +5,7 @@ package solvers
 package templates
 
 import purescala.Definitions.TypedFunDef
-import purescala.TypeTrees.TypeTree
+import purescala.Types.TypeTree
 
 case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) {
   override def toString = {
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index ddf513b8c..74b453bc1 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -5,10 +5,10 @@ package solvers
 package templates
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 import evaluators._
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 015dc2ada..443b2f5ab 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -6,10 +6,10 @@ package templates
 
 import utils._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 import evaluators._
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 6237fde6a..529dabf20 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -11,11 +11,11 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Extractors._
-import purescala.Trees._
-import purescala.TypeTreeOps._
+import purescala.Expressions._
+import purescala.TypeOps._
 import xlang.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 import scala.collection.mutable.{Map => MutableMap}
 import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index b9852dfe9..e111891c1 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -10,11 +10,11 @@ import _root_.z3.scala._
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 import solvers.templates._
 
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 1ee010c4f..aeaee81e0 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -9,10 +9,10 @@ import leon.solvers._
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 /** This is a rather direct mapping to Z3, where all functions are left uninterpreted.
  *  It reports the results as follows (based on the negation of the formula):
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 5558c745f..2532827ad 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -6,9 +6,9 @@ package solvers.z3
 import z3.scala._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 
 trait Z3ModelReconstruction {
   self: AbstractZ3Solver =>
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 72ac87a52..8e1392259 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -5,8 +5,8 @@ package synthesis
 
 import purescala.Definitions._
 import purescala.Constructors._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import Witnesses._
 
 case class ChooseInfo(fd: FunDef,
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 7b2450fac..ece2e85ce 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracle.scala b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
index e35c6e581..9af1d42c7 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracle.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
@@ -3,8 +3,8 @@
 package leon
 package synthesis
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index b6a0db402..cf6575bd6 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -5,8 +5,8 @@ package synthesis
 
 import graph._
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 abstract class CostModel(val name: String) {
   def solution(s: Solution): Cost
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 16edbd4ab..b1ce6099a 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -3,10 +3,10 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.TypeTrees.TypeTree
+import purescala.ExprOps._
+import purescala.Types.TypeTree
 import purescala.Common._
 import purescala.Constructors._
 import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 11bd6e704..d6dc34b2f 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -3,7 +3,7 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common.Tree
 import purescala.Definitions.Definition
 import purescala.ScalaPrinter
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index d3a7663e9..801748dd4 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -3,7 +3,7 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 import leon.utils.ASCIIHelpers._
 
 class Example(val ins: Seq[Expr])
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 684bae5c6..4a9314562 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.TreeNormalizations.linearArithmeticForm
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Common._
 import evaluators._
 
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index 187ec4d05..1f0bdaa47 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -3,7 +3,7 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 
 import graph._
 
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 297b3210f..f1257f091 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -3,9 +3,9 @@
 package leon
 package synthesis
 
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 import leon.purescala.Common._
 import leon.purescala.Constructors._
 import leon.purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 90f3eb4ff..e22367b8e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
 import rules._
 
 abstract class Rule(val name: String) extends RuleDSL {
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 2eb1e73f1..91c6020ee 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -4,10 +4,10 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees.{TypeTree,TupleType}
+import purescala.Expressions._
+import purescala.Types.{TypeTree,TupleType}
 import purescala.Definitions._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 import leon.utils.Simplifiers
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index e59e1eaad..3adc6f351 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -7,7 +7,7 @@ import solvers._
 import solvers.combinators.PortfolioSolverSynth
 import solvers.z3._
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions.{Program, FunDef}
 import purescala.Common.Identifier
 
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index de1916639..0da2b6c81 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -2,7 +2,7 @@
 package leon
 package synthesis
 
-import purescala.TreeOps._
+import purescala.ExprOps._
 
 import purescala.ScalaPrinter
 import purescala.Definitions.{Program, FunDef}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 44246404e..ee234633f 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -5,11 +5,11 @@ package synthesis
 
 import purescala.Common._
 import purescala.Definitions.{Program, FunDef, ModuleDef, DefType, ValDef}
-import purescala.TreeOps._
-import purescala.Trees._
+import purescala.ExprOps._
+import purescala.Expressions._
 import purescala.Constructors._
 import purescala.ScalaPrinter
-import purescala.TypeTrees._
+import purescala.Types._
 import solvers._
 import solvers.combinators._
 import solvers.z3._
diff --git a/src/main/scala/leon/synthesis/Witnesses.scala b/src/main/scala/leon/synthesis/Witnesses.scala
index 1c454f09b..4633f3271 100644
--- a/src/main/scala/leon/synthesis/Witnesses.scala
+++ b/src/main/scala/leon/synthesis/Witnesses.scala
@@ -1,10 +1,10 @@
 package leon.synthesis
 
 import leon.purescala._
-import TypeTrees._
+import Types._
 import Definitions.TypedFunDef
 import Extractors._
-import Trees.Expr
+import Expressions.Expr
 
 
 object Witnesses {
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 5bb9d6f5d..d27cbe9bc 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 73aa69f7a..e993c73dd 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -6,11 +6,11 @@ package rules
 
 import solvers._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 case object ADTInduction extends Rule("ADT Induction") {
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 6c12864c5..2c0817ce1 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -6,11 +6,11 @@ package rules
 
 import solvers._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 case object ADTLongInduction extends Rule("ADT Long Induction") {
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index a836f8843..5f5fed010 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -4,10 +4,10 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Definitions._
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 4d6dcca5c..dc2a06e4d 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TreeOps._
+import purescala.ExprOps._
 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 46fd17233..51e63ec0d 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Constructors._
 import evaluators._
 import codegen.CodeGenParams
diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index 4cf48c204..d594d22c4 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TypeTrees._
+import purescala.Types._
 
 import utils._
 
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f3191fdfc..e4c2c1ad1 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -9,13 +9,13 @@ import solvers._
 import solvers.z3._
 
 import verification._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.TypeTreeOps._
+import purescala.TypeOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.ScalaPrinter
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 203a35b7d..905cdff75 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Constructors._
 
 case object CaseSplit extends Rule("Case-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 71f4ea755..6b7e42599 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -4,11 +4,11 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index b6e57333c..d41bfb8df 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -4,10 +4,10 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
+import purescala.Types._
 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 89da1b14d..e9946dcce 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 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 d331b4928..977a3eb08 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Constructors._
 
 import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index bb43d716b..4add33594 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -5,8 +5,8 @@ package synthesis
 package rules
 
 import leon.utils._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index a2a6f9955..17792cad8 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -5,8 +5,8 @@ package synthesis
 package rules
 
 import solvers._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 ea115e42c..a29721e7e 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 86ccb02ad..b0649e251 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 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 249c62f30..96f3de79d 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -10,8 +10,8 @@ import solvers._
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 478511031..114fa697c 100644
--- a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Constructors._
 
 case object InnerCaseSplit extends Rule("Inner-Case-Split"){
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index abf2545d5..216ce8ad7 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -5,11 +5,11 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 case object IntInduction extends Rule("Int Induction") {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index d943fb072..478d3fbd2 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -5,12 +5,12 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.TreeNormalizations._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Definitions._
 import LinearEquations.elimVariable
 import evaluators._
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 69217a336..3430bf8ab 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -5,12 +5,12 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.TreeNormalizations.linearArithmeticForm
 import purescala.TreeNormalizations.NonLinearExpressionException
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Constructors._
 import purescala.Definitions._
 import LinearEquations.elimVariable
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 5ad58a0a4..866fc3e02 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -5,8 +5,8 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 28256da4e..56cc85223 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 e329de9d1..08d9862ec 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
index f1356c77d..381d9cf2f 100644
--- a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/TEGIS.scala b/src/main/scala/leon/synthesis/rules/TEGIS.scala
index 06bf87c60..8aa44fe90 100644
--- a/src/main/scala/leon/synthesis/rules/TEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGIS.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TypeTrees._
+import purescala.Types._
 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 48ca570c2..78fbd8a5b 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Constructors._
 
 import evaluators._
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 5311caf12..ee215e78f 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 3c304c1fd..72c766ba4 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 077003e82..a2fc3150a 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TreeOps._
+import purescala.ExprOps._
 
 case object UnusedInput extends NormalizingRule("UnusedInput") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index b2f5ced92..af474fb7e 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -6,13 +6,13 @@ import bonsai._
 
 import Helpers._
 
-import purescala.Trees.{Or => LeonOr, _}
+import purescala.Expressions.{Or => LeonOr, _}
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.TypeTreeOps._
+import purescala.TypeOps._
 import purescala.Extractors._
 import purescala.ScalaPrinter
 import purescala.Constructors.finiteSet
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 77634ff76..cb73726c4 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -5,10 +5,10 @@ package synthesis
 package utils
 
 import purescala.Definitions._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Extractors._
-import purescala.TypeTreeOps._
-import purescala.Trees._
+import purescala.TypeOps._
+import purescala.Expressions._
 import purescala.DefOps._
 import purescala.Common._
 import Witnesses._
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index e73470f2a..371897288 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -4,11 +4,11 @@ package leon
 package termination
 
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 import leon.purescala.Constructors._
-import leon.purescala.TypeTreeOps._
+import leon.purescala.TypeOps._
 import leon.purescala.Common._
 
 import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 4a3e8270c..5f923fb0a 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -3,10 +3,10 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.TypeTreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import purescala.TypeOps._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Common._
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 817aec03d..3bb3e17a0 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -3,9 +3,9 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Common._
 import purescala.Extractors._
 import purescala.Definitions._
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index 127ff6681..df603dfb8 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -4,7 +4,7 @@ package leon
 package termination
 
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 
 import scala.collection.mutable.{Map => MutableMap}
 
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index ec6bb2b89..4765a73c4 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -5,8 +5,8 @@ package termination
 
 import purescala.Definitions._
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index f4fe5c65e..42cc27a2a 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -3,8 +3,8 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Common._
 import purescala.Definitions._
 
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 89824297a..210dfed17 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -3,7 +3,7 @@
 package leon
 package termination
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
 
 import scala.annotation.tailrec
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index c14a56a58..018eca2e7 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -3,8 +3,8 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 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 d50458d32..7bb8fba69 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -3,7 +3,7 @@
 package leon
 package termination
 
-import purescala.Trees._
+import purescala.Expressions._
 
 trait RelationComparator { self : StructuralSize =>
 
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 33f7c9da0..1036a25bf 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -3,9 +3,9 @@
 package leon
 package termination
 
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 import leon.purescala.Common._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index ada2df4a3..6ba21e23f 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -5,8 +5,8 @@ package termination
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 import scala.collection.mutable.{ Map => MutableMap }
 
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index d0f097d63..d0c8bf164 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -1,9 +1,9 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 206e4ac44..8788a9496 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -3,9 +3,9 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Common._
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index e4273dd85..5a686f060 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -4,7 +4,7 @@ package leon
 package termination
 
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.DefOps._
 
 abstract class TerminationChecker(val context: LeonContext, val program: Program) extends LeonComponent {
diff --git a/src/main/scala/leon/utils/GraphOps.scala b/src/main/scala/leon/utils/GraphOps.scala
index f7ad5646a..b7d3adf92 100644
--- a/src/main/scala/leon/utils/GraphOps.scala
+++ b/src/main/scala/leon/utils/GraphOps.scala
@@ -30,7 +30,7 @@ object GraphOps {
         graph.getOrElse(v, Set())
       }))
     }
-    leon.purescala.TreeOps.fixpoint(step, -1)(graph)
+    leon.purescala.ExprOps.fixpoint(step, -1)(graph)
   }
   
   def sources[A](graph : Map[A,Set[A]]) = {
diff --git a/src/main/scala/leon/utils/OracleTraverser.scala b/src/main/scala/leon/utils/OracleTraverser.scala
index 8c40f5f9e..3475a7a45 100644
--- a/src/main/scala/leon/utils/OracleTraverser.scala
+++ b/src/main/scala/leon/utils/OracleTraverser.scala
@@ -3,8 +3,8 @@
 package leon
 package utils
 
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Definitions._
 
 case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 86d711303..cd8cd8faa 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -2,8 +2,8 @@ package leon
 package utils
 
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.ScopeSimplifier
 import solvers.z3.UninterpretedZ3Solver
 import solvers._
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 1b9b86f26..7c8d7c4c7 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -4,9 +4,9 @@ package leon
 package utils
 
 import purescala.Common._
-import purescala.TreeOps.preTraversal
-import purescala.TypeTrees._
-import purescala.Trees._
+import purescala.ExprOps.preTraversal
+import purescala.Types._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 60f8bc232..660f6e123 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -5,11 +5,11 @@ package utils
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import xlang.Trees._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TypeTrees._
+import purescala.Types._
 
 object UnitElimination extends TransformationPhase {
 
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 4d590e40a..c849441e0 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -5,9 +5,9 @@ package verification
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 
 import solvers._
 import solvers.z3._
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index e297bcd16..6ba584014 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -3,8 +3,8 @@
 package leon
 package verification
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 9d7a7d890..b68abfa48 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -4,9 +4,9 @@ package leon
 package verification
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 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 6844f776e..cdeae613b 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -3,9 +3,9 @@
 package leon
 package utils
 
-import purescala.Trees._
+import purescala.Expressions._
 import xlang.Trees._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 8d80f5ffb..92bf550b4 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -4,8 +4,8 @@ package leon
 package verification
 
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 abstract class Tactic(vctx: VerificationContext) {
   val description : String
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index da53f8eac..f0bb893ae 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -2,7 +2,7 @@
 
 package leon.verification
 
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Definitions._
 import leon.purescala.Common._
 import leon.utils.{Position, Positioned}
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 2f03dbaa4..63a454ecc 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -6,10 +6,10 @@ import leon.TransformationPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.xlang.Trees._
 import leon.purescala.Extractors._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 
 object ArrayTransformation extends TransformationPhase {
 
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 9828e45f0..3a1c8498e 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -6,8 +6,8 @@ import leon.TransformationPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
 import leon.xlang.Trees._
 
 object EpsilonElimination extends TransformationPhase {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 474d7a2b9..219acc601 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -7,12 +7,12 @@ import leon.TransformationPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTreeOps._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
+import leon.purescala.TypeOps._
 import leon.xlang.Trees._
 
 object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef])] {
diff --git a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 8484b9840..38a42c494 100644
--- a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -3,7 +3,7 @@
 package leon
 package xlang
 
-import purescala.TreeOps.collect
+import purescala.ExprOps.collect
 import purescala.Definitions._
 
 import utils.Position
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index b76186d29..296bfe9f7 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -3,9 +3,9 @@
 package leon
 package xlang
 
-import purescala.Trees._
+import purescala.Expressions._
 import xlang.Trees._
-import purescala.TreeOps._
+import purescala.ExprOps._
 
 object TreeOps {
   
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index e3d23d2cc..226e69c03 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -4,8 +4,8 @@ package leon
 package xlang
 
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.Trees._
+import purescala.Types._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.{PrettyPrintable, PrinterContext}
 import utils._
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index 607a6cd64..ac17f0bda 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -5,8 +5,8 @@ package leon.test.codegen
 import leon._
 import leon.codegen._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 import leon.evaluators.{CodeGenEvaluator,EvaluationResults}
 import EvaluationResults._
 
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index dc79a820c..9f3c7969f 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -10,9 +10,9 @@ import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.DefOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.purescala.Constructors._
 
 class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index b0ea6159d..2642dba5c 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -10,9 +10,9 @@ import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.DefOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
 
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index fd5afaef0..45c7f066b 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -8,9 +8,9 @@ import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
 import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.datagen._
 
 import leon.evaluators._
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index dd72c6795..36b802cca 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -5,8 +5,8 @@ package leon.test.purescala
 import leon._
 import leon.test._
 import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 
 class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index 7335365aa..e2c2bb7a8 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -10,9 +10,9 @@ import leon.frontends.scalac.ExtractionPhase
 import leon.purescala.ScalaPrinter
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers.z3.UninterpretedZ3Solver
 import leon.solvers._
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index 61a7bbe9a..f898dfee0 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -7,9 +7,9 @@ import leon.test._
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
+import leon.purescala.Types._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
 import leon.purescala.TreeNormalizations._
 
 class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 68e132d7e..19ba9ae5d 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -9,9 +9,9 @@ import leon.LeonContext
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
 
 import leon.solvers.z3._
 
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
index 1036fcd88..254441004 100644
--- a/src/test/scala/leon/test/purescala/TreeTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -8,8 +8,8 @@ import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Constructors._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 class TreeTests extends LeonTestSuite {
 
diff --git a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
index f784faea2..332777cd4 100644
--- a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
@@ -9,8 +9,8 @@ import leon.solvers._
 import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 class EnumerationSolverTests extends LeonTestSuite {
   private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index cb8de56b3..8759d03ba 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -9,8 +9,8 @@ import leon.solvers._
 import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 class TimeoutSolverTests extends LeonTestSuite {
   private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with Interruptible{
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index 8fb31f280..0966c8b08 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -2,8 +2,8 @@ package leon.test.solvers
 
 import leon._
 import leon.test._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.solvers._
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 901d1e05b..e170dea4b 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -5,9 +5,9 @@ package leon.test.solvers.z3
 import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers._
 import leon.solvers.z3._
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index e5816f5b1..ce7f9ce47 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -5,9 +5,9 @@ package leon.test.solvers.z3
 import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers._
 import leon.solvers.z3._
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index cab51ede7..f9d6fc80a 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -6,9 +6,9 @@ import leon.test._
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers._
 import leon.solvers.z3._
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index dfa2b2ac7..46c35cb9e 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -3,9 +3,9 @@
 package leon.test.synthesis
 import leon.test._
 
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.test.purescala.WithLikelyEq
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 16091cd8e..a1ffa1081 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -5,8 +5,8 @@ import leon.test._
 
 import leon._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
 import leon.solvers.z3._
 import leon.solvers.Solver
 import leon.synthesis._
diff --git a/src/test/scala/leon/test/utils/Streams.scala b/src/test/scala/leon/test/utils/Streams.scala
index e75af01ef..dfca44725 100644
--- a/src/test/scala/leon/test/utils/Streams.scala
+++ b/src/test/scala/leon/test/utils/Streams.scala
@@ -8,9 +8,9 @@ import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
 import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.datagen._
 import leon.utils.StreamUtils._
 
-- 
GitLab