From 659ebb031839d120d5f7d9e324afb6fb484ff72f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 17 Mar 2015 12:09:11 +0100
Subject: [PATCH] More fixes
Notice the removal of type parameter in TemplateGenerator.groupWhile.
I am not sure what was intended (this method is currently unused).
---
.../leon/frontends/scalac/CodeExtraction.scala | 10 +++++-----
.../scala/leon/purescala/Definitions.scala | 16 ++++++++--------
src/main/scala/leon/purescala/TreeOps.scala | 18 +++++++++---------
.../leon/solvers/smtlib/SMTLIBTarget.scala | 2 +-
.../solvers/templates/TemplateGenerator.scala | 2 +-
.../leon/synthesis/rules/ADTInduction.scala | 10 +++++-----
.../termination/TerminationRegression.scala | 2 +-
7 files changed, 30 insertions(+), 30 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index bfbcd41af..cfcf667c5 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -831,7 +831,7 @@ trait CodeExtraction extends ASTExtractors {
private def extractObjectDef(id : Identifier, defs: List[Tree], isStandalone : Boolean) {
- val newDefs = defs.flatMap{ t => t match {
+ val newDefs = defs.flatMap {
case t if isIgnored(t.symbol) =>
None
@@ -850,10 +850,10 @@ trait CodeExtraction extends ASTExtractors {
Some(defsToDefs(sym))
case ExFieldDef(sym, _, _) =>
Some(defsToDefs(sym))
-
+
case _ =>
None
- }}
+ }
// We check nothing else is polluting the object
for (t <- defs) t match {
@@ -1919,9 +1919,9 @@ trait CodeExtraction extends ASTExtractors {
None
}
- if(exprOwners.exists(_ == None))
+ if(exprOwners.contains(None))
None
- else if(exprOwners.exists(_ == Some(None)))
+ else if(exprOwners.contains(Some(None)))
Some(None)
else if(exprOwners.exists(o1 => exprOwners.exists(o2 => o1 != o2)))
Some(None)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 2dbeb4f43..201835745 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -95,7 +95,7 @@ object Definitions {
val fstream = new FileWriter(filename)
val out = new BufferedWriter(fstream)
out.write(ScalaPrinter(this))
- out.close
+ out.close()
}
setSubDefOwners()
}
@@ -171,7 +171,7 @@ object Definitions {
val fstream = new FileWriter(filename)
val out = new BufferedWriter(fstream)
out.write(ScalaPrinter(this))
- out.close
+ out.close()
}
setSubDefOwners()
@@ -204,11 +204,11 @@ object Definitions {
case c @ CaseClassDef(_, _, None, _) => c
}
- def duplicate = copy(defs = defs map { _ match {
- case f : FunDef => f.duplicate
- case cd : ClassDef => cd.duplicate
+ def duplicate = copy(defs = defs map {
+ case f: FunDef => f.duplicate
+ case cd: ClassDef => cd.duplicate
case other => other // FIXME: huh?
- }})
+ })
setSubDefOwners()
@@ -252,10 +252,10 @@ object Definitions {
def knownChildren: Seq[ClassDef] = _children
def knownDescendents: Seq[ClassDef] = {
- knownChildren ++ (knownChildren.map(c => c match {
+ knownChildren ++ (knownChildren.map {
case acd: AbstractClassDef => acd.knownDescendents
case _ => Nil
- }).foldLeft(List[ClassDef]())(_ ++ _))
+ }.foldLeft(List[ClassDef]())(_ ++ _))
}
def knownCCDescendents: Seq[CaseClassDef] = knownDescendents.collect {
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 0003474db..fe0a0c6ce 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -537,10 +537,10 @@ object TreeOps {
Some(replace(Map((Variable(i) -> t)), b))
case letExpr @ Let(i,e,b) if isDeterministic(b) => {
- val occurences = count{ (e: Expr) => e match {
+ val occurences = count {
case Variable(x) if x == i => 1
case _ => 0
- }}(b)
+ }(b)
if(occurences == 0) {
Some(b)
@@ -1443,7 +1443,7 @@ object TreeOps {
}
def idHomo(i1: Identifier, i2: Identifier)(implicit map: Map[Identifier, Identifier]) = {
- i1 == i2 || map.get(i1).exists(_ == i2)
+ i1 == i2 || map.get(i1).contains(i2)
}
def fdHomo(fd1: FunDef, fd2: FunDef)(implicit map: Map[Identifier, Identifier]) = {
@@ -2202,21 +2202,21 @@ object TreeOps {
}
- val newCases = resCases.flatMap { c => c match {
- case SimpleCase(wp: WildcardPattern, m @ MatchExpr(ex, cases)) if ex == scrutinee =>
+ val newCases = resCases.flatMap {
+ case SimpleCase(wp: WildcardPattern, m@MatchExpr(ex, cases)) if ex == scrutinee =>
cases
- case SimpleCase(pattern, m @ MatchExpr(v @ Variable(id), cases)) =>
+ case c@SimpleCase(pattern, m@MatchExpr(v@Variable(id), cases)) =>
if (pattern.binders(id)) {
- cases.map{ nc =>
+ cases.map { nc =>
SimpleCase(mergePattern(pattern, id, nc.pattern), nc.rhs)
}
} else {
Seq(c)
}
- case _ =>
+ case c =>
Seq(c)
- }}
+ }
var finalMatch = matchExpr(scrutinee, List(newCases.head)).asInstanceOf[MatchExpr]
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 938dd2667..fca07352c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -601,7 +601,7 @@ trait SMTLIBTarget {
reporter.ifDebug { debug =>
SMTPrinter.printCommand(cmd, out)
out.write("\n")
- out.flush
+ out.flush()
}
interpreter.eval(cmd) match {
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index ef7a58f1c..8a35871f4 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -157,7 +157,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
// Group elements that satisfy p toghether
// List(a, a, a, b, c, a, a), with p = _ == a will produce:
// List(List(a,a,a), List(b), List(c), List(a, a))
- def groupWhile[T](p: T => Boolean, l: Seq[T]): Seq[Seq[T]] = {
+ def groupWhile(p: T => Boolean, l: Seq[T]): Seq[Seq[T]] = {
var res: Seq[Seq[T]] = Nil
var c = l
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 5dd0afe26..73aa69f7a 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -54,7 +54,7 @@ case object ADTInduction extends Rule("ADT Induction") {
val inputs = (for (id <- newIds) yield {
if (id.getType == origId.getType) {
val postXs = p.xs map (id => FreshIdentifier("r", id.getType, true))
- val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
+ val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable)
recCalls += postXs -> (Variable(id) +: residualArgs.map(id => Variable(id)))
@@ -65,9 +65,9 @@ case object ADTInduction extends Rule("ADT Induction") {
}
}).flatten
- val subPhi = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable(_)))), innerPhi)
- val subPC = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable(_)))), innerPC)
- val subWS = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable(_)))), innerWS)
+ val subPhi = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable))), innerPhi)
+ val subPC = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable))), innerPC)
+ val subWS = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable))), innerWS)
val subPre = CaseClassInstanceOf(cct, Variable(origId))
@@ -108,7 +108,7 @@ case object ADTInduction extends Rule("ADT Induction") {
Some(Solution(orJoin(globalPre),
sols.flatMap(_.defs).toSet+newFun,
- FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable(_))),
+ FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable)),
sols.forall(_.isTrusted)
))
}
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index da5436d03..c3b53c9f3 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -21,7 +21,7 @@ class TerminationRegression extends LeonTestSuite {
leon.frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase andThen leon.termination.TerminationPhase
private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
- val fullName = file.getPath()
+ val fullName = file.getPath
val start = fullName.indexOf("regression")
val displayName = if(start != -1) {
--
GitLab