Non-functional changes

src/main/scala/leon/evaluators/Evaluator.scala

@@ -59,8 +59,8 @@ trait DeterministicEvaluator extends Evaluator {
         case Right(errorMessage) =>
           val m = mapping.filter { case (k, v) => purescala.ExprOps.isValue(v) }
           super.eval(expr, m) match {
-            case res@evaluators.EvaluationResults.Successful(result) => res
-            case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
+            case res@EvaluationResults.Successful(result) => res
+            case _ => EvaluationResults.EvaluatorError(errorMessage)
           }
       }
     }
@@ -73,7 +73,8 @@ trait DeterministicEvaluator extends Evaluator {
     } else {
       _evalEnv(mapping) match {
         case Left(m) => m
-        case Right(msg) => mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
+        case Right(msg) =>
+          mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
       }
     }
   }
@@ -83,7 +84,7 @@ trait DeterministicEvaluator extends Evaluator {
   private def _evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
     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 mBuilder = scala.collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
     var changed = true
     while(f.nonEmpty && changed) {
       changed = false
@@ -100,7 +101,7 @@ trait DeterministicEvaluator extends Evaluator {
     if(!changed) {
       val str = "In the context " + mapping + ",\n" +
       (for((i, v) <- f) yield {
-        s"eval(${v}) returned the error: " + eval(v, mBuilder.toMap)
+        s"eval($v) returned the error: " + eval(v, mBuilder.toMap)
       }).mkString("\n")
       Right(str)
     } else Left(mBuilder.toMap)

src/main/scala/leon/evaluators/RecursiveEvaluator.scala

@@ -69,6 +69,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
 
     case Let(i,ex,b) =>
       val first = e(ex)
+      //println(s"Eval $i to $first")
       e(b)(rctx.withNewVar(i, first), gctx)
 
     case Assert(cond, oerr, body) =>
@@ -131,6 +132,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
 
       val evArgs = args map e
 
+      //println(s"calling ${tfd.id} with $evArgs")
+
       // build a mapping for the function...
       val frame = rctx.withNewVars(tfd.paramSubst(evArgs))
 
@@ -155,6 +158,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         e(body)(frame, gctx)
       }
 
+      //println(s"Gave $callResult")
+
       tfd.postcondition match  {
         case Some(post) =>
           e(application(post, Seq(callResult)))(frame, gctx) match {