From 4bd8ac56ee86005539bd08984e38c123128e4d52 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 22 Jan 2016 16:00:02 +0100
Subject: [PATCH] Fix bug with multiparameter ensuring specs
---
.../scala/leon/codegen/CodeGeneration.scala | 2 +-
.../scala/leon/purescala/Constructors.scala | 4 ++++
src/main/scala/leon/purescala/ExprOps.scala | 17 ++++++++++++++---
3 files changed, 19 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 6d70782ad..8b3dd1463 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -207,7 +207,7 @@ trait CodeGeneration {
val bodyWithPost = funDef.postcondition match {
case Some(post) if params.checkContracts =>
- Ensuring(bodyWithPre, post).toAssert
+ ensur(bodyWithPre, post).toAssert
case _ => bodyWithPre
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index a5ef87e1d..1be21b20f 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -405,4 +405,8 @@ object Constructors {
case _ => Require(pred, body)
}
+ def ensur(e: Expr, pred: Expr) = {
+ Ensuring(e, tupleWrapArg(pred))
+ }
+
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 4f6c968f3..38915fe51 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1941,8 +1941,8 @@ object ExprOps {
* @see [[Expressions.Require]]
*/
def withPostcondition(expr: Expr, oie: Option[Expr]) = (oie, expr) match {
- case (Some(npost), Ensuring(b, post)) => Ensuring(b, npost)
- case (Some(npost), b) => Ensuring(b, npost)
+ case (Some(npost), Ensuring(b, post)) => ensur(b, npost)
+ case (Some(npost), b) => ensur(b, npost)
case (None, Ensuring(b, p)) => b
case (None, b) => b
}
@@ -2217,6 +2217,17 @@ object ExprOps {
)
}
-
+ def tupleWrapArg(fun: Expr) = fun.getType match {
+ case FunctionType(args, res) if args.size > 1 =>
+ val newArgs = fun match {
+ case Lambda(args, _) => args map (_.id)
+ case _ => args map (arg => FreshIdentifier("x", arg.getType, alwaysShowUniqueID = true))
+ }
+ val res = FreshIdentifier("res", TupleType(args map (_.getType)), alwaysShowUniqueID = true)
+ val patt = TuplePattern(None, newArgs map (arg => WildcardPattern(Some(arg))))
+ Lambda(Seq(ValDef(res)), MatchExpr(res.toVariable, Seq(SimpleCase(patt, application(fun, newArgs map (_.toVariable))))))
+ case _ =>
+ fun
+ }
}
--
GitLab