From 618041940641ed94118cd3b49fc3b574cace5f0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 28 Apr 2016 14:16:16 +0200
Subject: [PATCH] Evaluates lambda applications by default.

---
 .../leon/evaluators/AbstractEvaluator.scala   | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index 2e0a7a2bb..b52804547 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -59,16 +59,14 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
  
   /** True if CaseClassSelector(...CaseClass(...))  have to be simplified. */
   var evaluateCaseClassSelector = true
+  /** True if Application(Lambda(), ...)  have to be simplified. */
+  var evaluateApplications = true
   
   protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = {
     implicit def aToC: AbstractEvaluator.this.underlying.RC = DefaultRecContext(rctx.mappings.filter{ case (k, v) => ExprOps.isValue(v) })
     expr match {
     case Variable(id) =>
       (rctx.mappings.get(id), rctx.mappingsAbstract.get(id)) match {
-        case (Some(v), None) if v != expr => // We further evaluate v to make sure it is a value
-          e(v)
-        case (Some(v), Some(va)) if v != expr =>
-          (e(v)._1, va)
         case (Some(v), Some(va)) =>
           (v, va)
         case _ =>
@@ -131,15 +129,17 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
       val (ecaller, tcaller) = e(caller)
       val nargs = args map e
       val (eargs, targs) = nargs.unzip
-      val abs_value = Application(tcaller, targs)
-      if (ExprOps.isValue(ecaller) && (eargs forall ExprOps.isValue)) {
-        (underlying.e(Application(ecaller, eargs)), abs_value)
-      } else ecaller match {
-        case l @ Lambda(params, body) =>
+      ecaller match {
+        case l @ Lambda(params, body) if evaluateApplications =>
           val mapping = (params map (_.id) zip nargs).toMap
           e(body)(rctx.withNewVars2(mapping), gctx)
         case _ =>
-          (Application(ecaller, eargs), abs_value)
+          val abs_value = Application(tcaller, targs)
+          if (ExprOps.isValue(ecaller) && (eargs forall ExprOps.isValue)) {
+            (underlying.e(Application(ecaller, eargs)), abs_value)
+          } else {
+            (Application(ecaller, eargs), abs_value)
+          }
       }
 
     case Operator(es, builder) =>
-- 
GitLab