diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a876001683a2592e567b42f68747e4b86d462d20
--- /dev/null
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -0,0 +1,96 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import purescala.Extractors.Operator
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Definitions.{TypedFunDef, Program}
+import purescala.DefOps
+import purescala.TypeOps
+import purescala.ExprOps
+import purescala.Expressions.Expr
+import leon.utils.DebugSectionSynthesis
+
+/** The evaluation returns a pair (e, t),
+ * where e is the expression evaluated as much as possible, and t is the way the expression has been evaluated.
+ * Caution: If and Match statement require the condition to be non-abstract. */
+class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext with HasDefaultRecContext {
+ lazy val scalaEv = new ScalacEvaluator(underlying, ctx, prog)
+
+ /** Evaluates resuts which can be evaluated directly
+ * For example, concatenation of two string literals */
+ val underlying = new DefaultEvaluator(ctx, prog)
+ underlying.setEvaluationFailOnChoose(true)
+ override type Value = (Expr, Expr)
+
+ override val description: String = "Evaluates string programs but keeps the formula which generated the string"
+ override val name: String = "String Tracing evaluator"
+
+ protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = expr match {
+ case Variable(id) =>
+ rctx.mappings.get(id) match {
+ case Some(v) if v != expr =>
+ e(v)
+ case _ =>
+ (expr, expr)
+ }
+
+ case e if ExprOps.isValue(e) =>
+ (e, e)
+
+ case IfExpr(cond, thenn, elze) =>
+ val first = underlying.e(cond)
+ first match {
+ case BooleanLiteral(true) =>
+ ctx.reporter.ifDebug(printer => printer(thenn))(DebugSectionSynthesis)
+ e(thenn)
+ case BooleanLiteral(false) => e(elze)
+ case _ => throw EvalError(typeErrorMsg(first, BooleanType))
+ }
+
+ case MatchExpr(scrut, cases) =>
+ val (escrut, tscrut) = e(scrut)
+ val rscrut = escrut
+ cases.toStream.map(c => underlying.matchesCase(rscrut, c)).find(_.nonEmpty) match {
+ case Some(Some((c, mappings))) =>
+ e(c.rhs)(rctx.withNewVars(mappings), gctx)
+ case _ =>
+ throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases :" + cases)
+ }
+
+ case FunctionInvocation(tfd, args) =>
+ if (gctx.stepsLeft < 0) {
+ throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
+ }
+ gctx.stepsLeft -= 1
+ val evArgs = args map e
+ val evArgsValues = evArgs.map(_._1)
+ val evArgsOrigin = evArgs.map(_._2)
+
+ // build a mapping for the function...
+ val frame = rctx.withNewVars(tfd.paramSubst(evArgsValues))
+
+ val callResult = if ((evArgsValues forall ExprOps.isValue) && tfd.fd.annotations("extern") && ctx.classDir.isDefined) {
+ (scalaEv.call(tfd, evArgsValues), FunctionInvocation(tfd, evArgsOrigin))
+ } else {
+ if((!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) || tfd.body.exists(b => ExprOps.exists(e => e.isInstanceOf[Choose])(b))) {
+ (FunctionInvocation(tfd, evArgsValues), FunctionInvocation(tfd, evArgsOrigin))
+ } else {
+ val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
+ e(body)(frame, gctx)
+ }
+ }
+ callResult
+ case Operator(es, builder) =>
+ val (ees, ts) = es.map(e).unzip
+ if(ees forall ExprOps.isValue) {
+ (underlying.e(builder(ees)), builder(ts))
+ } else {
+ (builder(ees), builder(ts))
+ }
+ }
+
+
+}
diff --git a/src/main/scala/leon/evaluators/ContextualEvaluator.scala b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
index 0fc33102a04716816fc3b2a83faa1384b37da1fd..eb57bbbf3550d8d177f92188d12d1ff3a3abbbd5 100644
--- a/src/main/scala/leon/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
@@ -20,7 +20,9 @@ abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps
def initRC(mappings: Map[Identifier, Expr]): RC
def initGC(model: solvers.Model, check: Boolean): GC
- case class EvalError(msg : String) extends Exception
+ case class EvalError(msg : String) extends Exception {
+ override def getMessage = msg + Option(super.getMessage).map("\n" + _).getOrElse("")
+ }
case class RuntimeError(msg : String) extends Exception
case class QuantificationError(msg: String) extends Exception
@@ -72,7 +74,7 @@ abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps
protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Value
- def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected ${expected.asString}, found ${tree.asString}."
+ def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected ${expected.asString}, found ${tree.asString} of type ${tree.getType}."
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index f7240f1b763951aee607241cc07bf41a5c535e4a..193361f0e85a43eef47e1f2376cfcef1e8fffc56 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -28,6 +28,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
protected var clpCache = Map[(Choose, Seq[Expr]), Expr]()
+
+ private var evaluationFailsOnChoose = false
+ /** Sets the flag if when encountering a Choose, it should fail instead of solving it. */
+ def setEvaluationFailOnChoose(b: Boolean) = { this.evaluationFailsOnChoose = b; this }
protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Variable(id) =>
@@ -37,7 +41,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Some(v) =>
v
case None =>
- throw EvalError("No value for identifier " + id.asString + " in mapping.")
+ throw EvalError("No value for identifier " + id.asString + " in mapping " + rctx.mappings)
}
case Application(caller, args) =>
@@ -577,6 +581,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
e(p.asConstraint)
case choose: Choose =>
+ if(evaluationFailsOnChoose) {
+ throw EvalError("Evaluator set to not solve choose constructs")
+ }
implicit val debugSection = utils.DebugSectionSynthesis
@@ -637,7 +644,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Some(Some((c, mappings))) =>
e(c.rhs)(rctx.withNewVars(mappings), gctx)
case _ =>
- throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases")
+ throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases:\n"+cases)
}
case gl: GenericValue => gl
@@ -645,9 +652,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case l : Literal[_] => l
case other =>
- context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
- println("RecursiveEvaluator error:" + other.asString)
- throw EvalError("Unhandled case in Evaluator : " + other.asString)
+ throw EvalError("Unhandled case in Evaluator : [" + other.getClass + "] " + other.asString)
}
def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[Identifier, Expr])] = {
diff --git a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
deleted file mode 100644
index 62cde913fae123ab0fcd8c3d019953af9efb5942..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
+++ /dev/null
@@ -1,127 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Extractors.Operator
-import purescala.Expressions._
-import purescala.Types._
-import purescala.Definitions.{TypedFunDef, Program}
-import purescala.DefOps
-import purescala.Expressions.Expr
-import leon.utils.DebugSectionSynthesis
-import org.apache.commons.lang3.StringEscapeUtils
-
-class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext with HasDefaultRecContext {
-
- val underlying = new DefaultEvaluator(ctx, prog) {
- override protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
-
- case FunctionInvocation(TypedFunDef(fd, Nil), Seq(input)) if fd == prog.library.escape.get =>
- e(input) match {
- case StringLiteral(s) =>
- StringLiteral(StringEscapeUtils.escapeJava(s))
- case _ => throw EvalError(typeErrorMsg(input, StringType))
- }
-
- case FunctionInvocation(tfd, args) =>
- if (gctx.stepsLeft < 0) {
- throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
- }
- gctx.stepsLeft -= 1
-
- val evArgs = args map e
-
- // build a mapping for the function...
- val frame = rctx.withNewVars(tfd.paramSubst(evArgs))
-
- val callResult = if (tfd.fd.annotations("extern") && ctx.classDir.isDefined) {
- scalaEv.call(tfd, evArgs)
- } else {
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Evaluation of function with unknown implementation.")
- }
-
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
- e(body)(frame, gctx)
- }
-
- callResult
-
- case Variable(id) =>
- rctx.mappings.get(id) match {
- case Some(v) if v != expr =>
- e(v)
- case Some(v) =>
- v
- case None =>
- expr
- }
- case StringConcat(s1, s2) =>
- val es1 = e(s1)
- val es2 = e(s2)
- (es1, es2) match {
- case (StringLiteral(_), StringLiteral(_)) =>
- (super.e(StringConcat(es1, es2)))
- case _ =>
- StringConcat(es1, es2)
- }
- case expr =>
- super.e(expr)
- }
- }
- override type Value = (Expr, Expr)
-
- override val description: String = "Evaluates string programs but keeps the formula which generated the string"
- override val name: String = "String Tracing evaluator"
-
- protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = expr match {
- case Variable(id) =>
- rctx.mappings.get(id) match {
- case Some(v) if v != expr =>
- e(v)
- case Some(v) =>
- (v, expr)
- case None =>
- (expr, expr)
- }
-
- case StringConcat(s1, s2) =>
- val (es1, t1) = e(s1)
- val (es2, t2) = e(s2)
- (es1, es2) match {
- case (StringLiteral(_), StringLiteral(_)) =>
- (underlying.e(StringConcat(es1, es2)), StringConcat(t1, t2))
- case _ =>
- (StringConcat(es1, es2), StringConcat(t1, t2))
- }
- case StringLength(s1) =>
- val (es1, t1) = e(s1)
- es1 match {
- case StringLiteral(_) =>
- (underlying.e(StringLength(es1)), StringLength(t1))
- case _ =>
- (StringLength(es1), StringLength(t1))
- }
-
- case expr@StringLiteral(s) =>
- (expr, expr)
-
- case IfExpr(cond, thenn, elze) =>
- val first = underlying.e(cond)
- first match {
- case BooleanLiteral(true) =>
- ctx.reporter.ifDebug(printer => printer(thenn))(DebugSectionSynthesis)
- e(thenn)
- case BooleanLiteral(false) => e(elze)
- case _ => throw EvalError(typeErrorMsg(first, BooleanType))
- }
-
- case Operator(es, builder) =>
- val (ees, ts) = es.map(e).unzip
- (underlying.e(builder(ees)), builder(ts))
-
- }
-
-
-}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index e3ce7d1e01780ce02ba424396dabd3670f426966..23b32e0ee96ec98dca890a4a17ae8541c20244cb 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -317,6 +317,13 @@ object Constructors {
}
/** $encodingof simplified `fn(realArgs)` (function application).
+ * Transforms
+ * {{{ ((x: A, y: B) => g(x, y))(c, d) }}}
+ * into
+ * {{{val x0 = c
+ * val y0 = d
+ * g(x0, y0)}}}
+ * and further simplifies it.
* @see [[purescala.Expressions.Lambda Lambda]]
* @see [[purescala.Expressions.Application Application]]
*/
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 2eeb5a4d44fbde9af89ae5d5c103bed1ba1b75ed..4efc97986400f312afeb19674615e9822c56c8e3 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -285,7 +285,8 @@ object DefOps {
* By default it is the function invocation using the new function definition.
* @return the new program with a map from the old functions to the new functions */
def replaceFunDefs(p: Program)(fdMapF: FunDef => Option[FunDef],
- fiMapF: (FunctionInvocation, FunDef) => Option[Expr] = defaultFiMap) = {
+ fiMapF: (FunctionInvocation, FunDef) => Option[Expr] = defaultFiMap)
+ : (Program, Map[FunDef, FunDef])= {
var fdMapCache = Map[FunDef, Option[FunDef]]()
def fdMap(fd: FunDef): FunDef = {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index ec304c0aef6dd48e9dd01edd7d3ed25f190d1a82..19d20604ddc9ff9c3187c2fe24ee50f46e658850 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1190,6 +1190,12 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => InfiniteIntegerLiteral(0)
case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5)
+ case StringConcat(StringLiteral(""), a) => a
+ case StringConcat(a, StringLiteral("")) => a
+ case StringConcat(StringLiteral(a), StringLiteral(b)) => StringLiteral(a+b)
+ case StringConcat(StringLiteral(a), StringConcat(StringLiteral(b), c)) => StringConcat(StringLiteral(a+b), c)
+ case StringConcat(StringConcat(c, StringLiteral(a)), StringLiteral(b)) => StringConcat(c, StringLiteral(a+b))
+ case StringConcat(a, StringConcat(b, c)) => StringConcat(StringConcat(a, b), c)
//default
case e => e
}).copiedFrom(expr)
@@ -1278,6 +1284,181 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
case _ =>
false
}
+
+ /** Checks whether two expressions can be homomorphic and returns the corresponding mapping */
+ def canBeHomomorphic(t1: Expr, t2: Expr): Option[Map[Identifier, Identifier]] = {
+ val freeT1Variables = ExprOps.variablesOf(t1)
+ val freeT2Variables = ExprOps.variablesOf(t2)
+
+ def mergeContexts(a: Option[Map[Identifier, Identifier]], b: =>Option[Map[Identifier, Identifier]]) = a match {
+ case Some(m) =>
+ b match {
+ case Some(n) if (m.keySet & n.keySet) forall (key => m(key) == n(key)) =>
+ Some(m ++ n)
+ case _ =>None
+ }
+ case _ => None
+ }
+ object Same {
+ def unapply(tt: (Expr, Expr)): Option[(Expr, Expr)] = {
+ if (tt._1.getClass == tt._2.getClass) {
+ Some(tt)
+ } else {
+ None
+ }
+ }
+ }
+ implicit class AugmentedContext(c: Option[Map[Identifier, Identifier]]) {
+ def &&(other: => Option[Map[Identifier, Identifier]]) = mergeContexts(c, other)
+ def --(other: Seq[Identifier]) =
+ c.map(_ -- other)
+ }
+ implicit class AugmentedBooleant(c: Boolean) {
+ def &&(other: => Option[Map[Identifier, Identifier]]) = if(c) other else None
+ }
+ implicit class AugmentedSeq[T](c: Seq[T]) {
+ def mergeall(p: T => Option[Map[Identifier, Identifier]]) =
+ (Option(Map[Identifier, Identifier]()) /: c) {
+ case (s, c) => s && p(c)
+ }
+ }
+
+
+ def idHomo(i1: Identifier, i2: Identifier): Option[Map[Identifier, Identifier]] = {
+ if(!(freeT1Variables(i1) || freeT2Variables(i2)) || i1 == i2) Some(Map(i1 -> i2)) else None
+ }
+
+ def fdHomo(fd1: FunDef, fd2: FunDef): Option[Map[Identifier, Identifier]] = {
+ if(fd1.params.size == fd2.params.size) {
+ val newMap = Map((
+ (fd1.id -> fd2.id) +:
+ (fd1.paramIds zip fd2.paramIds)): _*)
+ Option(newMap) && isHomo(fd1.fullBody, fd2.fullBody)
+ } else None
+ }
+
+ def isHomo(t1: Expr, t2: Expr): Option[Map[Identifier, Identifier]] = {
+ def casesMatch(cs1 : Seq[MatchCase], cs2 : Seq[MatchCase]) : Option[Map[Identifier, Identifier]] = {
+ def patternHomo(p1: Pattern, p2: Pattern): (Boolean, Map[Identifier, Identifier]) = (p1, p2) match {
+ case (InstanceOfPattern(ob1, cd1), InstanceOfPattern(ob2, cd2)) =>
+ (ob1.size == ob2.size && cd1 == cd2, Map((ob1 zip ob2).toSeq : _*))
+
+ case (WildcardPattern(ob1), WildcardPattern(ob2)) =>
+ (ob1.size == ob2.size, Map((ob1 zip ob2).toSeq : _*))
+
+ case (CaseClassPattern(ob1, ccd1, subs1), CaseClassPattern(ob2, ccd2, subs2)) =>
+ val m = Map[Identifier, Identifier]() ++ (ob1 zip ob2)
+
+ if (ob1.size == ob2.size && ccd1 == ccd2 && subs1.size == subs2.size) {
+ (subs1 zip subs2).map { case (p1, p2) => patternHomo(p1, p2) }.foldLeft((true, m)) {
+ case ((b1, m1), (b2,m2)) => (b1 && b2, m1 ++ m2)
+ }
+ } else {
+ (false, Map())
+ }
+
+ case (UnapplyPattern(ob1, fd1, subs1), UnapplyPattern(ob2, fd2, subs2)) =>
+ val m = Map[Identifier, Identifier]() ++ (ob1 zip ob2)
+
+ if (ob1.size == ob2.size && fd1 == fd2 && subs1.size == subs2.size) {
+ (subs1 zip subs2).map { case (p1, p2) => patternHomo(p1, p2) }.foldLeft((true, m)) {
+ case ((b1, m1), (b2,m2)) => (b1 && b2, m1 ++ m2)
+ }
+ } else {
+ (false, Map())
+ }
+
+ case (TuplePattern(ob1, subs1), TuplePattern(ob2, subs2)) =>
+ val m = Map[Identifier, Identifier]() ++ (ob1 zip ob2)
+
+ if (ob1.size == ob2.size && subs1.size == subs2.size) {
+ (subs1 zip subs2).map { case (p1, p2) => patternHomo(p1, p2) }.foldLeft((true, m)) {
+ case ((b1, m1), (b2,m2)) => (b1 && b2, m1 ++ m2)
+ }
+ } else {
+ (false, Map())
+ }
+
+ case (LiteralPattern(ob1, lit1), LiteralPattern(ob2,lit2)) =>
+ (ob1.size == ob2.size && lit1 == lit2, (ob1 zip ob2).toMap)
+
+ case _ =>
+ (false, Map())
+ }
+
+ (cs1 zip cs2).mergeall {
+ case (MatchCase(p1, g1, e1), MatchCase(p2, g2, e2)) =>
+ val (h, nm) = patternHomo(p1, p2)
+ val g: Option[Map[Identifier, Identifier]] = (g1, g2) match {
+ case (Some(g1), Some(g2)) => Some(nm) && isHomo(g1,g2)
+ case (None, None) => Some(Map())
+ case _ => None
+ }
+ val e = Some(nm) && isHomo(e1, e2)
+
+ h && g && e
+ }
+
+ }
+
+ import synthesis.Witnesses.Terminating
+
+ val res: Option[Map[Identifier, Identifier]] = (t1, t2) match {
+ case (Variable(i1), Variable(i2)) =>
+ idHomo(i1, i2)
+
+ case (Let(id1, v1, e1), Let(id2, v2, e2)) =>
+ isHomo(v1, v2) &&
+ isHomo(e1, e2) && Some(Map(id1 -> id2))
+
+ case (LetDef(fds1, e1), LetDef(fds2, e2)) =>
+ fds1.size == fds2.size &&
+ {
+ val zipped = fds1.zip(fds2)
+ (zipped mergeall (fds => fdHomo(fds._1, fds._2))) && Some(zipped.map(fds => fds._1.id -> fds._2.id).toMap) &&
+ isHomo(e1, e2)
+ }
+
+ case (MatchExpr(s1, cs1), MatchExpr(s2, cs2)) =>
+ cs1.size == cs2.size && casesMatch(cs1,cs2) && isHomo(s1, s2)
+
+ case (Passes(in1, out1, cs1), Passes(in2, out2, cs2)) =>
+ (cs1.size == cs2.size && casesMatch(cs1,cs2)) && isHomo(in1,in2) && isHomo(out1,out2)
+
+ case (FunctionInvocation(tfd1, args1), FunctionInvocation(tfd2, args2)) =>
+ // TODO: Check type params
+ fdHomo(tfd1.fd, tfd2.fd) &&
+ (args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
+
+ case (Terminating(tfd1, args1), Terminating(tfd2, args2)) =>
+ // TODO: Check type params
+ fdHomo(tfd1.fd, tfd2.fd) &&
+ (args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
+
+ case (Lambda(defs, body), Lambda(defs2, body2)) =>
+ // We remove variables introduced by lambdas.
+ (isHomo(body, body2) &&
+ (defs zip defs2).mergeall{ case (ValDef(a1), ValDef(a2)) => Option(Map(a1 -> a2)) }
+ ) -- (defs.map(_.id))
+
+ case (v1, v2) if isValue(v1) && isValue(v2) =>
+ v1 == v2 && Some(Map[Identifier, Identifier]())
+
+ case Same(Operator(es1, _), Operator(es2, _)) =>
+ (es1.size == es2.size) &&
+ (es1 zip es2).mergeall{ case (e1, e2) => isHomo(e1, e2) }
+
+ case _ =>
+ None
+ }
+
+ res
+ }
+
+ isHomo(t1,t2)
+
+
+ } // ensuring (res => res.isEmpty || isHomomorphic(t1, t2)(res.get))
/** Checks whether two trees are homomoprhic modulo an identifier map.
*
@@ -1408,7 +1589,8 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
fdHomo(tfd1.fd, tfd2.fd) &&
(args1 zip args2).forall{ case (a1, a2) => isHomo(a1, a2) }
- // TODO: Seems a lot is missing, like Literals
+ case (v1, v2) if isValue(v1) && isValue(v2) =>
+ v1 == v2
case Same(Deconstructor(es1, _), Deconstructor(es2, _)) =>
(es1.size == es2.size) &&
@@ -1980,4 +2162,42 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
fun
}
+ /** Returns true if expr is a value of type t */
+ def isValueOfType(e: Expr, t: TypeTree): Boolean = {
+ (e, t) match {
+ case (StringLiteral(_), StringType) => true
+ case (IntLiteral(_), Int32Type) => true
+ case (InfiniteIntegerLiteral(_), IntegerType) => true
+ case (CharLiteral(_), CharType) => true
+ case (FractionalLiteral(_, _), RealType) => true
+ case (BooleanLiteral(_), BooleanType) => true
+ case (UnitLiteral(), UnitType) => true
+ case (GenericValue(t, _), tp) => t == tp
+ case (Tuple(elems), TupleType(bases)) =>
+ elems zip bases forall (eb => isValueOfType(eb._1, eb._2))
+ case (FiniteSet(elems, tbase), SetType(base)) =>
+ tbase == base &&
+ (elems forall isValue)
+ case (FiniteMap(elems, tk, tv), MapType(from, to)) =>
+ tk == from && tv == to &&
+ (elems forall (kv => isValueOfType(kv._1, from) && isValueOfType(kv._2, to) ))
+ case (NonemptyArray(elems, defaultValues), ArrayType(base)) =>
+ elems.values forall (x => isValueOfType(x, base))
+ case (EmptyArray(tpe), ArrayType(base)) =>
+ tpe == base
+ case (CaseClass(ct, args), ct2@AbstractClassType(classDef, tps)) =>
+ TypeOps.isSubtypeOf(ct, ct2) &&
+ ((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
+ case (CaseClass(ct, args), ct2@CaseClassType(classDef, tps)) =>
+ ct == ct2 &&
+ ((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
+ case (Lambda(valdefs, body), FunctionType(ins, out)) =>
+ (valdefs zip ins forall (vdin => vdin._1.getType == vdin._2)) &&
+ body.getType == out
+ case _ => false
+ }
+ }
+
+ /** Returns true if expr is a value. Stronger than isGround */
+ val isValue = (e: Expr) => isValueOfType(e, e.getType)
}
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 380554d8c3d8c566bb6da32d274ecf1eea199d11..e06055dc4d9dfce8b24d2d8ddb698ebbbc781079 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -3,6 +3,7 @@
package leon
package purescala
+import collection.mutable.ListBuffer
import Common._
import Definitions._
import Expressions._
@@ -11,11 +12,15 @@ import Constructors.letDef
class ScopeSimplifier extends Transformer {
case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
-
+
def register(oldNew: (Identifier, Identifier)): Scope = {
val newId = oldNew._2
copy(inScope = inScope + newId, oldToNew = oldToNew + oldNew)
}
+
+ def register(oldNews: Seq[(Identifier, Identifier)]): Scope = {
+ (this /: oldNews){ case (oldScope, oldNew) => oldScope.register(oldNew) }
+ }
def registerFunDef(oldNew: (FunDef, FunDef)): Scope = {
copy(funDefs = funDefs + oldNew)
@@ -45,20 +50,21 @@ class ScopeSimplifier extends Transformer {
}
val fds_mapping = for((fd, newId) <- fds_newIds) yield {
+ val localScopeToRegister = ListBuffer[(Identifier, Identifier)]() // We record the mapping of these variables only for the function.
val newArgs = for(ValDef(id) <- fd.params) yield {
- val newArg = genId(id, newScope)
- newScope = newScope.register(id -> newArg)
+ val newArg = genId(id, newScope.register(localScopeToRegister))
+ localScopeToRegister += (id -> newArg) // This renaming happens only inside the function.
ValDef(newArg)
}
val newFd = fd.duplicate(id = newId, params = newArgs)
newScope = newScope.registerFunDef(fd -> newFd)
- (newFd, fd)
+ (newFd, localScopeToRegister, fd)
}
- for((newFd, fd) <- fds_mapping) {
- newFd.fullBody = rec(fd.fullBody, newScope)
+ for((newFd, localScopeToRegister, fd) <- fds_mapping) {
+ newFd.fullBody = rec(fd.fullBody, newScope.register(localScopeToRegister))
}
letDef(fds_mapping.map(_._1), rec(body, newScope))
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index aa4c204d00187ab211a7164a45ae41d8d77d8f8f..0257a0b7a7c5592215206eefbb6928c46cc9995f 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -1,58 +1,124 @@
package leon.purescala
-import leon.evaluators.StringTracingEvaluator
import leon.purescala
+import leon.solvers.{ HenkinModel, Model, SolverFactory }
+import leon.LeonContext
+import leon.evaluators
+import leon.utils.StreamUtils
+import leon.purescala.Quantification._
+import leon.utils.DebugSectionSynthesis
+import leon.utils.DebugSectionVerification
import purescala.Definitions.Program
-import leon.evaluators.StringTracingEvaluator
import purescala.Expressions._
import purescala.Types.StringType
-import leon.utils.DebugSectionSynthesis
-import leon.utils.DebugSectionVerification
-import leon.purescala.Quantification._
import purescala.Constructors._
import purescala.ExprOps._
-import purescala.Expressions.{Pattern, Expr}
+import purescala.Expressions._
+import purescala.Expressions.{Choose }
import purescala.Extractors._
import purescala.TypeOps._
import purescala.Types._
import purescala.Common._
-import purescala.Expressions._
import purescala.Definitions._
-import leon.solvers.{ HenkinModel, Model, SolverFactory }
-import leon.LeonContext
-import leon.evaluators
+import scala.collection.mutable.ListBuffer
+import leon.evaluators.DefaultEvaluator
+
+object SelfPrettyPrinter {
+ def prettyPrintersForType(inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
+ (new SelfPrettyPrinter).prettyPrintersForType(inputType)
+ }
+ def print(v: Expr, orElse: =>String, excluded: Set[FunDef] = Set())(implicit ctx: LeonContext, program: Program): String = {
+ (new SelfPrettyPrinter).print(v, orElse, excluded)
+ }
+}
/** This pretty-printer uses functions defined in Leon itself.
* If not pretty printing function is defined, return the default value instead
* @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself)
* @return a user defined string for the given typed expression. */
-object SelfPrettyPrinter {
- def print(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(implicit ctx: LeonContext, program: Program): String = {
- (program.definedFunctions find {
- case fd if !excluded(fd) =>
- fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") &&
+class SelfPrettyPrinter {
+ private var allowedFunctions = Set[FunDef]()
+ private var excluded = Set[FunDef]()
+ /** Functions whose name does not need to end with `tostring` or which can be abstract, i.e. which may contain a choose construct.*/
+ def allowFunction(fd: FunDef) = { allowedFunctions += fd; this }
+
+ def excludeFunctions(fds: Set[FunDef]) = { excluded ++= fds; this }
+ def excludeFunction(fd: FunDef) = { excluded += fd; this }
+
+ /** Returns a list of possible lambdas that can transform the input type to a String*/
+ def prettyPrintersForType(inputType: TypeTree/*, existingPp: Map[TypeTree, List[Lambda]] = Map()*/)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
+ // Use the other argument if you need recursive typing (?)
+ program.definedFunctions.toStream flatMap {
+ fd =>
+ val isCandidate = fd.returnType == StringType &&
+ fd.params.length >= 1 &&
+ !excluded(fd) &&
+ (allowedFunctions(fd) || (
+ //TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) &&
+ fd.id.name.toLowerCase().endsWith("tostring") &&
program.callGraph.transitiveCallees(fd).forall { fde =>
!purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
+ }))
+ if(isCandidate) {
+ prettyPrinterFromCandidate(fd, inputType)
+ } else Stream.Empty
+ }
+ }
+
+
+ def prettyPrinterFromCandidate(fd: FunDef, inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
+ TypeOps.canBeSubtypeOf(inputType, fd.tparams.map(_.tp), fd.params.head.getType) match {
+ case Some(genericTypeMap) =>
+ val defGenericTypeMap = genericTypeMap.map{ case (k, v) => (Definitions.TypeParameterDef(k), v) }
+ def gatherPrettyPrinters(funIds: List[Identifier], acc: ListBuffer[Stream[Lambda]] = ListBuffer()): Option[Stream[List[Lambda]]] = funIds match {
+ case Nil => Some(StreamUtils.cartesianProduct(acc.toList))
+ case funId::tail => // For each function, find an expression which could be provided if it exists.
+ funId.getType match {
+ case FunctionType(Seq(in), StringType) => // Should have one argument.
+ val candidates = prettyPrintersForType(in)
+ gatherPrettyPrinters(tail, acc += candidates)
+ case _ => None
+ }
+ }
+ val funIds = fd.params.tail.map(x => TypeOps.instantiateType(x.id, defGenericTypeMap)).toList
+ gatherPrettyPrinters(funIds) match {
+ case Some(l) => for(lambdas <- l) yield {
+ val x = FreshIdentifier("x", fd.params.head.getType) // verify the type
+ Lambda(Seq(ValDef(x)), functionInvocation(fd, Variable(x)::lambdas))
+ }
+ case _ => Stream.empty
}
- }) match {
- case Some(fd) =>
- //println("Found fd: " + fd.id.name)
- val ste = new StringTracingEvaluator(ctx, program)
- try {
- val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+ case None => Stream.empty
+ }
+ }
+
+
+ /** Actually prints the expression with as alternative the given orElse */
+ def print(v: Expr, orElse: =>String, excluded: Set[FunDef] = Set())(implicit ctx: LeonContext, program: Program): String = {
+ this.excluded = excluded
+ val s = prettyPrintersForType(v.getType) // TODO: Included the variable excluded if necessary.
+ if(s.isEmpty) {
+ orElse
+ } else {
+ val l: Lambda = s.head
+ println("Executing pretty printer for type " + v.getType + " : " + l + " on " + v)
+ val ste = new DefaultEvaluator(ctx, program)
+ try {
+ val toEvaluate = application(l, Seq(v))
+ val result = ste.eval(toEvaluate)
result.result match {
- case Some((StringLiteral(res), _)) if res != "" =>
+ case Some(StringLiteral(res)) if res != "" =>
res
- case _ =>
- orElse
- }
- } catch {
- case e: evaluators.ContextualEvaluator#EvalError =>
+ case res =>
+ println("not a string literal " + res)
orElse
}
- case None =>
- orElse
+ } catch {
+ case e: evaluators.ContextualEvaluator#EvalError =>
+ println("Error " + e.msg)
+ orElse
+ }
}
}
}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 1755966e0223c0a4fa75eb01eb4a681ed1ddbf1d..78a483446624a28482772efe5752a4f6f44e1995 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -22,6 +22,13 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
implicit val ctx = ctx0
val reporter = ctx.reporter
+
+ private var keepAbstractExamples = false
+ /** If true, will not evaluate examples to check them. */
+ def setKeepAbstractExamples(b: Boolean) = { this.keepAbstractExamples = b; this}
+ /** Sets if evalution of the result of tests should stop on choose statements.
+ * Useful for programming by Example */
+ def setEvaluationFailOnChoose(b: Boolean) = { evaluator.setEvaluationFailOnChoose(b); this }
def extractFromFunDef(fd: FunDef, partition: Boolean): ExamplesBank = fd.postcondition match {
case Some(Lambda(Seq(ValDef(id)), post)) =>
@@ -38,6 +45,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
Some(InOutExample(fd.params.map(p => t(p.id)), Seq(t(id))))
} else if ((ids & insIds) == insIds) {
Some(InExample(fd.params.map(p => t(p.id))))
+ } else if((ids & outsIds) == outsIds) { // Examples provided on a part of the inputs.
+ Some(InOutExample(fd.params.map(p => t.getOrElse(p.id, Variable(p.id))), Seq(t(id))))
} else {
None
}
@@ -64,27 +73,31 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case None =>
ExamplesBank(Nil, Nil)
}
-
- // Extract examples from the passes found in expression
+
+ /** Extract examples from the passes found in expression */
def extractFromProblem(p: Problem): ExamplesBank = {
val testClusters = extractTestsOf(and(p.pc, p.phi))
// Finally, we keep complete tests covering all as++xs
val allIds = (p.as ++ p.xs).toSet
val insIds = p.as.toSet
-
+ val outsIds = p.xs.toSet
+
val examples = testClusters.toSeq.flatMap { t =>
val ids = t.keySet
if ((ids & allIds) == allIds) {
Some(InOutExample(p.as.map(t), p.xs.map(t)))
} else if ((ids & insIds) == insIds) {
Some(InExample(p.as.map(t)))
+ } else if((ids & outsIds) == outsIds) { // Examples provided on a part of the inputs.
+ Some(InOutExample(p.as.map(p => t.getOrElse(p, Variable(p))), p.xs.map(t)))
} else {
None
}
}
def isValidExample(ex: Example): Boolean = {
+ if(this.keepAbstractExamples) return true // TODO: Abstract interpretation here ?
val (mapping, cond) = ex match {
case io: InOutExample =>
(Map((p.as zip io.ins) ++ (p.xs zip io.outs): _*), And(p.pc, p.phi))
@@ -114,6 +127,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
ExamplesBank(generatedExamples.toSeq ++ solverExamples.toList, Nil)
}
+ /** Extracts all passes constructs from the given postcondition, merges them if needed */
private def extractTestsOf(e: Expr): Set[Map[Identifier, Expr]] = {
val allTests = collect[Map[Identifier, Expr]] {
case Passes(ins, outs, cases) =>
@@ -130,14 +144,15 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case _ => test
}
}
-
- // Check whether we can extract all ids from example
- val results = exs.collect { case e if infos.forall(_._2.isDefinedAt(e)) =>
- infos.map{ case (id, f) => id -> f(e) }.toMap
+ try {
+ // Check whether we can extract all ids from example
+ val results = exs.collect { case e if this.keepAbstractExamples || infos.forall(_._2.isDefinedAt(e)) =>
+ infos.map{ case (id, f) => id -> f(e) }.toMap
+ }
+ results.toSet
+ } catch {
+ case e: IDExtractionException => Set()
}
-
- results.toSet
-
case _ =>
Set()
}(e)
@@ -146,7 +161,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
consolidateTests(allTests)
}
-
+ /** Processes ((in, out) passes {
+ * cs[=>Case pattExpr if guard => outR]*/
private def caseToExamples(in: Expr, out: Expr, cs: MatchCase, examplesPerCase: Int = 5): Seq[(Expr,Expr)] = {
def doSubstitute(subs : Seq[(Identifier, Expr)], e : Expr) =
@@ -180,16 +196,26 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
// If the input contains free variables, it does not provide concrete examples.
// We will instantiate them according to a simple grammar to get them.
+ if(this.keepAbstractExamples) {
+ cs.optGuard match {
+ case Some(BooleanLiteral(false)) =>
+ Seq()
+ case None =>
+ Seq((pattExpr, cs.rhs))
+ case Some(pred) =>
+ Seq((Require(pred, pattExpr), cs.rhs))
+ }
+ } else {
+ val dataGen = new GrammarDataGen(evaluator)
- val dataGen = new GrammarDataGen(evaluator)
-
- val theGuard = replace(Map(in -> pattExpr), cs.optGuard.getOrElse(BooleanLiteral(true)))
+ val theGuard = replace(Map(in -> pattExpr), cs.optGuard.getOrElse(BooleanLiteral(true)))
- dataGen.generateFor(freeVars, theGuard, examplesPerCase, 1000).toSeq map { vals =>
- val inst = freeVars.zip(vals).toMap
- val inR = replaceFromIDs(inst, pattExpr)
- val outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
- (inR, outR)
+ dataGen.generateFor(freeVars, theGuard, examplesPerCase, 1000).toSeq map { vals =>
+ val inst = freeVars.zip(vals).toMap
+ val inR = replaceFromIDs(inst, pattExpr)
+ val outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
+ (inR, outR)
+ }
}
}
}
@@ -232,6 +258,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
}
consolidated
}
+
+ case class IDExtractionException(msg: String) extends Exception(msg)
/** Extract ids in ins/outs args, and compute corresponding extractors for values map
*
@@ -251,13 +279,13 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case Tuple(vs) =>
vs.map(extractIds).zipWithIndex.flatMap{ case (ids, i) =>
ids.map{ case (id, e) =>
- (id, andThen({ case Tuple(vs) => vs(i) }, e))
+ (id, andThen({ case Tuple(vs) => vs(i) case e => throw new IDExtractionException("Expected Tuple, got " + e) }, e))
}
}
case CaseClass(cct, args) =>
args.map(extractIds).zipWithIndex.flatMap { case (ids, i) =>
ids.map{ case (id, e) =>
- (id, andThen({ case CaseClass(cct2, vs) if cct2 == cct => vs(i) } ,e))
+ (id, andThen({ case CaseClass(cct2, vs) if cct2 == cct => vs(i) case e => throw new IDExtractionException("Expected Case class of type " + cct + ", got " + e) } ,e))
}
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index dfe90d2f775e8ed3736020cb1e827c75fe602ad9..affa41df46292ae73a6b9a87150283ec8c0ee997 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -31,7 +31,8 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
}
def toExpr = {
- letDef(defs.toList, guardedTerm)
+ if(defs.isEmpty) guardedTerm else
+ LetDef(defs.toList, guardedTerm)
}
// Projects a solution (ignore several output variables)
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 6ce5f020ae88c649458b857afca76b207b68916f..9303b4d1ef9813a38109b35c17adadf546297252 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -3,17 +3,46 @@ package leon
package synthesis
package disambiguation
+import purescala.Types.FunctionType
import purescala.Common.FreshIdentifier
import purescala.Constructors.{ and, tupleWrap }
import purescala.Definitions.{ FunDef, Program, ValDef }
-import purescala.ExprOps.expressionToPattern
+import purescala.ExprOps
import purescala.Extractors.TopLevelAnds
import purescala.Expressions._
/**
* @author Mikael
*/
+object ExamplesAdder {
+ def replaceGenericValuesByVariable(e: Expr): (Expr, Map[Expr, Expr]) = {
+ var assignment = Map[Expr, Expr]()
+ var extension = 'a'
+ var id = ""
+ (ExprOps.postMap({ expr => expr match {
+ case g@GenericValue(tpe, index) =>
+ val newIdentifier = FreshIdentifier(tpe.id.name.take(1).toLowerCase() + tpe.id.name.drop(1) + extension + id, tpe.id.getType)
+ if(extension != 'z' && extension != 'Z')
+ extension = (extension.toInt + 1).toChar
+ else if(extension == 'z') // No more than 52 generic variables in practice?
+ extension = 'A'
+ else {
+ if(id == "") id = "1" else id = (id.toInt + 1).toString
+ }
+
+ val newVar = Variable(newIdentifier)
+ assignment += g -> newVar
+ Some(newVar)
+ case _ => None
+ } })(e), assignment)
+ }
+}
+
class ExamplesAdder(ctx0: LeonContext, program: Program) {
+ import ExamplesAdder._
+ var _removeFunctionParameters = false
+
+ def setRemoveFunctionParameters(b: Boolean) = { _removeFunctionParameters = b; this }
/** Accepts the nth alternative of a question (0 being the current one) */
def acceptQuestion[T <: Expr](fd: FunDef, q: Question[T], alternativeIndex: Int): Unit = {
@@ -24,7 +53,8 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
/** Adds the given input/output examples to the function definitions */
def addToFunDef(fd: FunDef, examples: Seq[(Expr, Expr)]) = {
- val inputVariables = tupleWrap(fd.params.map(p => Variable(p.id): Expr))
+ val params = if(_removeFunctionParameters) fd.params.filter(x => !x.getType.isInstanceOf[FunctionType]) else fd.params
+ val inputVariables = tupleWrap(params.map(p => Variable(p.id): Expr))
val newCases = examples.map{ case (in, out) => exampleToCase(in, out) }
fd.postcondition match {
case Some(Lambda(Seq(ValDef(id)), post)) =>
@@ -65,12 +95,12 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
}
private def exampleToCase(in: Expr, out: Expr): MatchCase = {
- val (inPattern, inGuard) = expressionToPattern(in)
- if(inGuard != BooleanLiteral(true)) {
+ val (inPattern, inGuard) = ExprOps.expressionToPattern(in)
+ if(inGuard == BooleanLiteral(true)) {
+ MatchCase(inPattern, None, out)
+ } else /*if (in == in_raw) { } *else*/ {
val id = FreshIdentifier("out", in.getType, true)
MatchCase(WildcardPattern(Some(id)), Some(Equals(Variable(id), in)), out)
- } else {
- MatchCase(inPattern, None, out)
}
}
}
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index d77c06c97de2808e38ab4c0e218fb614a99d8298..81f98f86432dc54ffb446f473fee3a1afcf358ca 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -13,6 +13,8 @@ import purescala.DefOps
import grammars._
import solvers.ModelBuilder
import scala.collection.mutable.ListBuffer
+import evaluators.AbstractEvaluator
+import scala.annotation.tailrec
object QuestionBuilder {
/** Sort methods for questions. You can build your own */
@@ -124,11 +126,48 @@ class QuestionBuilder[T <: Expr](
private def run(s: Solution, elems: Seq[(Identifier, Expr)]): Option[Expr] = {
val newProgram = DefOps.addFunDefs(p, s.defs, p.definedFunctions.head)
- val e = new DefaultEvaluator(c, newProgram)
+ val e = new AbstractEvaluator(c, newProgram)
val model = new ModelBuilder
model ++= elems
val modelResult = model.result()
- e.eval(s.term, modelResult).result
+ for{x <- e.eval(s.term, modelResult).result
+ res = x._1
+ simp = ExprOps.simplifyArithmetic(res)}
+ yield simp
+ }
+
+ /** Make all generic values unique.
+ * Duplicate generic values are not suitable for disambiguating questions since they remove an order. */
+ def makeGenericValuesUnique(a: Expr): Expr = {
+ var genVals = Set[Expr with Terminal]()
+ def freshenValue(g: Expr with Terminal): Option[Expr with Terminal] = g match {
+ case g: GenericValue => Some(GenericValue(g.tp, g.id + 1))
+ case StringLiteral(s) =>
+ val i = s.lastIndexWhere { c => c < '0' || c > '9' }
+ val prefix = s.take(i+1)
+ val suffix = s.drop(i+1)
+ Some(StringLiteral(prefix + (if(suffix == "") "0" else (suffix.toInt + 1).toString)))
+ case InfiniteIntegerLiteral(i) => Some(InfiniteIntegerLiteral(i+1))
+ case IntLiteral(i) => if(i == Integer.MAX_VALUE) None else Some(IntLiteral(i+1))
+ case CharLiteral(c) => if(c == Char.MaxValue) None else Some(CharLiteral((c+1).toChar))
+ case otherLiteral => None
+ }
+ @tailrec @inline def freshValue(g: Expr with Terminal): Expr with Terminal = {
+ if(genVals contains g)
+ freshenValue(g) match {
+ case None => g
+ case Some(v) => freshValue(v)
+ }
+ else {
+ genVals += g
+ g
+ }
+ }
+ ExprOps.postMap{ e => e match {
+ case g:Expr with Terminal =>
+ Some(freshValue(g))
+ case _ => None
+ }}(a)
}
/** Returns a list of input/output questions to ask to the user. */
@@ -136,7 +175,10 @@ class QuestionBuilder[T <: Expr](
if(solutions.isEmpty) return Nil
val datagen = new GrammarDataGen(new DefaultEvaluator(c, p), value_enumerator)
- val enumerated_inputs = datagen.generateMapping(input, BooleanLiteral(true), expressionsToTake, expressionsToTake).toList
+ val enumerated_inputs = datagen.generateMapping(input, BooleanLiteral(true), expressionsToTake, expressionsToTake)
+ .map(inputs =>
+ inputs.map(id_expr =>
+ (id_expr._1, makeGenericValuesUnique(id_expr._2)))).toList
val solution = solutions.head
val alternatives = solutions.drop(1).take(solutionsToTake).toList
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 7b72da5396b179a82d4f8111335b8c82b11c76c8..62878dd31761050b839f794beb066bceca051a56 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -6,23 +6,27 @@ package rules
import scala.annotation.tailrec
import scala.collection.mutable.ListBuffer
-
+import bonsai.enumerators.MemoizedEnumerator
+import evaluators.DefaultEvaluator
+import evaluators.AbstractEvaluator
+import purescala.Definitions.{FunDef, ValDef, Program, TypedFunDef, CaseClassDef, AbstractClassDef}
import purescala.Common._
import purescala.Types._
import purescala.Constructors._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.Extractors._
import purescala.TypeOps
import purescala.DefOps
import purescala.ExprOps
-
-import evaluators.StringTracingEvaluator
+import purescala.SelfPrettyPrinter
+import solvers.Model
+import solvers.ModelBuilder
+import solvers.string.StringSolver
import synthesis.programsets.DirectProgramSet
import synthesis.programsets.JoinProgramSet
+import leon.utils.DebugSectionSynthesis
+
-import solvers.ModelBuilder
-import solvers.string.StringSolver
/** A template generator for a given type tree.
@@ -67,60 +71,84 @@ case object StringRender extends Rule("StringRender") {
var EDIT_ME = "_edit_me_"
- var _defaultTypeToString: Option[Map[TypeTree, FunDef]] = None
-
- def defaultMapTypeToString()(implicit hctx: SearchContext): Map[TypeTree, FunDef] = {
- _defaultTypeToString.getOrElse{
- // Updates the cache with the functions converting standard types to string.
- val res = (hctx.program.library.StrOps.toSeq.flatMap { StrOps =>
- StrOps.defs.collect{ case d: FunDef if d.params.length == 1 && d.returnType == StringType => d.params.head.getType -> d }
- }).toMap
- _defaultTypeToString = Some(res)
- res
- }
- }
-
- /** Returns a toString function converter if it has been defined. */
- class WithFunDefConverter(implicit hctx: SearchContext) {
- def unapply(tpe: TypeTree): Option[FunDef] = {
- _defaultTypeToString.flatMap(_.get(tpe))
- }
- }
+ var enforceDefaultStringMethodsIfAvailable = true
+ var enforceSelfStringMethodsIfAvailable = false
val booleanTemplate = (a: Expr) => StringTemplateGenerator(Hole => IfExpr(a, Hole, Hole))
- /** Returns a seq of expressions such as `x + y + "1" + y + "2" + z` associated to an expected result string `"1, 2"`.
- * We use these equations so that we can find the values of the constants x, y, z and so on.
- * This uses a custom evaluator which does not concatenate string but reminds the calculation.
- */
- def createProblems(inlineFunc: Seq[FunDef], inlineExpr: Expr, examples: ExamplesBank): Seq[(Expr, String)] = ???
+ import StringSolver.{StringFormToken, StringForm, Problem => SProblem, Equation, Assignment}
- /** For each solution to the problem such as `x + "1" + y + j + "2" + z = 1, 2`, outputs all possible assignments if they exist. */
- def solveProblems(problems: Seq[(Expr, String)]): Seq[Map[Identifier, String]] = ???
+ /** Augment the left-hand-side to have possible function calls, such as x + "const" + customToString(_) ...
+ * Function calls will be eliminated when converting to a valid problem.
+ */
+ sealed abstract class AugmentedStringFormToken
+ case class RegularStringFormToken(e: StringFormToken) extends AugmentedStringFormToken
+ case class OtherStringFormToken(e: Expr) extends AugmentedStringFormToken
+ type AugmentedStringForm = List[AugmentedStringFormToken]
- import StringSolver.{StringFormToken, StringForm, Problem => SProblem, Equation, Assignment}
+ /** Augments the right-hand-side to have possible function calls, such as "const" + customToString(_) ...
+ * Function calls will be eliminated when converting to a valid problem.
+ */
+ sealed abstract class AugmentedStringChunkRHS
+ case class RegularStringChunk(e: String) extends AugmentedStringChunkRHS
+ case class OtherStringChunk(e: Expr) extends AugmentedStringChunkRHS
+ type AugmentedStringLiteral = List[AugmentedStringChunkRHS]
/** Converts an expression to a stringForm, suitable for StringSolver */
- def toStringForm(e: Expr, acc: List[StringFormToken] = Nil)(implicit hctx: SearchContext): Option[StringForm] = e match {
+ def toStringForm(e: Expr, acc: List[AugmentedStringFormToken] = Nil)(implicit hctx: SearchContext): Option[AugmentedStringForm] = e match {
case StringLiteral(s) =>
- Some(Left(s)::acc)
- case Variable(id) => Some(Right(id)::acc)
+ Some(RegularStringFormToken(Left(s))::acc)
+ case Variable(id) => Some(RegularStringFormToken(Right(id))::acc)
case StringConcat(lhs, rhs) =>
toStringForm(rhs, acc).flatMap(toStringForm(lhs, _))
+ case e:Application => Some(OtherStringFormToken(e)::acc)
+ case e:FunctionInvocation => Some(OtherStringFormToken(e)::acc)
case _ => None
}
/** Returns the string associated to the expression if it is computable */
- def toStringLiteral(e: Expr): Option[String] = e match {
- case StringLiteral(s) => Some(s)
- case StringConcat(lhs, rhs) => toStringLiteral(lhs).flatMap(k => toStringLiteral(rhs).map(l => k + l))
+ def toStringLiteral(e: Expr): Option[AugmentedStringLiteral] = e match {
+ case StringLiteral(s) => Some(List(RegularStringChunk(s)))
+ case StringConcat(lhs, rhs) =>
+ toStringLiteral(lhs).flatMap(k => toStringLiteral(rhs).map(l => (k.init, k.last, l) match {
+ case (kinit, RegularStringChunk(s), RegularStringChunk(sp)::ltail) =>
+ kinit ++ (RegularStringChunk(s + sp)::ltail)
+ case _ => k ++ l
+ }))
+ case e: Application => Some(List(OtherStringChunk(e)))
+ case e: FunctionInvocation => Some(List(OtherStringChunk(e)))
case _ => None
}
+ /** Converts an equality AugmentedStringForm == AugmentedStringLiteral to a list of equations
+ * For that, splits both strings on function applications. If they yield the same value, we can split, else it fails. */
+ def toEquations(lhs: AugmentedStringForm, rhs: AugmentedStringLiteral): Option[List[Equation]] = {
+ def rec(lhs: AugmentedStringForm, rhs: AugmentedStringLiteral,
+ accEqs: ListBuffer[Equation], accLeft: ListBuffer[StringFormToken], accRight: StringBuffer): Option[List[Equation]] = (lhs, rhs) match {
+ case (Nil, Nil) =>
+ (accLeft.toList, accRight.toString) match {
+ case (Nil, "") => Some(accEqs.toList)
+ case (lhs, rhs) => Some((accEqs += ((lhs, rhs))).toList)
+ }
+ case (OtherStringFormToken(e)::lhstail, OtherStringChunk(f)::rhstail) =>
+ if(ExprOps.canBeHomomorphic(e, f).nonEmpty) {
+ rec(lhstail, rhstail, accEqs += ((accLeft.toList, accRight.toString)), ListBuffer[StringFormToken](), new StringBuffer)
+ } else None
+ case (OtherStringFormToken(e)::lhstail, Nil) =>
+ None
+ case (Nil, OtherStringChunk(f)::rhstail) =>
+ None
+ case (lhs, RegularStringChunk(s)::rhstail) =>
+ rec(lhs, rhstail, accEqs, accLeft, accRight append s)
+ case (RegularStringFormToken(e)::lhstail, rhs) =>
+ rec(lhstail, rhs, accEqs, accLeft += e, accRight)
+ }
+ rec(lhs, rhs, ListBuffer[Equation](), ListBuffer[StringFormToken](), new StringBuffer)
+ }
+
/** Returns a stream of assignments compatible with input/output examples for the given template */
def findAssignments(p: Program, inputs: Seq[Identifier], examples: ExamplesBank, template: Expr)(implicit hctx: SearchContext): Stream[Map[Identifier, String]] = {
- //new Evaluator()
- val e = new StringTracingEvaluator(hctx.context, p)
+ val e = new AbstractEvaluator(hctx.context, p)
@tailrec def gatherEquations(s: List[InOutExample], acc: ListBuffer[Equation] = ListBuffer()): Option[SProblem] = s match {
case Nil => Some(acc.toList)
@@ -132,34 +160,39 @@ case object StringRender extends Rule("StringRender") {
val evalResult = e.eval(template, modelResult)
evalResult.result match {
case None =>
- hctx.reporter.debug("Eval = None : ["+template+"] in ["+inputs.zip(in)+"]")
+ hctx.reporter.info("Eval = None : ["+template+"] in ["+inputs.zip(in)+"]")
+ hctx.reporter.info(evalResult)
None
case Some((sfExpr, abstractSfExpr)) =>
//ctx.reporter.debug("Eval = ["+sfExpr+"] (from "+abstractSfExpr+")")
val sf = toStringForm(sfExpr)
val rhs = toStringLiteral(rhExpr.head)
- if(sf.isEmpty || rhs.isEmpty) {
- hctx.reporter.ifDebug(printer => printer("sf empty or rhs empty ["+sfExpr+"] => ["+sf+"] in ["+rhs+"]"))
- None
- } else gatherEquations(q, acc += ((sf.get, rhs.get)))
+ (sf, rhs) match {
+ case (Some(sfget), Some(rhsget)) =>
+ toEquations(sfget, rhsget) match {
+ case Some(equations) =>
+ gatherEquations(q, acc ++= equations)
+ case None =>
+ hctx.reporter.info("Could not extract equations from ["+sfget+"] == ["+rhsget+"]\n coming from ... == " + rhExpr)
+ None
+ }
+ case _ =>
+ hctx.reporter.info("sf empty or rhs empty ["+sfExpr+"] => ["+sf+"] in ["+rhs+"]")
+ None
+ }
}
} else {
- hctx.reporter.ifDebug(printer => printer("RHS.length != 1 : ["+rhExpr+"]"))
+ hctx.reporter.info("RHS.length != 1 : ["+rhExpr+"]")
None
}
}
gatherEquations((examples.valids ++ examples.invalids).collect{ case io:InOutExample => io }.toList) match {
- case Some(problem) =>
- hctx.reporter.debug("Problem: ["+StringSolver.renderProblem(problem)+"]")
- val res = StringSolver.solve(problem)
- hctx.reporter.debug("Solution found:"+res.nonEmpty)
- res
- case None =>
- hctx.reporter.ifDebug(printer => printer("No problem found"))
- Stream.empty
+ case Some(problem) => StringSolver.solve(problem)
+ case None => Stream.empty
}
}
+ /** With a given (template, fundefs, consts) will find consts so that (expr, funs) passes all the examples */
def findSolutions(examples: ExamplesBank, template: Stream[WithIds[Expr]], funDefs: Seq[(FunDef, Stream[WithIds[Expr]])])(implicit hctx: SearchContext, p: Problem): RuleApplication = {
// Fun is a stream of many function applications.
val funs= JoinProgramSet.direct(funDefs.map(fbody => fbody._2.map((fbody._1, _))).map(d => DirectProgramSet(d)))
@@ -169,7 +202,7 @@ case object StringRender extends Rule("StringRender") {
def computeSolutions(funDefsBodies: Seq[(FunDef, WithIds[Expr])], template: WithIds[Expr]): Stream[Assignment] = {
val funDefs = for((funDef, body) <- funDefsBodies) yield { funDef.body = Some(body._1); funDef }
val newProgram = DefOps.addFunDefs(hctx.program, funDefs, hctx.sctx.functionContext)
- findAssignments(newProgram, p.as, examples, template._1)
+ findAssignments(newProgram, p.as.filter{ x => !x.getType.isInstanceOf[FunctionType] }, examples, template._1)
}
val tagged_solutions =
@@ -212,7 +245,7 @@ case object StringRender extends Rule("StringRender") {
var transformMap = Map[FunDef, FunDef]()
def mapExpr(body: Expr): Expr = {
ExprOps.preMap((e: Expr) => e match {
- case FunctionInvocation(TypedFunDef(fd, _), args) if fd != program.library.escape.get => Some(FunctionInvocation(getMapping(fd).typed, args))
+ case FunctionInvocation(TypedFunDef(fd, _), args) if fds(fd) => Some(FunctionInvocation(getMapping(fd).typed, args))
case e => None
})(body)
}
@@ -234,10 +267,6 @@ case object StringRender extends Rule("StringRender") {
case class DependentType(caseClassParent: Option[TypeTree], inputName: String, typeToConvert: TypeTree)
- object StringSynthesisContext {
- def empty(implicit hctx: SearchContext) = new StringSynthesisContext(None, new StringSynthesisResult(Map(), Set()))
- }
-
type MapFunctions = Map[DependentType, (FunDef, Stream[WithIds[Expr]])]
/** Result of the current synthesis process */
@@ -259,17 +288,39 @@ case object StringRender extends Rule("StringRender") {
s0
}
}
+ type StringConverters = Map[TypeTree, List[Expr => Expr]]
+
+ /** Companion object to create a StringSynthesisContext */
+ object StringSynthesisContext {
+ def empty(
+ abstractStringConverters: StringConverters,
+ originalInputs: Set[Expr],
+ provided_functions: Seq[Identifier])(implicit hctx: SearchContext) =
+ new StringSynthesisContext(None, new StringSynthesisResult(Map(), Set()),
+ abstractStringConverters,
+ originalInputs,
+ provided_functions)
+ }
/** Context for the current synthesis process */
class StringSynthesisContext(
val currentCaseClassParent: Option[TypeTree],
- val result: StringSynthesisResult
+ val result: StringSynthesisResult,
+ val abstractStringConverters: StringConverters,
+ val originalInputs: Set[Expr],
+ val provided_functions: Seq[Identifier]
)(implicit hctx: SearchContext) {
def add(d: DependentType, f: FunDef, s: Stream[WithIds[Expr]]): StringSynthesisContext = {
- new StringSynthesisContext(currentCaseClassParent, result.add(d, f, s))
+ new StringSynthesisContext(currentCaseClassParent, result.add(d, f, s),
+ abstractStringConverters,
+ originalInputs,
+ provided_functions)
}
def copy(currentCaseClassParent: Option[TypeTree]=currentCaseClassParent, result: StringSynthesisResult = result): StringSynthesisContext =
- new StringSynthesisContext(currentCaseClassParent, result)
+ new StringSynthesisContext(currentCaseClassParent, result,
+ abstractStringConverters,
+ originalInputs,
+ provided_functions)
def freshFunName(s: String) = result.freshFunName(s)
}
@@ -289,7 +340,8 @@ case object StringRender extends Rule("StringRender") {
val funName = funName3(0).toLower + funName3.substring(1)
val funId = FreshIdentifier(ctx.freshFunName(funName), alwaysShowUniqueID = true)
val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
- val fd = new FunDef(funId, Nil, ValDef(argId) :: Nil, StringType) // Empty function.
+ val tparams = hctx.sctx.functionContext.tparams
+ val fd = new FunDef(funId, tparams, ValDef(argId) :: ctx.provided_functions.map(ValDef(_)).toList, StringType) // Empty function.
fd
}
@@ -365,54 +417,89 @@ case object StringRender extends Rule("StringRender") {
val dependentType = DependentType(ctx.currentCaseClassParent, input.asString(hctx.program)(hctx.context), input.getType)
ctx.result.adtToString.get(dependentType) match {
case Some(fd) =>
- gatherInputs(ctx, q, result += Stream((functionInvocation(fd._1, Seq(input)), Nil)))
+ gatherInputs(ctx, q, result += Stream((functionInvocation(fd._1, input::ctx.provided_functions.toList.map(Variable)), Nil)))
case None => // No function can render the current type.
+ // We should not rely on calling the original function on the first line of the body of the function itself.
+ val exprs1s = (new SelfPrettyPrinter)
+ .allowFunction(hctx.sctx.functionContext)
+ .excludeFunction(hctx.sctx.functionContext)
+ .prettyPrintersForType(input.getType)(hctx.context, hctx.program)
+ .map(l => (application(l, Seq(input)), List[Identifier]())) // Use already pre-defined pretty printers.
+ val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(fd, _)), _) if fd == hctx.sctx.functionContext => 0 case _ => 1}
+ val exprs2 = ctx.abstractStringConverters.getOrElse(input.getType, Nil).map(f => (f(input), List[Identifier]()))
+ val defaultConverters: Stream[WithIds[Expr]] = exprs1.toStream #::: exprs2.toStream
+ val recursiveConverters: Stream[WithIds[Expr]] =
+ (new SelfPrettyPrinter)
+ .prettyPrinterFromCandidate(hctx.sctx.functionContext, input.getType)(hctx.context, hctx.program)
+ .map(l => (application(l, Seq(input)), List[Identifier]()))
+
+ def mergeResults(templateConverters: =>Stream[WithIds[Expr]]): Stream[WithIds[Expr]] = {
+ if(defaultConverters.isEmpty) templateConverters
+ else if(enforceDefaultStringMethodsIfAvailable) {
+ if(enforceSelfStringMethodsIfAvailable)
+ recursiveConverters #::: defaultConverters
+ else {
+ defaultConverters #::: recursiveConverters
+ }
+ }
+ else recursiveConverters #::: defaultConverters #::: templateConverters
+ }
+
input.getType match {
case StringType =>
gatherInputs(ctx, q, result +=
- (Stream((input, Nil),
- (FunctionInvocation(
- hctx.program.library.escape.get.typed,
- Seq(input)): Expr, Nil))))
+ mergeResults(Stream((input, Nil),
+ (functionInvocation(
+ hctx.program.library.escape.get, List(input)): Expr, Nil))))
case BooleanType =>
val (bTemplate, vs) = booleanTemplate(input).instantiateWithVars
- gatherInputs(ctx, q, result += Stream((BooleanToString(input), Nil), (bTemplate, vs)))
+ gatherInputs(ctx, q, result += mergeResults(Stream((BooleanToString(input), Nil), (bTemplate, vs))))
case WithStringconverter(converter) => // Base case
- gatherInputs(ctx, q, result += Stream((converter(input), Nil)))
+ gatherInputs(ctx, q, result += mergeResults(Stream((converter(input), Nil))))
case t: ClassType =>
- // Create the empty function body and updates the assignments parts.
- val fd = createEmptyFunDef(ctx, dependentType)
- val ctx2 = preUpdateFunDefBody(dependentType, fd, ctx) // Inserts the FunDef in the assignments so that it can already be used.
- t.root match {
- case act@AbstractClassType(acd@AbstractClassDef(id, tparams, parent), tps) =>
- // Create a complete FunDef body with pattern matching
-
- val allKnownDescendantsAreCCAndHaveZeroArgs = act.knownCCDescendants.forall { x => x match {
- case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) => ccd.fields.isEmpty
- case _ => false
- }}
-
- //TODO: Test other templates not only with Wilcard patterns, but more cases options for non-recursive classes (e.g. Option, Boolean, Finite parameterless case classes.)
- val (ctx3, cases) = ((ctx2, ListBuffer[Stream[WithIds[MatchCase]]]()) /: act.knownCCDescendants) {
- case ((ctx22, acc), cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
- val (newCases, result) = extractCaseVariants(cct, ctx22)
- val ctx23 = ctx22.copy(result = result)
- (ctx23, acc += newCases)
- case ((adtToString, acc), e) => hctx.reporter.fatalError("Could not handle this class definition for string rendering " + e)
- }
-
- val allMatchExprsEnd = JoinProgramSet(cases.map(DirectProgramSet(_)), mergeMatchCases(fd)).programs // General pattern match expressions
- val allMatchExprs = if(allKnownDescendantsAreCCAndHaveZeroArgs) {
- Stream(constantPatternMatching(fd, act)) ++ allMatchExprsEnd
- } else allMatchExprsEnd
- gatherInputs(ctx3.add(dependentType, fd, allMatchExprs), q, result += Stream((functionInvocation(fd, Seq(input)), Nil)))
- case cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
- val (newCases, result3) = extractCaseVariants(cct, ctx2)
- val allMatchExprs = newCases.map(acase => mergeMatchCases(fd)(Seq(acase)))
- gatherInputs(ctx2.copy(result = result3).add(dependentType, fd, allMatchExprs), q, result += Stream((functionInvocation(fd, Seq(input)), Nil)))
+ if(enforceDefaultStringMethodsIfAvailable && !defaultConverters.isEmpty) {
+ gatherInputs(ctx, q, result += defaultConverters)
+ } else {
+ // Create the empty function body and updates the assignments parts.
+ val fd = createEmptyFunDef(ctx, dependentType)
+ val ctx2 = preUpdateFunDefBody(dependentType, fd, ctx) // Inserts the FunDef in the assignments so that it can already be used.
+ t.root match {
+ case act@AbstractClassType(acd@AbstractClassDef(id, tparams, parent), tps) =>
+ // Create a complete FunDef body with pattern matching
+
+ val allKnownDescendantsAreCCAndHaveZeroArgs = act.knownCCDescendants.forall { x => x match {
+ case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) => ccd.fields.isEmpty
+ case _ => false
+ }}
+
+ //TODO: Test other templates not only with Wilcard patterns, but more cases options for non-recursive classes (e.g. Option, Boolean, Finite parameterless case classes.)
+ val (ctx3, cases) = ((ctx2, ListBuffer[Stream[WithIds[MatchCase]]]()) /: act.knownCCDescendants) {
+ case ((ctx22, acc), cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
+ val (newCases, result) = extractCaseVariants(cct, ctx22)
+ val ctx23 = ctx22.copy(result = result)
+ (ctx23, acc += newCases)
+ case ((adtToString, acc), e) => hctx.reporter.fatalError("Could not handle this class definition for string rendering " + e)
+ }
+
+ val allMatchExprsEnd = JoinProgramSet(cases.map(DirectProgramSet(_)), mergeMatchCases(fd)).programs // General pattern match expressions
+ val allMatchExprs = if(allKnownDescendantsAreCCAndHaveZeroArgs) {
+ Stream(constantPatternMatching(fd, act)) ++ allMatchExprsEnd
+ } else allMatchExprsEnd
+ gatherInputs(ctx3.add(dependentType, fd, allMatchExprs), q,
+ result += Stream((functionInvocation(fd, input::ctx.provided_functions.toList.map(Variable)), Nil)))
+ case cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
+ val (newCases, result3) = extractCaseVariants(cct, ctx2)
+ val allMatchExprs = newCases.map(acase => mergeMatchCases(fd)(Seq(acase)))
+ gatherInputs(ctx2.copy(result = result3).add(dependentType, fd, allMatchExprs), q,
+ result += Stream((functionInvocation(fd, input::ctx.provided_functions.toList.map(Variable)), Nil)))
+ }
}
case TypeParameter(t) =>
- hctx.reporter.fatalError("Could not handle type parameter for string rendering " + t)
+ if(defaultConverters.isEmpty) {
+ hctx.reporter.fatalError("Could not handle type parameter for string rendering " + t)
+ } else {
+ gatherInputs(ctx, q, result += mergeResults(Stream.empty))
+ }
case tpe =>
hctx.reporter.fatalError("Could not handle class type for string rendering " + tpe)
}
@@ -448,7 +535,7 @@ case object StringRender extends Rule("StringRender") {
}
template
}
- (templates.flatten, ctx2.result) // TODO: Flatten or interleave?
+ (templates.flatten, ctx2.result)
}
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -456,15 +543,32 @@ case object StringRender extends Rule("StringRender") {
p.xs match {
case List(IsTyped(v, StringType)) =>
val description = "Creates a standard string conversion function"
-
- val defaultToStringFunctions = defaultMapTypeToString()
-
+
val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
+ .setKeepAbstractExamples(true)
+ .setEvaluationFailOnChoose(true)
val examples = examplesFinder.extractFromProblem(p)
+ val abstractStringConverters: StringConverters =
+ (p.as.flatMap { case x => x.getType match {
+ case FunctionType(Seq(aType), StringType) => List((aType, (arg: Expr) => application(Variable(x), Seq(arg))))
+ case _ => Nil
+ }}).groupBy(_._1).mapValues(_.map(_._2))
+
+ val (inputVariables, functionVariables) = p.as.partition ( x => x.getType match {
+ case f: FunctionType => false
+ case _ => true
+ })
+
val ruleInstantiations = ListBuffer[RuleInstantiation]()
+ val originalInputs = inputVariables.map(Variable)
ruleInstantiations += RuleInstantiation("String conversion") {
- val (expr, synthesisResult) = createFunDefsTemplates(StringSynthesisContext.empty, p.as.map(Variable))
+ val (expr, synthesisResult) = createFunDefsTemplates(
+ StringSynthesisContext.empty(
+ abstractStringConverters,
+ originalInputs.toSet,
+ functionVariables
+ ), originalInputs)
val funDefs = synthesisResult.adtToString
/*val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index e23c6fe92317ae92e9177dd4feb56c77a9a6bb64..36f442f2322e78248d2d454956fa46ddedb28037 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -7,7 +7,6 @@ import leon.purescala.Definitions._
import leon.purescala.Types._
import leon.purescala.PrettyPrinter
import leon.utils.Positioned
-import leon.evaluators.StringTracingEvaluator
import leon.solvers._
import leon.LeonContext
import leon.purescala.SelfPrettyPrinter
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index d695f4ca0877382eeb83838a3cf08267ee935cb6..bb28f259db42657e3365922fdcdad64442ecc1ba 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -3,7 +3,6 @@
package leon
package verification
-import evaluators.StringTracingEvaluator
import utils.DebugSectionSynthesis
import utils.DebugSectionVerification
import leon.purescala
diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
index 17260f7e5263cce8e61e57f5e8b684d1a736232f..fe548c1b013e3cbef8e5a7024286c1e9e8781e0f 100644
--- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
@@ -7,6 +7,7 @@ import leon.test._
import leon.purescala.Constructors._
import leon.purescala.Expressions._
import leon.purescala.ExprOps._
+import leon.purescala.Definitions._
import leon.purescala.Common._
class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
@@ -101,5 +102,35 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
assert(isSubtypeOf(simplestValue(act).getType, act))
assert(simplestValue(cct).getType == cct)
}
+
+ test("canBeHomomorphic") { implicit fix =>
+ import leon.purescala.ExprOps.canBeHomomorphic
+ import leon.purescala.Types._
+ import leon.purescala.Definitions._
+ val d = FreshIdentifier("d", IntegerType)
+ val x = FreshIdentifier("x", IntegerType)
+ val y = FreshIdentifier("y", IntegerType)
+ assert(canBeHomomorphic(Variable(d), Variable(x)).isEmpty)
+ val l1 = Lambda(Seq(ValDef(x)), Variable(x))
+ val l2 = Lambda(Seq(ValDef(y)), Variable(y))
+ assert(canBeHomomorphic(l1, l2).nonEmpty)
+ val fType = FunctionType(Seq(IntegerType), IntegerType)
+ val f = FreshIdentifier("f",
+ FunctionType(Seq(IntegerType, fType, fType), IntegerType))
+ val farg1 = FreshIdentifier("arg1", IntegerType)
+ val farg2 = FreshIdentifier("arg2", fType)
+ val farg3 = FreshIdentifier("arg3", fType)
+
+ val fdef = new FunDef(f, Seq(), Seq(ValDef(farg1), ValDef(farg2), ValDef(farg3)), IntegerType)
+
+ // Captured variables should be silent, even if they share the same identifier in two places of the code.
+ assert(canBeHomomorphic(
+ FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l2)),
+ FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l1))).nonEmpty)
+
+ assert(canBeHomomorphic(
+ StringLiteral("1"),
+ StringLiteral("2")).isEmpty)
+ }
}
diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cd6bd2ee75a9594d2c0be081db265e75c7a45620
--- /dev/null
+++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
@@ -0,0 +1,431 @@
+package leon.integration.solvers
+
+
+import org.scalatest.FunSuite
+import org.scalatest.Matchers
+import leon.test.helpers.ExpressionsDSL
+import leon.solvers.string.StringSolver
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Common.Identifier
+import leon.purescala.Expressions._
+import leon.purescala.Definitions._
+import leon.purescala.DefOps
+import leon.purescala.ExprOps
+import leon.purescala.Types._
+import leon.purescala.TypeOps
+import leon.purescala.Constructors._
+import leon.synthesis.rules.{StringRender, TypedTemplateGenerator}
+import scala.collection.mutable.{HashMap => MMap}
+import scala.concurrent.Future
+import scala.concurrent.ExecutionContext.Implicits.global
+import org.scalatest.concurrent.Timeouts
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.time.SpanSugar._
+import org.scalatest.FunSuite
+import org.scalatest.concurrent.Timeouts
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.time.SpanSugar._
+import leon.purescala.Types.Int32Type
+import leon.test.LeonTestSuiteWithProgram
+import leon.synthesis.SourceInfo
+import leon.synthesis.CostModels
+import leon.synthesis.graph.SimpleSearch
+import leon.synthesis.graph.AndNode
+import leon.synthesis.SearchContext
+import leon.synthesis.Synthesizer
+import leon.synthesis.SynthesisSettings
+import leon.synthesis.RuleApplication
+import leon.synthesis.RuleClosed
+import leon.evaluators._
+import leon.LeonContext
+import leon.synthesis.rules.DetupleInput
+import leon.synthesis.Rules
+import leon.solvers.ModelBuilder
+import scala.language.implicitConversions
+
+class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures {
+ test("Template Generator simple"){ case (ctx: LeonContext, program: Program) =>
+ val TTG = new TypedTemplateGenerator(IntegerType) {}
+ val e = TTG(hole => Plus(hole, hole))
+ val (expr, vars) = e.instantiateWithVars
+ vars should have length 2
+ expr shouldEqual Plus(Variable(vars(0)), Variable(vars(1)))
+
+ val f = TTG.nested(hole => (Minus(hole, expr), vars))
+ val (expr2, vars2) = f.instantiateWithVars
+ vars2 should have length 3
+ vars2(0) shouldEqual vars(0)
+ vars2(1) shouldEqual vars(1)
+ expr2 shouldEqual Minus(Variable(vars2(2)), expr)
+ }
+
+ trait withSymbols {
+ val x = FreshIdentifier("x", StringType)
+ val y = FreshIdentifier("y", StringType)
+ val i = FreshIdentifier("i", IntegerType)
+ val f = FreshIdentifier("f", FunctionType(Seq(IntegerType), StringType))
+ val fd = new FunDef(f, Nil, Seq(ValDef(i)), StringType)
+ val fdi = FunctionInvocation(fd.typed, Seq(Variable(i)))
+ }
+
+ test("toEquations working"){ case (ctx: LeonContext, program: Program) =>
+ import StringRender._
+ new withSymbols {
+ val lhs = RegularStringFormToken(Left("abc"))::RegularStringFormToken(Right(x))::OtherStringFormToken(fdi)::Nil
+ val rhs = RegularStringChunk("abcdef")::OtherStringChunk(fdi)::Nil
+ val p = toEquations(lhs, rhs)
+ p should not be 'empty
+ p.get should have length 1
+ }
+ }
+
+ test("toEquations working 2"){ case (ctx: LeonContext, program: Program) =>
+ import StringRender._
+ new withSymbols {
+ val lhs = RegularStringFormToken(Left("abc"))::RegularStringFormToken(Right(x))::OtherStringFormToken(fdi)::RegularStringFormToken(Right(y))::Nil
+ val rhs = RegularStringChunk("abcdef")::OtherStringChunk(fdi)::RegularStringChunk("123")::Nil
+ val p = toEquations(lhs, rhs)
+ p should not be 'empty
+ p.get should have length 2
+ }
+ }
+
+ test("toEquations failing"){ case (ctx: LeonContext, program: Program) =>
+ import StringRender._
+ new withSymbols {
+ val lhs = RegularStringFormToken(Left("abc"))::RegularStringFormToken(Right(x))::RegularStringFormToken(Right(y))::Nil
+ val rhs = RegularStringChunk("abcdef")::OtherStringChunk(fdi)::RegularStringChunk("123")::Nil
+ val p = toEquations(lhs, rhs)
+ p should be ('empty)
+ }
+ }
+
+ def applyStringRenderOn(functionName: String): (FunDef, Program) = {
+ val ci = synthesisInfos(functionName)
+ val search = new SimpleSearch(ctx, ci, ci.problem, CostModels.default, Some(200))
+ val synth = new Synthesizer(ctx, program, ci, SynthesisSettings(rules = Seq(StringRender)))
+ val orNode = search.g.root
+ if (!orNode.isExpanded) {
+ val hctx = SearchContext(synth.sctx, synth.ci, orNode, search)
+ orNode.expand(hctx)
+ }
+ val andNodes = orNode.descendants.collect {
+ case n: AndNode =>
+ n
+ }
+
+ val rulesApps = (for ((t, i) <- andNodes.zipWithIndex) yield {
+ val status = if (t.isDeadEnd) {
+ "closed"
+ } else {
+ "open"
+ }
+ t.ri.asString -> i
+ }).toMap
+ rulesApps should contain key "String conversion"
+
+ val rid = rulesApps("String conversion")
+ val path = List(rid)
+
+ val solutions = (search.traversePath(path) match {
+ case Some(an: AndNode) =>
+ val hctx = SearchContext(synth.sctx, synth.ci, an, search)
+ an.ri.apply(hctx)
+ case _ => throw new Exception("Was not an and node")
+ }) match {
+ case RuleClosed(solutions) => solutions
+ case _ => fail("no solution found")
+ }
+ solutions should not be 'empty
+ val newProgram = DefOps.addFunDefs(synth.program, solutions.head.defs, synth.sctx.functionContext)
+ val newFd = ci.fd.duplicate()
+ newFd.body = Some(solutions.head.term)
+ val (newProgram2, _) = DefOps.replaceFunDefs(newProgram)({ fd =>
+ if(fd == ci.fd) {
+ Some(newFd)
+ } else None
+ }, { (fi: FunctionInvocation, fd: FunDef) =>
+ Some(FunctionInvocation(fd.typed, fi.args))
+ })
+ (newFd, newProgram2)
+ }
+
+ def getFunctionArguments(functionName: String) = {
+ program.lookupFunDef("StringRenderSuite." + functionName) match {
+ case Some(fd) => fd.params
+ case None =>
+ fail("Could not find function " + functionName + " in sources. Other functions:" + program.definedFunctions.map(_.id.name).sorted)
+ }
+ }
+
+ implicit class StringUtils(s: String) {
+ def replaceByExample: String =
+ s.replaceAll("\\((\\w+):(.*) by example", "\\($1:$2 ensuring { (res: String) => ($1, res) passes { case _ if false => \"\" } }")
+ }
+
+ val sources = List("""
+ |import leon.lang._
+ |import leon.collection._
+ |import leon.lang.synthesis._
+ |import leon.annotation._
+ |
+ |object StringRenderSuite {
+ | def literalSynthesis(i: Int): String = ??? ensuring { (res: String) => (i, res) passes { case 42 => ":42." } }
+ |
+ | def booleanSynthesis(b: Boolean): String = ??? ensuring { (res: String) => (b, res) passes { case true => "yes" case false => "no" } }
+ | def booleanSynthesis2(b: Boolean): String = ??? ensuring { (res: String) => (b, res) passes { case true => "B: true" } }
+ | //def stringEscape(s: String): String = ??? ensuring { (res: String) => (s, res) passes { case "\n" => "done...\\n" } }
+ |
+ | case class Dummy(s: String)
+ | def dummyToString(d: Dummy): String = "{" + d.s + "}"
+ |
+ | case class Dummy2(s: String)
+ | def dummy2ToString(d: Dummy2): String = "<" + d.s + ">"
+ |
+ | case class Config(i: BigInt, t: (Int, String))
+ |
+ | def configToString(c: Config): String = ??? ensuring { (res: String) => (c, res) passes { case Config(BigInt(1), (2, "3")) => "1: 2 -> 3" } }
+ | def configToString2(c: Config): String = ??? ensuring { (res: String) => (c, res) passes { case Config(BigInt(1), (2, "3")) => "3: 1 -> 2" } }
+ |
+ | sealed abstract class Tree
+ | case class Knot(left: Tree, right: Tree) extends Tree
+ | case class Bud(v: String) extends Tree
+ |
+ | def treeToString(t: Tree): String = ???[String] ensuring {
+ | (res : String) => (t, res) passes {
+ | case Knot(Knot(Bud("17"), Bud("14")), Bud("23")) =>
+ | "<<17Y14>Y23>"
+ | case Bud("foo") =>
+ | "foo"
+ | case Knot(Bud("foo"), Bud("foo")) =>
+ | "<fooYfoo>"
+ | case Knot(Bud("foo"), Knot(Bud("bar"), Bud("foo"))) =>
+ | "<fooY<barYfoo>>"
+ | }
+ | }
+ |
+ | sealed abstract class BList[T]
+ | case class BCons[T](head: (T, T), tail: BList[T]) extends BList[T]
+ | case class BNil[T]() extends BList[T]
+ |
+ | def bListToString[T](b: BList[T], f: T => String) = ???[String] ensuring
+ | { (res: String) => (b, res) passes { case BNil() => "[]" case BCons(a, BCons(b, BCons(c, BNil()))) => "[" + f(a._1) + "-" + f(a._2) + ", " + f(b._1) + "-" + f(b._2) + ", " + f(c._1) + "-" + f(c._2) + "]" }}
+ |
+ | // Handling one rendering function at a time.
+ | case class BConfig(flags: BList[Dummy])
+ | def bConfigToString(b: BConfig): String = ???[String] ensuring
+ | { (res: String) => (b, res) passes { case BConfig(BNil()) => "Config" + bListToString[Dummy](BNil(), (x: Dummy) => dummyToString(x)) } }
+ |
+ | def customListToString[T](l: List[T], f: T => String): String = ???[String] ensuring
+ | { (res: String) => (l, res) passes { case _ if false => "" } }
+ |
+ | // Handling multiple rendering functions at the same time.
+ | case class DConfig(dums: List[Dummy], dums2: List[Dummy2])
+ | def dConfigToString(dc: DConfig): String = ???[String] ensuring
+ | { (res: String) => (dc, res) passes {
+ | case DConfig(Nil(), Nil()) =>
+ | "Solution:\n " + customListToString[Dummy](List[Dummy](), (x : Dummy) => dummyToString(x)) + "\n " + customListToString[Dummy2](List[Dummy2](), (x: Dummy2) => dummy2ToString(x)) } }
+ |
+ | case class Node(tag: String, l: List[Edge])
+ | case class Edge(start: Node, end: Node)
+ |
+ | def nodeToString(n: Node): String = ??? by example
+ | def edgeToString(e: Edge): String = ??? by example
+ | def listEdgeToString(l: List[Edge]): String = ??? by example
+ |}
+ """.stripMargin.replaceByExample)
+ implicit val (ctx, program) = getFixture()
+
+ val synthesisInfos = SourceInfo.extractFromProgram(ctx, program).map(si => si.fd.id.name -> si ).toMap
+
+ def synthesizeAndTest(functionName: String, tests: (Seq[Expr], String)*) {
+ val (fd, program) = applyStringRenderOn(functionName)
+ val when = new DefaultEvaluator(ctx, program)
+ val args = getFunctionArguments(functionName)
+ for((in, out) <- tests) {
+ val expr = functionInvocation(fd, in)
+ when.eval(expr) match {
+ case EvaluationResults.Successful(value) => value shouldEqual StringLiteral(out)
+ case EvaluationResults.EvaluatorError(msg) => fail(/*program + "\n" + */msg)
+ case EvaluationResults.RuntimeError(msg) => fail(/*program + "\n" + */"Runtime: " + msg)
+ }
+ }
+ }
+ def synthesizeAndAbstractTest(functionName: String)(tests: (FunDef, Program) => Seq[(Seq[Expr], Expr)]) {
+ val (fd, program) = applyStringRenderOn(functionName)
+ val when_abstract = new AbstractEvaluator(ctx, program)
+ val args = getFunctionArguments(functionName)
+ for((in, out) <- tests(fd, program)) {
+ val expr = functionInvocation(fd, in)
+ when_abstract.eval(expr) match {
+ case EvaluationResults.Successful(value) => val m = ExprOps.canBeHomomorphic(value._1, out)
+ assert(m.nonEmpty, value._1 + " was not homomorphic with " + out)
+ case EvaluationResults.EvaluatorError(msg) => fail(/*program + "\n" + */msg)
+ case EvaluationResults.RuntimeError(msg) => fail(/*program + "\n" + */"Runtime: " + msg)
+ }
+ }
+ }
+ abstract class CCBuilder(ccName: String, prefix: String = "StringRenderSuite.")(implicit program: Program) {
+ val caseClassName = prefix + ccName
+ def getType: TypeTree = program.lookupCaseClass(caseClassName).get.typed
+ def apply(s: Expr*): CaseClass = {
+ CaseClass(program.lookupCaseClass(caseClassName).get.typed, s.toSeq)
+ }
+ def apply(s: String): CaseClass = this.apply(StringLiteral(s))
+ }
+ abstract class ParamCCBuilder(caseClassName: String, prefix: String = "StringRenderSuite.")(implicit program: Program) {
+ def apply(types: TypeTree*)(s: Expr*): CaseClass = {
+ CaseClass(program.lookupCaseClass(prefix+caseClassName).get.typed(types),
+ s.toSeq)
+ }
+ }
+ def method(fName: String)(implicit program: Program) = {
+ program.lookupFunDef("StringRenderSuite." + fName).get
+ }
+ abstract class paramMethod(fName: String)(implicit program: Program) {
+ val fd = program.lookupFunDef("StringRenderSuite." + fName).get
+ def apply(types: TypeTree*)(args: Expr*) =
+ FunctionInvocation(fd.typed(types), args)
+ }
+ // Mimics the file above, allows construction of expressions.
+ case class Constructors(program: Program) {
+ implicit val p = program
+ implicit def CCBuilderToType(c: CCBuilder): TypeTree = c.getType
+ object Knot extends CCBuilder("Knot")
+ object Bud extends CCBuilder("Bud")
+ object Dummy extends CCBuilder("Dummy")
+ object Dummy2 extends CCBuilder("Dummy2")
+ object Cons extends ParamCCBuilder("Cons", "leon.collection.")
+ object Nil extends ParamCCBuilder("Nil", "leon.collection.")
+ object List {
+ def apply(types: TypeTree*)(elems: Expr*): CaseClass = {
+ elems.toList match {
+ case collection.immutable.Nil => Nil(types: _*)()
+ case a::b => Cons(types: _*)(a, List(types: _*)(b: _*))
+ }
+ }
+ }
+
+ object BCons extends ParamCCBuilder("BCons")
+ object BNil extends ParamCCBuilder("BNil")
+ object BList {
+ def apply(types: TypeTree*)(elems: Expr*): CaseClass = {
+ elems.toList match {
+ case collection.immutable.Nil => BNil(types: _*)()
+ case a::b => BCons(types: _*)(a, BList(types: _*)(b: _*))
+ }
+ }
+ def helper(types: TypeTree*)(elems: (Expr, Expr)*): CaseClass = {
+ this.apply(types: _*)(elems.map(x => tupleWrap(Seq(x._1, x._2))): _*)
+ }
+ }
+ object Config extends CCBuilder("Config") {
+ def apply(i: Int, b: (Int, String)): CaseClass =
+ this.apply(InfiniteIntegerLiteral(i), tupleWrap(Seq(IntLiteral(b._1), StringLiteral(b._2))))
+ }
+ object BConfig extends CCBuilder("BConfig")
+ object DConfig extends CCBuilder("DConfig")
+ lazy val dummyToString = method("dummyToString")
+ lazy val dummy2ToString = method("dummy2ToString")
+ lazy val bListToString = method("bListToString")
+ object customListToString extends paramMethod("customListToString")
+ }
+
+ test("Literal synthesis"){ case (ctx: LeonContext, program: Program) =>
+ synthesizeAndTest("literalSynthesis",
+ Seq(IntLiteral(156)) -> ":156.",
+ Seq(IntLiteral(-5)) -> ":-5.")
+ }
+
+ test("boolean Synthesis"){ case (ctx: LeonContext, program: Program) =>
+ synthesizeAndTest("booleanSynthesis",
+ Seq(BooleanLiteral(true)) -> "yes",
+ Seq(BooleanLiteral(false)) -> "no")
+ }
+
+ test("Boolean synthesis 2"){ case (ctx: LeonContext, program: Program) =>
+ synthesizeAndTest("booleanSynthesis2",
+ Seq(BooleanLiteral(true)) -> "B: true",
+ Seq(BooleanLiteral(false)) -> "B: false")
+ }
+
+ /*test("String escape synthesis"){ case (ctx: LeonContext, program: Program) =>
+ synthesizeAndTest("stringEscape",
+ Seq(StringLiteral("abc")) -> "done...abc",
+ Seq(StringLiteral("\t")) -> "done...\\t")
+
+ }*/
+
+ test("Case class synthesis"){ case (ctx: LeonContext, program: Program) =>
+ val c = Constructors(program); import c._
+ StringRender.enforceDefaultStringMethodsIfAvailable = false
+ synthesizeAndTest("configToString",
+ Seq(Config(4, (5, "foo"))) -> "4: 5 -> foo")
+ }
+
+ test("Out of order synthesis"){ case (ctx: LeonContext, program: Program) =>
+ val c = Constructors(program); import c._
+ StringRender.enforceDefaultStringMethodsIfAvailable = false
+ synthesizeAndTest("configToString2",
+ Seq(Config(4, (5, "foo"))) -> "foo: 4 -> 5")
+ }
+
+ test("Recursive case class synthesis"){ case (ctx: LeonContext, program: Program) =>
+ val c = Constructors(program); import c._
+ synthesizeAndTest("treeToString",
+ Seq(Knot(Knot(Bud("aa"), Bud("bb")), Knot(Bud("mm"), Bud("nn")))) ->
+ "<<aaYbb>Y<mmYnn>>")
+ }
+
+ test("Abstract synthesis"){ case (ctx: LeonContext, program: Program) =>
+ val c = Constructors(program); import c._
+ val d = FreshIdentifier("d", Dummy)
+
+ synthesizeAndTest("bListToString",
+ Seq(BList.helper(Dummy)(
+ (Dummy("a"), Dummy("b")),
+ (Dummy("c"), Dummy("d"))),
+ Lambda(Seq(ValDef(d)), FunctionInvocation(dummyToString.typed, Seq(Variable(d)))))
+ ->
+ "[{a}-{b}, {c}-{d}]")
+
+ }
+
+
+ test("Pretty-printing using inferred not yet defined functions in argument"){ case (ctx: LeonContext, program: Program) =>
+ StringRender.enforceDefaultStringMethodsIfAvailable = true
+ synthesizeAndAbstractTest("bConfigToString"){ (fd: FunDef, program: Program) =>
+ val c = Constructors(program); import c._
+ val arg = BList.helper(Dummy)((Dummy("a"), Dummy("b")))
+ val d = FreshIdentifier("d", Dummy)
+ val lambdaDummyToString = Lambda(Seq(ValDef(d)), FunctionInvocation(dummyToString.typed, Seq(Variable(d))))
+ val listDummyToString = functionInvocation(bListToString, Seq(arg, lambdaDummyToString))
+ Seq(Seq(BConfig(arg)) ->
+ StringConcat(StringLiteral("Config"), listDummyToString))
+ }
+ }
+
+ test("Pretty-printing using an existing not yet defined parametrized function") { case (ctx: LeonContext, program: Program) =>
+ StringRender.enforceDefaultStringMethodsIfAvailable = true
+
+ synthesizeAndAbstractTest("dConfigToString"){ (fd: FunDef, program: Program) =>
+ val c = Constructors(program); import c._
+
+ val listDummy1 = c.List(Dummy)(Dummy("a"), Dummy("b"), Dummy("c"))
+ val listDummy2 = c.List(Dummy2)(Dummy2("1"), Dummy2("2"))
+ val arg = DConfig(listDummy1, listDummy2)
+
+ val d = FreshIdentifier("d", Dummy)
+ val lambdaDummyToString = Lambda(Seq(ValDef(d)), FunctionInvocation(dummyToString.typed, Seq(Variable(d))))
+ val d2 = FreshIdentifier("d2", Dummy2)
+ val lambdaDummy2ToString = Lambda(Seq(ValDef(d2)), FunctionInvocation(dummy2ToString.typed, Seq(Variable(d2))))
+
+ Seq(Seq(arg) ->
+ StringConcat(StringConcat(StringConcat(
+ StringLiteral("Solution:\n "),
+ customListToString(Dummy)(listDummy1, lambdaDummyToString)),
+ StringLiteral("\n ")),
+ customListToString(Dummy2)(listDummy2, lambdaDummy2ToString)))
+ }
+ }
+}
\ No newline at end of file
diff --git a/testcases/stringrender/CalendarRender.scala b/testcases/stringrender/CalendarRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..062c908be0926f37871f4168330fd556b1d50a42
--- /dev/null
+++ b/testcases/stringrender/CalendarRender.scala
@@ -0,0 +1,59 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+import leon.collection._
+
+object CalendartoString {
+ val dayEventsSep = "\n"
+ val eventsSep = "\n"
+ val daysSep = "\n\n"
+ val hoursSep = "-"
+ val dayPlusPrefix = " (D+"
+ val dayPlusSuffix = ")"
+ val hoursDescriptionSep = " : "
+ val titleDescriptionSep = "\n"
+
+ case class Week(days: List[Day])
+ case class Day(name: String, events: List[Event])
+ case class Event(startHour: Int, startMinute: Int, durationMinutes: Int, description: String)
+
+ def renderHour(h: Int, m: Int) = {
+ //require(m >= 0 && m < 60 && h > 0)
+ val h_adjusted = h + m / 60
+ val realh = h_adjusted % 24
+ val realm = m % 60
+ val days = h_adjusted / 24
+ realh + "h" + (if(realm == 0) "" else (if(realm < 10) "0" + realm else realm.toString)) + (if(days > 0) dayPlusPrefix + days + dayPlusSuffix else "")
+ }
+
+ def renderEvent(e: Event) = {
+ renderHour(e.startHour, e.startMinute) + hoursSep + renderHour(e.startHour, e.startMinute + e.durationMinutes) + hoursDescriptionSep + e.description
+ }
+
+ def renderList[T](l: List[T], f: T => String, prefix: String, separator: String, suffix: String): String = l match {
+ case Nil() => prefix + suffix
+ case Cons(e, tail:Cons[T]) => prefix + f(e) + separator + renderList(tail, f, "", separator, suffix)
+ case Cons(e, Nil()) => prefix + f(e) + suffix
+ }
+
+ def renderDay(d: Day): String = {
+ renderList(d.events, (e: Event) => renderEvent(e), d.name + dayEventsSep, eventsSep, "")
+ }
+
+ def renderWeek(s: Week): String = {
+ renderList(s.days, (d: Day) => renderDay(d), """Dear manager,
+Here is what happened last week:
+""", daysSep, "")
+ } ensuring { (res: String) =>
+ (s, res) passes {
+ case Week(Cons(Day("Wednesday", Cons(Event(8, 30, 60, "First meeting"), Cons(Event(23, 15, 420, "Bus journey"), Nil()))), Cons(Day("Thursday", Cons(Event(12, 0, 65, "Meal with client"), Nil())), Nil()))) => """Dear manager,
+Here is what happened last week:
+Wednesday
+8h30-9h30 : First meeting
+23h15-6h15 (D+1) : Bus journey
+
+Thursday
+12h-13h05 : Meal with client"""
+ }
+ }
+}
\ No newline at end of file
diff --git a/testcases/stringrender/CustomRender.scala b/testcases/stringrender/CustomRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7f81d50f0bf756096222944dbb14bf6a9b405720
--- /dev/null
+++ b/testcases/stringrender/CustomRender.scala
@@ -0,0 +1,23 @@
+/**
+ * Name: CustomRender.scala
+ * Creation: 15.1.2015
+ * Author: Mikael Mayer (mikael.mayer@epfl.ch)
+ * Comments: Custom generic rendering
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object CustomRender {
+ def generic_list[T](l: List[T], f: T => String): String = {
+ ???
+ } ensuring {
+ (res: String) => ((l, res) passes {
+ case Nil() => "[]"
+ case Cons(a, Cons(b, Nil())) => "[" + f(a) + ", " + f(b) + "]"
+ })
+ }
+}
\ No newline at end of file
diff --git a/testcases/stringrender/JsonRender.scala b/testcases/stringrender/JsonRender.scala
index 2b858784576e6cd97a282a2cba59246f5c4fa84f..274ed3a0f9af8ed9128f14c983abf99d714c3393 100644
--- a/testcases/stringrender/JsonRender.scala
+++ b/testcases/stringrender/JsonRender.scala
@@ -1,8 +1,8 @@
/**
- * Name: ListRender.scala
- * Creation: 14.10.2015
- * Author: Mika�l Mayer (mikael.mayer@epfl.ch)
- * Comments: First benchmark ever for solving string transformation problems. List specifications.
+ * Name: JsonRender.scala
+ * Creation: 25.11.2015
+ * Author: Mikael Mayer (mikael.mayer@epfl.ch)
+ * Comments: Json specifications
*/
import leon.lang._
diff --git a/testcases/stringrender/ModularRender.scala b/testcases/stringrender/ModularRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4757e3cc3135fa5818abf1ee34fd4b8a072a00fe
--- /dev/null
+++ b/testcases/stringrender/ModularRender.scala
@@ -0,0 +1,42 @@
+/**
+ * Name: ModularRender.scala
+ * Creation: 26.01.2015
+ * Author: Mikael Mayer (mikael.mayer@epfl.ch)
+ * Comments: Modular rendering, in one order or the other.
+ */
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ModularRender {
+ def customToString[T](l : List[T], f : (T) => String): String = {
+ ???
+ } ensuring {
+ (res : String) => (l, res) passes {
+ case Nil() =>
+ "[]"
+ case Cons(t, Nil()) =>
+ "[" + f(t) + "]"
+ case Cons(ta, Cons(tb, Nil())) =>
+ "[" + f(ta) + ", " + f(tb) + "]"
+ case Cons(ta, Cons(tb, Cons(tc, Nil()))) =>
+ "[" + f(ta) + ", " + f(tb) + ", " + f(tc) + "]"
+ }
+ }
+
+ def booleanToString(b: Boolean) = if(!b) "Up" else "Down"
+
+ case class Configuration(flags: List[Boolean])
+
+ // We want to write Config:[Up,Down,Up....]
+ def ConfigToString(config : Configuration): String = {
+ ???
+ } ensuring {
+ (res : String) => (config, res) passes {
+ case _ if false =>
+ ""
+ }
+ }
+}
diff --git a/testcases/stringrender/SymbolGrammarRender.scala b/testcases/stringrender/SymbolGrammarRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5998e6b3895f59c4cff518f74e0ca860a59b2b4e
--- /dev/null
+++ b/testcases/stringrender/SymbolGrammarRender.scala
@@ -0,0 +1,60 @@
+/**
+ * Name: SymbolGrammarRender.scala
+ * Creation: 14.01.2016
+ * Author: Mika�l Mayer (mikael.mayer@epfl.ch)
+ * Comments: Grammar rendering specifications starting with symbols
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object GrammarRender {
+ /** A tagged symbol */
+ abstract class Symbol
+ /** A tagged non-terminal, used for markovization */
+ case class NonTerminal(tag: String, vcontext: List[Symbol], hcontext: List[Symbol]) extends Symbol
+ /** A tagged terminal */
+ case class Terminal(tag: String) extends Symbol
+
+ /** All possible right-hand-side of rules */
+ case class Expansion(ls: List[List[Symbol]])
+ /** A grammar here has a start sequence instead of a start symbol */
+ case class Grammar(start: List[Symbol], rules: List[(Symbol, Expansion)])
+
+ def symbol_markov(s: Grammar): String = {
+ ???[String]
+ } ensuring {
+ (res : String) => (s, res) passes {
+ case Terminal("foo") =>
+ "Tfoo"
+ case Terminal("\"'\n\t") =>
+ "T\"'\n\t"
+ case NonTerminal("foo", Nil(), Nil()) =>
+ "Nfoo"
+ case NonTerminal("\"'\n\t", Nil(), Nil()) =>
+ "N\"'\n\t"
+ case NonTerminal("foo", Nil(), Cons(Terminal("foo"), Nil())) =>
+ "Nfoo_hTfoo"
+ case NonTerminal("foo", Cons(Terminal("foo"), Nil()), Nil()) =>
+ "Nfoo_vTfoo"
+ case NonTerminal("foo", Nil(), Cons(NonTerminal("foo", Nil(), Nil()), Cons(NonTerminal("foo", Nil(), Nil()), Nil()))) =>
+ "Nfoo_hNfoo_Nfoo"
+ case NonTerminal("foo", Cons(Terminal("foo"), Nil()), Cons(NonTerminal("foo", Nil(), Nil()), Nil())) =>
+ "Nfoo_vTfoo_hNfoo"
+ case NonTerminal("foo", Cons(NonTerminal("foo", Nil(), Nil()), Cons(NonTerminal("foo", Nil(), Nil()), Nil())), Nil()) =>
+ "Nfoo_vNfoo_Nfoo"
+ }
+ }
+
+ def grammarToString(p : Grammar): String = {
+ ???[String]
+ } ensuring {
+ (res : String) => (p, res) passes {
+ case _ if false =>
+ ""
+ }
+ }
+}
\ No newline at end of file
diff --git a/testcases/web/synthesis/25_String_OutOfOrder.scala b/testcases/web/synthesis/25_String_OutOfOrder.scala
index 72785cf605cfbfe26bb70abd37651c32d5eddd42..ec855caeee8e2f2eb67b0743438d85c7902dc47d 100644
--- a/testcases/web/synthesis/25_String_OutOfOrder.scala
+++ b/testcases/web/synthesis/25_String_OutOfOrder.scala
@@ -5,13 +5,13 @@ import leon.collection.ListOps._
import leon.lang.synthesis._
object OutOfOrderToString {
- def argumentsToString(i: Int, j: Int): String = {
+ def arguments(i: Int, j: Int): String = {
???
} ensuring { (res: String) => ((i, j), res) passes {
case (1, 2) => "2, 1"
} }
- def tupleToString(i: (Int, Int)): String = {
+ def tuple(i: (Int, Int)): String = {
???
} ensuring { (res: String) => (i, res) passes {
case (1, 2) => "2, 1"
@@ -27,7 +27,7 @@ object OutOfOrderToString {
}
}
- def listPairToString(l : List[(Int, Int)]): String = {
+ def listPair(l : List[(Int, Int)]): String = {
???[String]
} ensuring {
(res : String) => (l, res) passes {
@@ -36,7 +36,7 @@ object OutOfOrderToString {
}
}
- def reverselistPairToString(l: List[(Int, Int)]): String = {
+ def reverselistPair(l: List[(Int, Int)]): String = {
???
} ensuring { (res: String) => (l, res) passes {
case Cons((1, 2), Cons((3,4), Nil())) => "4 -> 3, 2 -> 1"
@@ -44,7 +44,7 @@ object OutOfOrderToString {
case class Rule(input: Int, applied: Option[Int])
- def ruleToString(r : Rule): String = {
+ def rule(r : Rule): String = {
???
} ensuring {
(res : String) => (r, res) passes {
diff --git a/testcases/web/synthesis/26_Modular_Render.scala b/testcases/web/synthesis/26_Modular_Render.scala
new file mode 100644
index 0000000000000000000000000000000000000000..54a5cc3fbf9f4af852d4de797307af8e84278c4f
--- /dev/null
+++ b/testcases/web/synthesis/26_Modular_Render.scala
@@ -0,0 +1,43 @@
+/**
+ * Name: ModularRender.scala
+ * Creation: 26.01.2015
+ * Author: Mikael Mayer (mikael.mayer@epfl.ch)
+ * Comments: Modular rendering, in one order or the other.
+ */
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ModularRender {
+ def customToString[T](l : List[T], f : (T) => String): String = {
+ ???
+ } ensuring {
+ (res : String) => (l, res) passes {
+ case _ if false => ""
+ }
+ }
+
+ def booleanToString(b: Boolean) = if(b) "Up" else "Down"
+ def intToString(b: BigInt) = b.toString
+
+ case class Configuration(flags: List[Boolean], strokes: List[BigInt])
+
+ // We want to write
+ // Solution:
+ // [Up, Down, Up....]
+ // [1, 2, 5, ...]
+ def ConfigToString(config : Configuration): String = {
+ ???
+ } ensuring {
+ (res : String) => (config, res) passes {
+ case _ if false =>
+ ""
+ }
+ }
+
+ /** Wrong lemma for demonstration */
+ def configurationsAreSimple(c: Configuration) =
+ (c.flags.size < 3 || c.strokes.size < 2 || c.flags(0) == c.flags(1) || c.strokes(0) == c.strokes(1)) holds
+}