A few small fixes

src/main/scala/inox/ast/Definitions.scala

@@ -78,7 +78,7 @@ trait Definitions { self: Trees =>
     def toVariable: Variable = to[Variable]
     def freshen: ValDef = ValDef(id.freshen, tpe).copiedFrom(this)
 
-    val flags: Set[Annotation] = Set.empty
+    val flags: Set[Flag] = Set.empty
 
     override def equals(that: Any): Boolean = super[VariableSymbol].equals(that)
     override def hashCode: Int = super[VariableSymbol].hashCode
@@ -171,30 +171,30 @@ trait Definitions { self: Trees =>
     def freshen = TypeParameterDef(tp.freshen)
     val id = tp.id
   }
- 
-  // Compiler annotations given in the source code as @annot
-  case class Annotation(val annot: String, val args: Seq[Option[Any]]) extends Printable {
-    def asString(implicit opts: PrinterOptions): String = annot + (if (args.isEmpty) "" else {
-      args.map { case p: Printable => p.asString case arg => arg.toString }.mkString("(", ",", ")")
+
+  /** Represents source code annotations and some other meaningful flags. */
+  abstract class Flag(name: String, args: Seq[Any]) extends Printable {
+    def asString(implicit opts: PrinterOptions): String = name + (if (args.isEmpty) "" else {
+      args.map(arg => self.asString(arg)(opts)).mkString("(", ", ", ")")
     })
   }
 
   /** Denotes that this adt is refined by invariant ''id'' */
-  class HasADTInvariant(id: Identifier) extends Annotation("invariant", Seq(Some(id)))
+  case class HasADTInvariant(id: Identifier) extends Flag("invariant", Seq(id))
 
-  object HasADTInvariant {
-    def apply(id: Identifier): HasADTInvariant = new HasADTInvariant(id)
-    def unapply(annot: Annotation): Option[Identifier] = annot match {
-      case Annotation("invariant", Seq(Some(id: Identifier))) => Some(id)
-      case _ => None
-    }
+  // Compiler annotations given in the source code as @annot
+  case class Annotation(val name: String, val args: Seq[Any]) extends Flag(name, args)
+
+  def extractFlag(name: String, args: Seq[Any]): Flag = (name, args) match {
+    case ("invariant", id: Identifier) => HasADTInvariant(id)
+    case _ => Annotation(name, args)
   }
 
   /** Represents an ADT definition (either the ADT sort or a constructor). */
   sealed trait ADTDefinition extends Definition {
     val id: Identifier
     val tparams: Seq[TypeParameterDef]
-    val flags: Set[Annotation]
+    val flags: Set[Flag]
 
     /** The root of the class hierarchy */
     def root(implicit s: Symbols): ADTDefinition
@@ -221,7 +221,7 @@ trait Definitions { self: Trees =>
   class ADTSort(val id: Identifier,
                 val tparams: Seq[TypeParameterDef],
                 val cons: Seq[Identifier],
-                val flags: Set[Annotation]) extends ADTDefinition {
+                val flags: Set[Flag]) extends ADTDefinition {
     val isSort = true
 
     def constructors(implicit s: Symbols): Seq[ADTConstructor] = cons
@@ -272,7 +272,7 @@ trait Definitions { self: Trees =>
                        val tparams: Seq[TypeParameterDef],
                        val sort: Option[Identifier],
                        val fields: Seq[ValDef],
-                       val flags: Set[Annotation]) extends ADTDefinition {
+                       val flags: Set[Flag]) extends ADTDefinition {
 
     val isSort = false
     /** Returns the index of the field with the specified id */
@@ -355,7 +355,7 @@ trait Definitions { self: Trees =>
     val params: Seq[ValDef],
     val returnType: Type,
     val fullBody: Expr,
-    val flags: Set[Annotation]
+    val flags: Set[Flag]
   ) extends Definition {
 
     /** Wraps this [[FunDef]] in a in [[TypedFunDef]] with the specified type parameters */

src/main/scala/inox/ast/Printers.scala

@@ -77,19 +77,18 @@ trait Printers {
   private val dbquote = "\""
 
   def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
-    ppPrefix(tree)
-    ppBody(tree)
-    ppSuffix(tree)
-  }
-
-  protected def ppPrefix(tree: Tree)(implicit ctx: PrinterContext): Unit = {
     if (requiresBraces(tree, ctx.parent) && !ctx.parent.contains(tree)) {
       p"""|{
           |  $tree
           |}"""
-      return
+    } else {
+      ppPrefix(tree)
+      ppBody(tree)
+      ppSuffix(tree)
     }
+  }
 
+  protected def ppPrefix(tree: Tree)(implicit ctx: PrinterContext): Unit = {
     if (ctx.opts.printTypes) {
       tree match {
         case t: Expr =>
@@ -234,9 +233,9 @@ trait Printers {
     case BVLShiftRight(l, r) => optP {
       p"$l >>> $r"
     }
-    case fs@FiniteSet(rs, _) => p"{${rs.distinct}}"
-    case fs@FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
-    case fm@FiniteMap(rs, _, _) => p"{${rs.toMap.toSeq}}"
+    case fs @ FiniteSet(rs, _) => p"{${rs.distinct}}"
+    case fs @ FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
+    case fm @ FiniteMap(rs, _, _) => p"{${rs.toMap.toSeq}}"
     case Not(ElementOfSet(e, s)) => p"$e \u2209 $s"
     case ElementOfSet(e, s) => p"$e \u2208 $s"
     case SubsetOf(l, r) => p"$l \u2286 $r"
@@ -254,8 +253,8 @@ trait Printers {
 
     case Not(expr) => p"\u00AC$expr"
 
-    case vd@ValDef(id, tpe) =>
-      p"$id : $tpe"
+    case vd @ ValDef(id, tpe) =>
+      p"$id: $tpe"
 
     case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
     case TypeParameterDef(tp) => p"$tp"
@@ -311,20 +310,18 @@ trait Printers {
 
     case fd: FunDef =>
       for (an <- fd.flags) {
-        p"""|@$an
+        p"""|@${an.asString(ctx.opts)}
             |"""
       }
 
       p"def ${fd.id}${nary(fd.tparams, ", ", "[", "]")}"
       if (fd.params.nonEmpty) {
-        p"(${fd.params}): "
+        p"(${fd.params})"
       }
 
-      p"${fd.returnType} = "
+      p": ${fd.returnType} = "
       p"${fd.fullBody}"
 
-    case (tree: PrettyPrintable) => tree.printWith(ctx)
-
     case _ => ctx.sb.append("Tree? (" + tree.getClass + ")")
   }
 
@@ -359,11 +356,10 @@ trait Printers {
 
   protected def isSimpleExpr(e: Expr): Boolean = e match {
     case _: Let => false
-    case p: PrettyPrintable => p.isSimpleExpr
     case _ => true
   }
 
-  protected def noBracesSub(e: Expr): Seq[Expr] = e match {
+  protected def noBracesSub(e: Tree): Seq[Expr] = e match {
     case Let(_, _, bd) => Seq(bd)
     case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
     case _ => Seq()
@@ -371,13 +367,12 @@ trait Printers {
 
   protected def requiresBraces(ex: Tree, within: Option[Tree]) = (ex, within) match {
     case (e: Expr, _) if isSimpleExpr(e) => false
-    case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
+    case (e: Expr, Some(within)) if noBracesSub(within) contains e => false
     case (e: Expr, Some(_)) => true
     case _ => false
   }
 
   protected def precedence(ex: Expr): Int = ex match {
-    case (pa: PrettyPrintable) => pa.printPrecedence
     // 0: Letters
     case (_: ElementOfSet | _: Modulo) => 0
     // 1: |
@@ -403,7 +398,6 @@ trait Printers {
   }
 
   protected def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
-    case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
     case (_, None) => false
     case (_, Some(
     _: Definition | _: Let | _: IfExpr | _: ADT | _: Lambda | _: Choose | _: Tuple
@@ -511,22 +505,16 @@ trait Printers {
     nary(ts.map(typed))
   }
 
-  trait PrettyPrintable {
-    self: Tree =>
-
-    def printWith(implicit pctx: PrinterContext): Unit
-
-    def printPrecedence: Int = 1000
-
-    def printRequiresParentheses(within: Option[Tree]): Boolean = false
-
-    def isSimpleExpr: Boolean = false
-  }
-
   def prettyPrint(tree: Tree, opts: PrinterOptions = PrinterOptions()): String = {
     val ctx = PrinterContext(tree, Nil, opts.baseIndent, opts)
     pp(tree)(ctx)
     ctx.sb.toString
   }
 
+  def asString(obj: Any)(implicit opts: PrinterOptions): String = obj match {
+    case tree: Tree => prettyPrint(tree, opts)
+    case id: Identifier => if (opts.printUniqueIds) id.uniqueName else id.toString
+    case _ => obj.toString
+  }
+
 }