From aa95e1b88dc7808b1b2a6be61098cbbfce0aa74c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 9 Oct 2015 16:57:00 +0200
Subject: [PATCH] Finitemaps are now maps, surprisingly.
---
src/main/scala/leon/evaluators/ScalacEvaluator.scala | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/src/main/scala/leon/evaluators/ScalacEvaluator.scala b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
index 2b13d2655..2356bdf33 100644
--- a/src/main/scala/leon/evaluators/ScalacEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
@@ -163,9 +163,6 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
}
def leonToScalac(e: Expr): AnyRef = e match {
- case eo: ExternalObject =>
- eo
-
case CharLiteral(v) =>
new java.lang.Character(v)
@@ -274,7 +271,7 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
FiniteMap(s.iterator.map {
case (k, v) => scalacToLeon(k, ktpe) -> scalacToLeon(v, vtpe)
- }.toSeq, ktpe, vtpe)
+ }.toMap, ktpe, vtpe)
case FunctionType(_, _) =>
unsupported("It is not possible to pass a closure from @extern back to leon")
@@ -459,8 +456,6 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
}
}
-case class ExternalObject(o: Any, getType: TypeTree) extends Expr with Terminal
-
object LeonJVMCallBacks {
def callBack(token: Int, className: String, methodName: String, args: Array[AnyRef]): AnyRef = {
val ev = RuntimeResources.get[ScalacEvaluator](token)
--
GitLab