From abce83acabebea2988e18af953444a7b3a1a3ac6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Thu, 15 Oct 2015 14:20:37 +0200
Subject: [PATCH] Updated test cases and added 4 others.
---
testcases/stringrender/BinaryTreeRender.scala | 2 +-
testcases/stringrender/GrammarRender.scala | 241 ++++++++++++++++++
testcases/stringrender/IntWrapperRender.scala | 66 +++++
testcases/stringrender/ListBigIntRender.scala | 183 +++++++++++++
.../stringrender/TupleWrapperRender.scala | 66 +++++
5 files changed, 557 insertions(+), 1 deletion(-)
create mode 100644 testcases/stringrender/GrammarRender.scala
create mode 100644 testcases/stringrender/IntWrapperRender.scala
create mode 100644 testcases/stringrender/ListBigIntRender.scala
create mode 100644 testcases/stringrender/TupleWrapperRender.scala
diff --git a/testcases/stringrender/BinaryTreeRender.scala b/testcases/stringrender/BinaryTreeRender.scala
index 8bc109dd4..901c330b8 100644
--- a/testcases/stringrender/BinaryTreeRender.scala
+++ b/testcases/stringrender/BinaryTreeRender.scala
@@ -2,7 +2,7 @@
* Name: BinaryTreeRender.scala
* Creation: 14.10.2015
* Author: Mika�l Mayer (mikael.mayer@epfl.ch)
- * Comments: First benchmark ever for solving string transformation problems. Tree specifications
+ * Comments: Binary tree rendering specifications.
*/
import leon.lang._
diff --git a/testcases/stringrender/GrammarRender.scala b/testcases/stringrender/GrammarRender.scala
new file mode 100644
index 000000000..a24a64ff1
--- /dev/null
+++ b/testcases/stringrender/GrammarRender.scala
@@ -0,0 +1,241 @@
+/**
+ * Name: GrammarRender.scala
+ * Creation: 15.10.2015
+ * Author: Mika�l Mayer (mikael.mayer@epfl.ch)
+ * Comments: Grammar rendering specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object Gra��arRender {
+ abstract class Symbol
+ case class Terminal(i: Int) extends Symbol
+ case class NonTerminal(i: Int) extends Symbol
+
+ case class Rule(left: Symbol, right: List[Symbol])
+ case class Grammar(start: Symbol, rules: List[Rule])
+
+ /** Synthesis by example specs */
+ @inline def psStandard(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) => "Grammar(NonTerminal(0), Nil())"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil())) =>
+ "Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil()))"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil())))"
+ }
+
+ @inline def psRemoveNames(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) => "(S0, ())"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ "(S0, ((S0, (t1, ())), ()))"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "(S0, ((S0, (t1, ())), ((S0, (S0, (t1, ()))), ())))"
+ }
+
+ @inline def psArrowRules(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) => "(S0, ())"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ "(S0, ((S0 -> (t1, ())), ()))"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "(S0, ((S0 -> (t1, ())), ((S0 -> (S0, (t1, ()))), ())))"
+ }
+
+ @inline def psListRules(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) => "(S0, [])"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ "(S0, [S0 -> [t1]])"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "(S0, [S0 -> [t1], S0 -> [S0, t1])"
+ }
+
+ // The difficulty here is that two lists have to be rendered differently.
+ @inline def psSpaceRules(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) => "(S0, [])"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ "(S0, [S0 -> t1])"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "(S0, [S0 -> t1, S0 -> S0 t1)"
+ }
+
+ // Full HTML generation
+ @inline def psHTMLRules(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) => "<b>Start:</b> S0<br><pre></pre>"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ "<b>Start:</b> S0<br><pre>S0 -> t1</pte>"
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "<b>Start:</b> S0<br><pre>S0 -> t1<br>S0 -> S0 t1</pte>"
+ }
+ // Full HTML generation
+ @inline def psPlainTextRules(s: Grammar)(res: String) = (s, res) passes {
+ case Grammar(NonTerminal(0), Nil()) =>
+ """Start:S0"""
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Nil)) =>
+ """Start:S0
+ |S0 -> t1""".stripMargin
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ """Start:S0
+ |S0 -> t1
+ |S0 -> S0 t1""".stripMargin
+ }
+
+ /** Each function's body is the solution of the previous problem.
+ * We want to check that the Leon can repair the programs and also find some ambiguities.*/
+ def render0RemoveNames(s: Grammar): String = {
+ def renderSymbol(s: Symbol) = s match {
+ case NonTerminal(i) => "NonTerminal(" + i + ")"
+ case Terminal(i) => "Terminal(" + i + ")"
+ }
+ def renderRule(r: Rule): String = {
+ def renderListSymbol(s: List[Symbol]): String = s match {
+ case Nil() => "Nil()"
+ case Cons(a, q) => "Cons(" + rendersymbol(a) + ", " + renderListsymbol(q) + ")"
+ }
+ "Rule(" + renderSymbol(r.left) + ", " + renderListSymbol(r.right) + ")"
+ }
+ def renderListRules(s: List[Rules]): String = s match {
+ case Nil() => "Nil()"
+ case Cons(r, q) => "Cons(" + renderRule(r) + ", " + renderListRules(q) + ")"
+ }
+ "Grammar(" + renderSymbol(s.start) + ", " + renderListRules(s.rules) + ")"
+ } ensuring psRemoveNames(s)
+
+ def render1ArrowRules(s: Grammar): String = {
+ def renderSymbol(s: Symbol) = s match {
+ case NonTerminal(i) => "S" + i
+ case Terminal(i) => "t" + i
+ }
+ def renderRule(r: Rule): String = {
+ def renderListSymbol(s: List[Symbol]): String = s match {
+ case Nil() => "()"
+ case Cons(a, q) => "(" + rendersymbol(a) + ", " + renderListsymbol(q) + ")"
+ }
+ "(" + renderSymbol(r.left) + ", " + renderListSymbol(r.right) + ")"
+ }
+ def renderListRules(s: List[Rules]): String = s match {
+ case Nil() => "()"
+ case Cons(r, q) => "(" + renderRule(r) + ", " + renderListRules(q) + ")"
+ }
+ "(" + renderSymbol(s.start) + ", " + renderListRules(s.rules) + ")"
+ } ensuring psArrowRules(s)
+
+ def render2ListRules(s: Grammar): String = {
+ def renderSymbol(s: Symbol) = s match {
+ case NonTerminal(i) => "S" + i
+ case Terminal(i) => "t" + i
+ }
+ def renderRule(r: Rule): String = {
+ def renderListSymbol(s: List[Symbol]): String = s match {
+ case Nil() => "()"
+ case Cons(a, q) => "(" + rendersymbol(a) + ", " + renderListsymbol(q) + ")"
+ }
+ "(" + renderSymbol(r.left) + " -> " + renderListSymbol(r.right) + ")"
+ }
+ def renderListRules(s: List[Rules]): String = s match {
+ case Nil() => "()"
+ case Cons(r, q) => "(" + renderRule(r) + ", " + renderListRules(q) + ")"
+ }
+ "(" + renderSymbol(s.start) + ", " + renderListRules(s.rules) + ")"
+ } ensuring psListRules(s)
+
+ def render3SpaceRules(s: Grammar): String = {
+ def renderSymbol(s: Symbol) = s match {
+ case NonTerminal(i) => "S" + i
+ case Terminal(i) => "t" + i
+ }
+ def renderRule(r: Rule): String = {
+ def renderListSymbol(s: List[Symbol]): String = s match {
+ case Nil() => ""
+ case Cons(a, Nil) => rendersymbol(a)
+ case Cons(a, q) => rendersymbol(a) + ", " + renderListsymbol(q)
+ }
+ renderSymbol(r.left) + " -> [" + renderListSymbol(r.right) + "]"
+ }
+ def renderListRules(s: List[Rules]): String = s match {
+ case Nil() => ""
+ case Cons(r, Nil()) => renderRule(r)
+ case Cons(r, q) => renderRule(r) + ", " + renderListRules(q)
+ }
+ "(" + renderSymbol(s.start) + ", [" + renderListRules(s.rules) + "])"
+ } ensuring psSpaceRules(s)
+
+ def render4HTMLRules(s: Grammar): String = {
+ def renderSymbol(s: Symbol) = s match {
+ case NonTerminal(i) => "S" + i
+ case Terminal(i) => "t" + i
+ }
+ def renderRule(r: Rule): String = {
+ def renderListSymbol(s: List[Symbol]): String = s match {
+ case Nil() => ""
+ case Cons(a, Nil) => rendersymbol(a)
+ case Cons(a, q) => rendersymbol(a) + " " + renderListsymbol(q)
+ }
+ renderSymbol(r.left) + " -> " + renderListSymbol(r.right) + ""
+ }
+ def renderListRules(s: List[Rules]): String = s match {
+ case Nil() => ""
+ case Cons(r, Nil()) => renderRule(r)
+ case Cons(r, q) => renderRule(r) + ", " + renderListRules(q)
+ }
+ "(" + renderSymbol(s.start) + ", [" + renderListRules(s.rules) + "])"
+ } ensuring psHTMLRules(s)
+
+ case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
+ "<b>Start:</b> S0<br><pre>S0 -> t1<br>S0 -> S0 t1</pte>"
+
+ /* The initial body of this function is the solution of render3 */
+ def render5PlainTextRules(s: Grammar): String = {
+ def renderSymbol(s: Symbol) = s match {
+ case NonTerminal(i) => "S" + i
+ case Terminal(i) => "t" + i
+ }
+ def renderRule(r: Rule): String = {
+ def renderListSymbol(s: List[Symbol]): String = s match {
+ case Nil() => ""
+ case Cons(a, Nil) => rendersymbol(a)
+ case Cons(a, q) => rendersymbol(a) + " " + renderListsymbol(q)
+ }
+ renderSymbol(r.left) + " -> " + renderListSymbol(r.right) + ""
+ }
+ def renderListRules(s: List[Rules]): String = s match {
+ case Nil() => ""
+ case Cons(r, Nil()) => renderRule(r)
+ case Cons(r, q) => renderRule(r) + ", " + renderListRules(q)
+ }
+ "(" + renderSymbol(s.start) + ", [" + renderListRules(s.rules) + "])"
+ } ensuring psPlainTextRules(s)
+
+ //////////////////////////////////////////////
+ // Non-incremental examples: pure synthesis //
+ //////////////////////////////////////////////
+ def synthesizeStandard(s: Grammar): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesizeRemoveNames(s: Grammar): String = {
+ ???[String]
+ } ensuring psRemoveNames(s)
+
+ def synthesizeArrowRules(s: Grammar): String = {
+ ???[String]
+ } ensuring psArrowRules(s)
+
+ def synthesizeListRules(s: Grammar): String = {
+ ???[String]
+ } ensuring psListRules(s)
+
+ def synthesizeSpaceRules(s: Grammar): String = {
+ ???[String]
+ } ensuring psSpaceRules(s)
+
+ def synthesizeHTMLRules(s: Grammar): String = {
+ ???[String]
+ } ensuring psHTMLRules(s)
+
+ def synthesizePlainTextRules(s: Grammar): String = {
+ ???[String]
+ } ensuring psPlainTextRules(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/IntWrapperRender.scala b/testcases/stringrender/IntWrapperRender.scala
new file mode 100644
index 000000000..8484512df
--- /dev/null
+++ b/testcases/stringrender/IntWrapperRender.scala
@@ -0,0 +1,66 @@
+/**
+ * Name: IntWrapperRender.scala
+ * Creation: 15.10.2015
+ * Author: Mikaël Mayer (mikael.mayer@epfl.ch)
+ * Comments: First benchmark ever for solving string transformation problems. List specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object IntWrapperRender {
+ case class IntWrapper(i: Int)
+
+ def psStandard(s: IntWrapper)(res: String) = (s, res) passes {
+ case IntWrapper(0) => "IntWrapper(0)"
+ case IntWrapper(-1) => "IntWrapper(-1)"
+ case IntWrapper(12) => "IntWrapper(12)"
+ }
+
+ def psUnwrapped(s: IntWrapper)(res: String) = (s, res) passes {
+ case IntWrapper(0) => "0"
+ case IntWrapper(-1) => "-1"
+ case IntWrapper(12) => "12"
+ }
+
+ def psNameChangedPrefix(s: IntWrapper)(res: String) = (s, res) passes {
+ case IntWrapper(0) => "number: 0"
+ case IntWrapper(-1) => "number: -1"
+ case IntWrapper(12) => "number: 12"
+ }
+
+ def psNameChangedSuffix(s: IntWrapper)(res: String) = (s, res) passes {
+ case IntWrapper(0) => "0.0"
+ case IntWrapper(-1) => "-1.0" // Here there should be an ambiguity before this line.
+ case IntWrapper(12) => "12.0"
+ }
+
+ def psDuplicate(s: IntWrapper)(res: String) = (s, res) passes {
+ case IntWrapper(0) => "0 0"
+ case IntWrapper(-1) => "-1 -1"
+ case IntWrapper(12) => "12 12"
+ }
+
+ def synthesisStandard(s: IntWrapper): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesisUnwrapped(s: IntWrapper): String = {
+ ???[String]
+ } ensuring psUnwrapped(s)
+
+ def synthesisNameChangedPrefix(s: IntWrapper): String = {
+ ???[String]
+ } ensuring psNameChangedPrefix(s)
+
+ def synthesisNameChangedSuffix(s: IntWrapper): String = {
+ ???[String]
+ } ensuring psNameChangedSuffix(s)
+
+ def synthesisDuplicate(s: IntWrapper): String = {
+ ???[String]
+ } ensuring psDuplicate(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/ListBigIntRender.scala b/testcases/stringrender/ListBigIntRender.scala
new file mode 100644
index 000000000..c048606a5
--- /dev/null
+++ b/testcases/stringrender/ListBigIntRender.scala
@@ -0,0 +1,183 @@
+/**
+ * Name: ListBigIntRender.scala
+ * Creation: 15.10.2015
+ * Author: Mika�l Mayer (mikael.mayer@epfl.ch)
+ * Comments: List of BigInt specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ListBigIntRender {
+ /** Synthesis by example specs */
+ @inline def psStandard(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "Cons(BigInt(12), Cons(BigInt(-1), Nil))"
+ case Cons(BigInt(1), Nil) => "Cons(BigInt(1), Nil)"
+ case Nil => "Nil"
+ }
+
+ @inline def psRemoveBigInt(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "Cons(12, Cons(-1, Nil))"
+ case Cons(BigInt(1), Nil) => "Cons(1, Nil)"
+ case Nil => "Nil"
+ }
+
+ @inline def psRemoveCons(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "(12, (-1, Nil))"
+ case Cons(BigInt(1), Nil) => "(1, Nil)"
+ case Nil => "Nil"
+ }
+
+ @inline def psRemoveNil(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "(12, (-1, ))"
+ case Cons(BigInt(1), Nil) => "(1, )"
+ case Nil => ""
+ }
+
+ @inline def psRemoveLastComma(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "(12, (-1))"
+ case Cons(BigInt(1), Nil) => "(1)"
+ case Nil => "()"
+ }
+
+ @inline def psRemoveParentheses(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "12, -1"
+ case Cons(BigInt(1), Nil) => "1"
+ case Nil => ""
+ }
+
+ @inline def psWrapParentheses(s: List[BigInt])(res: String) = (s, res) passes {
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "(12, -1)"
+ case Cons(BigInt(1), Nil) => "(1)"
+ case Nil => "()"
+ }
+
+ @inline def psList(s: List[BigInt])(res: String) = (s, res) passes {
+ case Nil => "List()"
+ case Cons(BigInt(1), Nil) => "List(1)"
+ case Cons(BigInt(12), Cons(BigInt(-1), Nil)) => "List(12, -1)"
+ }
+
+ /** Each function's body is the solution of the previous problem.
+ * We want to check that the Leon can repair the programs and also find some ambiguities.*/
+ def render0RemoveBigInt(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ b.toString()
+ }
+ s match {
+ case Nil => "Nil"
+ case Cons(a, b) => "Cons(" + renderBigInt(a) + ", " + render1RemoveCons(b) + ")"
+ }
+ } ensuring psRemoveCons(s)
+
+ def render1RemoveCons(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ val a = b.toString()
+ a.substring(6, a.length - 1)
+ }
+ s match {
+ case Nil => "Nil"
+ case Cons(a, b) => "Cons(" + renderBigInt(a) + ", " + render1RemoveCons(b) + ")"
+ }
+ } ensuring psRemoveCons(s)
+
+ def render2RemoveNil(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ val a = b.toString()
+ a.substring(6, a.length - 1)
+ }
+ s match {
+ case Nil => "Nil"
+ case Cons(a, b) => "(" + renderBigInt(a) + ", " + render2RemoveNil(b) + ")"
+ }
+ } ensuring psRemoveNil(s)
+
+ def render3RemoveLastComma(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ val a = b.toString()
+ a.substring(6, a.length - 1)
+ }
+ s match {
+ case Nil => ""
+ case Cons(a, b) => "(" + renderBigInt(a) + ", " + render3RemoveLastComma(b) + ")"
+ }
+ } ensuring psRemoveLastComma(s)
+
+ def render4RemoveParentheses(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ val a = b.toString()
+ a.substring(6, a.length - 1)
+ }
+ s match {
+ case Nil => ""
+ case Cons(a, Nil) => "(" + renderBigInt(a) + ")"
+ case Cons(a, b) => "(" + renderBigInt(a) + ", " + render4RemoveParentheses(b) + ")"
+ }
+ } ensuring psRemoveParentheses(s)
+
+ /* harder example: It needs to repair by wrapping the recursive call in a sub-method
+ * in order to add strings to the left and to the right (see render6List) */
+ def render5WrapParentheses(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ val a = b.toString()
+ a.substring(6, a.length - 1)
+ }
+ s match {
+ case Nil => ""
+ case Cons(a, Nil) => renderBigInt(a)
+ case Cons(a, b) => renderBigInt(a) + ", " + render5WrapParentheses(b)
+ }
+ } ensuring psWrapParentheses(s)
+
+ def render6List(s: List[BigInt]): String = {
+ def renderBigInt(b: BigInt): String = {
+ val a = b.toString()
+ a.substring(6, a.length - 1)
+ }
+ def rec(s: List[BigInt]): String =
+ s match {
+ case Nil => ""
+ case Cons(a, Nil) => renderBigInt(a)
+ case Cons(a, b) => renderBigInt(a) + ", " + render6List(b)
+ }
+ "(" + rec(s) + ")"
+ } ensuring psList(s)
+
+ //////////////////////////////////////////////
+ // Non-incremental examples: pure synthesis //
+ //////////////////////////////////////////////
+ def synthesizeStandard(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesizeRemoveBigInt(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psRemoveBigInt(s)
+
+ def synthesizeRemoveCons(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psRemoveCons(s)
+
+ def synthesizeRemoveNil(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psRemoveNil(s)
+
+ def synthesizeRemoveLastComma(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psRemoveLastComma(s)
+
+ def synthesizeRemoveParentheses(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psRemoveParentheses(s)
+
+ def synthesizeWrapParentheses(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psWrapParentheses(s)
+
+ def synthesizeList(s: List[BigInt]): String = {
+ ???[String]
+ } ensuring psList(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/TupleWrapperRender.scala b/testcases/stringrender/TupleWrapperRender.scala
new file mode 100644
index 000000000..d1c754df1
--- /dev/null
+++ b/testcases/stringrender/TupleWrapperRender.scala
@@ -0,0 +1,66 @@
+/**
+ * Name: TupleWrapperRender.scala
+ * Creation: 15.10.2015
+ * Author: Mikaël Mayer (mikael.mayer@epfl.ch)
+ * Comments: Tuple rendering specifications.
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object TupleWrapperRender {
+ case class TupleWrapper(i: Int, j: Int)
+
+ def psStandard(s: TupleWrapper)(res: String) = (s, res) passes {
+ case TupleWrapper(0, 0) => "TupleWrapper(0, 0)"
+ case TupleWrapper(-1, 2) => "TupleWrapper(-1, 2)"
+ case TupleWrapper(12, 5) => "TupleWrapper(12, 5)"
+ }
+
+ def psUnwrapped(s: TupleWrapper)(res: String) = (s, res) passes {
+ case TupleWrapper(0, 0) => "0, 0"
+ case TupleWrapper(-1, 2) => "-1, 2"
+ case TupleWrapper(12, 5) => "(12, 5)"
+ }
+
+ def psNameChangedPrefix(s: TupleWrapper)(res: String) = (s, res) passes {
+ case TupleWrapper(0, 0) => "x = 0, y = 0"
+ case TupleWrapper(-1, 2) => "x = -1, y = 2"
+ case TupleWrapper(12, 5) => "x = 12, y = 5"
+ }
+
+ def psNameChangedSuffix(s: TupleWrapper)(res: String) = (s, res) passes {
+ case TupleWrapper(0, 0) => "0.0,0.0"
+ case TupleWrapper(-1, 2) => "-1.0,2.0" // Here there should be an ambiguity before this line.
+ case TupleWrapper(12, 5) => "12.0,5.0"
+ }
+
+ def psDuplicate(s: TupleWrapper)(res: String) = (s, res) passes {
+ case TupleWrapper(0, 0) => "d 0,0 0,15 15,15 15,0"
+ case TupleWrapper(-1, 2) => "d -1,-2 -1,15 15,15 15,2"
+ case TupleWrapper(12, 5) => "d 12,5 12,15 15,15 15,5"
+ }
+
+ def synthesisStandard(s: TupleWrapper): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesisUnwrapped(s: TupleWrapper): String = {
+ ???[String]
+ } ensuring psUnwrapped(s)
+
+ def synthesisNameChangedPrefix(s: TupleWrapper): String = {
+ ???[String]
+ } ensuring psNameChangedPrefix(s)
+
+ def synthesisNameChangedSuffix(s: TupleWrapper): String = {
+ ???[String]
+ } ensuring psNameChangedSuffix(s)
+
+ def synthesisDuplicate(s: TupleWrapper): String = {
+ ???[String]
+ } ensuring psDuplicate(s)
+}
\ No newline at end of file
--
GitLab