From 2113abb6b9a32073ad33c21b02741dcec66bb76b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 18 Apr 2016 16:22:21 +0200
Subject: [PATCH] Corrected the display with respect to maps outputed in leon (
-> Some)
---
src/main/scala/leon/evaluators/RecursiveEvaluator.scala | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 28843738b..cfb45f733 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -117,7 +117,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val res = pre_str + mp_map.map{ case (k, v) =>
(e(application(fk, Seq(k))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) }) +
inkv_str +
- (e(application(fv, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })}.mkString(betweenkv_str) + post_str
+ (v match {
+ case CaseClass(some, Seq(v)) if some == program.library.Some.get.typed(Seq(tb)) =>
+ (e(application(fv, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })
+ case _ => throw EvalError(typeErrorMsg(v, program.library.Some.get.typed(Seq(tb))))
+ })}.mkString(betweenkv_str) + post_str
StringLiteral(res)
--
GitLab