From fea65b24d5af65ee1b73997180d7cc7fe83adf4c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 26 Apr 2016 15:46:29 +0200
Subject: [PATCH] Corrected typo in Focus.scala Corrected bug in isValue
Corrected evaluation in Evaluator (partition already evaluated)
---
src/main/scala/leon/evaluators/Evaluator.scala | 5 +++--
src/main/scala/leon/purescala/ExprOps.scala | 1 +
src/main/scala/leon/repair/rules/Focus.scala | 2 +-
3 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index c924e8bb5..a4cb12831 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -75,8 +75,9 @@ trait DeterministicEvaluator extends Evaluator {
/** From a not yet well evaluated context with dependencies between variables, returns a head where all exprs are values (as a Left())
* If this does not succeed, it provides an error message as Right()*/
private def _evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
- var f= mapping.toSet
- var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]()
+ val (evaled, nonevaled) = mapping.partition{ case (id, expr) => purescala.ExprOps.isValue(expr)}
+ var f= nonevaled.toSet
+ var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
var changed = true
while(f.nonEmpty && changed) {
changed = false
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 1828709ef..f3a9a94ca 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2177,6 +2177,7 @@ object ExprOps extends GenTreeOps[Expr] {
case (FiniteLambda(mapping, default, tpe), exTpe@FunctionType(ins, out)) =>
tpe == exTpe
case (Lambda(valdefs, body), FunctionType(ins, out)) =>
+ variablesOf(e).isEmpty &&
(valdefs zip ins forall (vdin => (vdin._1.getType == vdin._2) < s"${vdin._1.getType} is not equal to ${vdin._2}")) &&
(body.getType == out) < s"${body.getType} is not equal to ${out}"
case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index cd0da333b..1645b7bcc 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -66,7 +66,7 @@ case object Focus extends PreprocessingRule("Focus") {
def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator): Boolean = {
p.eb.invalids.exists { ex =>
- evaluator.evalEnvExpr(e, env).result match {
+ evaluator.evalEnvExpr(e, (p.as zip ex.ins).toMap ++ env) match {
case Some(BooleanLiteral(b)) => b
case _ => true
}
--
GitLab