Added basic map to string support

Corrected bug with unicode chars in the build.sbt

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)

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

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

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+")")

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)
   }

testcases/stringrender/MapRender.scala

+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)
+  }
+}
+