diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 28cbe5f3ef3ca6e2a13eacf4356c17db360f0e2b..03b168fd2071d84e85d162365eae2e73b22431ac 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1316,8 +1316,8 @@ trait CodeGeneration {
val cch = cf.addConstructor(constrParams : _*).codeHandler
- for (lzy <- lazyFields) { initLazyField(cch, cName, lzy, false) }
- for (field <- strictFields) { initStrictField(cch, cName, field, false)}
+ for (lzy <- lazyFields) { initLazyField(cch, cName, lzy, isStatic = false) }
+ for (field <- strictFields) { initStrictField(cch, cName, field, isStatic = false)}
// Call parent constructor
cch << ALoad(0)
@@ -1425,7 +1425,7 @@ trait CodeGeneration {
val namesTypes = ccd.fields.map { vd => (vd.id.name, typeToJVM(vd.getType)) }
// definition of the constructor
- if(!params.doInstrument && !params.requireMonitor && ccd.fields.isEmpty && ccd.methods.filter{ _.canBeField }.isEmpty) {
+ if(!params.doInstrument && !params.requireMonitor && ccd.fields.isEmpty && !ccd.methods.exists(_.canBeField)) {
cf.addDefaultConstructor
} else {
for((nme, jvmt) <- namesTypes) {
@@ -1484,8 +1484,8 @@ trait CodeGeneration {
// Now initialize fields
- for (lzy <- lazyFields) { initLazyField(cch, cName, lzy, false)}
- for (field <- strictFields) { initStrictField(cch, cName , field, false)}
+ for (lzy <- lazyFields) { initLazyField(cch, cName, lzy, isStatic = false)}
+ for (field <- strictFields) { initStrictField(cch, cName , field, isStatic = false)}
cch << RETURN
cch.freeze
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index ce8dce09ab23a27e47976780a7d395375f42c1f6..b7097ee5f7400a03bc8ac47fc67268ab1560b3fe 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -321,7 +321,7 @@ class CompilationUnit(val ctx: LeonContext,
args.zipWithIndex.toMap
}
- mkExpr(e, ch)(Locals(newMapping, Map.empty, Map.empty, true))
+ mkExpr(e, ch)(Locals(newMapping, Map.empty, Map.empty, isStatic = true))
e.getType match {
case Int32Type | BooleanType | UnitType =>
@@ -400,8 +400,8 @@ class CompilationUnit(val ctx: LeonContext,
ch << Ldc(Int.MaxValue) // Allow "infinite" method calls
ch << InvokeSpecial(MonitorClass, cafebabe.Defaults.constructorName, "(I)V")
ch << AStore(ch.getFreshVar) // position 0
- for (lzy <- lazyFields) { initLazyField(ch, cName, lzy, true)}
- for (field <- strictFields) { initStrictField(ch, cName , field, true)}
+ for (lzy <- lazyFields) { initLazyField(ch, cName, lzy, isStatic = true)}
+ for (field <- strictFields) { initStrictField(ch, cName , field, isStatic = true)}
ch << RETURN
ch.freeze
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 679da530c486e308c22c77b97efc19ee2d4d6229..c05355bdc4c2c2bbbc8b1d1f107c01f687d7dd8e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -363,7 +363,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case RealDivision(l,r) =>
(e(l), e(r)) match {
case (RealLiteral(i1), RealLiteral(i2)) =>
- if(i2 != 0) RealLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
+ if (i2 != 0) RealLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index d3dc099a44b98e337750e68c8a538cb24691b05a..5f217f2295262e81591039ca95c0fdcda2e495a9 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -40,7 +40,7 @@ object Constructors {
*/
def tupleSelect(t: Expr, index: Int, originalSize: Int): Expr = tupleSelect(t, index, originalSize > 1)
- /** $encodingof ``val id = e; bd`, and returns `bd` if the identifier is not bound in `bd`.
+ /** $encodingof ``val id = e; bd``, and returns `bd` if the identifier is not bound in `bd`.
* @see [[purescala.Expressions.Let]]
*/
def let(id: Identifier, e: Expr, bd: Expr) = {
@@ -49,7 +49,7 @@ object Constructors {
else bd
}
- /** $encodingof ``val (id1, id2, ...) = e; bd`, and returns `bd` if the identifiers are not bound in `bd`.
+ /** $encodingof ``val (id1, id2, ...) = e; bd``, and returns `bd` if the identifiers are not bound in `bd`.
* @see [[purescala.Expressions.Let]]
*/
def letTuple(binders: Seq[Identifier], value: Expr, body: Expr) = binders match {
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index b8afe63777c0f8fcc009e8993f779b933259ea50..2ba4f9221e735b758f15270fe0761ddaacf8b23c 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -4,7 +4,7 @@ package leon.purescala
import Definitions._
import Expressions._
-import ExprOps.{preMap, postMap, functionCallsOf}
+import ExprOps.{preMap, functionCallsOf}
object DefOps {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 428bf107fa0f9fda713baa05c4381c5afb292653..25a2d0e93cf46d36c78fed5796846a1e47d89674 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -825,9 +825,9 @@ object ExprOps {
bindIn(b) ++ map
case up@UnapplyPattern(b, _, subps) =>
- bindIn(b) ++ unwrapTuple(up.getUnsafe(in), subps.size).zip(subps).map{
+ bindIn(b) ++ unwrapTuple(up.getUnsafe(in), subps.size).zip(subps).flatMap {
case (e, p) => mapForPattern(e, p)
- }.flatten.toMap
+ }.toMap
case other =>
bindIn(other.binder)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 7722c4e2aaf0f2228c128b83b7640290082eeea5..bace7746c6c7d0eb86320ac36daae771ba34d58c 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -160,13 +160,13 @@ object Extractors {
(as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))
))
case NonemptyArray(elems, Some((default, length))) =>
- val all = elems.map(_._2).toSeq :+ default :+ length
+ val all = elems.values.toSeq :+ default :+ length
Some((all, as => {
val l = as.length
nonemptyArray(as.take(l - 2), Some((as(l - 2), as(l - 1))))
}))
case NonemptyArray(elems, None) =>
- val all = elems.map(_._2).toSeq
+ val all = elems.values.toSeq
Some((all, finiteArray))
case Tuple(args) => Some((args, tupleWrap))
case IfExpr(cond, thenn, elze) => Some((
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 52ac89493691c893d99e1964b5e269ab183b4e4a..87905111f0ee42180a3ef2ab50f7975bcac2e5d3 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -21,7 +21,7 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
type GC = GlobalContext
def initRC(mappings: Map[Identifier, Expr]) = CollectingRecContext(mappings, None)
- def initGC = new GlobalContext()
+ def initGC() = new GlobalContext()
type FI = (FunDef, Seq[Expr])
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index c41ae4a01efe2b3d491c556b7e4838bada6cc141..a8a043047c616311bc134c95d9cf231b5448aa7c 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -11,7 +11,6 @@ import purescala.Types._
import purescala.DefOps._
import purescala.Constructors._
import purescala.Extractors.unwrapTuple
-import purescala.ScalaPrinter
import evaluators._
import solvers._
import utils._
@@ -22,11 +21,8 @@ import synthesis.rules._
import synthesis.Witnesses._
import rules._
import graph.DotGenerator
-import leon.utils.ASCIIHelpers.title
import grammars._
-import scala.concurrent.duration._
-
class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeoutMs: Option[Long], repairTimeoutMs: Option[Long]) {
implicit val ctx = ctx0
@@ -84,14 +80,14 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val timeVerify = timer.stop
if (doBenchmark) {
- val be = (BenchmarkEntry.fromContext(ctx) ++ Map(
+ val be = BenchmarkEntry.fromContext(ctx) ++ Map(
"function" -> fd.id.name,
"time_tests" -> timeTests,
"time_synthesis" -> timeSynth,
"time_verification" -> timeVerify,
"success" -> solutions.nonEmpty,
"verified" -> solutions.forall(_._2)
- ))
+ )
val bh = new BenchmarksHistory("repairs.dat")
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 19bf277410fff3e9bf76e23afd9e9c8a9c8df4cb..135d47ebcb1bb0a492d46258b81e840d0916c75f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -20,5 +20,5 @@ class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) ext
) ++ userDefinedOps(ctx)
}
- val allowQuantifiedAssersions: Boolean = false
+ protected val allowQuantifiedAssertions: Boolean = false
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 3684d61bf14cefe200d07e729e9ea5ba96cf0ee3..83076f8dc6c0bf3588697370e52d0f2d49bc4df4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -41,5 +41,5 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
throw LeonFatalError(Some(s"Solver $name does not support model extraction."))
}
- protected val allowQuantifiedAssersions: Boolean = true
+ protected val allowQuantifiedAssertions: Boolean = true
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 6f849908ec27d5c3c36e029296ab968a2ade0e3a..6bc216b535c746664ae2cb4ace9fe591af206134 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -88,7 +88,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
if (smtFunDecls.nonEmpty) {
sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
// Assert contracts for defined functions
- if (allowQuantifiedAssersions) for {
+ if (allowQuantifiedAssertions) for {
// If we encounter a function that does not refer to the current function,
// it is sound to assume its contracts for all inputs
tfd <- withParams if !refersToCurrent(tfd.fd)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index 95b3310d42b8b4cbe5983104f286d409a06d2eb8..0d761fe214656eb145047769a2adc8aef8e5232a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -18,7 +18,7 @@ trait SMTLIBQuantifiedSolver extends SMTLIBSolver {
})
}
- protected val allowQuantifiedAssersions: Boolean
+ protected val allowQuantifiedAssertions: Boolean
protected val typedFunDefExplorationLimit = 10000
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 3fcaacd4426c8e27f7bc4bdb9955aca53087429b..cd49ece38c08e681dc5a6abe696112533339f4af 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -40,9 +40,10 @@ abstract class SMTLIBSolver(val context: LeonContext,
protected val reporter = context.reporter
/* Interface with Interpreter */
- def interpreterOps(ctx: LeonContext): Seq[String]
- def getNewInterpreter(ctx: LeonContext): SMTInterpreter
+ protected def interpreterOps(ctx: LeonContext): Seq[String]
+
+ protected def getNewInterpreter(ctx: LeonContext): SMTInterpreter
protected val interpreter = getNewInterpreter(context)
@@ -73,7 +74,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
/* Interruptible interface */
- protected var interrupted = false
+ private var interrupted = false
context.interruptManager.registerForInterrupts(this)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index dc91864b686ab05594051ea031b196122fe83f5a..b520dfe5be60f586ae05bda1e48f8bf82c0e70fc 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -20,7 +20,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
with SMTLIBQuantifiedSolver
{
- protected val allowQuantifiedAssersions: Boolean = true
+ protected val allowQuantifiedAssertions: Boolean = true
override def targetName = "z3-q"
@@ -52,7 +52,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
// If we encounter a function that does not refer to the current function,
// it is sound to assume its contracts for all inputs
- if (allowQuantifiedAssersions) for {
+ if (allowQuantifiedAssertions) for {
tfd <- notSeen if !refersToCurrent(tfd.fd)
post <- tfd.postcondition
} {
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index b2683eb588cdabcd5baaedd20e0c4e8300e0bd50..94bc6afb2f2aa1de6e28fdf0fb793460b7a37054 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -81,52 +81,7 @@ trait AbstractZ3Solver extends Solver {
z3.mkFreshFuncDecl(gv.tp.id.uniqueName+"#"+gv.id+"!val", Seq(), typeToSort(gv.tp))
}
}
-
- class Bijection[A, B] {
- var leonToZ3 = Map[A, B]()
- var z3ToLeon = Map[B, A]()
-
- def +=(a: A, b: B): Unit = {
- leonToZ3 += a -> b
- z3ToLeon += b -> a
- }
-
- def +=(t: (A,B)): Unit = {
- this += (t._1, t._2)
- }
-
-
- def clear(): Unit = {
- z3ToLeon = Map()
- leonToZ3 = Map()
- }
-
- def getZ3(a: A): Option[B] = leonToZ3.get(a)
- def getLeon(b: B): Option[A] = z3ToLeon.get(b)
-
- def toZ3(a: A): B = getZ3(a).get
- def toLeon(b: B): A = getLeon(b).get
-
- def toZ3OrCompute(a: A)(c: => B) = {
- getZ3(a).getOrElse {
- val res = c
- this += a -> res
- res
- }
- }
-
- def toLeonOrCompute(b: B)(c: => A) = {
- getLeon(b).getOrElse {
- val res = c
- this += res -> b
- res
- }
- }
-
- def containsLeon(a: A): Boolean = leonToZ3 contains a
- def containsZ3(b: B): Boolean = z3ToLeon contains b
- }
-
+
// ADT Manager
protected val adtManager = new ADTManager(context)
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index d63bca0b55f898b5e1ccebd235b841f029a62f7c..c33a31cebe0c430a7c2b21c932529ca5b72ed053 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -107,7 +107,7 @@ class SimpleSearch(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: Cost
def findNodeToExpandFrom(from: Node): Option[Node] = {
counter += 1
ctx.timers.synthesis.search.find.timed {
- if (!bound.isDefined || counter <= bound.get) {
+ if (bound.isEmpty || counter <= bound.get) {
if (expansionBuffer.isEmpty) {
findIn(from)
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4a377acd239ace5c6180625a36563584ec88a584..c76a59bbb006cd3b72774063289d2939ce52059b 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -22,8 +22,6 @@ import evaluators._
import datagen._
import codegen.CodeGenParams
-import utils._
-
abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
case class CegisParams(
@@ -721,7 +719,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val failedTestsStats = new MutableMap[Example, Int]().withDefaultValue(0)
- def hasInputExamples = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
+ def hasInputExamples = baseExampleInputs.nonEmpty || cachedInputIterator.hasNext
var n = 1
def allInputExamples() = {
@@ -819,7 +817,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
doFilter = false
result = Some(RuleClosed(sols))
case Right(cexs) =>
- baseExampleInputs ++= cexs.map(InExample(_))
+ baseExampleInputs ++= cexs.map(InExample)
if (nPassing <= validateUpTo) {
// All programs failed verification, we filter everything out and unfold
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 1ff65119585e1fd2c6b5481d0e4040f4e2453dcc..0336a8aaea93f6a3b919cd5f69b62f77d46ca584 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -26,7 +26,12 @@ object UnitElimination extends TransformationPhase {
//first introduce new signatures without Unit parameters
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.params.exists(vd => vd.getType == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType)).setPos(fd)
+ val freshFunDef = new FunDef(
+ FreshIdentifier(fd.id.name),
+ fd.tparams,
+ fd.returnType,
+ fd.params.filterNot(vd => vd.getType == UnitType)
+ ).setPos(fd)
freshFunDef.copyContentFrom(fd)
fun2FreshFun += (fd -> freshFunDef)
} else {
@@ -59,23 +64,24 @@ object UnitElimination extends TransformationPhase {
private def removeUnit(expr: Expr): Expr = {
assert(expr.getType != UnitType)
expr match {
- case fi@FunctionInvocation(tfd, args) => {
+ case fi@FunctionInvocation(tfd, args) =>
val newArgs = args.filterNot(arg => arg.getType == UnitType)
FunctionInvocation(fun2FreshFun(tfd.fd).typed(tfd.tps), newArgs).setPos(fi)
- }
- case t@Tuple(args) => {
- val TupleType(tpes) = t.getType
- val (newTpes, newArgs) = tpes.zip(args).filterNot{ case (UnitType, _) => true case _ => false }.unzip
+
+ case IsTyped(Tuple(args), TupleType(tpes)) =>
+ val newArgs = tpes.zip(args).collect {
+ case (tp, arg) if tp != UnitType => arg
+ }
tupleWrap(newArgs.map(removeUnit)) // @mk: FIXME this may actually return a Unit, is that cool?
- }
- case ts@TupleSelect(t, index) => {
+
+ case ts@TupleSelect(t, index) =>
val TupleType(tpes) = t.getType
val simpleTypes = tpes map simplifyType
val newArity = tpes.count(_ != UnitType)
val newIndex = simpleTypes.take(index).count(_ != UnitType)
tupleSelect(removeUnit(t), newIndex, newArity)
- }
- case Let(id, e, b) => {
+
+ case Let(id, e, b) =>
if(id.getType == UnitType)
removeUnit(b)
else {
@@ -91,13 +97,18 @@ object UnitElimination extends TransformationPhase {
case _ => Let(id, removeUnit(e), removeUnit(b))
}
}
- }
- case LetDef(fd, b) => {
+
+ case LetDef(fd, b) =>
if(fd.returnType == UnitType)
removeUnit(b)
else {
val (newFd, rest) = if(fd.params.exists(vd => vd.getType == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType)).setPos(fd)
+ val freshFunDef = new FunDef(
+ FreshIdentifier(fd.id.name),
+ fd.tparams,
+ fd.returnType,
+ fd.params.filterNot(vd => vd.getType == UnitType)
+ ).setPos(fd)
freshFunDef.copyContentFrom(fd)
fun2FreshFun += (fd -> freshFunDef)
freshFunDef.fullBody = removeUnit(fd.fullBody)
@@ -113,24 +124,26 @@ object UnitElimination extends TransformationPhase {
}
LetDef(newFd, rest)
}
- }
- case ite@IfExpr(cond, tExpr, eExpr) => {
+
+ case ite@IfExpr(cond, tExpr, eExpr) =>
val thenRec = removeUnit(tExpr)
val elseRec = removeUnit(eExpr)
IfExpr(removeUnit(cond), thenRec, elseRec)
- }
- case v @ Variable(id) => if(id2FreshId.isDefinedAt(id)) Variable(id2FreshId(id)) else v
- case m @ MatchExpr(scrut, cses) => {
+
+ case v @ Variable(id) =>
+ if(id2FreshId.isDefinedAt(id))
+ Variable(id2FreshId(id))
+ else v
+
+ case m @ MatchExpr(scrut, cses) =>
val scrutRec = removeUnit(scrut)
val csesRec = cses.map{ cse =>
MatchCase(cse.pattern, cse.optGuard map removeUnit, removeUnit(cse.rhs))
}
matchExpr(scrutRec, csesRec).setPos(m)
- }
- case Operator(args, recons) => {
+
+ case Operator(args, recons) =>
recons(args.map(removeUnit))
- }
- // FIXME: It's dead (code) Jim!
case _ => sys.error("not supported: " + expr)
}