From 2d0bff2bad2664759736ae16234f1dc29e855ae3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 2 Dec 2015 11:35:38 +0100
Subject: [PATCH] Reformatted examples and added two not yet parsing testcases.
---
testcases/stringrender/BinaryTreeRender.scala | 22 ++---
testcases/stringrender/Example-Stack.scala | 95 +++++++++++++++++++
2 files changed, 106 insertions(+), 11 deletions(-)
diff --git a/testcases/stringrender/BinaryTreeRender.scala b/testcases/stringrender/BinaryTreeRender.scala
index e019df6b6..3805cbbec 100644
--- a/testcases/stringrender/BinaryTreeRender.scala
+++ b/testcases/stringrender/BinaryTreeRender.scala
@@ -17,53 +17,53 @@ object TreeRender {
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 psStandard(s: Tree[Int]) = (res: String) => (s, res) passes {
+ case Node(Node(Leaf[Int](), 2, Leaf[Int]()), 1, Node(Leaf[Int](), -3, Leaf[Int]())) => "Node(Node(Leaf(), 2, Leaf()), 1, Node(Leaf(), -3, Leaf()))"
+ case Node(Leaf[Int](), 1, Leaf[Int]()) => "Node(Leaf(), 1, Leaf())"
+ case Leaf[Int]() => "Leaf()"
}
- @inline def psRemoveNode(s: Tree[Int])(res: String) = (s, res) passes {
+ @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 {
+ @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 {
+ @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 {
+ @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 {
+ @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 {
+ @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 {
+ @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"
diff --git a/testcases/stringrender/Example-Stack.scala b/testcases/stringrender/Example-Stack.scala
index b01dd6f26..532a9a5cc 100644
--- a/testcases/stringrender/Example-Stack.scala
+++ b/testcases/stringrender/Example-Stack.scala
@@ -385,5 +385,100 @@ object AtomicStack {
"T1: call Push(5)\nT1: internal\nT2: call Pop()\nT1: ret Push(5)\nT2: internal\nT2: ret Pop() -> 5"
}
}
+
+ // Warning: Spacing differs from records to records.
+ // Warning: The displaying of a tuple might depend on its operands.
+ /*def configurationToString(p: List[Configuration[StackTid, StackMethodName, Option[BigInt], StackState, List[BigInt]]]): String = {
+ ???[String]
+ } ensuring {
+ res => (p, res) passes {
+ case Cons(Configuration(Nil(), Map(T1() -> Some((Push(), Some(BigInt(5)), ValueState(BigInt(5)))))),
+ Cons(Configuration(Cons(5, Nil()), Map(T1() -> Some((Push(), Some(BigInt(5)), FinalState())))),
+ Cons(Configuration(Cons(5, Nil()), Map(T2() -> Some((Pop(), None(), InitState())), T1() -> Some((Push(), Some(BigInt(5)), FinalState())))),
+ Cons(Configuration(Cons(5, Nil()), Map(T2() -> Some((Pop(), None(), InitState())), T1() -> None())),
+ Cons(Configuration(Nil(), Map(T2() -> Some((Pop(), None(), ValueState(BigInt(5)))), T1() -> None())),
+ Cons(Configuration(Nil(), Map(T2() -> None(), T1() -> None())), Nil())))))) =>
+ """([], {
+ T1 -> Push(5): ValueState(5)
+})
+
+
+([5], {
+ T1 -> Push(5): FinalState
+})
+
+
+([5], {
+ T2 -> Pop(): InitState;
+ T1 -> Push(5): FinalState
+})
+
+
+([5], {
+ T2 -> Pop(): InitState;
+ T1 -> idle
+})
+
+
+([], {
+ T2 -> Pop(): ValueState(5);
+ T1 -> idle
+})
+
+
+([], {
+ T2 -> idle;
+ T1 -> idle
+})"""
+
+ }
+ }
+
+ /// Out of order configurationToString
+ def configurationToStringOOO(p: List[Configuration[StackTid, StackMethodName, Option[BigInt], StackState, List[BigInt]]]): String = {
+ ???[String]
+ } ensuring {
+ res => (p, res) passes {
+ case Cons(Configuration(Nil(), Map(T1() -> Some((Push(), Some(BigInt(5)), ValueState(BigInt(5)))))),
+ Cons(Configuration(Cons(BigInt(5), Nil()), Map(T1() -> Some((Push(), Some(BigInt(5)), FinalState())))),
+ Cons(Configuration(Cons(BigInt(5), Nil()), Map(T2() -> Some((Pop(), None(), InitState())), T1() -> Some((Push(), Some(BigInt(5)), FinalState())))),
+ Cons(Configuration(Cons(BigInt(5), Nil()), Map(T2() -> Some((Pop(), None(), InitState())), T1() -> None())),
+ Cons(Configuration(Nil(), Map(T2() -> Some((Pop(), None(), ValueState(BigInt(5)))), T1() -> None())),
+ Cons(Configuration(Nil(), Map(T2() -> None(), T1() -> None())), Nil())))))) =>
+ """([], {
+ T1 -> ValueState(5) in Push(5)
+})
+
+
+([5], {
+ T1 -> FinalState in Push(5)
+})
+
+
+([5], {
+ T2 -> InitState in Pop();
+ T1 -> FinalState in Push(5)
+})
+
+
+([5], {
+ T2 -> InitState in Pop();
+ T1 -> idle
+})
+
+
+([], {
+ T2 -> ValueState(5) in Pop();
+ T1 -> idle
+})
+
+
+([], {
+ T2 -> idle;
+ T1 -> idle
+})"""
+
+ }
+ }*/
}
--
GitLab