From 06ae9b2a1db40dde9d865a5ff2150d91a636694d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Sat, 12 Dec 2015 09:36:08 +0100
Subject: [PATCH] Introduced StringSynthesisContext
---
.../leon/synthesis/rules/StringRender.scala | 36 ++++++++++---------
1 file changed, 19 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 30ef401de..7df6ba9c9 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -242,6 +242,10 @@ case object StringRender extends Rule("StringRender") {
case class DependentType(caseClassParent: Option[TypeTree], inputName: String, typeToConvert: TypeTree)
+ case class StringSynthesisContext(
+ currentCaseClassParent: Option[TypeTree],
+ adtToString: Map[DependentType, (FunDef, Stream[WithIds[Expr]])]
+ )(implicit hctx: SearchContext)
/** Creates an empty function definition for the dependent type */
def createEmptyFunDef(tpe: DependentType)(implicit hctx: SearchContext): FunDef = {
@@ -280,8 +284,7 @@ case object StringRender extends Rule("StringRender") {
* @param inputs The list of inputs. Make sure each identifier is typed.
**/
def createFunDefsTemplates(
- currentCaseClassParent: Option[TypeTree],
- adtToString: Map[DependentType, (FunDef, Stream[WithIds[Expr]])],
+ ctx: StringSynthesisContext,
inputs: Seq[Identifier])(implicit hctx: SearchContext): (Stream[WithIds[Expr]], Map[DependentType, (FunDef, Stream[WithIds[Expr]])]) = {
def extractCaseVariants(cct: CaseClassType, assignments2: Map[DependentType, (FunDef, Stream[WithIds[Expr]])])
@@ -290,7 +293,7 @@ case object StringRender extends Rule("StringRender") {
val typeMap = tparams.zip(tparams2).toMap
val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id )
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
- val (rhs, assignments2tmp2) = createFunDefsTemplates(Some(cct), assignments2, fields) // Invoke functions for each of the fields.
+ val (rhs, assignments2tmp2) = createFunDefsTemplates(StringSynthesisContext(Some(cct), assignments2), fields) // Invoke functions for each of the fields.
val newCases = rhs.map(e => (MatchCase(pattern, None, e._1), e._2))
(assignments2tmp2, newCases)
}
@@ -328,29 +331,28 @@ case object StringRender extends Rule("StringRender") {
* Each expression is tagged with a list of identifiers, which is the list of variables which need to be found.
* @return Along with the list, an updated function definitions to transform (parent-dependent) types to strings */
@tailrec def gatherInputs(
- currentCaseClassParent: Option[TypeTree],
- assignments1: Map[DependentType, (FunDef, Stream[WithIds[Expr]])],
+ ctx: StringSynthesisContext,
inputs: List[Identifier],
result: ListBuffer[Stream[WithIds[Expr]]] = ListBuffer()): (List[Stream[WithIds[Expr]]], Map[DependentType, (FunDef, Stream[WithIds[Expr]])]) = inputs match {
- case Nil => (result.toList, assignments1)
+ case Nil => (result.toList, ctx.adtToString)
case input::q =>
- val dependentType = DependentType(currentCaseClassParent, input.asString(hctx.program)(hctx.context), input.getType)
- assignments1.get(dependentType) match {
+ val dependentType = DependentType(ctx.currentCaseClassParent, input.asString(hctx.program)(hctx.context), input.getType)
+ ctx.adtToString.get(dependentType) match {
case Some(fd) =>
- gatherInputs(currentCaseClassParent, assignments1, q, result += Stream((functionInvocation(fd._1, Seq(Variable(input))), Nil)))
+ gatherInputs(ctx, q, result += Stream((functionInvocation(fd._1, Seq(Variable(input))), Nil)))
case None => // No function can render the current type.
input.getType match {
case StringType =>
- gatherInputs(currentCaseClassParent, assignments1, q, result += Stream((Variable(input), Nil)))
+ gatherInputs(ctx, q, result += Stream((Variable(input), Nil)))
case BooleanType =>
val (bTemplate, vs) = booleanTemplate(input).instantiateWithVars
- gatherInputs(currentCaseClassParent, assignments1, q, result += Stream((BooleanToString(Variable(input)), Nil)) #::: Stream((bTemplate, vs)))
+ gatherInputs(ctx, q, result += Stream((BooleanToString(Variable(input)), Nil)) #::: Stream((bTemplate, vs)))
case WithStringconverter(converter) => // Base case
- gatherInputs(currentCaseClassParent, assignments1, q, result += Stream((converter(Variable(input)), Nil)))
+ gatherInputs(ctx, q, result += Stream((converter(Variable(input)), Nil)))
case t: ClassType =>
// Create the empty function body and updates the assignments parts.
val fd = createEmptyFunDef(dependentType)
- val assignments2 = preUpdateFunDefBody(dependentType, fd, assignments1) // Inserts the FunDef in the assignments so that it can already be used.
+ val assignments2 = preUpdateFunDefBody(dependentType, fd, ctx.adtToString) // Inserts the FunDef in the assignments so that it can already be used.
t.root match {
case act@AbstractClassType(acd@AbstractClassDef(id, tparams, parent), tps) =>
// Create a complete FunDef body with pattern matching
@@ -373,12 +375,12 @@ case object StringRender extends Rule("StringRender") {
Stream(constantPatternMatching(fd, act)) ++ allMatchExprsEnd
} else allMatchExprsEnd
val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
- gatherInputs(currentCaseClassParent, assignments4, q, result += Stream((functionInvocation(fd, Seq(Variable(input))), Nil)))
+ gatherInputs(ctx.copy(adtToString = assignments4), q, result += Stream((functionInvocation(fd, Seq(Variable(input))), Nil)))
case cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
val (assignments3, newCases) = extractCaseVariants(cct, assignments2)
val allMatchExprs = newCases.map(acase => mergeMatchCases(fd)(Seq(acase)))
val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
- gatherInputs(currentCaseClassParent, assignments4, q, result += Stream((functionInvocation(fd, Seq(Variable(input))), Nil)))
+ gatherInputs(ctx.copy(adtToString = assignments4), q, result += Stream((functionInvocation(fd, Seq(Variable(input))), Nil)))
}
case TypeParameter(t) =>
hctx.reporter.fatalError("Could not handle type parameter for string rendering " + t)
@@ -387,7 +389,7 @@ case object StringRender extends Rule("StringRender") {
}
}
}
- val (exprs, assignments) = gatherInputs(currentCaseClassParent, adtToString, inputs.toList)
+ val (exprs, assignments) = gatherInputs(ctx, inputs.toList)
/* Add post, pre and in-between holes, and returns a single expr along with the new assignments. */
val template: Stream[WithIds[Expr]] = exprs match {
case Nil =>
@@ -418,7 +420,7 @@ case object StringRender extends Rule("StringRender") {
val ruleInstantiations = ListBuffer[RuleInstantiation]()
ruleInstantiations += RuleInstantiation("String conversion") {
- val (expr, funDefs) = createFunDefsTemplates(None, Map(), p.as)
+ val (expr, funDefs) = createFunDefsTemplates(StringSynthesisContext(None, Map()), p.as)
val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
t + "\n" + s._2._1.toString
--
GitLab