Merge pull request #1091 from utwente-fmt/issue-1080

Make printing nodes in verificationerrors easier

src/col/vct/col/ast/node/NodeImpl.scala

@@ -52,7 +52,7 @@ trait NodeImpl[G] extends Show { this: Node[G] =>
     if(childrenErrors.nonEmpty) {
       childrenErrors
     } else {
-      VerificationError.context(CurrentCheckNodeContext(this)) {
+      VerificationError.withContext(CurrentCheckNodeContext(this)) {
         check(context)
       }
     }
@@ -128,9 +128,11 @@ trait NodeImpl[G] extends Show { this: Node[G] =>
     Group(show).toStringWithContext
   }
 
-
-  def messageInContext(node: Node[_], message: String): String = {
+  def bareMessageInContext(node: Node[_], message: String): String = {
     implicit val ctx: Ctx = Ctx().namesIn(this)
-    BOLD_HR + this.show.highlight(node).strip() + "\n" + HR + message + "\n" + BOLD_HR
+    this.show.highlight(node).strip() + "\n" + HR + message + "\n"
   }
+
+  def messageInContext(node: Node[_], message: String): String =
+    BOLD_HR + bareMessageInContext(node, message) + BOLD_HR
 }

src/col/vct/col/ast/node/ProgramImpl.scala

@@ -4,14 +4,14 @@ import vct.col.ast.{Node, Program}
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
 import vct.col.print.{Ctx, Doc}
-import vct.col.util.CurrentProgramCheckContext
+import vct.col.util.CurrentCheckProgramContext
 import vct.result.VerificationError
 
 trait ProgramImpl[G] extends Declarator[G] { this: Program[G] =>
   def check: Seq[CheckError] = checkTrans(CheckContext())
 
   override def checkContextRecursor[T](context: CheckContext[G], f: (CheckContext[G], Node[G]) => T): Seq[T] =
-    VerificationError.context(CurrentProgramCheckContext(this)) {
+    VerificationError.withContext(CurrentCheckProgramContext(this)) {
       super.checkContextRecursor(context, f)
     }
 

src/col/vct/col/ast/statement/StatementImpl.scala

@@ -6,7 +6,7 @@ import vct.col.print._
 
 trait StatementImpl[G] extends NodeFamilyImpl[G] { this: Statement[G] =>
   def layoutAsBlock(implicit ctx: Ctx): Doc =
-    Text("{") <>> Doc.stack(blockElementsForLayout) <+/> "}"
+    Text("{") <>> foldBlock(_ <+/> _) <+/> "}"
 
-  def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] = Seq(this)
+  def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = show
 }

src/col/vct/col/ast/statement/composite/BlockImpl.scala

@@ -5,6 +5,5 @@ import vct.col.print._
 
 trait BlockImpl[G] { this: Block[G] =>
   override def layout(implicit ctx: Ctx): Doc = layoutAsBlock
-  override def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] =
-    statements.flatMap(_.blockElementsForLayout)
+  override def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = NodeDoc(this, Doc.fold(statements.map(_.foldBlock(f)))(f))
 }

src/col/vct/col/ast/statement/composite/LoopImpl.scala

@@ -77,19 +77,26 @@ trait LoopImpl[G] { this: Loop[G] =>
       Group(Text("while") <+> "(" <> Doc.arg(cond) <> ")") <+> body.layoutAsBlock
     ))
 
-  def layoutControlElement(e: Show)(implicit ctx: Ctx): Option[Show] = Some(e match {
-    case Eval(e) => e.show
-    case a: Assign[G] => a.layoutAsExpr
-    case e: VeyMontAssignExpression[G] => return layoutControlElement(e.assign)
-    case e: VeyMontCommExpression[G] => return layoutControlElement(e.assign)
-    case LocalDecl(local) => local.show
-    case JavaLocalDeclarationStatement(local) => local.show
-
-    case _ => return None
-  })
+  def simpleControlElements(stat: Statement[G])(implicit ctx: Ctx): Option[Doc] = stat match {
+    case Eval(e) => Some(e.show)
+    case a: Assign[G] => Some(a.layoutAsExpr)
+    case e: VeyMontAssignExpression[G] => simpleControlElements(e.assign)
+    case e: VeyMontCommExpression[G] => simpleControlElements(e.assign)
+    case LocalDecl(local) => Some(local.show)
+    case JavaLocalDeclarationStatement(local) => Some(local.show)
+
+    case Block(stats) =>
+      stats
+        .map(simpleControlElements(_))
+        .foldLeft[Option[Seq[Doc]]](Some(Nil)) {
+          case (Some(acc), Some(more)) => Some(acc :+ more)
+          case (_, _) => None
+        }
+        .map(elems => NodeDoc(stat, Doc.fold(elems)(_ <> "," <+/> _)))
+  }
 
   def layoutControl(stat: Statement[G])(implicit ctx: Ctx): Doc =
-    Group(Doc.args(stat.blockElementsForLayout.map(layoutControlElement(_).getOrElse(return stat.show))))
+    simpleControlElements(stat).map(doc => Group(Doc.arg(doc))).getOrElse(stat.show)
 
   def layoutGenericFor(implicit ctx: Ctx): Doc =
     Doc.stack(Seq(

src/col/vct/col/ast/statement/composite/ScopeImpl.scala

@@ -11,9 +11,11 @@ trait ScopeImpl[G] {
     context.withScope(locals, toScan = Seq(body))
 
   override def layout(implicit ctx: Ctx): Doc = layoutAsBlock
-  override def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] =
-    locals.map(local => ctx.syntax match {
-      case Ctx.Silver => Text("var") <+> local
-      case _ => local.show <> ";"
-    }) ++ body.blockElementsForLayout
+  override def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc =
+    NodeDoc(this,
+      Doc.fold(locals.map(local => ctx.syntax match {
+        case Ctx.Silver => Text("var") <+> local
+        case _ => local.show <> ";"
+      }) :+ body.foldBlock(f))(f)
+    )
 }

src/col/vct/col/ast/statement/composite/SwitchImpl.scala

@@ -13,30 +13,6 @@ trait SwitchImpl[G] { this: Switch[G] =>
 
   def isNotCase(s: Show): Boolean = !isCase(s)
 
-  @tailrec
-  private def layoutContentWithCaseLabel(content: Seq[Show], acc: Show)(implicit ctx: Ctx): Show = {
-    if(content.isEmpty) acc
-    else {
-      val label = content.head
-      val more = content.tail
-      val (uncased, casePrefix) = more.span(isNotCase)
-      val newAcc = acc.show <+/> label <> Nest(Line <> Doc.stack(uncased))
-      layoutContentWithCaseLabel(casePrefix, newAcc)
-    }
-  }
-
-  def layoutContent(implicit ctx: Ctx): Doc = {
-    val elements = body.blockElementsForLayout
-    val (uncased, casePrefix) = elements.span(isNotCase)
-
-    if(casePrefix.isEmpty) {
-      // PB: very weird switch, or we just can't peek through blocks
-      Line <> Doc.stack(uncased)
-    } else {
-      Nest(Line <> Doc.stack(uncased)) <> layoutContentWithCaseLabel(casePrefix, Empty)
-    }
-  }
-
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("switch") <+> "(" <> Doc.arg(expr) <> ")") <+> "{" <> Nest(layoutContent) <+/> "}"
+    Group(Text("switch") <+> "(" <> Doc.arg(expr) <> ")") <+> "{" <>> body.foldBlock(_ <+/> _) <+/> "}"
 }

src/col/vct/col/ast/statement/terminal/FramedProofImpl.scala

@@ -13,7 +13,7 @@ trait FramedProofImpl[G] { this: FramedProof[G] =>
     ))
 
   def layoutWithSpec(implicit ctx: Ctx): Doc =
-    Doc.spec(Show.lazily(frameHeader(_))) <+/> Doc.stack(body.blockElementsForLayout) <+/> Doc.inlineSpec(Text("}"))
+    Doc.spec(Show.lazily(frameHeader(_))) <+/> body.foldBlock(_ <+/> _) <+/> Doc.inlineSpec(Text("}"))
 
   def layoutNative(implicit ctx: Ctx): Doc =
     Doc.stack(Seq(

src/col/vct/col/ast/statement/terminal/LabelImpl.scala

@@ -1,23 +1,22 @@
 package vct.col.ast.statement.terminal
 
 import vct.col.ast.Label
-import vct.col.print.{Ctx, Doc, Show, Text}
+import vct.col.print.{Ctx, Doc, NodeDoc, Show, Text}
 
 trait LabelImpl[G] { this: Label[G] =>
-  override def blockElementsForLayout(implicit ctx: Ctx): Seq[Show] = ctx.syntax match {
-    case Ctx.PVL => Seq(layoutLabel) ++ stat.blockElementsForLayout
-    case Ctx.Silver => Seq(layoutLabel) ++ stat.blockElementsForLayout
-    case Ctx.Java => Seq(this)
-    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Seq(layoutLabel) ++ stat.blockElementsForLayout
+  override def foldBlock(f: (Doc, Doc) => Doc)(implicit ctx: Ctx): Doc = ctx.syntax match {
+    case Ctx.PVL => f(layoutLabel, stat.foldBlock(f))
+    case Ctx.Silver => f(layoutLabel, stat.foldBlock(f))
+    case Ctx.Java => layoutLabel <+> stat.show
+    case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => f(layoutLabel, stat.foldBlock(f))
   }
 
-  def layoutLabel(implicit ctx: Ctx): Doc = ctx.syntax match {
+  def layoutLabel(implicit ctx: Ctx): Doc = NodeDoc(this, ctx.syntax match {
     case Ctx.PVL => Text("label") <+> ctx.name(decl) <> ";"
     case Ctx.Silver => Text("label") <+> ctx.name(decl)
     case Ctx.Java => Text(ctx.name(decl)) <> ":"
     case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => Text(ctx.name(decl)) <> ":"
-  }
+  })
 
-  override def layout(implicit ctx: Ctx): Doc =
-    Doc.stack(blockElementsForLayout)
+  override def layout(implicit ctx: Ctx): Doc = foldBlock(_ <+/> _)
 }

src/col/vct/col/check/Check.scala

@@ -16,50 +16,47 @@ case object Check {
 }
 
 sealed trait CheckError {
-  override def toString: String = this match {
+  def message(context: (Node[_], String) => String): String = (this match {
     case TypeError(expr, _) if expr.t.isInstanceOf[TNotAValue[_]] =>
-      expr.o.messageInContext(s"This expression is not a value.")
+      Seq(context(expr, s"This expression is not a value."))
     case TypeErrorText(expr, _) if expr.t.isInstanceOf[TNotAValue[_]] =>
-      expr.o.messageInContext(s"This expression is not a value.")
+      Seq(context(expr, s"This expression is not a value."))
     case TypeError(expr, expectedType) =>
-      expr.o.messageInContext(s"Expected the type of this expression to be `$expectedType`, but got ${expr.t}.")
+      Seq(context(expr, s"Expected the type of this expression to be `$expectedType`, but got ${expr.t}."))
     case TypeErrorText(expr, expectedType) =>
-      expr.o.messageInContext(s"Expected the type of this expression to be $expectedType, but got ${expr.t}.")
+      Seq(context(expr, s"Expected the type of this expression to be $expectedType, but got ${expr.t}."))
     case TypeErrorExplanation(expr, message) =>
-      expr.o.messageInContext(message)
+      Seq(context(expr, message))
     case GenericTypeError(t, expectedType) =>
-      t.o.messageInContext(s"This type variable refers to a name that is not actually a type.")
+      Seq(context(t, s"This type variable refers to a name that is not actually a type."))
     case OutOfScopeError(use, ref) =>
-      Origin.messagesInContext(Seq(
-        (use.o, "This usage is out of scope,"),
-        (ref.decl.o, "since it is declared here.")
-      ))
+      Seq(context(use, "This usage is out of scope,"), context(ref.decl, "since it is declared here."))
     case OutOfWriteScopeError(reason, use, ref) =>
-      Origin.messagesInContext(Seq(
-        (use.o, "This may not be rewritten to, since ..."),
-        (reason.o, "declarations outside this node must not be altered, and ..."),
-        (ref.decl.o, "... it is declared here.")
-      ))
+      Seq(
+        context(use, "This may not be rewritten to, since ..."),
+        context(reason, "declarations outside this node must not be altered, and ..."),
+        context(ref.decl, "... it is declared here."),
+      )
     case DoesNotDefine(declarator, declaration, use) =>
-      Origin.messagesInContext(Seq(
-        (use.o, "This uses a declaration, which is declared"),
-        (declaration.o, "here, but it was expected to be declared"),
-        (declarator.o, "in this declarator."),
-      ))
+      Seq(
+        context(use, "This uses a declaration, which is declared"),
+        context(declaration, "here, but it was expected to be declared"),
+        context(declarator.asInstanceOf[Node[_]], "in this declarator."),
+      )
     // TODO PB: these are kind of obsolete? maybe?
     case IncomparableTypes(left, right) =>
       ???
     case TupleTypeCount(tup) =>
       ???
     case NotAPredicateApplication(res) =>
-      res.o.messageInContext("This expression is not a (scaled) predicate application")
+      Seq(context(res, "This expression is not a (scaled) predicate application"))
     case AbstractPredicate(res) =>
-      res.o.messageInContext("This predicate is abstract, and hence cannot be meaningfully folded or unfolded")
+      Seq(context(res, "This predicate is abstract, and hence cannot be meaningfully folded or unfolded"))
     case RedundantCatchClause(clause) =>
-      clause.o.messageInContext("This catch clause is redundant, because it is subsumed by the caught types of earlier catch clauses in this block.")
+      Seq(context(clause, "This catch clause is redundant, because it is subsumed by the caught types of earlier catch clauses in this block."))
     case ResultOutsidePostcondition(res) =>
-      res.o.messageInContext("\\result may only occur in the postcondition.")
-  }
+      Seq(context(res, "\\result may only occur in the postcondition."))
+  }).mkString(Origin.BOLD_HR, Origin.HR, Origin.BOLD_HR)
 }
 case class TypeError(expr: Expr[_], expectedType: Type[_]) extends CheckError
 case class TypeErrorText(expr: Expr[_], expectedType: String) extends CheckError

src/col/vct/col/origin/Origin.scala

@@ -208,14 +208,18 @@ case class Origin(originContents: Seq[OriginContent]) extends Blame[Verification
     }
   }
 
-  def messageInContext(message: String): String = {
+  def bareMessageInContext(message: String): String = {
     val contextMessage = getContext match {
       case Some(value) => value.context.strip()
       case None => "[unknown context]"
     }
-    BOLD_HR + contextMessage + "\n" + HR + message + "\n" + BOLD_HR
+
+    contextMessage + "\n" + HR + message + "\n"
   }
 
+  def messageInContext(message: String): String =
+    BOLD_HR + bareMessageInContext(message) + BOLD_HR
+
   override def blame(error: VerificationFailure): Unit = {
     Logger("vct").error(error.toString)
   }

src/col/vct/col/rewrite/NonLatchingRewriter.scala

@@ -1,14 +1,14 @@
 package vct.col.rewrite
 
 import vct.col.ast._
-import vct.col.util.CurrentProgramRewriteContext
+import vct.col.util.CurrentRewriteProgramContext
 import vct.result.VerificationError
 
 class NonLatchingRewriter[Pre, Post]() extends AbstractRewriter[Pre, Post] {
   override def dispatch(context: Verification[Pre]): Verification[Post] = rewriteDefault(context)
   override def dispatch(context: VerificationContext[Pre]): VerificationContext[Post] = rewriteDefault(context)
   override def dispatch(program: Program[Pre]): Program[Post] =
-    VerificationError.context(CurrentProgramRewriteContext(program)) {
+    VerificationError.withContext(CurrentRewriteProgramContext(program)) {
       rewriteDefault(program)
     }
 

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -18,12 +18,14 @@ case class NopCoercingRewriter[Pre <: Generation]() extends CoercingRewriter[Pre
 case object CoercingRewriter {
   sealed trait CoercionError extends SystemError {
     override def text: String =
-      "Internal type error: CoercionErrors must not bubble. " + (this match {
-        case IncoercibleDummy => "(No alternative matched, see stack trace)"
-        case Incoercible(e, target) => s"Expression `$e` could not be coerced to `$target``"
-        case IncoercibleText(e, target) => s"Expression `$e` could not be coerced to $target."
-        case IncoercibleExplanation(e, message) => s"At `$e`: $message"
-      })
+      messageContext(
+        "Internal type error: CoercionErrors must not bubble. " + (this match {
+          case IncoercibleDummy => "(No alternative matched, see stack trace)"
+          case Incoercible(e, target) => s"Expression `$e` could not be coerced to `$target``"
+          case IncoercibleText(e, target) => s"Expression `$e` could not be coerced to $target."
+          case IncoercibleExplanation(e, message) => s"At `$e`: $message"
+        })
+      )
   }
 
   case object IncoercibleDummy extends CoercionError

src/col/vct/col/util/ConstructingSuccessorOfContext.scala

@@ -1,6 +1,14 @@
 package vct.col.util
 
 import vct.col.ast.Declaration
+import vct.col.print.Doc
 import vct.result.VerificationError
 
-case class ConstructingSuccessorOfContext(decl: Declaration[_]) extends VerificationError.Context
+case class ConstructingSuccessorOfContext(decl: Declaration[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    err.context[CurrentRewriteProgramContext].map { ctx =>
+      Doc.messagesInContext(Seq(
+        (ctx.program, decl, message)
+      ))
+    }
+}

src/col/vct/col/util/CurrentCheckNodeContext.scala

@@ -1,6 +1,14 @@
 package vct.col.util
 
 import vct.col.ast.Node
+import vct.col.print.Doc
 import vct.result.VerificationError
 
-case class CurrentCheckNodeContext(node: Node[_]) extends VerificationError.Context
+case class CurrentCheckNodeContext(node: Node[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    err.context[CurrentCheckProgramContext].map { ctx =>
+      Doc.messagesInContext(Seq(
+        (ctx.program, node, message)
+      ))
+    }
+}

src/col/vct/col/util/CurrentCheckProgramContext.scala

@@ -0,0 +1,12 @@
+package vct.col.util
+
+import vct.col.ast.Program
+import vct.col.print.Doc
+import vct.result.VerificationError
+
+case class CurrentCheckProgramContext(program: Program[_]) extends CurrentProgramContext {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    Some(Doc.messagesInContext(Seq(
+      (program, program, message)
+    )))
+}

src/col/vct/col/util/CurrentProgramContext.scala

@@ -0,0 +1,20 @@
+package vct.col.util
+
+import vct.col.ast.{Node, Program}
+import vct.col.origin.Origin
+import vct.result.VerificationError
+
+object CurrentProgramContext {
+  def bareNodeContext(err: VerificationError, node: Node[_], message: String): String =
+    err.context[CurrentProgramContext] match {
+      case Some(ctx) => ctx.program.bareMessageInContext(node, message)
+      case None => node.toString + "\n" + Origin.HR + message
+    }
+
+  def nodeContext(err: VerificationError, node: Node[_], message: String): String =
+    Origin.BOLD_HR + bareNodeContext(err, node, message) + "\n" + Origin.BOLD_HR
+}
+
+trait CurrentProgramContext extends VerificationError.Context {
+  def program: Program[_]
+}