From d53a135d944724ded87ba1d87129f3bc4e24add6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 17 May 2012 16:50:44 +0200
Subject: [PATCH] print post condition as ensuring and precondition as require
---
.../scala/leon/purescala/ScalaPrinter.scala | 47 ++++++++++---------
1 file changed, 26 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 31ede51a8..689e3c394 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -372,7 +372,7 @@ object ScalaPrinter {
nsb
}
- case ResultVariable() => sb.append("#res")
+ case ResultVariable() => sb.append("res")
case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col)
case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg
@@ -434,10 +434,7 @@ object ScalaPrinter {
defn match {
case Program(id, mainObj) => {
assert(lvl == 0)
- sb.append("package ")
- sb.append(id)
- sb.append(" {\n")
- pp(mainObj, sb, lvl+1).append("}\n")
+ pp(mainObj, sb, lvl)
}
case ObjectDef(id, defs, invs) => {
@@ -502,19 +499,6 @@ object ScalaPrinter {
nsb.append("@" + a + "\n")
}
- pre.foreach(prec => {
- ind(nsb, lvl)
- nsb.append("@pre : ")
- nsb = pp(prec, nsb, lvl)
- nsb.append("\n")
- })
-
- post.foreach(postc => {
- ind(nsb, lvl)
- nsb.append("@post: ")
- nsb = pp(postc, nsb, lvl)
- nsb.append("\n")
- })
ind(nsb, lvl)
nsb.append("def ")
@@ -538,10 +522,31 @@ object ScalaPrinter {
nsb.append(") : ")
nsb = pp(rt, nsb, lvl)
nsb.append(" = ")
- if(body.isDefined)
- pp(body.get, nsb, lvl)
- else
+ if(body.isDefined) {
+ pre match {
+ case None => pp(body.get, nsb, lvl)
+ case Some(prec) => {
+ nsb.append("{\n")
+ ind(nsb, lvl+1)
+ nsb.append("require(")
+ nsb = pp(prec, nsb, lvl+1)
+ nsb.append(")\n")
+ pp(body.get, nsb, lvl+1)
+ nsb.append("\n")
+ ind(nsb, lvl)
+ nsb.append("}")
+ }
+ }
+ } else
nsb.append("[unknown function implementation]")
+
+ post.foreach(postc => {
+ nsb.append(" ensuring(res => ") //TODO, not very general solution...
+ nsb = pp(postc, nsb, lvl)
+ nsb.append(")")
+ })
+
+ nsb
}
case _ => sb.append("Defn?")
--
GitLab