From 639412e333207bd601106fa538ef33a5e34f9bf4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 2 May 2016 18:53:12 +0200
Subject: [PATCH] Add a hard synthesis regression
---
.../regression/synthesis/Misc/RunLength.scala | 50 +++++++++++++++++++
1 file changed, 50 insertions(+)
create mode 100644 src/test/resources/regression/synthesis/Misc/RunLength.scala
diff --git a/src/test/resources/regression/synthesis/Misc/RunLength.scala b/src/test/resources/regression/synthesis/Misc/RunLength.scala
new file mode 100644
index 000000000..1969220be
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Misc/RunLength.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+import leon.collection._
+
+object RunLength {
+
+ def decode[A](l: List[(BigInt, A)]): List[A] = {
+ def fill[A](i: BigInt, a: A): List[A] = {
+ if (i > 0) a :: fill(i - 1, a)
+ else Nil[A]()
+ }
+ l match {
+ case Nil() => Nil[A]()
+ case Cons((i, x), xs) =>
+ fill(i, x) ++ decode(xs)
+ }
+ }
+
+ def legal[A](l: List[(BigInt, A)]): Boolean = l match {
+ case Nil() => true
+ case Cons((i, _), Nil()) => i > 0
+ case Cons((i, x), tl@Cons((_, y), _)) =>
+ i > 0 && x != y && legal(tl)
+ }
+
+ def encode[A](l: List[A]): List[(BigInt, A)] = {
+ // Solution
+ /*l match {
+ case Nil() => Nil[(BigInt, A)]()
+ case Cons(x, xs) =>
+ val rec = encode(xs)
+ rec match {
+ case Nil() =>
+ Cons( (BigInt(1), x), Nil[(BigInt,A)]())
+ case Cons( (recC, recEl), recTl) =>
+ if (x == recEl) {
+ Cons( (1+recC, x), recTl)
+ } else {
+ Cons( (BigInt(1), x), rec )
+ }
+ }
+ }*/
+ ???[List[(BigInt, A)]]
+ } ensuring {
+ (res: List[(BigInt, A)]) =>
+ legal(res) && decode(res) == l
+ }
+
+}
--
GitLab