From 8e90ce68249cb85e0e7cf313c6e34c59b436da66 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 19 Aug 2014 13:42:29 +0200
Subject: [PATCH] Some list benchmarks with tests as spec
---
testcases/synthesis/io-examples/Lists.scala | 22 +++++++++++++++++++++
1 file changed, 22 insertions(+)
create mode 100644 testcases/synthesis/io-examples/Lists.scala
diff --git a/testcases/synthesis/io-examples/Lists.scala b/testcases/synthesis/io-examples/Lists.scala
new file mode 100644
index 000000000..62335cc36
--- /dev/null
+++ b/testcases/synthesis/io-examples/Lists.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object Lists {
+
+ def safetail(l: List[Int]): List[Int] = choose { (res : List[Int]) =>
+ passes(l, res)(Map(
+ Cons(1, Cons(2, Cons(3, Cons(4, Nil())))) -> Cons(2, Cons(3, Cons(4, Nil()))),
+ Cons(2, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())),
+ Nil() -> Nil()
+ ))
+ }
+
+ def uniq(l: List[Int]): List[Int] = choose { (res : List[Int]) =>
+ passes(l, res)(Map(
+ Cons(1, Cons(1, Cons(1, Cons(2, Nil())))) -> Cons(1, Cons(2, Nil())),
+ Cons(3, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())),
+ Nil() -> Nil()
+ ))
+ }
+}
--
GitLab