From e9e458f0eae66a220468c749f2800f52c2853ef1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Sun, 22 Nov 2015 02:46:17 +0100
Subject: [PATCH] Top-level chooses have their spec extracted
---
.../leon/synthesis/ConversionPhase.scala | 22 ++++++++++++++++++-
1 file changed, 21 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index d76cff69b..366037b2a 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -76,6 +76,18 @@ object ConversionPhase extends UnitPhase[Program] {
* choose(x => post(x))
* }
*
+ * 4) Functions that have only a choose as body gets their spec from the choose.
+ *
+ * def foo(a: T) = {
+ * choose(x => post(a, x))
+ * }
+ *
+ * gets converted to:
+ *
+ * def foo(a: T) = {
+ * choose(x => post(a, x))
+ * } ensuring { x => post(a, x) }
+ *
*/
def convert(e : Expr, ctx : LeonContext) : Expr = {
@@ -115,7 +127,7 @@ object ConversionPhase extends UnitPhase[Program] {
}
}
- body match {
+ val fullBody = body match {
case Some(body) =>
var holes = List[Identifier]()
@@ -172,6 +184,14 @@ object ConversionPhase extends UnitPhase[Program] {
val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
withPrecondition(Choose(newPost), pre)
}
+
+ // extract spec from chooses at the top-level
+ fullBody match {
+ case Choose(spec) =>
+ withPostcondition(fullBody, Some(spec))
+ case _ =>
+ fullBody
+ }
}
--
GitLab