From d325618d692eea5deabbb1b221ed1c3b593253ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 18 Jan 2016 15:57:51 +0100
Subject: [PATCH] The self pretty printer now unifies toString functions to
print using generic functions if found.
---
.../leon/evaluators/ContextualEvaluator.scala | 2 +-
.../leon/purescala/SelfPrettyPrinter.scala | 96 +++++++++++++------
2 files changed, 69 insertions(+), 29 deletions(-)
diff --git a/src/main/scala/leon/evaluators/ContextualEvaluator.scala b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
index 0fc33102a..0c23ef39c 100644
--- a/src/main/scala/leon/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
@@ -72,7 +72,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/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 35e4d1f61..2a2b7307c 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -2,58 +2,98 @@ package leon.purescala
import leon.evaluators.StringTracingEvaluator
import leon.purescala
-import purescala.Definitions.Program
+import leon.solvers.{ HenkinModel, Model, SolverFactory }
+import leon.LeonContext
+import leon.evaluators
+import leon.utils.StreamUtils
import leon.evaluators.StringTracingEvaluator
-import purescala.Expressions._
-import purescala.Types.StringType
+import leon.purescala.Quantification._
import leon.utils.DebugSectionSynthesis
import leon.utils.DebugSectionVerification
-import leon.purescala.Quantification._
+import purescala.Definitions.Program
+import purescala.Expressions._
+import purescala.Types.StringType
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 purescala.SelfPrettyPrinter
-import leon.solvers.{ HenkinModel, Model, SolverFactory }
-import leon.LeonContext
-import leon.evaluators
+import scala.collection.mutable.ListBuffer
+import leon.evaluators.DefaultEvaluator
+
/** 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") &&
+ /** 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 flatMap {
+ fd =>
+ val isCandidate = fd.returnType == StringType &&
+ fd.params.length >= 1 &&
+ //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)
}
- }) 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)))
+ if(isCandidate) {
+ // InputType is concrete, the types of params may be abstract.
+ 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 _ => Nil
+ }
+ case None => Nil
+ }
+ } else Nil
+ }).toStream
+ }
+
+ /** Actually prints the expression with as alternative the given orElse */
+ def print(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(implicit ctx: LeonContext, program: Program): String = {
+ val s = prettyPrintersForType(v.getType)
+ if(s.isEmpty) {
+ orElse
+ } else {
+ val l: Lambda = s.head
+ 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 =>
orElse
}
- case None =>
- orElse
+ } catch {
+ case e: evaluators.ContextualEvaluator#EvalError =>
+ orElse
+ }
}
}
}
\ No newline at end of file
--
GitLab