From 29ec0e594dacc6e5f739a1054a359cd78dc39a32 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 2 Mar 2015 17:34:36 +0100
Subject: [PATCH] Fix evaluation of lambda applications
---
src/main/scala/leon/evaluators/DefaultEvaluator.scala | 2 +-
src/main/scala/leon/evaluators/DualEvaluator.scala | 2 +-
.../scala/leon/evaluators/RecursiveEvaluator.scala | 10 +++++-----
src/main/scala/leon/evaluators/TracingEvaluator.scala | 2 +-
src/main/scala/leon/repair/RepairNDEvaluator.scala | 4 ++--
.../scala/leon/repair/RepairTrackingEvaluator.scala | 4 ++--
6 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index d92c65399..bf27ce8bd 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -15,6 +15,6 @@ class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluat
def initGC = new GlobalContext()
case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext {
- def withVars(news: Map[Identifier, Expr]) = copy(news)
+ def newVars(news: Map[Identifier, Expr]) = copy(news)
}
}
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index 7903f8c5e..b350aafc5 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -26,7 +26,7 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) exte
val isCompiled = prog.definedFunctions.toSet
case class DefaultRecContext(mappings: Map[Identifier, Expr], needJVMRef: Boolean = false) extends RecContext {
- def withVars(news: Map[Identifier, Expr]) = copy(news)
+ def newVars(news: Map[Identifier, Expr]) = copy(news)
}
case class RawObject(o: AnyRef, tpe: TypeTree) extends Expr {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index a741602dd..b62d2ffc5 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -32,14 +32,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
trait RecContext {
def mappings: Map[Identifier, Expr]
- def withVars(news: Map[Identifier, Expr]): RC;
+ def newVars(news: Map[Identifier, Expr]): RC;
def withNewVar(id: Identifier, v: Expr): RC = {
- withVars(mappings + (id -> v))
+ newVars(mappings + (id -> v))
}
def withNewVars(news: Map[Identifier, Expr]): RC = {
- withVars(mappings ++ news)
+ newVars(mappings ++ news)
}
}
@@ -89,7 +89,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Lambda(params, body) =>
val newArgs = args.map(e)
val mapping = (params.map(_.id) zip newArgs).toMap
- e(body)(rctx.withVars(mapping), gctx)
+ e(body)(rctx.withNewVars(mapping), gctx)
case f =>
throw EvalError("Cannot apply non-lambda function " + f)
}
@@ -149,7 +149,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val evArgs = args.map(a => e(a))
// build a mapping for the function...
- val frame = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
+ val frame = rctx.newVars((tfd.params.map(_.id) zip evArgs).toMap)
if(tfd.hasPrecondition) {
e(tfd.precondition.get)(frame, gctx) match {
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index c95b5f716..8321a9c5c 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -21,7 +21,7 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
class TracingGlobalContext(var values: List[(Tree, Expr)]) extends GlobalContext
case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext {
- def withVars(news: Map[Identifier, Expr]) = copy(mappings = news)
+ def newVars(news: Map[Identifier, Expr]) = copy(mappings = news)
}
override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = {
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index 054e20aa3..4dd78d134 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -26,7 +26,7 @@ class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr
val evArgs = args.map(a => e(a))
// build a mapping for the function...
- val frame = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
+ val frame = rctx.newVars((tfd.params.map(_.id) zip evArgs).toMap)
if(tfd.hasPrecondition) {
e(tfd.precondition.get)(frame, gctx) match {
@@ -76,4 +76,4 @@ class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 5b8791f47..791b7ec01 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -45,7 +45,7 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
def fiStatus = fiStatus_.toMap.withDefaultValue(false)
case class CollectingRecContext(mappings: Map[Identifier, Expr], lastFI : Option[FI]) extends RecContext {
- def withVars(news: Map[Identifier, Expr]) = copy(news, lastFI)
+ def newVars(news: Map[Identifier, Expr]) = copy(news, lastFI)
def withLastFI(fi : FI) = copy(lastFI = Some(fi))
}
@@ -59,7 +59,7 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
val evArgs = args.map(a => e(a))
// build a mapping for the function...
- val frameBlamingCaller = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
+ val frameBlamingCaller = rctx.newVars((tfd.params.map(_.id) zip evArgs).toMap)
if(tfd.hasPrecondition) {
e(tfd.precondition.get)(frameBlamingCaller, gctx) match {
--
GitLab