From 1ecef8e84e9a7bc9ca0374c1b45fbe158af16cb0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Thu, 3 Dec 2015 15:48:00 +0100
Subject: [PATCH] Added string conversion. Corrected String render.
---
src/sphinx/synthesis.rst | 44 ++++++++++++++++++-
src/sphinx/verification.rst | 14 ++++++
testcases/stringrender/BinaryTreeRender.scala | 20 ++++-----
3 files changed, 67 insertions(+), 11 deletions(-)
diff --git a/src/sphinx/synthesis.rst b/src/sphinx/synthesis.rst
index b70298a9b..17ed8eab1 100644
--- a/src/sphinx/synthesis.rst
+++ b/src/sphinx/synthesis.rst
@@ -104,7 +104,7 @@ this rule generates two sub-chooses, and combines them as follows:
}
-Inequalite Split
+Inequality Split
^^^^^^^^^^^^^^^^
Given two input variables `a` and `b` of numeric type, this rule
@@ -404,3 +404,45 @@ generally faster way of discovering candidate expressions. However, these
expressions are not guaranteed to be valid since they have only been validated
by tests. Leon's synthesis framework supports untrusted solutions which trigger
an end-to-end validation step that relies on verification.
+
+
+String Conversion
+^^^^^^^^^^^^^^^^^
+
+This rule applies to pretty-printing problems given a non-empty list of examples, i.e. of the type:
+
+.. code-block:: scala
+
+ choose ((x: String) =>
+ (input, x) passes {
+ case InputExample1 => "Output Example1"
+ case InputExample2 => "Output Example2"
+ }
+ )
+
+It will create a set of functions and an expression that will be consistent with the example. The example need to ensure the following properties:
+
+* **Primitive display**: All primitive values (int, boolean, Bigint) present in the InputExample must appear in the OutputExample. The exception being Boolean which can also be rendered differently (e.g. as "yes" and "no")
+* **Linearization**: The output example must use the same order as the definition of InputExample; that is, no Set, Map or out of order rendering (e.g. ``case (1, 2) => "2, 1"`` will not work)
+
+To further optimize the search, it is also better to ensure the following property
+
+* **Constant case class display**: By default, if a hierarchy of case classes only contains parameterless variants, such as
+
+.. code-block:: scala
+
+ abstract class StackThread
+ case class T1() extends StackThread
+ case class T2() extends StackThread
+
+it will first try to render expressions with the following function:
+
+.. code-block:: scala
+
+ def StackThreadToString(t: StackThread) = t match {
+ case T1() => "T1"
+ case T2() => "T2"
+ }
+ CONST + StackThreadToString(t) + CONST
+
+where CONST will be inferred from the examples.
diff --git a/src/sphinx/verification.rst b/src/sphinx/verification.rst
index 10b27b6f7..eed345093 100644
--- a/src/sphinx/verification.rst
+++ b/src/sphinx/verification.rst
@@ -215,3 +215,17 @@ As an example, the following code should issue a warning with Scala:
But Leon will prove that the pattern matching is actually exhaustive,
relying on the given precondition.
+
+Pretty-printing
+---------------
+
+If a global function name ends with "``toString``" with any case, has only one argument and returns a string, this function will be used when printing verification examples. This function can be synthesized (see the synthesis section). For example,
+
+.. code-block:: scala
+
+ def intToString(i: Int) = "#" + i.toString + ",..."
+ def allIntsAreLessThan9(i: Int) = i <= 9 holds
+
+It will display the counter example for ``allIntsAreLessThan9`` as:
+
+ Counter-example: ``#10,...``
diff --git a/testcases/stringrender/BinaryTreeRender.scala b/testcases/stringrender/BinaryTreeRender.scala
index 3805cbbec..3e939217d 100644
--- a/testcases/stringrender/BinaryTreeRender.scala
+++ b/testcases/stringrender/BinaryTreeRender.scala
@@ -1,7 +1,7 @@
/**
* Name: BinaryTreeRender.scala
* Creation: 14.10.2015
- * Author: Mika�l Mayer (mikael.mayer@epfl.ch)
+ * Author: Mikael Mayer (mikael.mayer@epfl.ch)
* Comments: Binary tree rendering specifications.
*/
@@ -13,7 +13,7 @@ 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 Node[T](left: Tree[T], i: T, right: Tree[T]) extends Tree[T]
case class Leaf[T]() extends Tree[T]
/** Synthesis by example specs */
@@ -73,35 +73,35 @@ object TreeRender {
//////////////////////////////////////////////
// Non-incremental examples: pure synthesis //
//////////////////////////////////////////////
- def synthesizeStandard(s: List[Int]): String = {
+ def synthesizeStandard(s: Tree[Int]): String = {
???[String]
} ensuring psStandard(s)
- def synthesizeRemoveNode(s: List[Int]): String = {
+ def synthesizeRemoveNode(s: Tree[Int]): String = {
???[String]
} ensuring psRemoveNode(s)
- def synthesizeRemoveLeaf(s: List[Int]): String = {
+ def synthesizeRemoveLeaf(s: Tree[Int]): String = {
???[String]
} ensuring psRemoveLeaf(s)
- def synthesizeRemoveComma(s: List[Int]): String = {
+ def synthesizeRemoveComma(s: Tree[Int]): String = {
???[String]
} ensuring psRemoveComma(s)
- def synthesizeRemoveParentheses(s: List[Int]): String = {
+ def synthesizeRemoveParentheses(s: Tree[Int]): String = {
???[String]
} ensuring psRemoveParentheses(s)
- def synthesizePrefix(s: List[Int]): String = {
+ def synthesizePrefix(s: Tree[Int]): String = {
???[String]
} ensuring psPrefix(s)
- def synthesizeLispLike(s: List[Int]): String = {
+ def synthesizeLispLike(s: Tree[Int]): String = {
???[String]
} ensuring psLispLike(s)
- def synthesizeSuffix(s: List[Int]): String = {
+ def synthesizeSuffix(s: Tree[Int]): String = {
???[String]
} ensuring psSuffix(s)
}
\ No newline at end of file
--
GitLab