diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index a876001683a2592e567b42f68747e4b86d462d20..f86f5389a79751524b9b61e60dd8b7b804df8ee1 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -4,6 +4,7 @@ package leon
package evaluators
import purescala.Extractors.Operator
+import purescala.Constructors._
import purescala.Expressions._
import purescala.Types._
import purescala.Definitions.{TypedFunDef, Program}
@@ -73,10 +74,10 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
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))
+ (scalaEv.call(tfd, evArgsValues), functionInvocation(tfd.fd, 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))
+ (functionInvocation(tfd.fd, evArgsValues), functionInvocation(tfd.fd, evArgsOrigin))
} else {
val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
e(body)(frame, gctx)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 2672cfe7ff958744d7dc92287d1b71a284c5018c..ca52d4592842da60629423e9d0ba3ff52ea2a73c 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1426,13 +1426,11 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
(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) &&
+ idHomo(tfd1.fd.id, tfd2.fd.id) && tfd1.tps.zip(tfd2.tps).mergeall{ case (t1, t2) => if(t1 == t2) Option(Map()) else None} &&
(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) &&
+ idHomo(tfd1.fd.id, tfd2.fd.id) && tfd1.tps.zip(tfd2.tps).mergeall{ case (t1, t2) => if(t1 == t2) Option(Map()) else None} &&
(args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
case (Lambda(defs, body), Lambda(defs2, body2)) =>
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 16129a49080f8676d1101d790d39331b87fca095..d1cc5f86c6659b2fca51d42b3ebbb0feab20d084 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -37,6 +37,7 @@ object SelfPrettyPrinter {
* @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. */
class SelfPrettyPrinter {
+ implicit val section = leon.utils.DebugSectionEvaluation
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.*/
@@ -45,20 +46,16 @@ class SelfPrettyPrinter {
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*/
+ /** Returns a list of possible lambdas that can transform the input type to a String.
+ * At this point, it does not consider yet the inputType. Only [[prettyPrinterFromCandidate]] will consider it. */
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)
- }))
+ fd.id.name.toLowerCase().endsWith("tostring")))
if(isCandidate) {
prettyPrinterFromCandidate(fd, inputType)
} else Stream.Empty
@@ -83,7 +80,7 @@ class SelfPrettyPrinter {
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
+ val x = FreshIdentifier("x", inputType) // verify the type
Lambda(Seq(ValDef(x)), functionInvocation(fd, Variable(x)::lambdas))
}
case _ => Stream.empty
@@ -97,28 +94,33 @@ class SelfPrettyPrinter {
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 != "" =>
- res
- case res =>
- println("not a string literal " + res)
+ s.take(100).find(l => l match { // Limit the number of pretty-printers.
+ case Lambda(_, FunctionInvocation(TypedFunDef(fd, _), _)) =>
+ (program.callGraph.transitiveCallees(fd) + fd).forall { fde =>
+ !ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
+ }
+ case _ => false
+ }) match {
+ case None => orElse
+ case Some(l) =>
+ ctx.reporter.debug("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 != "" =>
+ res
+ case res =>
+ ctx.reporter.debug("not a string literal " + res)
+ orElse
+ }
+ } catch {
+ case e: evaluators.ContextualEvaluator#EvalError =>
+ ctx.reporter.debug("Error " + e.msg)
orElse
}
- } catch {
- case e: evaluators.ContextualEvaluator#EvalError =>
- println("Error " + e.msg)
- orElse
- }
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 62878dd31761050b839f794beb066bceca051a56..715d54385e07a86f642fa454b78bcf72f020b528 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -245,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 fds(fd) => Some(FunctionInvocation(getMapping(fd).typed, args))
+ case FunctionInvocation(TypedFunDef(fd, _), args) if fds(fd) => Some(functionInvocation(getMapping(fd), args))
case e => None
})(body)
}