From aa85fc4abba457b763609b171b6d24518ae86a4a Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Mon, 27 Apr 2015 16:00:05 +0200 Subject: [PATCH] Simplifications --- .../scala/leon/evaluators/RecursiveEvaluator.scala | 12 ++++-------- .../scala/leon/evaluators/TracingEvaluator.scala | 2 -- .../scala/leon/frontends/scalac/CodeExtraction.scala | 6 ------ 3 files changed, 4 insertions(+), 16 deletions(-) diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala index 925ad6313..e1de9e64c 100644 --- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala +++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala @@ -11,7 +11,6 @@ import purescala.Types._ import purescala.Constructors._ import purescala.Extractors._ -import xlang.Expressions._ import solvers.SolverFactory import synthesis.ConvertHoles.convertHoles @@ -437,7 +436,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int replaceFromIDs(mapping, l) case ArrayLength(a) => - var FiniteArray(elems, default, IntLiteral(length)) = e(a) + val FiniteArray(_, _, IntLiteral(length)) = e(a) IntLiteral(length) case ArrayUpdated(a, i, v) => @@ -452,7 +451,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int case ArraySelect(a, i) => val IntLiteral(index) = e(i) - val FiniteArray(elems, default, length) = e(a) + val FiniteArray(elems, default, _) = e(a) try { elems.get(index).orElse(default).get } catch { @@ -504,7 +503,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int e(impl) case choose @ Choose(_, None) => - import purescala.ExprOps.simplestValue implicit val debugSection = utils.DebugSectionSynthesis @@ -514,9 +512,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int val ins = p.as.map(rctx.mappings(_)) - if (clpCache contains (choose, ins)) { - clpCache((choose, ins)) - } else { + clpCache.getOrElse((choose, ins), { val tStart = System.currentTimeMillis val solver = SolverFactory.getFromSettings(ctx, program).getNewSolver() @@ -553,7 +549,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int } finally { solver.free() } - } + }) case MatchExpr(scrut, cases) => val rscrut = e(scrut) diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala index 9d1dbc28c..b6bb072f0 100644 --- a/src/main/scala/leon/evaluators/TracingEvaluator.scala +++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala @@ -5,9 +5,7 @@ package evaluators import purescala.Common._ import purescala.Expressions._ -import purescala.Extractors._ import purescala.Definitions._ -import purescala.ExprOps._ import purescala.Types._ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog, maxSteps) { diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index e8771c17a..408cdfe16 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -3,9 +3,7 @@ package leon package frontends.scalac -import scala.tools.nsc._ import scala.reflect.internal.util._ -import scala.tools.nsc.plugins._ import scala.language.implicitConversions @@ -37,7 +35,6 @@ trait CodeExtraction extends ASTExtractors { import global.definitions._ import StructuralExtractors._ import ExpressionExtractors._ - import ExtractorHelpers._ import scala.collection.immutable.Set val reporter = self.ctx.reporter @@ -1145,7 +1142,6 @@ trait CodeExtraction extends ASTExtractors { case ExTuple(tpes, exprs) => val tupleExprs = exprs.map(e => extractTree(e)) - val tupleType = TupleType(tupleExprs.map(expr => expr.getType)) Tuple(tupleExprs) case ExErrorExpression(str, tpt) => @@ -1349,8 +1345,6 @@ trait CodeExtraction extends ASTExtractors { } case hole @ ExHoleExpression(tpt, exprs) => - val leonExprs = exprs.map(extractTree) - Hole(extractType(tpt), exprs.map(extractTree)) case ops @ ExWithOracleExpression(oracles, body) => -- GitLab