From c911543e084b239f3e770377b330270ca4b61198 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 12 Jan 2016 18:46:45 +0100
Subject: [PATCH] Added two collections of pretty-printer which can be used
later to render some elements.
---
src/main/scala/leon/synthesis/rules/StringRender.scala | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index f03c54b56..5f9d85105 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -469,6 +469,16 @@ case object StringRender extends Rule("StringRender") {
val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
val examples = examplesFinder.extractFromProblem(p)
+ val stringConverters: Map[TypeTree, List[Expr => Expr]] =
+ hctx.program.definedFunctions.filter(fd => fd.returnType == StringType && fd.params.length == 1)
+ .groupBy({ fd => fd.paramIds.head.getType }).mapValues(fds =>
+ fds.map((fd : FunDef) => ((x: Expr) => functionInvocation(fd, Seq(x)))))
+ val internalStringConverters: Map[TypeTree, List[Expr => Expr]] =
+ (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 ruleInstantiations = ListBuffer[RuleInstantiation]()
ruleInstantiations += RuleInstantiation("String conversion") {
val (expr, synthesisResult) = createFunDefsTemplates(StringSynthesisContext.empty, p.as.map(Variable))
--
GitLab