diff --git a/library/leon/collection/List.scala b/library/leon/collection/List.scala
index 5803bbf993def9d80019a7f7839860cf249db729..a7bf09527b530d64e1f29811f7074ef764ae694e 100644
--- a/library/leon/collection/List.scala
+++ b/library/leon/collection/List.scala
@@ -575,15 +575,15 @@ object List {
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 mkString[A](l: List[A], mid: 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 {
+ l match {
case Nil() => ""
case Cons(a, b) => f(a) + rec(b)
- }) + post
+ }
}
}
diff --git a/library/leon/lang/Bag.scala b/library/leon/lang/Bag.scala
index 2825bd1fa4d5ca5136adb9dd0afc391b10ca5cbb..6a6be20a4a2622d4877872c2c44e91dc6a958270 100644
--- a/library/leon/lang/Bag.scala
+++ b/library/leon/lang/Bag.scala
@@ -11,6 +11,13 @@ object Bag {
def apply[T](elems: (T, BigInt)*) = {
new Bag[T](scala.collection.immutable.Map[T, BigInt](elems : _*))
}
+
+ @extern @library
+ def mkString[A](bag: Bag[A], infix: String, f: A => String) = {
+ bag.theBag.flatMap{ case (k, v) =>
+ List.range(1, v.toString.toInt).map(_ => f(k))
+ }.toList.sorted.mkString(infix)
+ }
}
@ignore
diff --git a/library/leon/lang/Map.scala b/library/leon/lang/Map.scala
index 5f6ee3bafd5d77be79d80025a506e649a31220e8..ce66a93d553c068eaf5e3dc66b37e3fbb9abc500 100644
--- a/library/leon/lang/Map.scala
+++ b/library/leon/lang/Map.scala
@@ -14,8 +14,8 @@ object Map {
}
@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
+ def mkString[A, B](map: Map[A, B], inkv: String, betweenkv: String, fA : A => String, fB: B => String) = {
+ map.theMap.map{ case (k, v) => fA(k) + inkv + fB(v)}.toList.sorted.mkString(betweenkv)
}
}
diff --git a/library/leon/lang/Set.scala b/library/leon/lang/Set.scala
index 351af3f6abb256229cfe27d3a13ce7ad9c191e17..6e973258c711aa109822568dbb7cab5a2fe2b23a 100644
--- a/library/leon/lang/Set.scala
+++ b/library/leon/lang/Set.scala
@@ -11,6 +11,11 @@ object Set {
def apply[T](elems: T*) = {
new Set[T](scala.collection.immutable.Set[T](elems : _*))
}
+
+ @extern @library
+ def mkString[A](map: Set[A], infix: String, fA : A => String) = {
+ map.theSet.map(fA).toList.sorted.mkString(infix)
+ }
}
@ignore
diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index 2b105aaefc2767ae090e4ed8344c264e543cfcc9..b0c113dfa07d9f8a69d91f1d2c027c13589994a0 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -62,6 +62,28 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
/** True if Application(Lambda(), ...) have to be simplified. */
var evaluateApplications = true
+ // Used to make the final mkString for maps, sets, and bags. First column is the key to sort the expression on, second are the values and third are the trees.
+ protected def mkString(elements: List[(String, Expr, Expr)], infix: (Expr, Expr)): (Expr, Expr) = {
+ val (infix_value, infix_tree) = infix
+ val (sorting_key, elements_value, elements_tree) = elements.sortBy(f => f._1).unzip3
+
+ val fst = infix_value match {
+ case StringLiteral(v) if elements_value.forall(_.isInstanceOf[StringLiteral]) =>
+ StringLiteral(elements_value.map(_.asInstanceOf[StringLiteral].value).mkString(v))
+ case infix_value =>
+ elements_value match {
+ case Nil => StringLiteral("")
+ case a::q => q.foldLeft(a: Expr){ case (a, s) => StringConcat(StringConcat(a, infix_value), s) }
+ }
+ }
+
+ val snd = elements_tree match {
+ case Nil => StringLiteral("")
+ case a::q => q.foldLeft(a){ case (a, s) => StringConcat(StringConcat(a, infix_tree), s) }
+ }
+ (fst, snd)
+ }
+
protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = {
implicit def aToC: AbstractEvaluator.this.underlying.RC = DefaultRecContext(rctx.mappings.filter{ case (k, v) => ExprOps.isValue(v) })
expr match {
@@ -92,6 +114,59 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
case Some(Some((c, mappings))) => e(c.rhs)(rctx.withNewVars2(mappings), gctx)
case _ => throw RuntimeError("MatchError(Abstract evaluation): "+escrut.asString+" did not match any of the cases :\n" + cases.mkString("\n"))
}
+
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta, tb)), Seq(mp, inkv, betweenkv, fk, fv)) if fd == program.library.mapMkString.get =>
+ val (inkv_str, inkv_tree) = e(inkv)
+ val infix = e(betweenkv)
+ val (mp_map, mp_tree) = e(mp) match {
+ case (FiniteMap(theMap, keyType, valueType), t) => (theMap, t)
+ case (e, f) =>
+ println("First argument is not a finite map: " + e)
+ throw EvalError(typeErrorMsg(mp, MapType(ta, tb)))
+ }
+
+ val res1 = mp_map.toList.map{ case (k, v) =>
+ val (kvalue, ktree) = e(application(fk, Seq(k)))
+ val (vvalue, vtree) = e(application(fv, Seq(v)))
+ val abs_value = StringConcat(StringConcat(ktree, inkv_tree), vtree)
+ kvalue match {
+ case StringLiteral(k) =>
+ if(ExprOps.isValue(vvalue) && ExprOps.isValue(inkv_str)) {
+ underlying.e(StringConcat(StringConcat(kvalue, inkv_str), vvalue)) match {
+ case sl@StringLiteral(s) => (s, sl, abs_value)
+ case e => throw RuntimeError("Not a string literal: " + e)
+ }
+ } else {
+ (k, StringConcat(StringConcat(kvalue, inkv_str), vvalue), abs_value)
+ }
+ case _ =>
+ throw RuntimeError("cannot infer the order on which to print the map " + mp_map)
+ }
+ }
+
+ mkString(res1, infix)
+
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.setMkString.get =>
+ val infix = e(inf)
+ val (mp_set, mp_tree) = e(mp) match { case (FiniteSet(elems, valueType), t) => (elems, t) case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
+
+ val res = mp_set.toList.map{ case v =>
+ e(application(f, Seq(v))) match { case (sl@StringLiteral(s), t) => (s, sl, t)
+ case _ => throw EvalError(typeErrorMsg(v, StringType)) } }
+
+ mkString(res, infix)
+
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.bagMkString.get =>
+ val infix = e(inf)
+ val (mp_bag, mp_tree) = e(mp) match { case (FiniteBag(elems, valueType), t) => (elems, t) case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
+
+ val res = mp_bag.toList.flatMap{ case (k, v) =>
+ val fk = (e(application(f, Seq(k))) match { case (sl@StringLiteral(s), t) => (s, sl, t) case _ => throw EvalError(typeErrorMsg(k, StringType)) })
+ val times = (e(v)) match { case (InfiniteIntegerLiteral(i), t) => i case _ => throw EvalError(typeErrorMsg(k, IntegerType)) }
+ List.fill(times.toString.toInt)(fk)
+ }
+
+ mkString(res, infix)
case FunctionInvocation(tfd, args) =>
if (gctx.stepsLeft < 0) {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index a709de91fdf5af88ff64fa9393dd0a25e2d122dc..f5536ee98318c4b9a2005a2af3bd82b8d0b3d71e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -111,23 +111,42 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
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)) }
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta, tb)), Seq(mp, inkv, betweenkv, fk, fv)) if fd == program.library.mapMkString.get =>
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 mp_map = e(mp) match { case FiniteMap(theMap, keyType, valueType) => theMap case _ => throw EvalError(typeErrorMsg(mp, MapType(ta, tb))) }
- val res = pre_str + mp_map.map{ case (k, v) =>
+ val res = mp_map.map{ case (k, v) =>
(e(application(fk, Seq(k))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) }) +
inkv_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
+ })}.toList.sorted.mkString(betweenkv_str)
StringLiteral(res)
+
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.setMkString.get =>
+ val inf_str = e(inf) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inf, StringType)) }
+ val mp_set = e(mp) match { case FiniteSet(elems, valueType) => elems case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
+
+ val res = mp_set.map{ case v =>
+ e(application(f, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(v, StringType)) } }.toList.sorted.mkString(inf_str)
+
+ StringLiteral(res)
+
+ case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.bagMkString.get =>
+ val inf_str = e(inf) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inf, StringType)) }
+ val mp_bag = e(mp) match { case FiniteBag(elems, valueType) => elems case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
+
+ val res = mp_bag.flatMap{ case (k, v) =>
+ val fk = (e(application(f, Seq(k))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })
+ val times = (e(v)) match { case InfiniteIntegerLiteral(i) => i case _ => throw EvalError(typeErrorMsg(k, IntegerType)) }
+ List.range(1, times.toString.toInt).map(_ => fk)
+ }.toList.sorted.mkString(inf_str)
+
+ StringLiteral(res)
case FunctionInvocation(tfd, args) =>
if (gctx.stepsLeft < 0) {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b812bcf573bf5c9d8cbb3942c15b4f4056b15e5d..5bb663fd1224101008920d68071fd421c6306f09 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -219,7 +219,12 @@ class PrettyPrinter(opts: PrinterOptions,
case Tuple(exprs) => p"($exprs)"
case TupleSelect(t, i) => p"$t._$i"
case NoTree(tpe) => p"<empty tree>[$tpe]"
- case Choose(pred) => p"choose($pred)"
+ case Choose(pred) =>
+ val choose = (for{scope <- getScope
+ program <- opgm }
+ yield simplifyPath("leon" :: "lang" :: "synthesis" :: "choose" :: Nil, scope, false)(program))
+ .getOrElse("leon.lang.synthesis.choose")
+ p"$choose($pred)"
case e @ Error(tpe, err) => p"""error[$tpe]("$err")"""
case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
case IsInstanceOf(e, cct) =>
@@ -330,7 +335,7 @@ class PrettyPrinter(opts: PrinterOptions,
case RealDivision(l,r) => optP { p"$l / $r" }
case fs @ FiniteSet(rs, _) => p"{${rs.toSeq}}"
case fs @ FiniteBag(rs, _) => p"{$rs}"
- case fm @ FiniteMap(rs, _, _) => p"{$rs}"
+ case fm @ FiniteMap(rs, _, _) => p"{${rs.toSeq}}"
case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
case ElementOfSet(e,s) => p"$e \u2208 $s"
case SubsetOf(l,r) => p"$l \u2286 $r"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 40dcbdab8188f71988d78e58ffb200224de57891..393c38ad356796e4007220146317bb46ef0c62bb 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -25,7 +25,6 @@ class ScalaPrinter(opts: PrinterOptions,
case _ => true
}))
case Not(Equals(l, r)) => optP { p"$l != $r" }
- case Choose(pred) => p"choose($pred)"
case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
case SetAdd(s,e) => optP { p"$s + $e" }
@@ -36,14 +35,14 @@ class ScalaPrinter(opts: PrinterOptions,
case SetCardinality(s) => p"$s.size"
case SubsetOf(subset,superset) => p"$subset.subsetOf($superset)"
- case b @ FiniteBag(els, t) => p"Bag[$t]($els)"
+ case b @ FiniteBag(els, t) => p"Bag[$t](${els.toSeq})"
case BagAdd(s,e) => optP { p"$s + $e" }
case BagUnion(l,r) => optP { p"$l ++ $r" }
case BagDifference(l,r) => optP { p"$l -- $r" }
case BagIntersection(l,r) => optP { p"$l & $r" }
case MapUnion(l,r) => optP { p"$l ++ $r" }
- case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
+ case m @ FiniteMap(els, k, v) => p"Map[$k,$v](${els.toSeq})"
case InfiniteIntegerLiteral(v) => p"BigInt($v)"
case a@FiniteArray(elems, oDef, size) =>
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 546e5726382d814ba533dc3de87241c7517e0f99..e43c882c234d55f68b14b13aff1187fbd6d74b3e 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -80,6 +80,7 @@ object TypeOps extends GenTreeOps[TypeTree] {
case (_: TupleType, _: TupleType) |
(_: SetType, _: SetType) |
(_: MapType, _: MapType) |
+ (_: BagType, _: BagType) |
(_: FunctionType, _: FunctionType) =>
val NAryType(ts1, _) = tpe
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 1fc502212b66d709d8dcd41efc726b264e59dec2..3e9b99c88d12c58fbc090f38eed387ddae582d75 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -27,6 +27,10 @@ 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 }
+
+ lazy val setMkString = lookup("leon.lang.Set.mkString").collectFirst { case fd : FunDef => fd }
+
+ lazy val bagMkString = lookup("leon.lang.Bag.mkString").collectFirst { case fd : FunDef => fd }
def lookup(name: String): Seq[Definition] = {
pgm.lookupAll(name)