From aa23697f85f44ddd3f37467d8a0bb7e5b92ec120 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 11 Aug 2015 15:17:07 +0200
Subject: [PATCH] Correctly parenthesize implications
---
src/main/scala/leon/purescala/PrettyPrinter.scala | 2 +-
src/main/scala/leon/purescala/ScalaPrinter.scala | 11 +++++------
2 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6952542d6..b36b2e1cc 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -609,7 +609,7 @@ class PrettyPrinter(opts: PrinterOptions,
case (_: Modulo) => 1
case (_: Or | BinaryMethodCall(_, "||", _)) => 2
case (_: And | BinaryMethodCall(_, "&&", _)) => 3
- case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
+ case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan | _: Implies) => 4
case (_: Equals | _: Not) => 5
case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 979ccd38c..5fd883b94 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -25,17 +25,16 @@ class ScalaPrinter(opts: PrinterOptions,
case f: FunDef if f.isSynthetic => false
case _ => true
}))
- case Not(Equals(l, r)) => p"$l != $r"
- case Implies(l,r) => p"$l ==> $r"
+ case Not(Equals(l, r)) => optP { 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 SetUnion(l,r) => optP { p"$l ++ $r" }
+ case MapUnion(l,r) => optP { p"$l ++ $r" }
+ case SetDifference(l,r) => optP { p"$l -- $r" }
+ case SetIntersection(l,r) => optP { p"$l & $r" }
case SetCardinality(s) => p"$s.size"
case InfiniteIntegerLiteral(v) => p"BigInt($v)"
--
GitLab