From 3a3715768c86f506e3de3919473757ca22056690 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 1 Sep 2016 15:18:52 +0200
Subject: [PATCH] A few small fixes
---
src/main/scala/inox/ast/Definitions.scala | 34 +++++++-------
src/main/scala/inox/ast/Printers.scala | 56 +++++++++--------------
2 files changed, 39 insertions(+), 51 deletions(-)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index cac42a3e0..b56a5e32e 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/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 */
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index cde78421c..341dd21d2 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/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
+ }
+
}
--
GitLab