From a9f697de7e9a3dd18bca72e3ab4cf4cd9232fefb Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 18 May 2016 16:10:45 +0200
Subject: [PATCH] static ensuring
---
library/leon/lang/StaticChecks.scala | 14 ++++++++++++++
.../leon/frontends/scalac/ASTExtractors.scala | 2 ++
2 files changed, 16 insertions(+)
create mode 100644 library/leon/lang/StaticChecks.scala
diff --git a/library/leon/lang/StaticChecks.scala b/library/leon/lang/StaticChecks.scala
new file mode 100644
index 000000000..e53f2def0
--- /dev/null
+++ b/library/leon/lang/StaticChecks.scala
@@ -0,0 +1,14 @@
+package leon.lang
+
+import leon.annotation._
+import scala.language.implicitConversions
+
+object StaticChecks {
+
+ case class Ensuring[A](x: A) {
+ def ensuring(cond: (A) => Boolean): A = x
+ }
+
+ implicit def any2Ensuring[A](x: A): Ensuring[A] = Ensuring(x)
+
+}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 02a58ad29..5fb96861d 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -171,6 +171,8 @@ trait ASTExtractors {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
case Apply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "Ensuring"), _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
=> Some((body, contract))
+ case Apply(Select(Apply(TypeApply(ExSelected("leon", "lang", "StaticChecks", "any2Ensuring"), _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
+ => Some((body, contract))
case _ => None
}
}
--
GitLab