From 664507809f3ec763532447d837345e859ce71c67 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 26 May 2016 11:22:07 +0200
Subject: [PATCH] A.holds.because(B) = A.holds(because(B)) = A.holds(B) = A
holds because (B) = A.holds because(B) = A holds B
---
library/leon/lang/package.scala | 2 +-
.../leon/frontends/scalac/ASTExtractors.scala | 29 ++++++++++++++++++-
.../frontends/scalac/CodeExtraction.scala | 17 ++++++++++-
3 files changed, 45 insertions(+), 3 deletions(-)
diff --git a/library/leon/lang/package.scala b/library/leon/lang/package.scala
index 8898b5637..f9173b6fe 100644
--- a/library/leon/lang/package.scala
+++ b/library/leon/lang/package.scala
@@ -13,7 +13,7 @@ package object lang {
def holds : Boolean = {
underlying
} ensuring {
- _ == true
+ (res: Boolean) => res
}
@inline
def holds(becauseOfThat: Boolean) = {
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 5fb96861d..172380794 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -177,7 +177,7 @@ trait ASTExtractors {
}
}
- /** Matches the `holds` expression at the end of any boolean expression, and return the boolean expression.*/
+ /** Matches the `holds` expression at the end of any boolean expression, and returns the boolean expression.*/
object ExHoldsExpression {
def unapply(tree: Select) : Option[Tree] = tree match {
case Select(
@@ -188,6 +188,33 @@ trait ASTExtractors {
}
}
+ /** Matches the `holds` expression at the end of any boolean expression with a proof as argument, and returns both of themn.*/
+ object ExHoldsWithProofExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case Apply(Select(Apply(ExSelected("leon", "lang", "package", "BooleanDecorations"), body :: Nil), ExNamed("holds")), proof :: Nil) =>
+ Some((body, proof))
+ case _ => None
+ }
+ }
+
+ /** Matches the `because` method at the end of any boolean expression, and return the assertion and the cause. If no "because" method, still returns the expression */
+ object ExMaybeBecauseExpressionWrapper {
+ def unapply(tree: Tree) : Some[Tree] = tree match {
+ case Apply(ExSelected("leon", "lang", "package", "because"), body :: Nil) =>
+ unapply(body)
+ case body => Some(body)
+ }
+ }
+
+ /** Matches the `because` method at the end of any boolean expression, and return the assertion and the cause.*/
+ object ExBecauseExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case Apply(Select(Apply(ExSelected("leon", "proof", "package", "boolean2ProofOps"), body :: Nil), ExNamed("because")), proof :: Nil) =>
+ Some((body, proof))
+ case _ => None
+ }
+ }
+
/** Matches the `bigLength` expression at the end of any string expression, and returns the expression.*/
object ExBigLengthExpression {
def unapply(tree: Apply) : Option[Tree] = tree match {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 99ca8aa07..92829ce8c 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1164,6 +1164,13 @@ trait CodeExtraction extends ASTExtractors {
Ensuring(b, closure)
+ case t @ ExHoldsWithProofExpression(body, ExMaybeBecauseExpressionWrapper(proof)) =>
+ val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
+ val p = extractTreeOrNoTree(proof)
+ val post = Lambda(Seq(LeonValDef(resId)), And(Seq(p, Variable(resId)))).setPos(current.pos)
+ val b = extractTreeOrNoTree(body)
+ Ensuring(b, post)
+
case t @ ExHoldsExpression(body) =>
val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
val post = Lambda(Seq(LeonValDef(resId)), Variable(resId)).setPos(current.pos)
@@ -1171,7 +1178,15 @@ trait CodeExtraction extends ASTExtractors {
val b = extractTreeOrNoTree(body)
Ensuring(b, post)
-
+
+ // If the because statement encompasses a holds statement
+ case t @ ExBecauseExpression(ExHoldsExpression(body), proof) =>
+ val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
+ val p = extractTreeOrNoTree(proof)
+ val post = Lambda(Seq(LeonValDef(resId)), And(Seq(p, Variable(resId)))).setPos(current.pos)
+ val b = extractTreeOrNoTree(body)
+ Ensuring(b, post)
+
case t @ ExComputesExpression(body, expected) =>
val b = extractTreeOrNoTree(body).setPos(body.pos)
val expected_expr = extractTreeOrNoTree(expected).setPos(expected.pos)
--
GitLab