make systemerrors use context by default, and turn non-fatal exceptio…

…ns into systemerrors

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)
       }
     }

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/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/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 VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    Some(Doc.messagesInContext(Seq(
+      (program, program, message)
+    )))
+}

src/col/vct/col/util/CurrentRewriteNodeContext.scala

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

src/col/vct/col/util/CurrentRewriteProgramContext.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 CurrentRewriteProgramContext(program: Program[_]) extends VerificationError.Context {
+  override def tryMessageContext(message: String, err: VerificationError): Option[String] =
+    Some(Doc.messagesInContext(Seq(
+      (program, program, message)
+    )))
+}

src/col/vct/col/util/FrozenScopes.scala

@@ -22,7 +22,7 @@ class FrozenScopes[Pre, Post, PreDecl <: Declaration[Pre], PostDecl <: Declarati
   override def computeSucc(decl: PreDecl): Option[PostDecl] = scopes.collectFirst { case m if m.contains(decl) => m(decl) }
 
   override def succ[RefDecl <: Declaration[Post]](decl: PreDecl)(implicit tag: ClassTag[RefDecl]): Ref[Post, RefDecl] =
-    VerificationError.context(ConstructingSuccessorOfContext(decl)) {
+    VerificationError.withContext(ConstructingSuccessorOfContext(decl)) {
       TimeTravel.cause { causeIdx =>
         new LazyRef(computeSucc(decl).getOrElse(TimeTravel.badEffect(causeIdx, throw Scopes.NoSuccessor(decl))), Some(EqualityMeasure(this, decl)))
       }

src/col/vct/col/util/Scopes.scala

@@ -13,6 +13,7 @@ import vct.result.VerificationError.SystemError
 import scala.collection.mutable
 import scala.collection.mutable.ArrayBuffer
 import scala.reflect.ClassTag
+import scala.util.Try
 
 object Scopes {
   case class WrongDeclarationCount(kind: ClassTag[_], count: Int) extends SystemError {
@@ -36,25 +37,18 @@ object Scopes {
 
   case class NoSuccessor(pre: Declaration[_]) extends SystemError {
     override def text: String = {
-      (
-        getContext[CurrentProgramCheckContext],
-        getContext[CurrentCheckNodeContext],
-        getContext[CurrentProgramRewriteContext],
-        getContext[ConstructingSuccessorOfContext],
-      ) match {
-        case (
-          Some(CurrentProgramCheckContext(useProgram)),
-          Some(CurrentCheckNodeContext(useNode)),
-          Some(CurrentProgramRewriteContext(predProgram)),
-          Some(ConstructingSuccessorOfContext(predDecl)),
-        ) =>
-          Doc.messagesInContext(Seq(
-            (predProgram, predDecl, "A reference to the successor of this declaration was made, ..."),
-            (useProgram, useNode, "... but it has no successor in this position.")
-          ))
-        case _ => pre.o.messageInContext("A reference to the successor of this declaration was made, but it has no successor.")
+      Try {
+        val useProgram = getContext[CurrentCheckProgramContext].program
+        val useNode = getContext[CurrentCheckNodeContext].node
+        val predProgram = getContext[CurrentRewriteProgramContext].program
+        val predDecl = getContext[ConstructingSuccessorOfContext].decl
+        Doc.messagesInContext(Seq(
+          (predProgram, predDecl, "A reference to the successor of this declaration was made, ..."),
+          (useProgram, useNode, "... but it has no successor in this position.")
+        ))
+      } getOrElse {
+        pre.o.messageInContext("A reference to the successor of this declaration was made, but it has no successor.")
       }
-
     }
   }
 }

src/colhelper/ColDefs.scala

@@ -17,6 +17,8 @@ object ColDefs {
     q"import vct.col.ref.Ref",
     q"import vct.col.resolve.ctx.Referrable",
     q"import vct.col.origin.ExpectedError",
+    q"import vct.result.VerificationError",
+    q"import vct.col.util.CurrentRewriteNodeContext",
     q"import hre.data.BitString",
   )
 

src/colhelper/ColHelperRewriteHelpers.scala

@@ -15,7 +15,7 @@ case class ColHelperRewriteHelpers(info: ColDescription) extends ColHelperMaker
 
       def rewrite(..${cls.params.map(rewriteHelperParam) ++
         cls.blameType.toSeq.map(t => Term.Param(Nil, q"blame", Some(t), Some(q"rewriter.dispatch(subject.blame)"))) :+
-        Term.Param(List(), q"o", Some(t"Origin"), Some(q"rewriter.dispatch(subject.o)"))}): ${cls.typ}[Post] = {
+        Term.Param(List(), q"o", Some(t"Origin"), Some(q"rewriter.dispatch(subject.o)"))}): ${cls.typ}[Post] = VerificationError.withContext(CurrentRewriteNodeContext(subject)) {
         ${ColDefs.DECLARATION_NAMESPACE.foldLeft(
           cls.make(cls.params.map(p => Term.Name(p.name.value)), q"blame", q"o")
         ){

src/hre/hre/io/CollectString.scala

@@ -0,0 +1,13 @@
+package hre.io
+
+import java.io.{ByteArrayOutputStream, PrintStream}
+import java.nio.charset.StandardCharsets
+
+object CollectString {
+  def apply(f: PrintStream => Unit): String = {
+    val bytes = new ByteArrayOutputStream
+    val print = new PrintStream(bytes)
+    f(print)
+    new String(bytes.toByteArray, StandardCharsets.UTF_8)
+  }
+}