diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 149940742fd55824e2295f0ad11590c646f418d3..b5cffb4d752dcb9cd21b00fe96ca66e6139df286 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -30,12 +30,12 @@ object Definitions {
case _ => false
}
- def writeScalaFile(filename: String) {
+ def writeScalaFile(filename: String, opgm: Option[Program] = None) {
import java.io.FileWriter
import java.io.BufferedWriter
val fstream = new FileWriter(filename)
val out = new BufferedWriter(fstream)
- out.write(ScalaPrinter(this))
+ out.write(ScalaPrinter(this, opgm = opgm))
out.close()
}
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 1767e38db86b75f6287c73e2d8cc2f00ddd58754..d179cc7eb1ccb03f0172ea1b0f276e64218a010f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -41,16 +41,6 @@ class PrettyPrinter(opts: PrinterOptions,
}
}
- protected def optB(body: => Any)(implicit ctx: PrinterContext) = {
- if (requiresBraces(ctx.current, ctx.parent)) {
- sb.append("{")
- body
- sb.append("}")
- } else {
- body
- }
- }
-
def printWithPath(df: Definition)(implicit ctx: PrinterContext) {
(opgm, ctx.parents.collectFirst { case (d: Definition) => d }) match {
case (Some(pgm), Some(scope)) =>
@@ -91,22 +81,20 @@ class PrettyPrinter(opts: PrinterOptions,
p"$id"
case Let(b,d,e) =>
- optB { d match {
- case _:LetDef | _ : Let | LetPattern(_,_,_) | _:Assert =>
- p"""|val $b = {
- | $d
- |}
- |$e"""
- case _ =>
- p"""|val $b = $d;
- |$e"""
- }}
- case LetDef(fd,body) =>
- optB {
- p"""|$fd
- |$body"""
+ if (isSimpleExpr(d)) {
+ p"""|val $b = $d
+ |$e"""
+ } else {
+ p"""|val $b = {
+ | $d
+ |}
+ |$e"""
}
+ case LetDef(fd,body) =>
+ p"""|$fd
+ |$body"""
+
case Require(pre, body) =>
p"""|require($pre)
|$body"""
@@ -514,39 +502,22 @@ class PrettyPrinter(opts: PrinterOptions,
}
if (fd.canBeStrictField) {
- p"""|val ${fd.id} : ${fd.returnType} = {
- |"""
+ p"val ${fd.id} : "
} else if (fd.canBeLazyField) {
- p"""|lazy val ${fd.id} : ${fd.returnType} = {
- |"""
+ p"lazy val ${fd.id} : "
} else if (fd.tparams.nonEmpty) {
- p"""|def ${fd.id}[${nary(fd.tparams, ",")}](${fd.params}): ${fd.returnType} = {
- |"""
+ p"def ${fd.id}[${nary(fd.tparams, ",")}](${fd.params}): "
} else {
- p"""|def ${fd.id}(${fd.params}): ${fd.returnType} = {
- |"""
- }
-
-
- fd.precondition.foreach { case pre =>
- p"""| require($pre)
- |"""
- }
-
- fd.body match {
- case Some(b) =>
- p" $b"
-
- case None =>
- p" ???"
+ p"def ${fd.id}(${fd.params}): "
}
- p"""|
- |}"""
+ p"${fd.returnType} = "
- fd.postcondition.foreach { post =>
- p"""| ensuring {
- | $post
+ if (isSimpleExpr(fd.fullBody)) {
+ p"${fd.fullBody}"
+ } else {
+ p"""|{
+ | ${fd.fullBody}
|}"""
}
@@ -601,16 +572,9 @@ class PrettyPrinter(opts: PrinterOptions,
}
}
- def requiresBraces(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
- case (pa: PrettyPrintable, _) => pa.printRequiresBraces(within)
- case (_, None) => false
- case (_: LetDef, Some(_: FunDef)) => true
- case (_: Require, Some(_: Ensuring)) => false
- case (_: Require, _) => true
- case (_: Assert, Some(_: Definition)) => true
- case (_, Some(_: Definition)) => false
- case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetDef )) => false
- case (_, _) => true
+ def isSimpleExpr(e: Expr): Boolean = e match {
+ case _: LetDef | _: Let | LetPattern(_, _, _) | _: Assert => false
+ case _ => true
}
def precedence(ex: Expr): Int = ex match {
@@ -658,7 +622,7 @@ class EquivalencePrettyPrinter(opts: PrinterOptions, opgm: Option[Program]) exte
override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
case id: Identifier =>
- p"""${id.name}"""
+ p"${id.name}"
case _ =>
super.pp(tree)
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 0bf34096ce0fc61a98063a9f2e449dd0787a65ff..979ccd38c0f653f0b29214b44f6da1d7da44bc12 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -22,24 +22,24 @@ class ScalaPrinter(opts: PrinterOptions,
case m: ModuleDef =>
// Don't print synthetic functions
super.pp(m.copy(defs = m.defs.filter {
- case f:FunDef if f.isSynthetic => false
+ case f: FunDef if f.isSynthetic => false
case _ => true
}))
- case Not(Equals(l, r)) => p"$l != $r"
- case Implies(l,r) => pp(or(not(l), r))
- case Choose(pred) => p"choose($pred)"
- case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
- case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
+ case Not(Equals(l, r)) => p"$l != $r"
+ case Implies(l,r) => p"$l ==> $r"
+ case Choose(pred) => p"choose($pred)"
+ case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
+ case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
- case ElementOfSet(e,s) => p"$s.contains(e)"
- case SetUnion(l,r) => p"$l ++ $r"
- case MapUnion(l,r) => p"$l ++ $r"
- case SetDifference(l,r) => p"$l -- $r"
- case SetIntersection(l,r) => p"$l & $r"
- case SetCardinality(s) => p"$s.size"
- case InfiniteIntegerLiteral(v) => p"BigInt($v)"
+ case ElementOfSet(e,s) => p"$s.contains(e)"
+ case SetUnion(l,r) => p"$l ++ $r"
+ case MapUnion(l,r) => p"$l ++ $r"
+ case SetDifference(l,r) => p"$l -- $r"
+ case SetIntersection(l,r) => p"$l & $r"
+ case SetCardinality(s) => p"$s.size"
+ case InfiniteIntegerLiteral(v) => p"BigInt($v)"
- case a@FiniteArray(elems, oDef, size) => {
+ case a@FiniteArray(elems, oDef, size) =>
import ExprOps._
val ArrayType(underlying) = a.getType
val default = oDef.getOrElse(simplestValue(underlying))
@@ -63,9 +63,8 @@ class ScalaPrinter(opts: PrinterOptions,
}
}
- }
- case Not(expr) => p"!$expr"
+ case Not(expr) => p"!$expr"
case _ =>
super.pp(tree)
}
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index c79002a2089cbea3f258df179d1a1bd094f87a62..0f2ed5a9c3aa7982a4dab617931bafc44754f363 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -6,13 +6,13 @@ package repair
import purescala.Definitions._
import purescala.DefOps._
-object RepairPhase extends LeonPhase[Program, Program] {
+object RepairPhase extends UnitPhase[Program]() {
val name = "Repair"
val description = "Repairing"
implicit val debugSection = utils.DebugSectionRepair
- def run(ctx: LeonContext)(program: Program): Program = {
+ def apply(ctx: LeonContext, program: Program) = {
val repairFuns: Option[Seq[String]] = ctx.findOption(SharedOptions.optFunctions)
val verifTimeoutMs: Option[Long] = ctx.findOption(SharedOptions.optTimeout) map { _ * 1000 }
@@ -33,6 +33,5 @@ object RepairPhase extends LeonPhase[Program, Program] {
rep.repair()
}
- program
}
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index df6f429051f06df6bf25735c5004b2274a436dcf..ff8cd5a5cde66eb2d3f78d6a565a519ce114f273 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -111,7 +111,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
for ( ((sol, isTrusted), i) <- solutions.zipWithIndex) {
reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+ (if(isTrusted) "" else " (untrusted)" ) + ":"))
val expr = sol.toSimplifiedExpr(ctx, synth.program)
- reporter.info(expr.asString(ctx))
+ reporter.info(expr.asString(program)(ctx))
}
}
} finally {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 1439ca25a9a967ce2f2fa6484f39e5dc7e15868b..5cb59722f058d9f183260b4540bb7f77901ba86b 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -102,7 +102,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
for (fd <- functions) {
ctx.reporter.info(ASCIIHelpers.title(fd.id.name))
- ctx.reporter.info(ScalaPrinter(fd))
+ ctx.reporter.info(ScalaPrinter(fd, opgm = Some(p)))
ctx.reporter.info("")
}
diff --git a/src/main/scala/leon/utils/FileOutputPhase.scala b/src/main/scala/leon/utils/FileOutputPhase.scala
index be92b7086b74357e7ce03b880a03f6d7cb6f812b..3862d9385b2474ad776f030773749f8cc658539e 100644
--- a/src/main/scala/leon/utils/FileOutputPhase.scala
+++ b/src/main/scala/leon/utils/FileOutputPhase.scala
@@ -32,7 +32,7 @@ object FileOutputPhase extends UnitPhase[Program] {
for (u <- p.units if u.isMainUnit) {
val outputFile = s"$outputFolder${File.separator}${u.id.toString}.scala"
- try { u.writeScalaFile(outputFile) }
+ try { u.writeScalaFile(outputFile, Some(p)) }
catch {
case _ : java.io.IOException => ctx.reporter.fatalError("Could not write on " + outputFile)
}