From 1f1b44602c6d57c3256b1180c759e7760f1ce2c6 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 4 May 2015 12:38:47 +0200
Subject: [PATCH] Style fixes
---
src/main/scala/leon/LeonOption.scala | 5 ++--
src/main/scala/leon/purescala/ExprOps.scala | 10 ++++----
.../scala/leon/purescala/Expressions.scala | 2 +-
.../leon/synthesis/SynthesisContext.scala | 23 ++++++++++---------
.../leon/synthesis/rules/CEGISLike.scala | 7 ++----
.../leon/test/synthesis/SynthesisSuite.scala | 9 ++------
6 files changed, 24 insertions(+), 32 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 06269e696..0e87e34fa 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -42,11 +42,10 @@ abstract class LeonOptionDef[+A] {
}
case class LeonFlagOptionDef(name: String, description: String, default: Boolean) extends LeonOptionDef[Boolean] {
- val parser = booleanParser(default)
+ val parser = booleanParser
val usageRhs = ""
}
-
case class LeonStringOptionDef(name: String, description: String, default: String, usageRhs: String) extends LeonOptionDef[String] {
val parser = stringParser
}
@@ -78,7 +77,7 @@ object OptionParsers {
val longParser: OptionParser[Long] = _.toLong
val stringParser: OptionParser[String] = x => x
- def booleanParser(default: Boolean): OptionParser[Boolean] = {
+ def booleanParser: OptionParser[Boolean] = {
case "on" | "true" | "yes" | "" => true
case "off" | "false" | "no" => false
case _ => throw new IllegalArgumentException
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b945d3eb2..b4866c399 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -347,7 +347,7 @@ object ExprOps {
}
def variablesOf(expr: Expr): Set[Identifier] = {
- foldRight[Set[Identifier]]({
+ foldRight[Set[Identifier]]{
case (e, subs) =>
val subvs = subs.foldLeft(Set[Identifier]())(_ ++ _)
@@ -361,7 +361,7 @@ object ExprOps {
case Forall(args, body) => subvs -- args.map(_.id)
case _ => subvs
}
- })(expr)
+ }(expr)
}
def containsFunctionCalls(expr: Expr): Boolean = {
@@ -431,7 +431,7 @@ object ExprOps {
}
- postMap({
+ postMap{
case m @ MatchExpr(s, cses) =>
Some(matchExpr(s, cses.map(freshenCase)).copiedFrom(m))
@@ -443,11 +443,11 @@ object ExprOps {
Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
case _ => None
- })(expr)
+ }(expr)
}
def depth(e: Expr): Int = {
- foldRight[Int]({ (e, sub) => 1 + (0 +: sub).max })(e)
+ foldRight[Int]{ (e, sub) => 1 + (0 +: sub).max }(e)
}
def applyAsMatches(p : Passes, f : Expr => Expr) = {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 596ddc2df..fc94305e6 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -442,7 +442,7 @@ object Expressions {
case class MapGet(map: Expr, key: Expr) extends Expr {
val getType = map.getType match {
- case MapType(from, to) => to
+ case MapType(_, to) => to
case _ => Untyped
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index d0419f81a..d9b9a6039 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -15,10 +15,11 @@ case class SynthesisContext(
context: LeonContext,
settings: SynthesisSettings,
functionContext: FunDef,
- program: Program,
- reporter: Reporter
+ program: Program
) {
+ val reporter = context.reporter
+
val rules = settings.rules
val allSolvers: Map[String, SolverFactory[SynthesisContext.SynthesisSolver]] = Map(
@@ -28,12 +29,13 @@ case class SynthesisContext(
val solversToUse = allSolvers.filterKeys(settings.selectedSolvers)
- val solverFactory: SolverFactory[SynthesisContext.SynthesisSolver] = if (solversToUse.isEmpty) {
- reporter.fatalError("No solver selected. Aborting")
- } else if (solversToUse.size == 1) {
- solversToUse.values.head
- } else {
- SolverFactory( () => new PortfolioSolverSynth(context, solversToUse.values.toSeq) with TimeoutAssumptionSolver)
+ val solverFactory: SolverFactory[SynthesisContext.SynthesisSolver] = solversToUse.values.toSeq match {
+ case Seq() =>
+ reporter.fatalError("No solver selected. Aborting")
+ case Seq(value) =>
+ value
+ case more =>
+ SolverFactory( () => new PortfolioSolverSynth(context, more) with TimeoutAssumptionSolver )
}
def newSolver: SynthesisContext.SynthesisSolver = {
@@ -56,8 +58,7 @@ object SynthesisContext {
synth.context,
synth.settings,
synth.ci.fd,
- synth.program,
- synth.reporter)
+ synth.program
+ )
}
}
-
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 908ff0e10..fce0363fb 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -194,7 +194,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private def computeCExpr(): Expr = {
- val lets = (for ((c, alts) <- cTree) yield {
+ val lets = for ((c, alts) <- cTree) yield {
val activeAlts = alts.filter(a => isBActive(a._1))
val expr = activeAlts.foldLeft(simplestValue(c.getType): Expr) {
@@ -202,7 +202,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
(c, expr)
- })
+ }
// We order the lets base don dependencies
def defFor(c: Identifier): Expr = {
@@ -575,9 +575,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
closedBs = Map[Identifier, Set[Identifier]]()
- // Set of Cs that still have no active alternatives after unfolding
- var postClosedCs = Set[Identifier]()
-
for (c <- unfoldBehind) {
var alts = grammar.getProductions(labels(c))
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index d2aa2d412..c043ac0fa 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -92,14 +92,9 @@ class SynthesisSuite extends LeonTestSuite {
for ((f,cis) <- results; ci <- cis) {
info(f"${ci.fd.id.toString}%-20s")
+ val sctx = SynthesisContext(ctx, opts, ci.fd, program)
- val sctx = SynthesisContext(ctx,
- opts,
- ci.fd,
- program,
- ctx.reporter)
-
- val p = ci.problem
+ val p = ci.problem
if (strats.isDefinedAt(f.id.name)) {
val search = new TestSearch(ctx, ci, p, strats(f.id.name))
--
GitLab