From b82deb1ef1d0702529e002c477b17d779f7bc7be Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 17 Mar 2014 21:21:30 +0100
Subject: [PATCH] Pretty printing fixes/improvements
---
.../frontends/scalac/CodeExtraction.scala | 2 +-
.../scala/leon/purescala/PrettyPrinter.scala | 59 ++++++++++++++-----
.../scala/leon/purescala/ScalaPrinter.scala | 15 +++++
.../verification/VerificationCondition.scala | 8 ++-
.../verification/VerificationReport.scala | 1 +
.../regression/frontends/Operators.scala | 9 +++
6 files changed, 76 insertions(+), 18 deletions(-)
create mode 100644 src/test/resources/regression/frontends/Operators.scala
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 149e91bd4..a9502dff9 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -108,7 +108,7 @@ trait CodeExtraction extends ASTExtractors {
class Extraction(units: List[CompilationUnit]) {
private var currentFunDef: FunDef = null
- //This is a bit missleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
+ //This is a bit misleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
//that it can have any owner
private var owners: Map[Identifier, Option[FunDef]] = Map()
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 0973edddb..1c6c95cb1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -125,27 +125,49 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
}
- def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
-
- tree match {
- case id: Identifier =>
- if (opts.printUniqueIds) {
- p"${id.uniqueName}"
+ def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = tree match {
+
+ case id: Identifier =>
+ val name = if (opts.printUniqueIds) {
+ id.uniqueName
} else {
- p"${id.toString}"
+ id.toString
}
-
+ val alphaNumDollar = "[\\w\\$]"
+ // FIXME this does not account for class names with operator symbols
+ def isLegalScalaId(id : String) = id.matches(
+ s"${alphaNumDollar}+|[${alphaNumDollar}+_]?[!@#%^&*+-\\|~/?><:]+"
+ )
+ // Replace $opname with operator symbols
+ val candidate = scala.reflect.NameTransformer.decode(name)
+
+ if (isLegalScalaId(candidate)) p"$candidate" else p"$name"
+
case Variable(id) =>
p"$id"
case LetTuple(bs,d,e) =>
- p"""|val ($bs) = $d;
- |$e"""
-
+ e match {
+ case _:LetDef | _ : Let | _ : LetTuple =>
+ p"""|val ($bs) = {
+ | $d
+ |}
+ |$e"""
+ case _ =>
+ p"""|val ($bs) = $d;
+ |$e"""
+ }
case Let(b,d,e) =>
- p"""|val $b = $d;
- |$e"""
-
+ e match {
+ case _:LetDef | _ : Let | _ : LetTuple =>
+ p"""|val $b = {
+ | $d
+ |}
+ |$e"""
+ case _ =>
+ p"""|val $b = $d;
+ |$e"""
+ }
case LetDef(fd,body) =>
p"""|$fd
|$body"""
@@ -391,7 +413,11 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
parent.foreach{ par =>
- p" extends ${par.id}"
+ if (par.tps.nonEmpty){
+ p" extends ${par.id}[${par.tps}]"
+ } else {
+ p" extends ${par.id}"
+ }
}
if (ccd.methods.nonEmpty) {
@@ -435,7 +461,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (tree: PrettyPrintable) => tree.printWith(ctx)
case _ => sb.append("Tree? (" + tree.getClass + ")")
- }
+
}
def requiresBraces(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
@@ -471,6 +497,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef | _: IfExpr)) => false
case (_, Some(_: FunctionInvocation)) => false
case (ie: IfExpr, _) => true
+ case (me: MatchExpr, _ ) => true
case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
case (_, _) => true
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 4807224e5..74ff651d1 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -12,8 +12,15 @@ import PrinterHelpers._
/** This pretty-printer only print valid scala syntax */
class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, sb) {
+ import Common._
+ import Trees._
+ import TypeTrees._
+ import Definitions._
+
+ import java.lang.StringBuffer
override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+
tree match {
case Not(Equals(l, r)) => p"$l != $r"
case Iff(l,r) => p"$l == $r"
@@ -27,6 +34,14 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
p"Set($rs)"
}
}
+ case m @ FiniteMap(els) => {
+ m.getType match {
+ case MapType(k,v) =>
+ p"Map[$k,$v]($els)"
+ case _ =>
+ p"Map($els)"
+ }
+ }
case ElementOfSet(e,s) => p"$s.contains(e)"
case SetUnion(l,r) => p"$l ++ $r"
case MapUnion(l,r) => p"$l ++ $r"
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index fd03419d4..4e690547d 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -13,7 +13,7 @@ import leon.solvers._
class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind, val tactic: Tactic, val info: String = "") extends Positioned {
// None = still unknown
// Some(true) = valid
- // Some(false) = valid
+ // Some(false) = invalid
var hasValue = false
var value : Option[Boolean] = None
var solvedWith : Option[Solver] = None
@@ -35,6 +35,12 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
case Some(s) => s.name
case None => ""
}
+
+ override def toString = {
+ kind.toString + " in function " + funDef.id.name + "\n" +
+ condition.toString
+ }
+
}
abstract class VCKind(val name: String, val abbrv: String) {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index b6522f5a6..59d4ef4e6 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -4,6 +4,7 @@ package leon
package verification
import purescala.Definitions.FunDef
+import purescala.ScalaPrinter
class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
import scala.math.Ordering.Implicits._
diff --git a/src/test/resources/regression/frontends/Operators.scala b/src/test/resources/regression/frontends/Operators.scala
new file mode 100644
index 000000000..d91673051
--- /dev/null
+++ b/src/test/resources/regression/frontends/Operators.scala
@@ -0,0 +1,9 @@
+object Operators {
+
+ case class HasOps(i : Int){
+ def + (j : HasOps) = this.i + j.i
+ }
+
+ def x = HasOps(12) + HasOps(30)
+
+}
\ No newline at end of file
--
GitLab