From 66114616248c77681448c6bb53166cc0c3a05fbc Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Thu, 10 Mar 2016 14:35:00 +0100 Subject: [PATCH] Remove unused commits mostly --- .../leon/laziness/ClosurePreAsserter.scala | 5 ---- .../leon/laziness/FreeVariableFactory.scala | 20 ------------- .../laziness/LazinessEliminationPhase.scala | 27 ----------------- .../scala/leon/laziness/LazinessUtil.scala | 14 --------- .../leon/laziness/LazyClosureConverter.scala | 14 --------- .../leon/laziness/LazyClosureFactory.scala | 16 ---------- .../leon/laziness/LazyExpressionLifter.scala | 23 --------------- .../leon/laziness/LazyFunctionsManager.scala | 18 ------------ .../leon/laziness/LazyInstrumenter.scala | 17 ----------- .../leon/laziness/LazyVerificationPhase.scala | 29 +++---------------- .../scala/leon/laziness/TypeChecker.scala | 4 +-- .../scala/leon/laziness/TypeRectifier.scala | 19 +----------- 12 files changed, 6 insertions(+), 200 deletions(-) diff --git a/src/main/scala/leon/laziness/ClosurePreAsserter.scala b/src/main/scala/leon/laziness/ClosurePreAsserter.scala index a55cbbc00..18398850c 100644 --- a/src/main/scala/leon/laziness/ClosurePreAsserter.scala +++ b/src/main/scala/leon/laziness/ClosurePreAsserter.scala @@ -1,20 +1,15 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ import purescala.DefOps._ -import purescala.Extractors._ import purescala.Types._ import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ import leon.invariant.util.ProgramUtil._ import leon.invariant.util.PredicateUtil._ import LazinessUtil._ diff --git a/src/main/scala/leon/laziness/FreeVariableFactory.scala b/src/main/scala/leon/laziness/FreeVariableFactory.scala index 9e93edb5e..441da84ba 100644 --- a/src/main/scala/leon/laziness/FreeVariableFactory.scala +++ b/src/main/scala/leon/laziness/FreeVariableFactory.scala @@ -1,31 +1,11 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ -import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ -import purescala.ExprOps._ -import purescala.DefOps._ -import purescala.Extractors._ import purescala.Types._ -import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase -import LazinessUtil._ -import invariant.util.ProgramUtil._ /** * A class that maintains a data type that can used to diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala index 60daeb0d3..37e14755f 100644 --- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala +++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala @@ -1,40 +1,13 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ import invariant.structure.FunctionUtils._ import purescala.ScalaPrinter -import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ -import purescala.Extractors._ -import purescala.Types._ -import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import leon.verification.VerificationPhase -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.solvers._ -import leon.solvers.z3._ -import leon.transformations._ -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase import LazinessUtil._ -import invariant.datastructure._ -import invariant.util.ProgramUtil._ -import purescala.Constructors._ -import leon.verification._ -import PredicateUtil._ -import leon.invariant.engine._ import LazyVerificationPhase._ import utils._ import java.io. diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala index 903ef54e9..f65c385ed 100644 --- a/src/main/scala/leon/laziness/LazinessUtil.scala +++ b/src/main/scala/leon/laziness/LazinessUtil.scala @@ -1,30 +1,16 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ -import invariant.util._ -import invariant.structure.FunctionUtils._ import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ -import purescala.ExprOps._ import purescala.DefOps._ -import purescala.Extractors._ import purescala.Types._ -import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ import java.io.File import java.io.FileWriter import java.io.BufferedWriter import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase -import purescala.PrinterOptions object LazinessUtil { diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala index a47855f26..58fa16741 100644 --- a/src/main/scala/leon/laziness/LazyClosureConverter.scala +++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala @@ -1,29 +1,15 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ import purescala.Extractors._ import purescala.Types._ import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase import LazinessUtil._ import ProgramUtil._ import PredicateUtil._ diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala index faab5ef4d..1a69fa89d 100644 --- a/src/main/scala/leon/laziness/LazyClosureFactory.scala +++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala @@ -1,29 +1,13 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ -import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ -import purescala.Extractors._ import purescala.Types._ import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase import LazinessUtil._ //case class ClosureData(tpe: TypeTree, absDef: AbstractClassDef, caseClass: Seq[CaseClassDef]) diff --git a/src/main/scala/leon/laziness/LazyExpressionLifter.scala b/src/main/scala/leon/laziness/LazyExpressionLifter.scala index 96683d611..545fb761e 100644 --- a/src/main/scala/leon/laziness/LazyExpressionLifter.scala +++ b/src/main/scala/leon/laziness/LazyExpressionLifter.scala @@ -1,41 +1,18 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ import purescala.Extractors._ import purescala.Types._ import purescala.TypeOps._ import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import leon.verification.VerificationPhase -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.solvers._ -import leon.solvers.z3._ -import leon.transformations._ -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase import LazinessUtil._ -import invariant.datastructure._ import invariant.util.ProgramUtil._ -import purescala.Constructors._ -import leon.verification._ -import PredicateUtil._ -import leon.invariant.engine._ import FreeVariableFactory._ object LazyExpressionLifter { diff --git a/src/main/scala/leon/laziness/LazyFunctionsManager.scala b/src/main/scala/leon/laziness/LazyFunctionsManager.scala index b5197ac4c..46220895e 100644 --- a/src/main/scala/leon/laziness/LazyFunctionsManager.scala +++ b/src/main/scala/leon/laziness/LazyFunctionsManager.scala @@ -1,29 +1,11 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ -import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter -import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ import purescala.Extractors._ -import purescala.Types._ -import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase import LazinessUtil._ class LazyFunctionsManager(p: Program) { diff --git a/src/main/scala/leon/laziness/LazyInstrumenter.scala b/src/main/scala/leon/laziness/LazyInstrumenter.scala index 764a5606f..6dc5a7e50 100644 --- a/src/main/scala/leon/laziness/LazyInstrumenter.scala +++ b/src/main/scala/leon/laziness/LazyInstrumenter.scala @@ -1,28 +1,11 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ -import invariant.util._ -import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ -import purescala.ExprOps._ -import purescala.DefOps._ -import purescala.Extractors._ import purescala.Types._ import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main import leon.transformations._ import LazinessUtil._ diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala index dcc0384d7..ed1a93c88 100644 --- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala +++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala @@ -1,40 +1,19 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ import invariant.util._ import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ -import purescala.Extractors._ -import purescala.Types._ -import leon.invariant.util.TypeUtil._ -import leon.invariant.util.LetTupleSimplification._ -import leon.verification.VerificationPhase -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.solvers._ -import leon.solvers.z3._ -import leon.transformations._ -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase +import solvers._ +import transformations._ import LazinessUtil._ -import invariant.datastructure._ -import invariant.util.ProgramUtil._ import purescala.Constructors._ -import leon.verification._ +import verification._ import PredicateUtil._ -import leon.invariant.engine._ +import invariant.engine._ object LazyVerificationPhase { diff --git a/src/main/scala/leon/laziness/TypeChecker.scala b/src/main/scala/leon/laziness/TypeChecker.scala index 96687b856..ab9c1b3e0 100644 --- a/src/main/scala/leon/laziness/TypeChecker.scala +++ b/src/main/scala/leon/laziness/TypeChecker.scala @@ -1,15 +1,13 @@ package leon package laziness -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ -import purescala.ExprOps._ import purescala.Extractors._ import purescala.Types._ import purescala.TypeOps._ -import leon.invariant.util.TypeUtil._ +import invariant.util.TypeUtil._ object TypeChecker { /** diff --git a/src/main/scala/leon/laziness/TypeRectifier.scala b/src/main/scala/leon/laziness/TypeRectifier.scala index a048a969a..72d61bd7c 100644 --- a/src/main/scala/leon/laziness/TypeRectifier.scala +++ b/src/main/scala/leon/laziness/TypeRectifier.scala @@ -1,29 +1,15 @@ package leon package laziness -import invariant.factories._ -import invariant.util.Util._ -import invariant.util._ import invariant.structure.FunctionUtils._ -import purescala.ScalaPrinter import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.DefOps._ import purescala.Extractors._ import purescala.Types._ import leon.invariant.util.TypeUtil._ import leon.invariant.util.LetTupleSimplification._ -import java.io.File -import java.io.FileWriter -import java.io.BufferedWriter -import scala.util.matching.Regex -import leon.purescala.PrettyPrinter -import leon.LeonContext -import leon.LeonOptionDef -import leon.Main -import leon.TransformationPhase import LazinessUtil._ import leon.invariant.datastructure.DisjointSets import invariant.util.ProgramUtil._ @@ -34,14 +20,11 @@ import invariant.util.ProgramUtil._ * Result is a program in which all type paramters of functions, types of * parameters of functions are correct. * The subsequent phase performs a local type inference. - * @param placeHolderParameter Expected to returns true iff a type parameter - * is meant as a placeholder and cannot be used - * to represent a unified type */ class TypeRectifier(p: Program, clFactory: LazyClosureFactory) { val typeClasses = { - var tc = new DisjointSets[TypeTree]() + val tc = new DisjointSets[TypeTree]() p.definedFunctions.foreach { case fd if fd.hasBody && !fd.isLibrary && !fd.isInvariant => postTraversal { -- GitLab