From 1aa65ccb60905320dea16bb20a5b4d5e4ba57ff1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 16:57:29 +0200
Subject: [PATCH] Add choose with return types, example
---
library/Utils.scala | 14 +++++++-------
testcases/Choose.scala | 7 +++++++
2 files changed, 14 insertions(+), 7 deletions(-)
create mode 100644 testcases/Choose.scala
diff --git a/library/Utils.scala b/library/Utils.scala
index 44b05cd36..12c81d7a0 100644
--- a/library/Utils.scala
+++ b/library/Utils.scala
@@ -22,11 +22,11 @@ object Utils {
private def noChoose = throw new RuntimeException("Implementation not supported")
- def choose[A](predicate: A => Boolean) = noChoose
- def choose[A, B](predicate: (A, B) => Boolean) = noChoose
- def choose[A, B, C](predicate: (A, B, C) => Boolean) = noChoose
- def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean) = noChoose
- def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean) = noChoose
- def choose[A, B, C, D, E, F](predicate: (A, B, C, D, E, F) => Boolean) = noChoose
- def choose[A, B, C, D, E, F, G](predicate: (A, B, C, D, E, F, G) => Boolean) = noChoose
+ def choose[A](predicate: A => Boolean): A = noChoose
+ def choose[A, B](predicate: (A, B) => Boolean): (A, B) = noChoose
+ def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noChoose
+ def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose
+ def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose
+ def choose[A, B, C, D, E, F](predicate: (A, B, C, D, E, F) => Boolean): (A, B, C, D, E, F) = noChoose
+ def choose[A, B, C, D, E, F, G](predicate: (A, B, C, D, E, F, G) => Boolean): (A, B, C, D, E, F, G) = noChoose
}
diff --git a/testcases/Choose.scala b/testcases/Choose.scala
new file mode 100644
index 000000000..22dbc18f4
--- /dev/null
+++ b/testcases/Choose.scala
@@ -0,0 +1,7 @@
+import leon.Utils._
+
+object Abs {
+
+ def abs(x: Int): Int = choose{ x: Int => x > 0 }
+
+}
--
GitLab