diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
index 7baeb86cefaf26235c1ecd982e1eefaa889d7965..4bd6dd0dafa62ba6768aa55fdf717dae92f90f54 100644
--- a/src/main/scala/leon/Stopwatch.scala
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -24,7 +24,7 @@ class StopwatchCollection(name: String) {
result
}
- override def toString = "%20s: %5dms".format(name, acc)
+ override def toString = f"$name%20s: ${acc}%5dms"
}
/** Implements a stopwatch for profiling purposes */
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 9cfc6170a5c05e8faa6bca8cef7c6557ea39755d..023ef61ac98ad6650360f7682df7542ef2b25b19 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -319,22 +319,22 @@ trait CodeGeneration {
case SubsetOf(s1, s2) =>
mkExpr(s1, ch)
mkExpr(s2, ch)
- ch << InvokeVirtual(SetClass, "subsetOf", "(L%s;)Z".format(SetClass))
+ ch << InvokeVirtual(SetClass, "subsetOf", s"(L$SetClass;)Z")
case SetIntersection(s1, s2) =>
mkExpr(s1, ch)
mkExpr(s2, ch)
- ch << InvokeVirtual(SetClass, "intersect", "(L%s;)L%s;".format(SetClass,SetClass))
+ ch << InvokeVirtual(SetClass, "intersect", s"(L$SetClass;)L$SetClass;")
case SetUnion(s1, s2) =>
mkExpr(s1, ch)
mkExpr(s2, ch)
- ch << InvokeVirtual(SetClass, "union", "(L%s;)L%s;".format(SetClass,SetClass))
+ ch << InvokeVirtual(SetClass, "union", s"(L$SetClass;)L$SetClass;")
case SetDifference(s1, s2) =>
mkExpr(s1, ch)
mkExpr(s2, ch)
- ch << InvokeVirtual(SetClass, "minus", "(L%s;)L%s;".format(SetClass,SetClass))
+ ch << InvokeVirtual(SetClass, "minus", s"(L$SetClass;)L$SetClass;")
// Maps
case FiniteMap(ss) =>
@@ -361,7 +361,7 @@ trait CodeGeneration {
case MapUnion(m1, m2) =>
mkExpr(m1, ch)
mkExpr(m2, ch)
- ch << InvokeVirtual(MapClass, "union", "(L%s;)L%s;".format(MapClass,MapClass))
+ ch << InvokeVirtual(MapClass, "union", s"(L$MapClass;)L$MapClass;")
// Branching
case IfExpr(c, t, e) =>
@@ -630,31 +630,31 @@ trait CodeGeneration {
case Plus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << InvokeVirtual(BigIntClass, "add", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "add", s"(L$BigIntClass;)L$BigIntClass;")
case Minus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << InvokeVirtual(BigIntClass, "sub", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "sub", s"(L$BigIntClass;)L$BigIntClass;")
case Times(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << InvokeVirtual(BigIntClass, "mult", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "mult", s"(L$BigIntClass;)L$BigIntClass;")
case Division(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << InvokeVirtual(BigIntClass, "div", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "div", s"(L$BigIntClass;)L$BigIntClass;")
case Modulo(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
- ch << InvokeVirtual(BigIntClass, "mod", "(L%s;)L%s;".format(BigIntClass, BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "mod", s"(L$BigIntClass;)L$BigIntClass;")
case UMinus(e) =>
mkExpr(e, ch)
- ch << InvokeVirtual(BigIntClass, "neg", "()L%s;".format(BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "neg", s"()L$BigIntClass;")
//BV arithmetic
case BVPlus(l, r) =>
@@ -745,7 +745,7 @@ trait CodeGeneration {
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
- case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
+ case other => throw CompilationException(s"Cannot compile finite array expression whose type is $other.")
}
//srcArrary and targetArray is on the stack
ch << DUP_X1 //insert targetArray under srcArray
@@ -769,7 +769,7 @@ trait CodeGeneration {
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
- case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
+ case other => throw CompilationException(s"Cannot compile finite array expression whose type is $other.")
}
for((i, e) <- elems) {
ch << DUP << Ldc(i)
@@ -863,7 +863,7 @@ trait CodeGeneration {
case at @ ArrayType(et) =>
ch << New(BoxedArrayClass) << DUP
mkExpr(e, ch)
- ch << InvokeSpecial(BoxedArrayClass, constructorName, "(%s)V".format(typeToJVM(at)))
+ ch << InvokeSpecial(BoxedArrayClass, constructorName, s"(${typeToJVM(at)})V")
case _ =>
mkExpr(e, ch)
@@ -884,7 +884,7 @@ trait CodeGeneration {
ch << New(BoxedCharClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedCharClass, constructorName, "(C)V")
case at @ ArrayType(et) =>
- ch << New(BoxedArrayClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedArrayClass, constructorName, "(%s)V".format(typeToJVM(at)))
+ ch << New(BoxedArrayClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedArrayClass, constructorName, s"(${typeToJVM(at)})V")
case _ =>
}
}
@@ -925,7 +925,7 @@ trait CodeGeneration {
case tp : TypeParameter =>
case tp : ArrayType =>
- ch << CheckCast(BoxedArrayClass) << InvokeVirtual(BoxedArrayClass, "arrayValue", "()%s".format(typeToJVM(tp)))
+ ch << CheckCast(BoxedArrayClass) << InvokeVirtual(BoxedArrayClass, "arrayValue", s"()${typeToJVM(tp)}")
ch << CheckCast(typeToJVM(tp))
case _ =>
@@ -982,7 +982,7 @@ trait CodeGeneration {
case Int32Type =>
ch << If_ICmpLt(thenn) << Goto(elze)
case IntegerType =>
- ch << InvokeVirtual(BigIntClass, "lessThan", "(L%s;)Z".format(BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "lessThan", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
}
@@ -993,7 +993,7 @@ trait CodeGeneration {
case Int32Type =>
ch << If_ICmpGt(thenn) << Goto(elze)
case IntegerType =>
- ch << InvokeVirtual(BigIntClass, "greaterThan", "(L%s;)Z".format(BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "greaterThan", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
}
@@ -1004,7 +1004,7 @@ trait CodeGeneration {
case Int32Type =>
ch << If_ICmpLe(thenn) << Goto(elze)
case IntegerType =>
- ch << InvokeVirtual(BigIntClass, "lessEquals", "(L%s;)Z".format(BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "lessEquals", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
}
@@ -1015,7 +1015,7 @@ trait CodeGeneration {
case Int32Type =>
ch << If_ICmpGe(thenn) << Goto(elze)
case IntegerType =>
- ch << InvokeVirtual(BigIntClass, "greaterEquals", "(L%s;)Z".format(BigIntClass))
+ ch << InvokeVirtual(BigIntClass, "greaterEquals", s"(L$BigIntClass;)Z")
ch << IfEq(elze) << Goto(thenn)
}
@@ -1377,7 +1377,7 @@ trait CodeGeneration {
// If we are monitoring function calls, we have an extra argument on the constructor
val realArgs = if (params.requireMonitor) {
("L" + MonitorClass + ";") +: (namesTypes map (_._2))
- } else (namesTypes map (_._2))
+ } else namesTypes map (_._2)
// Offset of the first Scala parameter of the constructor
val paramOffset = if (params.requireMonitor) 2 else 1
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 6fcdbc00f823a1a6b98301fb47ad3ce96fb4906f..b166be16bd3fe82bb93170ec7560e19c189193e1 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -245,7 +245,7 @@ class CompilationUnit(val ctx: LeonContext,
def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
if(e.getType == Untyped) {
- throw new IllegalArgumentException("Cannot compile untyped expression [%s].".format(e))
+ throw new IllegalArgumentException(s"Cannot compile untyped expression [$e].")
}
compiledN += 1
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index fac16d509df7dcc972255e0684970a405f76cd99..c9fbbff703e82b993c2fe3dd0506512d260069d9 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -46,7 +46,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
private def getConstructorFor(t: CaseClassType, act: AbstractClassType): Constructor[Expr, TypeTree] = {
// We "up-cast" the returnType of the specific caseclass generator to match its superclass
- getConstructors(t)(0).copy(retType = act)
+ getConstructors(t).head.copy(retType = act)
}
@@ -175,7 +175,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case act : AbstractClassType =>
getConstructorFor(cct, act)
case cct : CaseClassType =>
- getConstructors(cct)(0)
+ getConstructors(cct).head
}
val fields = cc.productElements()
@@ -201,7 +201,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val parts = unwrapTupleType(tpe, t.getArity)
- val c = getConstructors(tpe)(0)
+ val c = getConstructors(tpe).head
val elems = for (i <- 0 until t.getArity) yield {
if (((r >> i) & 1) == 1) {
@@ -245,7 +245,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val result = ce.evalFromJVM(jvmArgs, monitor)
// jvmArgs is getting updated by evaluating
- val pattern = valueToPattern(jvmArgs(0), ttype)
+ val pattern = valueToPattern(jvmArgs.head, ttype)
(EvaluationResults.Successful(result), if (!pattern._2) Some(pattern._1) else None)
} catch {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 8d8cdd317b37ad78fc743c85067c7888237fbdb4..7650cd5c21ce90952b99deb3f56e2f558364eaeb 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -634,6 +634,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
}
- def typeErrorMsg(tree : Expr, expected : TypeTree) : String = "Type error : expected %s, found %s.".format(expected, tree)
+ def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected $expected, found $tree."
}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index a66f16300a7ecaafbc08538d8a3c07461ed140f8..bc239010561c542fa23b4c804a8dcc936c041241 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -338,7 +338,7 @@ trait ASTExtractors {
object ExMainFunctionDef {
def unapply(dd: DefDef): Boolean = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 1 => {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss.head.size == 1 => {
true
}
case _ => false
@@ -432,7 +432,7 @@ trait ASTExtractors {
// Split the name into pieces, to find owner of the parameter + param.index
// Form has to be <owner name>$default$<param index>
- val symPieces = sym.name.toString.reverse.split("\\$",3).reverse map { _.reverse }
+ val symPieces = sym.name.toString.reverse.split("\\$", 3).reverseMap(_.reverse)
try {
if (symPieces(1) != "default" || symPieces(0) == "copy") throw new IllegalArgumentException("")
@@ -508,7 +508,7 @@ trait ASTExtractors {
case a @ Apply(
TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "withOracle"), types),
Function(vds, body) :: Nil) =>
- Some(((types zip vds.map(_.symbol)).toList, body))
+ Some(((types zip vds.map(_.symbol)), body))
case _ => None
}
}
@@ -525,7 +525,7 @@ trait ASTExtractors {
case a @ Apply(
TypeApply(s @ ExSymbol("leon", "lang", "forall"), types),
Function(vds, predicateBody) :: Nil) =>
- Some(((types zip vds.map(_.symbol)).toList, predicateBody))
+ Some(((types zip vds.map(_.symbol)), predicateBody))
case _ => None
}
}
@@ -708,7 +708,7 @@ trait ASTExtractors {
object ExSomeConstruction {
def unapply(tree: Apply) : Option[(Type,Tree)] = tree match {
case Apply(s @ Select(New(tpt), n), arg) if arg.size == 1 && n == nme.CONSTRUCTOR && tpt.symbol.name.toString == "Some" => tpt.tpe match {
- case TypeRef(_, sym, tpe :: Nil) => Some((tpe, arg(0)))
+ case TypeRef(_, sym, tpe :: Nil) => Some((tpe, arg.head))
case _ => None
}
case _ => None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index fae40d7661428af2a8bdb8493efb9643f5bfcd84..1e1fa28bf53c1fc0e1ea3ea0a93bec607584cdb2 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -184,7 +184,7 @@ trait CodeExtraction extends ASTExtractors {
}
def isIgnored(s: Symbol) = {
- (annotationsOf(s) contains "ignore") || (s.isImplicit) || (s.fullName.toString.endsWith(".main"))
+ (annotationsOf(s) contains "ignore") || s.isImplicit || s.fullName.toString.endsWith(".main")
}
def isExtern(s: Symbol) = {
@@ -195,24 +195,24 @@ trait CodeExtraction extends ASTExtractors {
try {
def isLib(u : CompilationUnit) = Build.libFiles contains u.source.file.absolute.path
- val templates: List[TempUnit] = units.reverse.map { u => u.body match {
-
+ val templates: List[TempUnit] = units.reverseMap { u => u.body match {
+
// Unit with a single package object
case PackageDef(refTree, List(PackageDef(inner, List(ExObjectDef(n, templ))))) if n == "package" =>
// File name without extension
val unitName = extractPackageRef(inner).mkString("$") + "$package"
- val id = FreshIdentifier(unitName+ "$standalone")
+ val id = FreshIdentifier(unitName + "$standalone")
TempUnit(unitName,
extractPackageRef(refTree) ++ extractPackageRef(inner),
- List( TempModule(id, templ.body, true) ),
+ List(TempModule(id, templ.body, true)),
imports.getOrElse(refTree, Nil),
!isLib(u)
)
-
- case pd @ PackageDef(refTree, lst) =>
-
+
+ case pd@PackageDef(refTree, lst) =>
+
var standaloneDefs = List[Tree]()
-
+
val modules = lst.flatMap {
case t if isIgnored(t.symbol) =>
@@ -258,16 +258,16 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(other, "Expected: top-level object/class.")
None
}
-
+
// File name without extension
val unitName = u.source.file.name.replaceFirst("[.][^.]+$", "")
- val finalModules =
- if (standaloneDefs.isEmpty) modules
+ val finalModules =
+ if (standaloneDefs.isEmpty) modules
else {
- val id = FreshIdentifier(unitName+ "$standalone")
- ( TempModule(id , standaloneDefs, true) ) :: modules
+ val id = FreshIdentifier(unitName + "$standalone")
+ TempModule(id, standaloneDefs, true) :: modules
}
-
+
TempUnit(unitName,
extractPackageRef(refTree),
finalModules,
@@ -342,7 +342,7 @@ trait CodeExtraction extends ASTExtractors {
case EmptyTree => List()
case _ => ctx.reporter.internalError("getSelectChain: unexpected Tree:\n" + e.toString)
}
- rec(e).reverse map { _.toString }
+ rec(e).reverseMap(_.toString)
}
private def extractPackageRef(refPath : RefTree) : PackageRef =
@@ -381,7 +381,7 @@ trait CodeExtraction extends ASTExtractors {
def oracleType(pos: Position, tpe: LeonType) = {
classesToClasses.find {
- case (sym, cl) => (sym.fullName.toString == "leon.lang.synthesis.Oracle")
+ case (sym, cl) => sym.fullName.toString == "leon.lang.synthesis.Oracle"
} match {
case Some((_, cd)) =>
classDefToClassType(cd, List(tpe))
@@ -1481,7 +1481,7 @@ trait CodeExtraction extends ASTExtractors {
val toUnderlying = extractType(tt)
val singletons: Seq[(LeonExpr, LeonExpr)] = elems.collect {
- case ExTuple(tpes, trees) if (trees.size == 2) =>
+ case ExTuple(tpes, trees) if trees.size == 2 =>
(extractTree(trees(0)), extractTree(trees(1)))
}
@@ -1929,7 +1929,7 @@ trait CodeExtraction extends ASTExtractors {
else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
Some(None)
else
- exprOwners(0)
+ exprOwners.head
}
def getOwner(expr: LeonExpr): Option[Option[FunDef]] = getOwner(getReturnedExpr(expr))
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index e503f3ac1f7a89e495442a2ede93ce67dbc6ae83..ca74326fe2dcdd9e3fac2802a03dd23ccf7c1350 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -246,7 +246,7 @@ object Definitions {
_methods = Nil
}
- def methods = _methods.toList
+ def methods = _methods
def knownChildren: Seq[ClassDef] = _children
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index d132d4fdf858d3b924761f2fec98126ac7b9c37b..893192822389b485c348217e89a30e916d223c66 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -528,7 +528,7 @@ object ExprOps {
def simplerLet(t: Expr) : Option[Expr] = t match {
case letExpr @ Let(i, t: Terminal, b) if isDeterministic(b) =>
- Some(replace(Map((Variable(i) -> t)), b))
+ Some(replace(Map(Variable(i) -> t), b))
case letExpr @ Let(i,e,b) if isDeterministic(b) => {
val occurrences = count {
@@ -539,7 +539,7 @@ object ExprOps {
if(occurrences == 0) {
Some(b)
} else if(occurrences == 1) {
- Some(replace(Map((Variable(i) -> e)), b))
+ Some(replace(Map(Variable(i) -> e), b))
} else {
None
}
@@ -550,7 +550,7 @@ object ExprOps {
val (remIds, remExprs) = (ids zip exprs).filter {
case (id, value: Terminal) =>
- newBody = replace(Map((Variable(id) -> value)), newBody)
+ newBody = replace(Map(Variable(id) -> value), newBody)
//we replace, so we drop old
false
case (id, value) =>
@@ -562,7 +562,7 @@ object ExprOps {
if(occurences == 0) {
false
} else if(occurences == 1) {
- newBody = replace(Map((Variable(id) -> value)), newBody)
+ newBody = replace(Map(Variable(id) -> value), newBody)
false
} else {
true
@@ -604,7 +604,7 @@ object ExprOps {
Some(body)
} else if(total == 1) {
val substMap : Map[Expr,Expr] = ids.map(Variable(_) : Expr).zipWithIndex.toMap.map {
- case (v,i) => (v -> tupleSelect(tExpr, i + 1, ids.size).copiedFrom(v))
+ case (v,i) => v -> tupleSelect(tExpr, i + 1, ids.size).copiedFrom(v)
}
Some(replace(substMap, body))
@@ -1969,7 +1969,7 @@ object ExprOps {
Some((cct.tps.head, Nil))
} else if (Some(cct.classDef) == lib.Cons) {
isListLiteral(args(1)).map { case (_, t) =>
- (cct.tps.head, args(0) :: t)
+ (cct.tps.head, args.head :: t)
}
} else None
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index f47672cb38d1518a3321a28ffc09f5c7a4365adf..0f4f93582a986e73e077b0c088cb4cc95d1a3ba1 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -185,7 +185,7 @@ object Extractors {
val lib = p.library
if (Some(cct.classDef) == lib.String) {
- isListLiteral(args(0)) match {
+ isListLiteral(args.head) match {
case Some((_, chars)) =>
val str = chars.map {
case CharLiteral(c) => Some(c)
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 6d970b65d867021ff162eff3fbae7b12f46285b8..1edd4ccbd64fb9d261d48dc1ffe4fdf1ec2fdddd 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -20,36 +20,38 @@ object MethodLifting extends TransformationPhase {
// First we create the appropriate functions from methods:
var mdToFds = Map[FunDef, FunDef]()
- program.classHierarchyRoots.filter(_.methods.nonEmpty) flatMap { cd =>
- cd.methods.map { fd =>
- // We import class type params and freshen them
- val ctParams = cd.tparams map { _.freshen }
- val tparamsMap = cd.tparams.zip(ctParams map { _.tp }).toMap
-
- val id = FreshIdentifier(cd.id.name+"$"+fd.id.name).setPos(fd.id)
- val recType = classDefToClassType(cd, ctParams.map(_.tp))
- val retType = instantiateType(fd.returnType, tparamsMap)
- val fdParams = fd.params map { vd =>
- val newId = FreshIdentifier(vd.id.name, instantiateType(vd.id.getType, tparamsMap))
- ValDef(newId).setPos(vd.getPos)
- }
- val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
-
- val receiver = FreshIdentifier("$this", recType).setPos(cd.id)
-
- val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams, fd.defType)
- nfd.copyContentFrom(fd)
- nfd.setPos(fd)
- nfd.fullBody = instantiateType(nfd.fullBody, tparamsMap, paramsMap)
-
- mdToFds += fd -> nfd
+ for {
+ cd <- program.classHierarchyRoots
+ if cd.methods.nonEmpty
+ fd <- cd.methods
+ } {
+ // We import class type params and freshen them
+ val ctParams = cd.tparams map { _.freshen }
+ val tparamsMap = cd.tparams.zip(ctParams map { _.tp }).toMap
+
+ val id = FreshIdentifier(cd.id.name+"$"+fd.id.name).setPos(fd.id)
+ val recType = classDefToClassType(cd, ctParams.map(_.tp))
+ val retType = instantiateType(fd.returnType, tparamsMap)
+ val fdParams = fd.params map { vd =>
+ val newId = FreshIdentifier(vd.id.name, instantiateType(vd.id.getType, tparamsMap))
+ ValDef(newId).setPos(vd.getPos)
}
+ val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
+
+ val receiver = FreshIdentifier("$this", recType).setPos(cd.id)
+
+ val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams, fd.defType)
+ nfd.copyContentFrom(fd)
+ nfd.setPos(fd)
+ nfd.fullBody = instantiateType(nfd.fullBody, tparamsMap, paramsMap)
+
+ mdToFds += fd -> nfd
}
def translateMethod(fd: FunDef) = {
val (nfd, rec) = mdToFds.get(fd) match {
case Some(nfd) =>
- (nfd, Some(() => Variable(nfd.params(0).id)))
+ (nfd, Some(() => Variable(nfd.params.head.id)))
case None =>
(fd, None)
}
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 755b2c784341658f734a4e08dafec6b1c5c7d78e..7a102bf835010166e890a78baa9a6894bdf234ff 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -54,7 +54,7 @@ object TreeNormalizations {
}
var exprs: Seq[Expr] = expandedForm(expr)
- val res: Array[Expr] = new Array(xs.size + 1)
+ val res: Array[Expr] = new Array(xs.length + 1)
xs.zipWithIndex.foreach{case (id, index) => {
val (terms, rests) = exprs.partition(containsId(_, id))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index d3700d15e1d5d6a3fc773cf6ffbf13a345398853..455a6fbdfaf8e257bb4a4a0762ac93ba780f2acd 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -599,9 +599,9 @@ trait SMTLIBTarget {
val RawArrayValue(_, elems, default) = fromSMT(args(1), RawArrayType(Int32Type, baseType))
if(size > 10) {
- val definedElements = elems.collect{
+ val definedElements = elems.collect {
case (IntLiteral(i), value) => (i, value)
- }.toMap
+ }
finiteArray(definedElements, Some(default, IntLiteral(size)), baseType)
} else {
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 331bc00089e3bb3d6ab1758b9d497a1d98664cb2..a22d18facc6ad62117ed2ee5967012e802454e54 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -723,7 +723,7 @@ trait AbstractZ3Solver
kind match {
case Z3NumeralIntAST(Some(v)) => {
- val leading = t.toString.substring(0, 2 min t.toString.size)
+ val leading = t.toString.substring(0, 2 min t.toString.length)
if(leading == "#x") {
_root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
case Some(hexa) => IntLiteral(hexa.toInt)
@@ -755,10 +755,10 @@ trait AbstractZ3Solver
FunctionInvocation(tfd, args.map(rec))
} else if(argsSize == 1 && (reverseADTTesters contains decl)) {
val cct = reverseADTTesters(decl)
- CaseClassInstanceOf(cct, rec(args(0)))
+ CaseClassInstanceOf(cct, rec(args.head))
} else if(argsSize == 1 && (reverseADTFieldSelectors contains decl)) {
val (cct, fid) = reverseADTFieldSelectors(decl)
- CaseClassSelector(cct, rec(args(0)), fid)
+ CaseClassSelector(cct, rec(args.head), fid)
} else if(reverseADTConstructors contains decl) {
val cct = reverseADTConstructors(decl)
assert(argsSize == cct.fields.size)
@@ -884,10 +884,10 @@ trait AbstractZ3Solver
FunctionInvocation(tfd, args.map(rec))
} else if(argsSize == 1 && reverseADTTesters.isDefinedAt(decl)) {
val cct = reverseADTTesters(decl)
- CaseClassInstanceOf(cct, rec(args(0)))
+ CaseClassInstanceOf(cct, rec(args.head))
} else if(argsSize == 1 && reverseADTFieldSelectors.isDefinedAt(decl)) {
val (cct, fid) = reverseADTFieldSelectors(decl)
- CaseClassSelector(cct, rec(args(0)), fid)
+ CaseClassSelector(cct, rec(args.head), fid)
} else if(reverseADTConstructors.isDefinedAt(decl)) {
val cct = reverseADTConstructors(decl)
CaseClass(cct, args.map(rec))
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 4829f828bffbd549ebc9e0a89501621fbb0db9c5..e4d0fb3bd3bd93ba86922afd0e513dda72795028 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -72,20 +72,20 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
val functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
- if(functions containsZ3 p._1) {
+ if (functions containsZ3 p._1) {
val tfd = functions.toLeon(p._1)
- if(!tfd.hasImplementation) {
- val (cses, default) = p._2
+ if (!tfd.hasImplementation) {
+ val (cses, default) = p._2
val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
- andJoin(
- q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
- ),
- fromZ3Formula(model, q._2),
- expr))
+ andJoin(
+ q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
+ ),
+ fromZ3Formula(model, q._2),
+ expr))
Seq((tfd.id, ite))
} else Seq()
} else Seq()
- }).toMap
+ })
val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
if(functions containsZ3 p._1) {
@@ -314,7 +314,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
case Z3AppAST(decl, args) =>
z3.getDeclKind(decl) match {
case Z3DeclKind.OpNot =>
- (args(0), true)
+ (args.head, true)
case Z3DeclKind.OpUninterpreted =>
(c, false)
}
diff --git a/src/main/scala/leon/synthesis/Algebra.scala b/src/main/scala/leon/synthesis/Algebra.scala
index f63a7fec20036bb41c0c3fa90910e86b01ce24da..e1c7a5141ccdc55e8cbccc2f06afcdf33a679534 100644
--- a/src/main/scala/leon/synthesis/Algebra.scala
+++ b/src/main/scala/leon/synthesis/Algebra.scala
@@ -48,7 +48,7 @@ object Algebra {
def gcd(as: Seq[Int]): Int = {
require(as.length >= 1)
if(as.length == 1)
- as(0).abs
+ as.head.abs
else {
var tmp = gcd(as(0), as(1))
var i = 2
@@ -83,7 +83,7 @@ object Algebra {
def gcd(as: Seq[BigInt]): BigInt = {
require(as.length >= 1)
if(as.length == 1)
- as(0).abs
+ as.head.abs
else {
var tmp = gcd(as(0), as(1))
var i = 2
@@ -114,7 +114,7 @@ object Algebra {
def lcm(as: Seq[Int]): Int = {
require(as.length >= 1)
if(as.length == 1)
- as(0).abs
+ as.head.abs
else {
var tmp = lcm(as(0), as(1))
var i = 2
@@ -192,18 +192,18 @@ object Algebra {
//val that the sol vector with the term in the equation
def eval(sol: Array[Int], equation: Array[Int]): Int = {
- require(sol.size == equation.size)
+ require(sol.length == equation.length)
sol.zip(equation).foldLeft(0)((acc, p) => acc + p._1 * p._2)
}
//multiply the matrix by the vector: [M1 M2 .. Mn] * [v1 .. vn] = v1*M1 + ... + vn*Mn]
def mult(matrix: Array[Array[Int]], vector: Array[Int]): Array[Int] = {
- require(vector.size == matrix(0).size && vector.size > 0)
+ require(vector.length == matrix(0).length && vector.length > 0)
val tmat = matrix.transpose
var tmp: Array[Int] = null
tmp = mult(vector(0), tmat(0))
var i = 1
- while(i < vector.size) {
+ while(i < vector.length) {
tmp = add(tmp, mult(vector(i), tmat(i)))
i += 1
}
@@ -213,7 +213,7 @@ object Algebra {
def mult(c: Int, v: Array[Int]): Array[Int] = v.map(_ * c)
def add(v1: Array[Int], v2: Array[Int]): Array[Int] = {
- require(v1.size == v2.size)
+ require(v1.length == v2.length)
v1.zip(v2).map(p => p._1 + p._2)
}
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index e5ae300888a3c61591dea004da505ff4a05002c8..2d0d1c623e0f4e781cb7b1594dba54e6161fa732 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -37,12 +37,12 @@ object LinearEquations {
val freshVars: Array[Identifier] = basis(0).map(_ => FreshIdentifier("v", IntegerType, true))
val tbasis = basis.transpose
- assert(freshVars.size == tbasis.size)
+ assert(freshVars.length == tbasis.length)
val basisWithFreshVars: Array[Array[Expr]] = freshVars.zip(tbasis).map{
case (lambda, column) => column.map((i: BigInt) => Times(InfiniteIntegerLiteral(i), Variable(lambda)): Expr)
}.transpose
val combinationBasis: Array[Expr] = basisWithFreshVars.map((v: Array[Expr]) => v.foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, e) => Plus(acc, e)))
- assert(combinationBasis.size == sol.size)
+ assert(combinationBasis.length == sol.size)
val subst: List[Expr] = sol.zip(combinationBasis.toList).map(p => Plus(p._1, p._2): Expr)
(pre, subst, freshVars.toList)
@@ -59,9 +59,9 @@ object LinearEquations {
//we are returning a matrix where the columns are the vectors
def linearSet(evaluator: Evaluator, as: Set[Identifier], coef: Array[BigInt]): Array[Array[BigInt]] = {
- val K = Array.ofDim[BigInt](coef.size, coef.size-1)
- for(i <- 0 until K.size) {
- for(j <- 0 until K(i).size) {
+ val K = Array.ofDim[BigInt](coef.length, coef.length-1)
+ for(i <- 0 until K.length) {
+ for(j <- 0 until K(i).length) {
if(i < j)
K(i)(j) = 0
else if(i == j) {
@@ -69,7 +69,7 @@ object LinearEquations {
}
}
}
- for(j <- 0 until K.size - 1) {
+ for(j <- 0 until K.length - 1) {
val (_, sols) = particularSolution(as, InfiniteIntegerLiteral(coef(j)*K(j)(j)) :: coef.drop(j+1).map(InfiniteIntegerLiteral).toList)
var i = 0
while(i < sols.size) {
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 349a4afbfce56a0128d62f6054ed630dc6175de2..61677d28d6b0741072f5f857ef8abdb5ab6b8783 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -104,7 +104,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
import hctx.sctx.reporter.info
- val prefix = "[%-20s] ".format(Option(ri.rule).getOrElse("?"))
+ val prefix = f"[${Option(ri.rule).getOrElse("?")}%-20s] "
info(prefix+ri.problem)
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index dfac6b7a9a394a407267d473761a393709c87882..74733489c62e9131e2bdfb9079a67cea64e3b716 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -81,7 +81,7 @@ case object ADTInduction extends Rule("ADT Induction") {
val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs, DefType.MethodDef)
- val cases = for ((sol, (problem, pre, cct, ids, calls)) <- (sols zip subProblemsInfo)) yield {
+ val cases = for ((sol, (problem, pre, cct, ids, calls)) <- sols zip subProblemsInfo) yield {
globalPre ::= and(pre, sol.pre)
val caze = CaseClassPattern(None, cct, ids.map(id => WildcardPattern(Some(id))))
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 36a37059ae1f050fa7b77ecbb500ffe056803f92..2770fd6ff77ff621a24eff8977413ef07e3903e7 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -162,7 +162,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
}
}
- Some(decomp(subProblemsInfo.map(_._1).toList, onSuccess, s"ADT Long Induction on '$origId'"))
+ Some(decomp(subProblemsInfo.map(_._1), onSuccess, s"ADT Long Induction on '$origId'"))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 19e902ad95dde7d343e1731201f5780046709c42..f178f6297d31d34e9cc352222d1b330cf7cd4db1 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -196,12 +196,12 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val lets = (for ((c, alts) <- cTree) yield {
val activeAlts = alts.filter(a => isBActive(a._1))
- val expr = activeAlts.foldLeft(simplestValue(c.getType): Expr){
+ val expr = activeAlts.foldLeft(simplestValue(c.getType): Expr) {
case (e, (b, ex, _)) => IfExpr(b.toVariable, ex, e)
}
(c, expr)
- }).toMap
+ })
// We order the lets base don dependencies
def defFor(c: Identifier): Expr = {
@@ -265,7 +265,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val chFd = hctx.ci.fd
val prog0 = hctx.program
- val affected = prog0.callGraph.transitiveCallers(chFd).toSet ++ Set(chFd, cTreeFd, phiFd) ++ fullSol.defs
+ val affected = prog0.callGraph.transitiveCallers(chFd) ++ Set(chFd, cTreeFd, phiFd) ++ fullSol.defs
cTreeFd.body = None
phiFd.body = Some(
@@ -894,7 +894,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
if (doFilter) {
- if (((nPassing < nInitial*filterThreshold)) && useBssFiltering) {
+ if (nPassing < nInitial * filterThreshold && useBssFiltering) {
// We shrink the program to only use the bs mentionned
val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
ndProgram.shrinkTo(bssToKeep, unfolding == maxUnfoldings)
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 1ba461dc00b5b924b2c345332e716b49c6f208c5..742aca7aa1fa19a9f0d85496b7136f722b1ab901 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -102,7 +102,7 @@ final case class Chain(relations: List[Relation]) {
val (start2, end2) = that.relations.splitAt(i2)
Chain(start1 ++ end2 ++ start2 ++ end1)
}
- }).toSet
+ })
}
lazy val inlined: Seq[Expr] = inlining.map(_._2)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 55a820841f0b62e0b45e6e94b217880120833ce5..063f03e606e1130a55540f700ef5987c88f185ac 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -121,7 +121,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
}
def clear(fd: FunDef) : Boolean = {
- lazy val unsolvedDefs = unsolved.map(_.funDefs).flatten.toSet
+ lazy val unsolvedDefs = unsolved.map(_.funDefs).flatten
lazy val problemDefs = problems.map({ case (problem, _) => problem.funDefs }).flatten.toSet
def issue(defs: Set[FunDef]) : Boolean = defs(fd) || (defs intersect program.callGraph.transitiveCallees(fd)).nonEmpty
! (issue(unsolvedDefs) || issue(problemDefs))
@@ -150,7 +150,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
nextProblems match {
case x :: xs if x == problem =>
assert(xs.isEmpty)
- if (index == processors.size - 1) unsolved += x
+ if (index == processors.length - 1) unsolved += x
else problems.enqueue(x -> (index + 1))
case list @ x :: xs =>
problems.enqueue(list.map(p => p -> 0) : _*)
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 1036a25bf9181112b5d5e30a603907a2222d954e..4d90c9b7ead960d76a1d4fed61e990d5bdd42683 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -67,7 +67,7 @@ class RelationProcessor(
if(na == a && nb == b) (a,b) else fix(f, na, nb)
}
- val ok = decreasing.collect({ case (fd, Success) => fd }).toSet
+ val ok = decreasing.collect({ case (fd, Success) => fd })
val nok = decreasing.collect({ case (fd, Dep(fds)) => fd -> fds }).toList
val (allOk, allNok) = fix(currentReducing, ok, nok)
(allOk, allNok.map(_._1).toSet ++ decreasing.collect({ case (fd, Failure) => fd }))
diff --git a/src/main/scala/leon/utils/Graphs.scala b/src/main/scala/leon/utils/Graphs.scala
index 0f6a75fed63e25617dc40f29c76ea25d75b424d0..a7da8e240f5f3ddcea72a687994660e845541346 100644
--- a/src/main/scala/leon/utils/Graphs.scala
+++ b/src/main/scala/leon/utils/Graphs.scala
@@ -41,7 +41,7 @@ object Graphs {
// Returns the set of edges between two vertices
def edgesBetween(from: Vertex, to: Vertex) = {
- E.filter(e => (e.v1 == from && e.v2 == to))
+ E.filter(e => e.v1 == from && e.v2 == to)
}
/**
@@ -99,8 +99,8 @@ object Graphs {
def this (vertices: Set[Vertex], edges: Set[Edge]) =
this(vertices,
edges,
- edges.groupBy(_.v2 : VertexAbs).toMap.withDefaultValue(Set()),
- edges.groupBy(_.v1 : VertexAbs).toMap.withDefaultValue(Set()))
+ edges.groupBy(_.v2: VertexAbs).withDefaultValue(Set()),
+ edges.groupBy(_.v1: VertexAbs).withDefaultValue(Set()))
def this() = this(Set(), Set())
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 9a27ea1c5927213809c007d278bc91a601f8b939..dd831923c7a79f32ccfcae565c08862f379979b2 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -7,6 +7,7 @@ import purescala.Definitions.Program
import purescala.{MethodLifting, CompleteAbstractDefinitions}
import synthesis.{ConvertWithOracle, ConvertHoles}
+import verification.InjectAsserts
object PreprocessingPhase extends TransformationPhase {
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index 73114c1f2f66f528ef98389264afc4237643939c..07b9bee601fa516592a0306cca5f78ae03daf823 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -9,7 +9,7 @@ object StreamUtils {
ss = ss.tail
}
if(ss.isEmpty) return Stream.empty
- if(ss.size == 1) return ss(0)
+ if(ss.size == 1) return ss.head
// TODO: This circular-shifts the list. I'd be interested in a constant time
// operation. Perhaps simply by choosing the right data-structure?
diff --git a/src/main/scala/leon/utils/Timer.scala b/src/main/scala/leon/utils/Timer.scala
index a0984dc752cee7865d24a50c9e50aea12eefd5ea..c1c7cd84b4f0f93dd574f2974d018ab25210f8a9 100644
--- a/src/main/scala/leon/utils/Timer.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -159,7 +159,7 @@ class TimerStorage extends Dynamic {
}
- ts.keys.reverse.map(n => n -> ts.fields(n)).foreach { case (name, nts) =>
+ ts.keys.reverseMap(n => n -> ts.fields(n)).foreach { case (name, nts) =>
output(nts, (ts -> name) :: path)
}
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index e0d97b931548aea887079489260d529b316db527..ea9cfceb7f920f591fc658e3d51569955886fd53 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -41,7 +41,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
filterInclusive(filterFuns.map(fdMatcher), Some(excludeByDefault _))
}
- val toVerify = program.definedFunctions.toList.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
+ val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
for(funDef <- toVerify) {
if (excludeByDefault(funDef)) {
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 0a67d9cc0d28f7e176dd0307a70016d959ce6245..674ad1507cdf696adbca1b1826738505b50a3fa8 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -1,13 +1,14 @@
/* Copyright 2009-2014 EPFL, Lausanne */
package leon
-package utils
+package verification
-import purescala.Expressions._
+import purescala._
+import Expressions._
+import ExprOps._
+import Definitions._
+import Constructors._
import xlang.Expressions._
-import purescala.ExprOps._
-import purescala.Definitions._
-import purescala.Constructors._
object InjectAsserts extends LeonPhase[Program, Program] {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 1b39389f6ab903b894360e685e03230beec3873f..2683ff2509cd401f3803b12bf628e27f03d3df2e 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -25,7 +25,7 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
var t = Table("Verification Summary")
t ++= conditions.map { vc =>
- val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
+ val timeStr = vc.time.map(t => f"$t%-3.3f").getOrElse("")
Row(Seq(
Cell(vc.funDef.id.toString),
Cell(vc.kind.name),
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 6891bdd4b21c025fbdfb3ac712bafad21f2437de..3333ab2553b53b225e755f1d6a0d3f858531a53c 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -18,7 +18,10 @@ object EpsilonElimination extends TransformationPhase {
def apply(ctx: LeonContext, pgm: Program): Program = {
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => fd.body.map(body => {
+ for {
+ fd <- allFuns
+ body <- fd.body
+ } {
val newBody = postMap{
case eps@Epsilon(pred, tpe) =>
val freshName = FreshIdentifier("epsilon")
@@ -33,7 +36,7 @@ object EpsilonElimination extends TransformationPhase {
None
}(body)
fd.body = Some(newBody)
- }))
+ }
pgm
}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index e3fc725b61021895fc7b3e9605d41a3a55e33e03..3f9c2b3e5f9634358c4df5d888d7195c7e8e4df9 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -27,11 +27,14 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
parent = null
val allFuns = pgm.definedFunctions
- allFuns.foreach(fd => fd.body.map(body => {
+ for {
+ fd <- allFuns
+ body <- fd.body
+ } {
parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
- }))
+ }
(pgm, wasLoop)
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 60d251dd641586617cee48c02053a1c2b51af17e..635e0c0428e49d76a2b1a934f43f2402f60761ec 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -88,7 +88,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
case _ => None
}
if(ois.forall(_.isDefined))
- Some(ois.map(_.get).toSet)
+ Some(ois.map(_.get))
else
None
case _ => None
diff --git a/src/test/scala/leon/test/purescala/WithLikelyEq.scala b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
index 68da72895183567bd583e5b9f5ec749dad04d3a0..fc9466a59cc12e5763f9ef977ea5af58b8c97264 100644
--- a/src/test/scala/leon/test/purescala/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
@@ -47,7 +47,7 @@ trait WithLikelyEq {
val counters: Array[Int] = vsOrder.map(_ => min)
var i = 0
- while(i < counters.size && isEq) {
+ while(i < counters.length && isEq) {
val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), InfiniteIntegerLiteral(c))}.toMap
val ne1 = replace(m, e1)
val ne2 = replace(m, e2)
@@ -68,11 +68,11 @@ trait WithLikelyEq {
if(counters(i) < max)
counters(i) += 1
else {
- while(i < counters.size && counters(i) >= max) {
+ while(i < counters.length && counters(i) >= max) {
counters(i) = min
i += 1
}
- if(i < counters.size) {
+ if(i < counters.length) {
counters(i) += 1
i = 0
}
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index cdf4d38d1ee7a0d496e3e461e6a99af861d60a56..7bfe129d603adb6d5138165c5586d4c818a2b272 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -43,8 +43,8 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
def checkVectorSpace(basis: Array[Array[Int]], equation: Array[Int]): Unit =
checkVectorSpace(basis.map(_.map(i => BigInt(i))), equation.map(i => BigInt(i)))
def checkVectorSpace(basis: Array[Array[BigInt]], equation: Array[BigInt]): Unit = {
- require(basis.size == basis(0).size + 1 && basis.size == equation.size)
- val n = basis(0).size
+ require(basis.length == basis(0).length + 1 && basis.length == equation.length)
+ val n = basis(0).length
val min: BigInt = -5
val max: BigInt = 5
val components = Array.fill(n)(min)
@@ -72,18 +72,18 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
//val that the sol vector with the term in the equation
def eval(sol: Array[BigInt], equation: Array[BigInt]): BigInt = {
- require(sol.size == equation.size)
+ require(sol.length == equation.length)
sol.zip(equation).foldLeft(BigInt(0))((acc, p) => acc + p._1 * p._2)
}
//multiply the matrix by the vector: [M1 M2 .. Mn] * [v1 .. vn] = v1*M1 + ... + vn*Mn]
def mult(matrix: Array[Array[BigInt]], vector: Array[BigInt]): Array[BigInt] = {
- require(vector.size == matrix(0).size && vector.size > 0)
+ require(vector.length == matrix(0).length && vector.length > 0)
val tmat = matrix.transpose
var tmp: Array[BigInt] = null
tmp = mult(vector(0), tmat(0))
var i = 1
- while(i < vector.size) {
+ while(i < vector.length) {
tmp = add(tmp, mult(vector(i), tmat(i)))
i += 1
}
@@ -92,7 +92,7 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
def mult(c: BigInt, v: Array[BigInt]): Array[BigInt] = v.map(_ * c)
def add(v1: Array[BigInt], v2: Array[BigInt]): Array[BigInt] = {
- require(v1.size == v2.size)
+ require(v1.length == v2.length)
v1.zip(v2).map(p => p._1 + p._2)
}
@@ -197,16 +197,16 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
val counters: Array[Int] = (1 to nbValues).map(_ => min).toArray
var i = 0
- while(i < counters.size) {
+ while(i < counters.length) {
app(counters)
if(counters(i) < max)
counters(i) += 1
else {
- while(i < counters.size && counters(i) >= max) {
+ while(i < counters.length && counters(i) >= max) {
counters(i) = min
i += 1
}
- if(i < counters.size) {
+ if(i < counters.length) {
counters(i) += 1
i = 0
}
diff --git a/src/test/scala/leon/test/utils/Streams.scala b/src/test/scala/leon/test/utils/Streams.scala
index 44849cad633241ad077a6c189f164a71c441b9c0..c2a18500a4d922a3a4a329da409fd86f13687515 100644
--- a/src/test/scala/leon/test/utils/Streams.scala
+++ b/src/test/scala/leon/test/utils/Streams.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-package leon.test.purescala
+package leon.test.utils
import leon.test._
import leon.purescala.Common._
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index c315794aa9a9239d131562e9710a983512eae078..425ee3c2cc064b08f4594d5124440bf936d4a65a 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -37,9 +37,9 @@ class XLangVerificationRegression extends LeonTestSuite {
fullName
}
- test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
+ test(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}") {
assert(file.exists && file.isFile && file.canRead,
- "Benchmark %s is not a readable file".format(displayName))
+ s"Benchmark $displayName is not a readable file")
val ctx = createLeonContext((file.getPath +: leonOptions) :_*)