From fb90ceb34d04dbe07d82b42eaa869c2a26cf957b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 14:45:39 +0200
Subject: [PATCH] Fix == bugs/ run Intellij inspection
---
src/main/scala/inox/ast/Extractors.scala | 4 ++--
src/main/scala/inox/ast/GenTreeOps.scala | 2 +-
src/main/scala/inox/ast/Printers.scala | 6 +++---
src/main/scala/inox/ast/SymbolOps.scala | 8 ++++----
src/main/scala/inox/ast/TypeOps.scala | 2 +-
src/main/scala/inox/evaluators/SolvingEvaluator.scala | 4 ++--
.../inox/solvers/unrolling/QuantificationTemplates.scala | 6 +++---
.../scala/inox/solvers/unrolling/UnrollingSolver.scala | 2 +-
src/main/scala/inox/utils/ASCIIHelpers.scala | 2 +-
src/main/scala/inox/utils/GraphPrinters.scala | 4 ++--
src/main/scala/inox/utils/SeqUtils.scala | 2 +-
src/main/scala/inox/utils/StreamUtils.scala | 8 ++++----
12 files changed, 25 insertions(+), 25 deletions(-)
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 173e2d5d1..c95132d7e 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -127,7 +127,7 @@ trait Extractors { self: Trees =>
case FiniteSet(els, base) =>
Some((els, els => FiniteSet(els, base)))
case FiniteBag(els, base) =>
- val subArgs = els.flatMap { case (k, v) => Seq(k, v) }.toSeq
+ val subArgs = els.flatMap { case (k, v) => Seq(k, v) }
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]): Seq[(Expr, Expr)] = kvs match {
case Seq(k, v, t @ _*) =>
@@ -139,7 +139,7 @@ trait Extractors { self: Trees =>
}
Some((subArgs, builder))
case FiniteMap(args, f, t) => {
- val subArgs = args.flatMap { case (k, v) => Seq(k, v) }.toSeq
+ val subArgs = args.flatMap { case (k, v) => Seq(k, v) }
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]): Seq[(Expr, Expr)] = kvs match {
case Seq(k, v, t @ _*) =>
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index d1690fbb3..273d2180d 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -439,7 +439,7 @@ trait GenTreeOps {
case _ =>
}
}
- return None
+ None
}
object Same {
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 9e751eec0..9cab659b5 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -86,7 +86,7 @@ trait Printers { self: Trees =>
case Variable(id, _) =>
p"$id"
- case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd == v2 && v2 == v3 =>
+ case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd.toVariable == v2 && v2 == v3 =>
p"$expr.substring($start)"
case Let(b,d,e) =>
@@ -137,7 +137,7 @@ trait Printers { self: Trees =>
case CaseClassSelector(e, id) => p"$e.$id"
case FunctionInvocation(id, tps, args) =>
- p"${id}${nary(tps, ", ", "[", "]")}"
+ p"$id${nary(tps, ", ", "[", "]")}"
if (args.nonEmpty) {
p"($args)"
}
@@ -146,7 +146,7 @@ trait Printers { self: Trees =>
p"$caller($args)"
case Lambda(Seq(vd), FunctionInvocation(id, Seq(), Seq(arg))) if vd == arg =>
- p"${id}"
+ p"$id"
case Lambda(args, body) =>
optP { p"($args) => $body" }
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 0cc2b401b..2fa81b40f 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -681,16 +681,16 @@ trait SymbolOps { self: TypeOps =>
case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
fbtpe == tpe &&
elements.forall{ case (key, value) => isValueOfType(key, tpe) && isValueOfType(value, IntegerType) }
- case (FiniteMap(elems, tk, tv), MapType(from, to)) =>
- (tk == from) < s"$tk not equal to $from" && (tv == to) < s"$tv not equal to $to" &&
- (elems forall (kv => isValueOfType(kv._1, from) < s"${kv._1} not a value of type ${from}" && isValueOfType(unWrapSome(kv._2), to) < s"${unWrapSome(kv._2)} not a value of type ${to}" ))
+ case (FiniteMap(elems, default, kt), MapType(from, to)) =>
+ (kt == from) < s"$kt not equal to $from" && (default.getType == to) < s"${default.getType} not equal to $to" &&
+ (elems forall (kv => isValueOfType(kv._1, from) < s"${kv._1} not a value of type $from" && isValueOfType(unWrapSome(kv._2), to) < s"${unWrapSome(kv._2)} not a value of type ${to}" ))
case (CaseClass(ct, args), ct2: ClassType) =>
isSubtypeOf(ct, ct2) < s"$ct not a subtype of $ct2" &&
((args zip ct.tcd.toCase.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2) < s"${argstyped._1} not a value of type ${argstyped._2}" ))
case (Lambda(valdefs, body), FunctionType(ins, out)) =>
variablesOf(e).isEmpty &&
(valdefs zip ins forall (vdin => isSubtypeOf(vdin._2, vdin._1.getType) < s"${vdin._2} is not a subtype of ${vdin._1.getType}")) &&
- (isSubtypeOf(body.getType, out)) < s"${body.getType} is not a subtype of ${out}"
+ isSubtypeOf(body.getType, out) < s"${body.getType} is not a subtype of $out"
case _ => false
}
}
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 84ae5e354..b7019771e 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -210,7 +210,7 @@ trait TypeOps {
def typeCardinality(tp: Type): Option[Int] = {
def cards(tps: Seq[Type]): Option[Seq[Int]] = {
- val cardinalities = tps.map(typeCardinality).flatten
+ val cardinalities = tps.flatMap(typeCardinality)
if (cardinalities.size == tps.size) {
Some(cardinalities)
} else {
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index fd18f7060..554f6a44a 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -29,8 +29,8 @@ trait SolvingEvaluator extends Evaluator {
val timer = ctx.timers.evaluators.specs.start()
val sf = getSolver(options.options.collect {
- case o @ InoxOption(opt, _) if opt == optForallCache => o
- }.toSeq : _*)
+ case o@InoxOption(opt, _) if opt == optForallCache => o
+ } : _*)
import SolverResponses._
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 250075f49..a46423abf 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -204,7 +204,7 @@ trait QuantificationTemplates { self: Templates =>
quantifications, ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, lambdaAxioms, templates)
private def assumptions: Seq[Encoded] =
- quantifications.collect { case q: GeneralQuantification => q.currentQ2Var }.toSeq
+ quantifications.collect { case q: GeneralQuantification => q.currentQ2Var }
def satisfactionAssumptions = assumptions
def refutationAssumptions = assumptions
@@ -369,7 +369,7 @@ trait QuantificationTemplates { self: Templates =>
q -> (grounds(q).toSet ++ constraints.flatMap { case (key, i) =>
if (correspond(matcherKey(m), key)) Some(bs -> m.args(i)) else None
})
- }).toMap
+ })
/* Transform the map to sequences into a sequence of maps making sure that the current
* matcher is part of the mapping (otherwise, instantiation has already taken place). */
@@ -711,7 +711,7 @@ trait QuantificationTemplates { self: Templates =>
def promoteQuantifications: Unit = {
val optGen = quantificationsManager.unrollGeneration
- if (!optGen.isDefined)
+ if (optGen.isEmpty)
throw FatalError("Attempting to promote inexistent quantifiers")
val diff = (currentGeneration - optGen.get) max 0
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 667e1b8e3..887e00844 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -385,7 +385,7 @@ trait AbstractUnrollingSolver
}
case InstantiateQuantifiers =>
- if (!templates.quantificationsManager.unrollGeneration.isDefined) {
+ if (templates.quantificationsManager.unrollGeneration.isEmpty) {
reporter.error("Something went wrong. The model is not transitive yet we can't instantiate!?")
CheckResult.cast(Unknown)
} else {
diff --git a/src/main/scala/inox/utils/ASCIIHelpers.scala b/src/main/scala/inox/utils/ASCIIHelpers.scala
index 3737bd973..162e6b69b 100644
--- a/src/main/scala/inox/utils/ASCIIHelpers.scala
+++ b/src/main/scala/inox/utils/ASCIIHelpers.scala
@@ -87,7 +87,7 @@ object ASCIIHelpers {
sb append " "
}
- val size = (i to i+c.spanning-1).map(colSizes).sum + (c.spanning-1) * 2
+ val size = (i until i + c.spanning).map(colSizes).sum + (c.spanning-1) * 2
if (size >= 0) {
if (c.align == Left) {
diff --git a/src/main/scala/inox/utils/GraphPrinters.scala b/src/main/scala/inox/utils/GraphPrinters.scala
index e4c04a8fc..1f08143d3 100644
--- a/src/main/scala/inox/utils/GraphPrinters.scala
+++ b/src/main/scala/inox/utils/GraphPrinters.scala
@@ -113,7 +113,7 @@ object GraphPrinters {
def nextColor = {
_nextColor += 1
- val colornumber: String = if((_nextColor/bgColors.size)%3 == 0) "" else ((_nextColor/bgColors.size)%3)+"";
+ val colornumber: String = if((_nextColor/bgColors.size)%3 == 0) "" else ((_nextColor/bgColors.size)%3)+""
bgColors(_nextColor%bgColors.size)+colornumber
}
@@ -169,7 +169,7 @@ object GraphPrinters {
"turquoise4", "violet", "violetred", "violetred1", "violetred2", "violetred3",
"violetred4", "wheat", "wheat1", "wheat2", "wheat3", "wheat4", "white",
"whitesmoke", "yellow", "yellow1", "yellow2", "yellow3", "yellow4",
- "yellowgreen");
+ "yellowgreen")
def randomColor = {
_nextColor += 1
diff --git a/src/main/scala/inox/utils/SeqUtils.scala b/src/main/scala/inox/utils/SeqUtils.scala
index 659e5291c..ad0c997cd 100644
--- a/src/main/scala/inox/utils/SeqUtils.scala
+++ b/src/main/scala/inox/utils/SeqUtils.scala
@@ -63,7 +63,7 @@ object SeqUtils {
var res: Seq[Seq[T]] = Nil
var c = es
- while (!c.isEmpty) {
+ while (c.nonEmpty) {
val (span, rest) = c.span(p)
if (span.isEmpty) {
diff --git a/src/main/scala/inox/utils/StreamUtils.scala b/src/main/scala/inox/utils/StreamUtils.scala
index da89263c5..a70addd07 100644
--- a/src/main/scala/inox/utils/StreamUtils.scala
+++ b/src/main/scala/inox/utils/StreamUtils.scala
@@ -36,10 +36,10 @@ object StreamUtils {
}
private def reverseCantorPair(z: Int): (Int, Int) = {
- val t = Math.floor((-1.0f + Math.sqrt(1.0f + 8.0f * z))/2.0f).toInt;
- val x = t * (t + 3) / 2 - z;
- val y = z - t * (t + 1) / 2;
- (x, y)
+ val t = Math.floor((-1.0f + Math.sqrt(1.0f + 8.0f * z))/2.0f).toInt
+ val x = t * (t + 3) / 2 - z
+ val y = z - t * (t + 1) / 2
+ (x, y)
}
/** Combines two streams into one using cantor's unpairing function.
--
GitLab