From 3b63c054620eadc28c529c1dccc329ca26c95ae8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 9 May 2016 19:30:12 +0200
Subject: [PATCH] SelfPrettyPrinter can now return functions with free
variables.
---
.../leon/purescala/SelfPrettyPrinter.scala | 139 +++++++++++++-----
1 file changed, 102 insertions(+), 37 deletions(-)
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 9212163a7..bba231525 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -33,64 +33,129 @@ object SelfPrettyPrinter {
}
}
-/** This pretty-printer uses functions defined in Leon itself.
- * If not pretty printing function is defined, return the default value instead
- */
-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.*/
- def allowFunction(fd: FunDef) = { allowedFunctions += fd; this }
+/** T is the type of pretty-printers which have to be found (e.g. Lambda or Lambdas with identifiers)
+ * U is the type of the arguments during gathering */
+trait PrettyPrinterFinder[T, U >: T] {
+ protected def isExcluded(fd: FunDef): Boolean
+ protected def isAllowed(fd: FunDef): Boolean
- def excludeFunctions(fds: Set[FunDef]) = { excluded ++= fds; this }
- def excludeFunction(fd: FunDef) = { excluded += fd; this }
+ @inline def isValidPrinterName(s: String) = { val n = s.toLowerCase(); n.endsWith("tostring") || n.endsWith("mkstring") }
+
+ @inline def isCandidate(fd: FunDef) = fd.returnType == StringType &&
+ fd.params.nonEmpty &&
+ !isExcluded(fd) &&
+ (isAllowed(fd) || isValidPrinterName(fd.id.name))
/** 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] = {
+ def prettyPrintersForType(inputType: TypeTree/*, existingPp: Map[TypeTree, List[Lambda]] = Map()*/)(implicit ctx: LeonContext, program: Program): Stream[T] = {
program.definedFunctions.toStream flatMap { fd =>
- val isCandidate =
- fd.returnType == StringType &&
- fd.params.nonEmpty &&
- !excluded(fd) &&
- (allowedFunctions(fd) || fd.id.name.toLowerCase().endsWith("tostring"))
-
- if(isCandidate) {
- prettyPrinterFromCandidate(fd, inputType)
- } else {
- Stream.Empty
- }
+ if(isCandidate(fd)) prettyPrinterFromCandidate(fd, inputType) else Stream.Empty
}
}
+ def getPrintersForType(t: TypeTree)(implicit ctx: LeonContext, program: Program): Option[Stream[U]] = t match {
+ case FunctionType(Seq(in), StringType) => // Should have one argument.
+ Some(prettyPrintersForType(in))
+ case _ => None
+ }
+
+ // To Implement
+ def buildLambda(inputType: TypeTree, fd: FunDef, slu: Stream[List[U]]): Stream[T]
- def prettyPrinterFromCandidate(fd: FunDef, inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
+ def prettyPrinterFromCandidate(fd: FunDef, inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[T] = {
+ println("Considering pretty printer " + fd.id.name + " with arg " + fd.params.head.getType + " for type " + inputType)
TypeOps.canBeSubtypeOf(inputType, fd.tparams.map(_.tp), fd.params.head.getType) match {
- case Some(genericTypeMap) =>
+ case Some(genericTypeMap) =>
+ println("Found a mapping")
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 {
+ def gatherPrettyPrinters(funIds: List[Identifier], acc: ListBuffer[Stream[U]] = ListBuffer[Stream[U]]()): Option[Stream[List[U]]] = 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
+ getPrintersForType(funId.getType) match {
+ case Some(u) => gatherPrettyPrinters(tail, acc += u)
+ case None =>
+ println("could not finish")
+ 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", inputType) // verify the type
- Lambda(Seq(ValDef(x)), functionInvocation(fd, Variable(x)::lambdas))
- }
- case _ => Stream.empty
+ case Some(l) => buildLambda(inputType, fd, l)
+ case None => Stream.empty
}
- case None => Stream.empty
+ case None => Stream.empty
}
}
+}
+
+/** This pretty-printer uses functions defined in Leon itself.
+ * If not pretty printing function is defined, return the default value instead
+ */
+class SelfPrettyPrinter extends PrettyPrinterFinder[Lambda, Lambda] { top =>
+ implicit val section = leon.utils.DebugSectionEvaluation
+ /* Functions whose name does not need to end with `tostring` or which can be abstract, i.e. which may contain a choose construct.*/
+ protected var allowedFunctions = Set[FunDef]()
+ /* Functions totally excluded from the set of pretty-printer candidates */
+ protected 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 }
+ /** Functions totally excluded from the set of pretty-printer candidates*/
+ def excludeFunctions(fds: Set[FunDef]) = { excluded ++= fds; this }
+ /** Function totally excluded from the set of pretty-printer candidates*/
+ def excludeFunction(fd: FunDef) = { excluded += fd; this }
+ protected def isExcluded(fd: FunDef): Boolean = top.excluded(fd)
+ protected def isAllowed(fd: FunDef): Boolean = top.allowedFunctions(fd)
+
+ override def getPrintersForType(t: TypeTree)(implicit ctx: LeonContext, program: Program): Option[Stream[Lambda]] = t match {
+ case FunctionType(Seq(StringType), StringType) => // Should have one argument.
+ val s = FreshIdentifier("s", StringType) // verify the type
+ Some(Stream(Lambda(Seq(ValDef(s)), Variable(s))) ++ super.getPrintersForType(t).getOrElse(Stream.empty) )
+ case _ => super.getPrintersForType(t)
+ }
+
+ /** From a list of lambdas used for pretty-printing the arguments of a function, builds the lambda for the function itself. */
+ def buildLambda(inputType: TypeTree, fd: FunDef, slu: Stream[List[Lambda]]): Stream[Lambda] = {
+ for(lambdas <- slu) yield {
+ val x = FreshIdentifier("x", inputType) // verify the type
+ Lambda(Seq(ValDef(x)), functionInvocation(fd, Variable(x)::lambdas))
+ }
+ }
+
+ object withPossibleParameters extends PrettyPrinterFinder[(Lambda, List[Identifier]), (Expr, List[Identifier])] {
+ protected def isExcluded(fd: FunDef): Boolean = top.excluded(fd)
+ protected def isAllowed(fd: FunDef): Boolean = top.allowedFunctions(fd)
+
+ /** If the returned identifiers are instantiated, each lambda becomes a pretty-printer.
+ * This allows to make use of mkString functions such as for maps */
+ def prettyPrintersForTypes(inputType: TypeTree)(implicit ctx: LeonContext, program: Program) = {
+ program.definedFunctions.toStream flatMap { fd =>
+ if(isCandidate(fd)) prettyPrinterFromCandidate(fd, inputType) else Stream.Empty
+ }
+ }
+
+ /** Adds the possibility to have holes in expression */
+ override def getPrintersForType(t: TypeTree)(implicit ctx: LeonContext, program: Program) = t match {
+ case FunctionType(Seq(StringType), StringType) => // Should have one argument.
+ val s = FreshIdentifier("s", StringType) // verify the type
+ Some(Stream((Lambda(Seq(ValDef(s)), Variable(s)), List())) ++ super.getPrintersForType(t).getOrElse(Stream.empty) )
+ case StringType =>
+ val const = FreshIdentifier("const", StringType)
+ Some(Stream((Variable(const), List(const))))
+ case _ => super.getPrintersForType(t)
+ }
+
+ /** From a list of expressions gathered for the parameters of the function definition, builds the lambda. */
+ def buildLambda(inputType: TypeTree, fd: FunDef, slu: Stream[List[(Expr, List[Identifier])]]) = {
+ for(lambdas <- slu) yield {
+ val (args, ids) = lambdas.unzip
+ val all_ids = ids.flatten
+ val x = FreshIdentifier("x", inputType) // verify the type
+ (Lambda(Seq(ValDef(x)), functionInvocation(fd, Variable(x)::args)), all_ids)
+ }
+ }
+ }
/** Actually prints the expression with as alternative the given orElse
* @param excluded The list of functions which should be excluded from pretty-printing
--
GitLab