Add EvaluationPhase to try out evaluation, fix evaluation of CharLiteral

src/main/scala/leon/Main.scala

@@ -21,7 +21,8 @@ object Main {
       synthesis.SynthesisPhase,
       termination.TerminationPhase,
       verification.AnalysisPhase,
-      repair.RepairPhase
+      repair.RepairPhase,
+      evaluators.EvaluationPhase
     )
   }
 
@@ -42,9 +43,10 @@ object Main {
     val optNoop        = LeonFlagOptionDef("noop",        "No operation performed, just output program",           false)
     val optVerify      = LeonFlagOptionDef("verify",      "Verify function contracts",                             true )
     val optHelp        = LeonFlagOptionDef("help",        "Show help message",                                     false)
+    val optEval        = LeonFlagOptionDef("eval",        "Evaluate ground functions",                             false)
 
     override val definedOptions: Set[LeonOptionDef[Any]] =
-      Set(optTermination, optRepair, optSynthesis, optXLang, optWatch, optNoop, optHelp, optVerify)
+      Set(optTermination, optRepair, optSynthesis, optXLang, optWatch, optNoop, optHelp, optVerify, optEval)
 
   }
 
@@ -128,6 +130,7 @@ object Main {
     import xlang.XLangAnalysisPhase
     import verification.AnalysisPhase
     import repair.RepairPhase
+    import evaluators.EvaluationPhase
     import MainComponent._
 
     val helpF        = ctx.findOptionOrDefault(optHelp)
@@ -137,6 +140,7 @@ object Main {
     val repairF      = ctx.findOptionOrDefault(optRepair)
     val terminationF = ctx.findOptionOrDefault(optTermination)
     val verifyF      = ctx.findOptionOrDefault(optVerify)
+    val evalF        = ctx.findOptionOrDefault(optEval)
 
     if (helpF) {
       displayVersion(ctx.reporter)
@@ -157,6 +161,7 @@ object Main {
         else if (repairF) RepairPhase
         else if (terminationF) TerminationPhase
         else if (xlangF) XLangAnalysisPhase
+        else if (evalF) EvaluationPhase
         else if (verifyF) FunctionClosure andThen AnalysisPhase
         else    NoopPhase()
       }

src/main/scala/leon/evaluators/EvaluationPhase.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import purescala.Definitions._
+import purescala.DefOps._
+import purescala.Expressions._
+
+object EvaluationPhase extends LeonPhase[Program, Unit] {
+  val name = "Evaluation"
+  val description = "Evaluating ground functions"
+
+  implicit val debugSection = utils.DebugSectionEvaluation
+
+  def run(ctx: LeonContext)(program: Program): Unit = {
+    val evalFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
+
+    val reporter = ctx.reporter
+
+    val fdFilter = {
+      import OptionsHelpers._
+
+      filterInclusive(evalFuns.map(fdMatcher), None)
+    }
+
+    val toEvaluate = funDefsFromMain(program).toList.filter(_.params.size == 0).filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
+
+    if (toEvaluate.isEmpty) reporter.warning("No ground functions found with the given names")
+    
+    val eval = new DefaultEvaluator(ctx, program)
+    for (fd <- toEvaluate) {
+      reporter.info(s" - Evaluating ${fd.id}")
+      val call = FunctionInvocation(fd.typedWithDef, Seq())
+      eval.eval(call) match {
+        case EvaluationResults.Successful(ex) =>
+          reporter.info(s"  => $ex")
+        case EvaluationResults.RuntimeError(msg) =>
+          reporter.warning(s"  Runtime Error: $msg")
+        case EvaluationResults.EvaluatorError(msg) =>
+          reporter.warning(s"  Evaluator Error: $msg")
+      }
+    }
+  }
+}

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

@@ -565,8 +565,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
           throw RuntimeError("MatchError: "+rscrut+" did not match any of the cases")
       }
 
+    case l : CharLiteral => l
+
     case other =>
-      context.reporter.error(other.getPos, "Error: don't know how to handle " + other + " in Evaluator.")
+      context.reporter.error(other.getPos, "Error: don't know how to handle " + other + " in Evaluator ("+other.getClass+").")
       throw EvalError("Unhandled case in Evaluator : " + other) 
   }