From 958a90a8d0094878246e3fa191f48fd510b45e26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 18 Apr 2016 14:29:56 +0200
Subject: [PATCH] Added basic map to string support Corrected bug with unicode
chars in the build.sbt
---
build.sbt | 2 +-
library/collection/List.scala | 13 +++++++++-
library/lang/Map.scala | 5 ++++
.../leon/evaluators/RecursiveEvaluator.scala | 14 +++++++++++
src/main/scala/leon/utils/Library.scala | 2 ++
testcases/stringrender/MapRender.scala | 25 +++++++++++++++++++
6 files changed, 59 insertions(+), 2 deletions(-)
create mode 100644 testcases/stringrender/MapRender.scala
diff --git a/build.sbt b/build.sbt
index 111613dd1..618d4f2ba 100644
--- a/build.sbt
+++ b/build.sbt
@@ -111,7 +111,7 @@ sourceGenerators in Compile <+= Def.task {
|object Build {
| val baseDirectory = \"\"\"${baseDirectory.value.toString}\"\"\"
| val libFiles = List(
- | ${libFiles.mkString("\"\"\"", "\"\"\",\n \"\"\"", "\"\"\"")}
+ | ${libFiles.mkString("\"\"\"", "\"\"\",\n \"\"\"", "\"\"\"").replaceAll("\\\\"+"u","\\\\\"\"\"+\"\"\"u")}
| )
|}""".stripMargin)
Seq(build)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 69c30d39f..61089979b 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -552,7 +552,6 @@ sealed abstract class List[T] {
def toSet: Set[T] = foldLeft(Set[T]()){
case (current, next) => current ++ Set(next)
}
-
}
@isabelle.constructor(name = "List.list.Cons")
@@ -577,6 +576,18 @@ object List {
else Cons[T](x, fill[T](n-1)(x))
} ensuring(res => (res.content == (if (n <= BigInt(0)) Set.empty[T] else Set(x))) &&
res.size == (if (n <= BigInt(0)) BigInt(0) else n))
+
+ @library
+ def mkString[A](l: List[A], pre: String, mid: String, post: String, f : A => String) = {
+ def rec(l: List[A]): String = l match {
+ case Nil() => ""
+ case Cons(a, b) => mid + f(a) + rec(b)
+ }
+ pre + (l match {
+ case Nil() => ""
+ case Cons(a, b) => f(a) + rec(b)
+ }) + post
+ }
}
@library
diff --git a/library/lang/Map.scala b/library/lang/Map.scala
index 2a08449cc..5f6ee3baf 100644
--- a/library/lang/Map.scala
+++ b/library/lang/Map.scala
@@ -12,6 +12,11 @@ object Map {
def apply[A,B](elems: (A,B)*) = {
new Map[A,B](scala.collection.immutable.Map[A,B](elems : _*))
}
+
+ @extern @library
+ def mkString[A, B](map: Map[A, B], pre: String, inkv: String, betweenkv: String, post: String, fA : A => String, fB: B => String) = {
+ pre + map.theMap.map{ case (k, v) => fA(k) + inkv + fB(v)}.mkString(betweenkv) + post
+ }
}
@ignore
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 4d70063fb..28843738b 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -107,6 +107,20 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case _ => throw EvalError(typeErrorMsg(input, StringType))
}
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta, tb)), Seq(mp, pre, inkv, betweenkv, post, fk, fv)) if fd == program.library.mapMkString.get =>
+ val pre_str = e(pre) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(pre, StringType)) }
+ val inkv_str = e(inkv) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inkv, StringType)) }
+ val post_str = e(post) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(post, StringType)) }
+ val betweenkv_str = e(betweenkv) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(betweenkv, StringType)) }
+ val (mp_map, keyType, valueType) = e(mp) match { case FiniteMap(theMap, keyType, valueType) => (theMap, keyType, valueType) case _ => throw EvalError(typeErrorMsg(mp, MapType(ta, tb))) }
+
+ 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
+
+ StringLiteral(res)
+
case FunctionInvocation(tfd, args) =>
if (gctx.stepsLeft < 0) {
throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 6bff50527..1fc502212 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -26,6 +26,8 @@ case class Library(pgm: Program) {
lazy val escape = lookup("leon.lang.StrOps.escape").collectFirst { case fd : FunDef => fd }
+ lazy val mapMkString = lookup("leon.lang.Map.mkString").collectFirst { case fd : FunDef => fd }
+
def lookup(name: String): Seq[Definition] = {
pgm.lookupAll(name)
}
diff --git a/testcases/stringrender/MapRender.scala b/testcases/stringrender/MapRender.scala
new file mode 100644
index 000000000..a5b27ad09
--- /dev/null
+++ b/testcases/stringrender/MapRender.scala
@@ -0,0 +1,25 @@
+import leon.collection._
+import leon.collection.List
+import leon.lang._
+import leon.proof.check
+import leon.lang.synthesis._
+import scala.language.postfixOps
+import leon.annotation._
+
+object MapRender {
+
+ def f(i: Int): Map[Int, Int] = {
+ Map(1 -> i)
+ } ensuring {
+ (m: Map[Int, Int]) => m(1) == 2
+ }
+
+ def g(m: Map[Int, Int]): Boolean = {
+ !m.contains(0) || !m.contains(1)
+ } holds
+
+ def mapIntIntToString(in : Map[Int, Int]): String = {
+ Map.mkString(in, "MyMap(\n "," -> ", ",\n ", ")", (i:Int) => i.toString, (i:Int) => i.toString)
+ }
+}
+
--
GitLab