From 3ecd4e98899c0ca52ae5102fbfb1ed751fd95adf Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 10 Sep 2015 13:36:10 +0200
Subject: [PATCH] req Constructor
---
src/main/scala/leon/purescala/Constructors.scala | 5 +++++
src/main/scala/leon/purescala/ExprOps.scala | 4 ++--
2 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 22697b7df..9d347eccf 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -394,7 +394,12 @@ object Constructors {
} else {
IsInstanceOf(expr, tpe)
}
+ }
+ def req(pred: Expr, body: Expr) = pred match {
+ case BooleanLiteral(true) => body
+ case BooleanLiteral(false) => Error(body.getType, "Precondition failed")
+ case _ => Require(pred, body)
}
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 91d36d7a9..484b468ba 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1741,10 +1741,10 @@ object ExprOps {
* @see [[Expressions.Require]]
*/
def withPrecondition(expr: Expr, pred: Option[Expr]): Expr = (pred, expr) match {
- case (Some(newPre), Require(pre, b)) => Require(newPre, b)
+ case (Some(newPre), Require(pre, b)) => req(newPre, b)
case (Some(newPre), Ensuring(Require(pre, b), p)) => Ensuring(Require(newPre, b), p)
case (Some(newPre), Ensuring(b, p)) => Ensuring(Require(newPre, b), p)
- case (Some(newPre), b) => Require(newPre, b)
+ case (Some(newPre), b) => req(newPre, b)
case (None, Require(pre, b)) => b
case (None, Ensuring(Require(pre, b), p)) => Ensuring(b, p)
case (None, b) => b
--
GitLab