Skip to content
Snippets Groups Projects
Commit d325618d authored by Mikaël Mayer's avatar Mikaël Mayer
Browse files

The self pretty printer now unifies toString functions to print using generic functions if found.

parent b79b4197
No related branches found
No related tags found
No related merge requests found
...@@ -72,7 +72,7 @@ abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps ...@@ -72,7 +72,7 @@ abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps
protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Value 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}."
} }
......
...@@ -2,58 +2,98 @@ package leon.purescala ...@@ -2,58 +2,98 @@ package leon.purescala
import leon.evaluators.StringTracingEvaluator import leon.evaluators.StringTracingEvaluator
import leon.purescala 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 leon.evaluators.StringTracingEvaluator
import purescala.Expressions._ import leon.purescala.Quantification._
import purescala.Types.StringType
import leon.utils.DebugSectionSynthesis import leon.utils.DebugSectionSynthesis
import leon.utils.DebugSectionVerification import leon.utils.DebugSectionVerification
import leon.purescala.Quantification._ import purescala.Definitions.Program
import purescala.Expressions._
import purescala.Types.StringType
import purescala.Constructors._ import purescala.Constructors._
import purescala.ExprOps._ import purescala.ExprOps._
import purescala.Expressions.{Pattern, Expr} import purescala.Expressions._
import purescala.Expressions.{Choose }
import purescala.Extractors._ import purescala.Extractors._
import purescala.TypeOps._ import purescala.TypeOps._
import purescala.Types._ import purescala.Types._
import purescala.Common._ import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._ import purescala.Definitions._
import purescala.SelfPrettyPrinter import scala.collection.mutable.ListBuffer
import leon.solvers.{ HenkinModel, Model, SolverFactory } import leon.evaluators.DefaultEvaluator
import leon.LeonContext
import leon.evaluators
/** This pretty-printer uses functions defined in Leon itself. /** This pretty-printer uses functions defined in Leon itself.
* If not pretty printing function is defined, return the default value instead * 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) * @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. */ * @return a user defined string for the given typed expression. */
object SelfPrettyPrinter { object SelfPrettyPrinter {
def print(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(implicit ctx: LeonContext, program: Program): String = { /** Returns a list of possible lambdas that can transform the input type to a String*/
(program.definedFunctions find { def prettyPrintersForType(inputType: TypeTree/*, existingPp: Map[TypeTree, List[Lambda]] = Map()*/)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
case fd if !excluded(fd) => // Use the other argument if you need recursive typing (?)
fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") && (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 => program.callGraph.transitiveCallees(fd).forall { fde =>
!purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody) !purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
} }
}) match { if(isCandidate) {
case Some(fd) => // InputType is concrete, the types of params may be abstract.
//println("Found fd: " + fd.id.name) TypeOps.canBeSubtypeOf(inputType, fd.tparams.map(_.tp), fd.params.head.getType) match {
val ste = new StringTracingEvaluator(ctx, program) case Some(genericTypeMap) =>
try { val defGenericTypeMap = genericTypeMap.map{ case (k, v) => (Definitions.TypeParameterDef(k), v) }
val result = ste.eval(FunctionInvocation(fd.typed, Seq(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 { result.result match {
case Some((StringLiteral(res), _)) if res != "" => case Some(StringLiteral(res)) if res != "" =>
res res
case _ => case res =>
orElse
}
} catch {
case e: evaluators.ContextualEvaluator#EvalError =>
orElse orElse
} }
case None => } catch {
orElse case e: evaluators.ContextualEvaluator#EvalError =>
orElse
}
} }
} }
} }
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment