From 77e380f0d53e70b1023c4fa150716971643b7b8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 14 Oct 2015 19:51:42 +0200
Subject: [PATCH] Added testcases/stringrender/BinaryTreeRender.scala and
ListRender.scala
---
testcases/stringrender/BinaryTreeRender.scala | 107 ++++++++++++++
testcases/stringrender/ListRender.scala | 139 ++++++++++++++++++
2 files changed, 246 insertions(+)
create mode 100644 testcases/stringrender/BinaryTreeRender.scala
create mode 100644 testcases/stringrender/ListRender.scala
diff --git a/testcases/stringrender/BinaryTreeRender.scala b/testcases/stringrender/BinaryTreeRender.scala
new file mode 100644
index 000000000..8bc109dd4
--- /dev/null
+++ b/testcases/stringrender/BinaryTreeRender.scala
@@ -0,0 +1,107 @@
+/**
+ * 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
+ */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object TreeRender {
+ sealed abstract class Tree[T]
+ case class Node[T](left: Node[T], i: T, right: Node[T]) extends Tree[T]
+ case class Leaf[T]() extends Tree[T]
+
+ /** Synthesis by example specs */
+ @inline def psStandard(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf))"
+ case Node(Leaf, 1, Leaf) => "Node(Leaf, 1, Leaf)"
+ case Leaf => "Leaf"
+ }
+
+ @inline def psRemoveNode(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "((Leaf, 2, Leaf), 1, (Leaf, -3, Leaf))"
+ case Node(Leaf, 1, Leaf) => "(Leaf, 1, Leaf)"
+ case Leaf => "Leaf"
+ }
+
+ @inline def psRemoveLeaf(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "((, 2, ), 1, (, -3, ))"
+ case Node(Leaf, 1, Leaf) => "(, 1, )"
+ case Leaf => ""
+ }
+
+ @inline def psRemoveComma(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "((2), 1, (-3))"
+ case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "(1, (2))"
+ case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "((2), 1)"
+ case Leaf => ""
+ }
+
+ @inline def psRemoveParentheses(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "(2), 1, (-3)"
+ case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "1, (2)"
+ case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "(2), 1"
+ case Leaf => ""
+ }
+
+ @inline def psPrefix(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "1 (2) (-3)"
+ case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "1 () (2)"
+ case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "1 (2) ()"
+ case Leaf => "()"
+ }
+
+ @inline def psLispLike(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "(1 (2) (-3))"
+ case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "(1 () (2))"
+ case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "(1 (2) ())"
+ case Leaf => "()"
+ }
+
+ @inline def psSuffix(s: Tree[Int])(res: String) = (s, res) passes {
+ case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "(2) (-3) 1"
+ case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "() (2) 1"
+ case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "(2) () 1"
+ case Leaf => "()"
+ }
+
+ //////////////////////////////////////////////
+ // Non-incremental examples: pure synthesis //
+ //////////////////////////////////////////////
+ def synthesizeStandard(s: List[Int]): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesizeRemoveNode(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveNode(s)
+
+ def synthesizeRemoveLeaf(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveLeaf(s)
+
+ def synthesizeRemoveComma(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveComma(s)
+
+ def synthesizeRemoveParentheses(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveParentheses(s)
+
+ def synthesizePrefix(s: List[Int]): String = {
+ ???[String]
+ } ensuring psPrefix(s)
+
+ def synthesizeLispLike(s: List[Int]): String = {
+ ???[String]
+ } ensuring psLispLike(s)
+
+ def synthesizeSuffix(s: List[Int]): String = {
+ ???[String]
+ } ensuring psSuffix(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/ListRender.scala b/testcases/stringrender/ListRender.scala
new file mode 100644
index 000000000..972ae273e
--- /dev/null
+++ b/testcases/stringrender/ListRender.scala
@@ -0,0 +1,139 @@
+/**
+ * Name: ListRender.scala
+ * Creation: 14.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 ListRender {
+ /** Synthesis by example specs */
+ @inline def psStandard(s: List[Int])(res: String) = (s, res) passes {
+ case Cons(12, Cons(-1, Nil)) => "Cons(12, Cons(-1, Nil))"
+ case Cons(1, Nil) => "Cons(1, Nil)"
+ case Nil => "Nil"
+ }
+
+ @inline def psRemoveCons(s: List[Int])(res: String) = (s, res) passes {
+ case Cons(12, Cons(-1, Nil)) => "(12, (-1, Nil))"
+ case Cons(1, Nil) => "(1, Nil)"
+ case Nil => "Nil"
+ }
+
+ @inline def psRemoveNil(s: List[Int])(res: String) = (s, res) passes {
+ case Cons(12, Cons(-1, Nil)) => "(12, (-1, ))"
+ case Cons(1, Nil) => "(1, )"
+ case Nil => ""
+ }
+
+ @inline def psRemoveLastComma(s: List[Int])(res: String) = (s, res) passes {
+ case Cons(12, Cons(-1, Nil)) => "(12, (-1))"
+ case Cons(1, Nil) => "(1)"
+ case Nil => "()"
+ }
+
+ @inline def psRemoveParentheses(s: List[Int])(res: String) = (s, res) passes {
+ case Cons(12, Cons(-1, Nil)) => "12, -1"
+ case Cons(1, Nil) => "1"
+ case Nil => ""
+ }
+
+ @inline def psWrapParentheses(s: List[Int])(res: String) = (s, res) passes {
+ case Cons(12, Cons(-1, Nil)) => "(12, -1)"
+ case Cons(1, Nil) => "(1)"
+ case Nil => "()"
+ }
+
+ @inline def psList(s: List[Int])(res: String) = (s, res) passes {
+ case Nil => "List()"
+ case Cons(1, Nil) => "List(1)"
+ case Cons(12, Cons(-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 render1RemoveCons(s: List[Int]): String = {
+ s match {
+ case Nil => "Nil"
+ case Cons(a, b) => "Cons(" + a + ", " + render1RemoveCons(b) + ")"
+ }
+ } ensuring psRemoveCons(s)
+
+ def render2RemoveNil(s: List[Int]): String = {
+ s match {
+ case Nil => "Nil"
+ case Cons(a, b) => "(" + a + ", " + render2RemoveNil(b) + ")"
+ }
+ } ensuring psRemoveNil(s)
+
+ def render3RemoveLastComma(s: List[Int]): String = {
+ s match {
+ case Nil => ""
+ case Cons(a, b) => "(" + a + ", " + render3RemoveLastComma(b) + ")"
+ }
+ } ensuring psRemoveLastComma(s)
+
+ def render4RemoveParentheses(s: List[Int]): String = {
+ s match {
+ case Nil => ""
+ case Cons(a, Nil) => "(" + a + ")"
+ case Cons(a, b) => "(" + 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[Int]): String = {
+ s match {
+ case Nil => ""
+ case Cons(a, Nil) => a.toString
+ case Cons(a, b) => a + ", " + render5WrapParentheses(b)
+ }
+ } ensuring psWrapParentheses(s)
+
+ def render6List(s: List[Int]): String = {
+ def rec(s: List[Int]): String =
+ s match {
+ case Nil => ""
+ case Cons(a, Nil) => a
+ case Cons(a, b) => a + ", " + render6List(b)
+ }
+ "(" + rec(s) + ")"
+ } ensuring psList(s)
+
+ //////////////////////////////////////////////
+ // Non-incremental examples: pure synthesis //
+ //////////////////////////////////////////////
+ def synthesizeStandard(s: List[Int]): String = {
+ ???[String]
+ } ensuring psStandard(s)
+
+ def synthesizeRemoveCons(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveCons(s)
+
+ def synthesizeRemoveNil(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveNil(s)
+
+ def synthesizeRemoveLastComma(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveLastComma(s)
+
+ def synthesizeRemoveParentheses(s: List[Int]): String = {
+ ???[String]
+ } ensuring psRemoveParentheses(s)
+
+ def synthesizeWrapParentheses(s: List[Int]): String = {
+ ???[String]
+ } ensuring psWrapParentheses(s)
+
+ def synthesizeList(s: List[Int]): String = {
+ ???[String]
+ } ensuring psList(s)
+}
\ No newline at end of file
--
GitLab