From 12116bae7f03be38f188698172cab814c8f2867a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 30 Mar 2015 18:30:19 +0200
Subject: [PATCH] Refactor boolean decorations, add ==>
---
library/lang/package.scala | 12 +++++-----
.../leon/frontends/scalac/ASTExtractors.scala | 23 +++++++++++++++++--
.../frontends/scalac/CodeExtraction.scala | 2 ++
3 files changed, 29 insertions(+), 8 deletions(-)
diff --git a/library/lang/package.scala b/library/lang/package.scala
index a80e25cba..a598c251e 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -7,16 +7,16 @@ import scala.language.implicitConversions
package object lang {
@ignore
- sealed class IsValid(val property : Boolean) {
+ implicit class BooleanDecorations(val underlying: Boolean) {
def holds : Boolean = {
- assert(property)
- property
+ assert(underlying)
+ underlying
+ }
+ def ==> (that: Boolean): Boolean = {
+ !underlying || that
}
}
- @ignore
- implicit def any2IsValid(x: Boolean) : IsValid = new IsValid(x)
-
@ignore
object InvariantFunction {
def invariant(x: Boolean): Unit = ()
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 06ab50a2e..3d8df24e1 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -155,12 +155,31 @@ trait ASTExtractors {
object ExHoldsExpression {
def unapply(tree: Select) : Option[Tree] = tree match {
- case Select(Apply(ExSymbol("leon", "lang", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
- Some(realExpr)
+ case Select(
+ Apply(ExSelected("leon", "lang", "package", "BooleanDecorations"), realExpr :: Nil),
+ ExNamed("holds")
+ ) => Some(realExpr)
case _ => None
}
}
+ object ExImplies {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case
+ Apply(
+ Select(
+ Apply(
+ ExSelected("leon", "lang", "package", "BooleanDecorations"),
+ lhs :: Nil
+ ),
+ ExNamed("$eq$eq$greater")
+ ),
+ rhs :: Nil
+ ) => Some((lhs, rhs))
+ case _ => None
+ }
+ }
+
object ExRequiredExpression {
/** Extracts the 'require' contract from an expression (only if it's the
* first call in the block). */
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3d89df12e..9e209b5d5 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1541,6 +1541,8 @@ trait CodeExtraction extends ASTExtractors {
CaseClass(CaseClassType(libraryCaseClass(str.pos, "leon.lang.string.String"), Seq()), Seq(charList))
+ case ExImplies(lhs, rhs) =>
+ Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos)
case c @ ExCall(rec, sym, tps, args) =>
val rrec = rec match {
--
GitLab