rename CheckError -> CheckMessage to allow for hints during type chec…

…king

src/col/vct/col/ast/declaration/DeclarationImpl.scala

@@ -1,7 +1,7 @@
 package vct.col.ast.declaration
 
 import vct.col.ast.Declaration
-import vct.col.check.{CheckContext, CheckError, TypeError, TypeErrorExplanation, TypeErrorText}
+import vct.col.check.{CheckContext, CheckMessage, TypeError, TypeErrorExplanation, TypeErrorText}
 import vct.col.debug.{DebugRewriteState, Dropped, NotProcessed}
 import vct.col.ref.{DirectRef, Ref}
 import vct.col.rewrite.InitialGeneration
@@ -21,7 +21,7 @@ trait DeclarationImpl[G] { this: Declaration[G] =>
     */
   def ref[Decl <: Declaration[G]](implicit tag: ClassTag[Decl], witness: this.type <:< Decl): Ref[G, Decl] = new DirectRef[G, Decl](this)
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     try {
       NopCoercingRewriter().coerce(this.asInstanceOf[Declaration[InitialGeneration]])
       Nil

src/col/vct/col/ast/declaration/adt/ADTAxiomImpl.scala

@@ -1,11 +1,11 @@
 package vct.col.ast.declaration.adt
 
 import vct.col.ast.{ADTAxiom, TBool}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait ADTAxiomImpl[G] { this: ADTAxiom[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] = axiom.checkSubType(TBool())
+  override def check(context: CheckContext[G]): Seq[CheckMessage] = axiom.checkSubType(TBool())
 
   override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
     case Ctx.Silver => Group(Text("axiom") <+> "{" <>> axiom.show <+/> "}")

src/col/vct/col/ast/declaration/category/AbstractFunctionImpl.scala

@@ -1,12 +1,12 @@
 package vct.col.ast.declaration.category
 
 import vct.col.ast.{AbstractFunction, Expr}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.origin.{Blame, ContractedFailure}
 
 trait AbstractFunctionImpl[G] extends ContractApplicableImpl[G] { this: AbstractFunction[G] =>
   override def body: Option[Expr[G]]
   def threadLocal: Boolean
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     body.toSeq.flatMap(_.checkSubType(returnType))
 }

src/col/vct/col/ast/declaration/category/AbstractMethodImpl.scala

@@ -1,7 +1,7 @@
 package vct.col.ast.declaration.category
 
 import vct.col.ast.{AbstractMethod, Declaration, LabelDecl, LocalDecl, Return, Statement, Variable}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.origin.{Blame, CallableFailure}
 
 trait AbstractMethodImpl[G] extends ContractApplicableImpl[G] { this: AbstractMethod[G] =>
@@ -15,7 +15,7 @@ trait AbstractMethodImpl[G] extends ContractApplicableImpl[G] { this: AbstractMe
   override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
     super.enterCheckContext(context).withScope(transSubnodes.collect { case decl: LocalDecl[G] => decl.local }.toSet)
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     body.toSeq.flatMap(_.transSubnodes.flatMap {
       case Return(e) => e.checkSubType(returnType)
       case _ => Nil

src/col/vct/col/ast/declaration/global/VeyMontSeqProgImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.declaration.global
 
 import vct.col.ast.{Class, Declaration, VeyMontSeqProg}
 import vct.col.ast.util.Declarator
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.origin.Origin
 import vct.col.print._
 

src/col/vct/col/ast/declaration/model/ModelActionImpl.scala

@@ -1,14 +1,14 @@
 package vct.col.ast.declaration.model
 
 import vct.col.ast.{ModelAction, Node, TBool, TProcess, Type}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait ModelActionImpl[G] { this: ModelAction[G] =>
   override def returnType: Type[G] = TProcess()
   override def body: Option[Node[G]] = None
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     requires.checkSubType(TBool()) ++ ensures.checkSubType(TBool())
 
   override def layout(implicit ctx: Ctx): Doc =

src/col/vct/col/ast/declaration/model/ModelProcessImpl.scala

@@ -1,13 +1,13 @@
 package vct.col.ast.declaration.model
 
 import vct.col.ast.{ModelProcess, Node, TBool, TProcess, Type}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait ModelProcessImpl[G] { this: ModelProcess[G] =>
   override def returnType: Type[G] = TProcess()
   override def body: Option[Node[G]] = Some(impl)
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     impl.checkSubType(TProcess()) ++ requires.checkSubType(TBool()) ++ ensures.checkSubType(TBool())
 
   override def layout(implicit ctx: Ctx): Doc =

src/col/vct/col/ast/expr/ExprImpl.scala

@@ -2,12 +2,12 @@ package vct.col.ast.expr
 
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.{Expr, ProcessPar, Star, Type}
-import vct.col.check.{CheckError, TypeError}
+import vct.col.check.{CheckMessage, TypeError}
 import vct.col.print._
 import vct.col.typerules.CoercionUtils
 
 trait ExprImpl[G] extends NodeFamilyImpl[G] { this: Expr[G] =>
-  def checkSubType(other: Type[G]): Seq[CheckError] =
+  def checkSubType(other: Type[G]): Seq[CheckMessage] =
     CoercionUtils.getCoercion(t, other) match {
       case Some(_) => Nil
       case None => Seq(TypeError(this, other))

src/col/vct/col/ast/expr/context/AmbiguousResultImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.expr.context
 
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.{AmbiguousResult, Type}
-import vct.col.check.{CheckContext, CheckError, ResultOutsidePostcondition}
+import vct.col.check.{CheckContext, CheckMessage, ResultOutsidePostcondition}
 import vct.col.err
 import vct.col.print._
 import vct.col.resolve.ctx._
@@ -24,7 +24,7 @@ trait AmbiguousResultImpl[G] extends NodeFamilyImpl[G] { this: AmbiguousResult[G
     case RefInstanceOperatorFunction(decl) => decl.returnType
   }
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     if (context.inPostCondition) super.check(context)
     else Seq(ResultOutsidePostcondition(this))
 

src/col/vct/col/ast/expr/context/ResultImpl.scala

@@ -2,13 +2,13 @@ package vct.col.ast.expr.context
 
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.{Result, Type}
-import vct.col.check.{CheckContext, CheckError, ResultOutsidePostcondition}
+import vct.col.check.{CheckContext, CheckMessage, ResultOutsidePostcondition}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 
 trait ResultImpl[G] extends NodeFamilyImpl[G] { this: Result[G] =>
   override def t: Type[G] = applicable.decl.returnType
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     if(context.inPostCondition) super.check(context)
     else Seq(ResultOutsidePostcondition(this))
 

src/col/vct/col/ast/expr/heap/read/DerefImpl.scala

@@ -2,12 +2,12 @@ package vct.col.ast.expr.heap.read
 
 import vct.col.ast.expr.ExprImpl
 import vct.col.ast.{Deref, TClass, Type}
-import vct.col.check.{Check, CheckContext, CheckError}
+import vct.col.check.{Check, CheckContext, CheckMessage}
 import vct.col.print.{Ctx, Doc, Group, Precedence}
 
 trait DerefImpl[G] extends ExprImpl[G] { this: Deref[G] =>
   override def t: Type[G] = ref.decl.t
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     Check.inOrder(
       super.check(context),
       obj.t.asClass.get.cls.decl.checkDefines(ref.decl, this)

src/col/vct/col/ast/expr/heap/read/ModelDerefImpl.scala

@@ -2,12 +2,12 @@ package vct.col.ast.expr.heap.read
 
 import vct.col.ast.expr.ExprImpl
 import vct.col.ast.{ModelDeref, Type}
-import vct.col.check.{Check, CheckContext, CheckError}
+import vct.col.check.{Check, CheckContext, CheckMessage}
 import vct.col.print.{Ctx, Doc, Precedence}
 
 trait ModelDerefImpl[G] extends ExprImpl[G] { this: ModelDeref[G] =>
   override def t: Type[G] = ref.decl.t
-  override def check(context: CheckContext[G]): Seq[CheckError] = {
+  override def check(context: CheckContext[G]): Seq[CheckMessage] = {
     Check.inOrder(
       super.check(context),
       obj.t.asModel.get.model.decl.checkDefines(ref.decl, this),

src/col/vct/col/ast/expr/literal/build/LiteralTupleImpl.scala

@@ -2,13 +2,13 @@ package vct.col.ast.expr.literal.build
 
 import vct.col.ast.expr.ExprImpl
 import vct.col.ast.{LiteralTuple, TTuple, Type}
-import vct.col.check.{CheckContext, CheckError, TupleTypeCount}
+import vct.col.check.{CheckContext, CheckMessage, TupleTypeCount}
 import vct.col.print.{Ctx, Doc, Group, Precedence, Text}
 
 trait LiteralTupleImpl[G] extends ExprImpl[G] { this: LiteralTuple[G] =>
   override def t: Type[G] = TTuple(ts)
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     if(ts.size == values.size) {
       super.check(context)
     } else {

src/col/vct/col/ast/expr/misc/LocalImpl.scala

@@ -2,12 +2,12 @@ package vct.col.ast.expr.misc
 
 import vct.col.ast.expr.ExprImpl
 import vct.col.ast.{Local, Type}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 
 trait LocalImpl[G] extends ExprImpl[G] { this: Local[G] =>
   override def t: Type[G] = ref.decl.t
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     context.checkInScope(this, ref)
 
   override def precedence: Int = Precedence.ATOMIC

src/col/vct/col/ast/expr/op/tuple/TupGetImpl.scala

@@ -3,13 +3,13 @@ package vct.col.ast.expr.op.tuple
 import vct.col
 import vct.col.ast.expr.ExprImpl
 import vct.col.ast.{TTuple, TupGet, Type}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print.{Ctx, Doc, Group, Precedence, Text}
 
 trait TupGetImpl[G] extends ExprImpl[G] { this: TupGet[G] =>
   def tupleType: TTuple[G] = tup.t.asTuple.get
   override def t: Type[G] = tupleType.elements(index)
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     super.check(context) match {
       case Nil => if(0 <= index && index < tupleType.elements.size) Nil else Seq(col.check.TypeErrorExplanation(this, "Tuple getter exceeds tuple size"))
       case some => some

src/col/vct/col/ast/expr/sideeffect/AssignExpressionImpl.scala

@@ -2,13 +2,13 @@ package vct.col.ast.expr.sideeffect
 
 import vct.col.ast.expr.ExprImpl
 import vct.col.ast.{AssignExpression, Expr, Local}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 
 trait AssignExpressionImpl[G] extends ExprImpl[G] { this: AssignExpression[G] =>
   def target: Expr[G]
   def value: Expr[G]
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     super.check(context) ++ (target match {
       case Local(ref) => context.checkInWriteScope(context.roScopeReason, this, ref)
       case _ => Nil

src/col/vct/col/ast/family/contract/ApplicableContractImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.family.contract
 
 import vct.col.ast.{ApplicableContract, BooleanValue, Node, UnitAccountedPredicate}
 import vct.col.ast.node.NodeFamilyImpl
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait ApplicableContractImpl[G] extends NodeFamilyImpl[G] { this: ApplicableContract[G] =>

src/col/vct/col/ast/family/invoking/InvokingNodeImpl.scala

@@ -1,7 +1,7 @@
 package vct.col.ast.family.invoking
 
 import vct.col.ast.{ContractApplicable, Expr, InvokingNode, Type, Variable}
-import vct.col.check.CheckError
+import vct.col.check.CheckMessage
 import vct.col.origin.{Blame, InvocationFailure}
 import vct.col.ref.Ref
 

src/col/vct/col/ast/family/parregion/ParRegionImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.family.parregion
 
 import vct.col.ast.ParRegion
 import vct.col.ast.node.NodeFamilyImpl
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.origin.{Blame, ParPreconditionFailed}
 
 trait ParRegionImpl[G] extends NodeFamilyImpl[G] { this: ParRegion[G] =>

src/col/vct/col/ast/lang/CDeclarationImpl.scala

@@ -1,11 +1,11 @@
 package vct.col.ast.lang
 
 import vct.col.ast.{CDeclaration, TResource}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait CDeclarationImpl[G] { this: CDeclaration[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] = kernelInvariant.checkSubType(TResource())
+  override def check(context: CheckContext[G]): Seq[CheckMessage] = kernelInvariant.checkSubType(TResource())
 
   // PB: Please keep in sync with ApplicableContractImpl
   def layoutContract(implicit ctx: Ctx): Doc =

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

@@ -10,7 +10,7 @@ import vct.col.typerules.{CoercingRewriter, NopCoercingRewriter}
   Expr (which always rewrites to an Expr), but also single-purpose nodes, such as a catch clause.
  */
 trait NodeFamilyImpl[G] extends NodeImpl[G] { this: NodeFamily[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     try {
       NopCoercingRewriter().coerceAny(this.asInstanceOf[NodeFamily[InitialGeneration]])
       Nil

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

@@ -38,15 +38,15 @@ import scala.runtime.ScalaRunTime
  * @tparam G The generation marker: not used as a concrete type.
  */
 trait NodeImpl[G] extends Show { this: Node[G] =>
-  def check(context: CheckContext[G]): Seq[CheckError]
+  def check(context: CheckContext[G]): Seq[CheckMessage]
   def o: Origin
 
   def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
     context
 
   /* Check children first, so that the check of nodes higher in the tree may depend on the type and correctness of
     subnodes */
-  final def checkTrans(context: CheckContext[G]): Seq[CheckError] = {
+  final def checkTrans(context: CheckContext[G]): Seq[CheckMessage] = {
     val childrenErrors = checkContextRecursor(context, (ctx, node) => node.checkTrans(ctx)).flatten
 
     if(childrenErrors.nonEmpty) {

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

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

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

@@ -1,11 +1,11 @@
 package vct.col.ast.node
 
 import vct.col.ast.Verification
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait VerificationImpl[G] { this: Verification[G] =>
-  def check: Seq[CheckError] = checkTrans(CheckContext())
+  def check: Seq[CheckMessage] = checkTrans(CheckContext())
 
   override def layout(implicit ctx: Ctx): Doc =
     if(tasks.size == 1) tasks.head.show

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

@@ -1,11 +1,11 @@
 package vct.col.ast.statement.composite
 
 import vct.col.ast.ParAtomic
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print.{Ctx, Doc, Group, Text}
 
 trait ParAtomicImpl[G] { this: ParAtomic[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     inv.flatMap(context.checkInScope(this, _))
 
   override def layout(implicit ctx: Ctx): Doc =

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

@@ -2,12 +2,12 @@ package vct.col.ast.statement.composite
 
 import vct.col.ast.{TNothing, TryCatchFinally, Type, Block}
 import vct.col.ast.node.NodeFamilyImpl
-import vct.col.check.{CheckContext, CheckError, RedundantCatchClause}
+import vct.col.check.{CheckContext, CheckMessage, RedundantCatchClause}
 import vct.col.print._
 import vct.col.typerules.Types
 
 trait TryCatchFinallyImpl[G] extends NodeFamilyImpl[G] { this: TryCatchFinally[G] =>
-  def checkOverlappingCatches: Seq[CheckError] = {
+  def checkOverlappingCatches: Seq[CheckMessage] = {
     this.catches.foldLeft[Type[G]](TNothing()) {
       case (caughtAlready, clause) =>
         if(caughtAlready.superTypeOf(clause.decl.t)) {
@@ -19,7 +19,7 @@ trait TryCatchFinallyImpl[G] extends NodeFamilyImpl[G] { this: TryCatchFinally[G
     Nil
   }
 
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     super.check(context) ++ checkOverlappingCatches
 
   override def layout(implicit ctx: Ctx): Doc =

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

@@ -1,11 +1,11 @@
 package vct.col.ast.statement.terminal
 
 import vct.col.ast.{Assign, Local}
-import vct.col.check.{CheckContext, CheckError}
+import vct.col.check.{CheckContext, CheckMessage}
 import vct.col.print._
 
 trait AssignImpl[G] extends NormallyCompletingStatementImpl[G] { this: Assign[G] =>
-  override def check(context: CheckContext[G]): Seq[CheckError] =
+  override def check(context: CheckContext[G]): Seq[CheckMessage] =
     super.check(context) ++ (target match {
       case Local(ref) => context.checkInWriteScope(context.roScopeReason, this, ref)
       case _ => Nil