From dc072e8d63b974698d956152427a5e5930c16e2c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 26 Jun 2012 19:05:25 +0200
Subject: [PATCH] integrate waypoint in evaluaiton and better printer for scala
---
src/main/scala/leon/Evaluator.scala | 1 +
.../scala/leon/purescala/ScalaPrinter.scala | 30 +++++++++++--------
2 files changed, 18 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index c3e0ca1a6..d5c5745c1 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -77,6 +77,7 @@ object Evaluator {
case _ => throw TypeErrorEx(TypeError(first, BooleanType))
}
}
+ case Waypoint(_, arg) => rec(ctx, arg)
case FunctionInvocation(fd, args) => {
val evArgs = args.map(a => rec(ctx, a))
// build a context for the function...
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 6018de2ca..501096c45 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -67,7 +67,7 @@ object ScalaPrinter {
case Variable(id) => sb.append(id)
case DeBruijnIndex(idx) => sys.error("Not Valid Scala")
case Let(b,d,e) => {
- sb.append("{\n")
+ sb.append("locally {\n")
ind(sb, lvl+1)
sb.append("val " + b + " = ")
pp(d, sb, lvl+1)
@@ -81,7 +81,7 @@ object ScalaPrinter {
sb
}
case LetVar(b,d,e) => {
- sb.append("{\n")
+ sb.append("locally {\n")
ind(sb, lvl+1)
sb.append("var " + b + " = ")
pp(d, sb, lvl+1)
@@ -496,11 +496,10 @@ object ScalaPrinter {
case fd @ FunDef(id, rt, args, body, pre, post) => {
var nsb = sb
- for(a <- fd.annotations) {
- ind(nsb, lvl)
- nsb.append("@" + a + "\n")
- }
-
+ //for(a <- fd.annotations) {
+ // ind(nsb, lvl)
+ // nsb.append("@" + a + "\n")
+ //}
ind(nsb, lvl)
nsb.append("def ")
@@ -523,7 +522,7 @@ object ScalaPrinter {
nsb.append(") : ")
nsb = pp(rt, nsb, lvl)
- nsb.append(" = ")
+ nsb.append(" = (")
if(body.isDefined) {
pre match {
case None => pp(body.get, nsb, lvl)
@@ -542,11 +541,16 @@ object ScalaPrinter {
} 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(")")
- })
+ post match {
+ case None => {
+ nsb.append(")")
+ }
+ case Some(postc) => {
+ nsb.append(" ensuring(res => ") //TODO, not very general solution...
+ nsb = pp(postc, nsb, lvl)
+ nsb.append("))")
+ }
+ }
nsb
}
--
GitLab