From c511a743de3480793835367d455971dcd337f16b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 17:56:40 +0200
Subject: [PATCH] Some work on printers
---
src/main/scala/inox/ast/Printers.scala | 44 ++++++++++++++++++--------
1 file changed, 31 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 9cab659b5..ddbe81659 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -23,9 +23,12 @@ trait Printers { self: Trees =>
printPositions: Boolean = false,
printUniqueIds: Boolean = false,
printTypes: Boolean = false,
- symbols: Option[Symbols] = None) {
- require(!printTypes || symbols.isDefined,
- "Can't print types without an available symbol table")
+ symbols: Option[Symbols] = None
+ ) {
+ require(
+ !printTypes || symbols.isDefined,
+ "Can't print types without an available symbol table"
+ )
}
object PrinterOptions {
@@ -145,7 +148,7 @@ trait Printers { self: Trees =>
case Application(caller, args) =>
p"$caller($args)"
- case Lambda(Seq(vd), FunctionInvocation(id, Seq(), Seq(arg))) if vd == arg =>
+ case Lambda(Seq(vd), FunctionInvocation(id, Seq(), Seq(arg))) if vd.toVariable == arg =>
p"$id"
case Lambda(args, body) =>
@@ -162,6 +165,8 @@ trait Printers { self: Trees =>
case LessEquals(l,r) => optP { p"$l <= $r" }
case GreaterEquals(l,r) => optP { p"$l >= $r" }
case BVXOr(l,r) => optP { p"$l ^ $r" }
+ case BVOr(l,r) => optP { p"$l | $r" }
+ case BVAnd(l,r) => optP { p"$l & $r" }
case BVShiftLeft(l,r) => optP { p"$l << $r" }
case BVAShiftRight(l,r) => optP { p"$l >> $r" }
case BVLShiftRight(l,r) => optP { p"$l >>> $r" }
@@ -187,7 +192,7 @@ trait Printers { self: Trees =>
case Not(expr) => p"\u00AC$expr"
case vd @ ValDef(id, tpe) =>
- p"$id : ${tpe}"
+ p"$id : $tpe"
case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
case TypeParameterDef(tp) => p"$tp"
@@ -238,7 +243,7 @@ trait Printers { self: Trees =>
ccd.parent.foreach { par =>
// Remember child and parents tparams are simple bijection
- p" extends ${par}${nary(ccd.tparams, ", ", "[", "]")}"
+ p" extends $par${nary(ccd.tparams, ", ", "[", "]")}"
}
case fd: FunDef =>
@@ -312,14 +317,27 @@ trait Printers { self: Trees =>
protected def precedence(ex: Expr): Int = ex match {
case (pa: PrettyPrintable) => pa.printPrecedence
- case (_: ElementOfSet) => 0
- case (_: Modulo) => 1
- case (_: Or) => 2
- case (_: And) => 3
- case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan | _: Implies) => 4
- case (_: Equals | _: Not) => 5
- case (_: Plus | _: Minus | _: SetUnion| _: SetDifference) => 7
+ // 0: Letters
+ case (_: ElementOfSet | _: Modulo) => 0
+ // 1: |
+ case (_: Or | _: BVOr) => 1
+ // 2: ^
+ case (_: BVXOr) => 2
+ // 3: &
+ case (_: And | _: BVAnd | _: SetIntersection) => 3
+ // 4: < >
+ case (
+ _: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan |
+ _: BVAShiftRight | _: BVLShiftRight | _: BVShiftLeft
+ ) => 4
+ // 5: = !
+ case (_: Equals | _: Not | _: Implies) => 5
+ // 6: :
+ // 7: + -
+ case (_: Plus | _: Minus | _: SetUnion | _: SetDifference | _: StringConcat) => 7
+ // 8: * / %
case (_: Times | _: Division | _: Remainder) => 8
+ // 9: Other special characters
case _ => 9
}
--
GitLab