From 5a3a65c9e6a20ff093b0acf8d89c7bb3495f8ff7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 17 Mar 2015 12:37:57 +0100
Subject: [PATCH] Even more fixes
---
src/main/scala/leon/purescala/Common.scala | 5 +++--
.../scala/leon/purescala/Constructors.scala | 13 ++++++------
.../scala/leon/purescala/Definitions.scala | 11 +++++-----
src/main/scala/leon/purescala/ExprOps.scala | 20 +++++++++----------
.../scala/leon/purescala/Expressions.scala | 15 ++++++--------
.../scala/leon/purescala/Extractors.scala | 12 +++++------
.../scala/leon/purescala/RestoreMethods.scala | 16 +++++++--------
.../scala/leon/purescala/Transformer.scala | 1 -
.../leon/purescala/TreeNormalizations.scala | 9 +++++----
src/main/scala/leon/purescala/TypeOps.scala | 1 -
.../scala/leon/synthesis/rules/CEGLESS.scala | 4 ++--
.../scala/leon/synthesis/rules/TEGLESS.scala | 2 +-
.../leon/verification/AnalysisPhase.scala | 6 +++---
.../leon/test/purescala/WithLikelyEq.scala | 4 ++--
14 files changed, 56 insertions(+), 63 deletions(-)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 6da84692b..8cb2b732e 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -4,11 +4,12 @@ package leon
package purescala
import utils._
+import Expressions.Variable
+import Types._
import Definitions.Definition
object Common {
- 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/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index dcca26675..24f43d756 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -3,13 +3,14 @@
package leon
package purescala
+import Expressions._
+import ExprOps._
+import Definitions._
+import TypeOps._
+import Common._
+import Types._
+
object Constructors {
- import Expressions._
- import ExprOps._
- import Definitions._
- import TypeOps._
- import Common._
- 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/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 680e7c099..e7dd7e202 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -3,15 +3,14 @@
package leon
package purescala
-import scala.collection.generic.CanBuildFrom
import utils.Library
+import Common._
+import Expressions._
+import ExprOps._
+import Types._
+import TypeOps._
object Definitions {
- import Common._
- import Expressions._
- import ExprOps._
- import Types._
- import TypeOps._
sealed abstract class Definition extends Tree {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 2f7f2ab35..fe049f5af 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -3,21 +3,19 @@
package leon
package purescala
+import Common._
+import Types._
+import Definitions._
+import Expressions._
+import TypeOps._
+import Extractors._
+import Constructors._
+import DefOps._
import utils.Simplifiers
-
-import leon.solvers._
-
+import solvers._
import scala.collection.concurrent.TrieMap
object ExprOps {
- import Common._
- import Types._
- import Definitions._
- import Expressions._
- import TypeOps._
- import Extractors._
- import Constructors._
- import DefOps._
/**
* Core API
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 32e56f1da..ec4038abc 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -3,21 +3,18 @@
package leon
package purescala
-import utils._
+import Common._
+import Types._
+import TypeOps._
+import Definitions._
+import Extractors._
+import Constructors._
/** AST definitions for Pure Scala. */
object Expressions {
- import Common._
- import Types._
- import TypeOps._
- import Definitions._
- import Extractors._
- import Constructors._
-
/* EXPRESSIONS */
abstract class Expr extends Tree with Typed with Serializable {
- // All Expr's have constant type
override val getType: TypeTree
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 9f705f388..8cde59fe8 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -4,15 +4,13 @@ package leon
package purescala
import Expressions._
+import Common._
+import Types._
+import Definitions._
+import Constructors._
+import ExprOps._
object Extractors {
- import Common._
- import Types._
- import TypeOps._
- import Definitions._
- import Extractors._
- import Constructors._
- import ExprOps._
object UnaryOperator {
def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index 353bb8697..64eb74bfa 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -1,12 +1,12 @@
-package leon.purescala
+package leon
+package purescala
-import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps.{replaceFromIDs,functionCallsOf}
-import leon.purescala.DefOps.{applyOnFunDef,preMapOnFunDef}
-import leon.purescala.Types._
+import Definitions._
+import Common._
+import Expressions._
+import ExprOps.{replaceFromIDs,functionCallsOf}
+import DefOps.{applyOnFunDef,preMapOnFunDef}
+import Types._
import utils.GraphOps._
object RestoreMethods extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/Transformer.scala b/src/main/scala/leon/purescala/Transformer.scala
index 46314714f..d4a307d99 100644
--- a/src/main/scala/leon/purescala/Transformer.scala
+++ b/src/main/scala/leon/purescala/Transformer.scala
@@ -5,7 +5,6 @@ package purescala
import purescala.Expressions._
-
trait Transformer {
def transform(e: Expr): Expr
}
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 7b80083e4..755b2c784 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -3,11 +3,12 @@
package leon
package purescala
+import Common._
+import Types._
+import Expressions._
+import ExprOps._
+
object TreeNormalizations {
- import Common._
- import Types._
- import Expressions._
- import ExprOps._
/* TODO: we should add CNF and DNF at least */
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 14eba4fe9..2fca2ea89 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -3,7 +3,6 @@
package leon
package purescala
-import ExprOps.postMap
import Types._
import Definitions._
import Common._
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 893657d4c..a746dcfdd 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -4,8 +4,8 @@ package leon
package synthesis
package rules
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
index f182305ac..c2a4cc4c6 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
@@ -4,7 +4,7 @@ package leon
package synthesis
package rules
-import purescala.TypeTrees._
+import purescala.Types._
import purescala.Extractors._
import utils._
import utils.ExpressionGrammars._
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index c849441e0..143f6a5cd 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -117,7 +117,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
reporter.synchronized {
def title(s : String) = s" => $s"
solverResult match {
- case _ if interruptManager.isInterrupted() =>
+ case _ if interruptManager.isInterrupted =>
reporter.warning(title("CANCELLED"))
vcInfo.time = Some(dt)
false
@@ -158,14 +158,14 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
if (checkInParallel) {
val allVCsPar = (for {(_, vcs) <- vcs.toSeq; vcInfo <- vcs} yield vcInfo).par
- for (vc <- allVCsPar if !interruptManager.isInterrupted() && !interrupt) {
+ for (vc <- allVCsPar if !interruptManager.isInterrupted && !interrupt) {
checkVC(vc)
interrupt = interruptOn(vc)
}
} else {
for {
(funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1.getPos < b._1.getPos)
- vc <- vcs if !interruptManager.isInterrupted() && !interrupt
+ vc <- vcs if !interruptManager.isInterrupted && !interrupt
} {
checkVC(vc)
interrupt = interruptOn(vc)
diff --git a/src/test/scala/leon/test/purescala/WithLikelyEq.scala b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
index 7fd034123..988247a59 100644
--- a/src/test/scala/leon/test/purescala/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
@@ -7,8 +7,8 @@ import leon.test._
import leon.evaluators._
import leon.purescala.Common._
import leon.purescala.Definitions._
-import leon.purescala.TreeOps.replace
-import leon.purescala.Trees._
+import leon.purescala.ExprOps.replace
+import leon.purescala.Expressions._
/*
* Determine if two expressions over arithmetic variables are likely to be equal.
--
GitLab