add some checks, flatten stack trace a bit

src/col/vct/col/ast/Node.scala

@@ -463,9 +463,10 @@ final case class AmbiguousThis[G]()(implicit val o: Origin) extends Expr[G] with
   var ref: Option[ThisTarget[G]] = None
 }
 
-final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with ThisObjectImpl[G]
-final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends Expr[G] with ThisModelImpl[G]
-final case class ThisSeqProg[G](cls: Ref[G, SeqProg[G]])(implicit val o: Origin) extends Expr[G] with ThisSeqProgImpl[G]
+sealed trait ThisDeclaration[G] extends Expr[G] with ThisDeclarationImpl[G]
+final case class ThisObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends ThisDeclaration[G] with ThisObjectImpl[G]
+final case class ThisModel[G](cls: Ref[G, Model[G]])(implicit val o: Origin) extends ThisDeclaration[G] with ThisModelImpl[G]
+final case class ThisSeqProg[G](cls: Ref[G, SeqProg[G]])(implicit val o: Origin) extends ThisDeclaration[G] with ThisSeqProgImpl[G]
 
 final case class AmbiguousResult[G]()(implicit val o: Origin) extends Expr[G] with AmbiguousResultImpl[G] {
   var ref: Option[ResultTarget[G]] = None

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

@@ -1,5 +1,6 @@
 package vct.col.ast.declaration
 
+import vct.col.ast.node.NodeImpl
 import vct.col.ast.{AbstractRewriter, Declaration}
 import vct.col.check.{CheckContext, CheckError, TypeError, TypeErrorExplanation, TypeErrorText}
 import vct.col.debug.{DebugRewriteState, Dropped, NotProcessed}
@@ -9,7 +10,7 @@ import vct.col.typerules.{CoercingRewriter, NopCoercingRewriter}
 
 import scala.reflect.ClassTag
 
-trait DeclarationImpl[G] { this: Declaration[G] =>
+trait DeclarationImpl[G] extends NodeImpl[G] { this: Declaration[G] =>
   var debugRewriteState: DebugRewriteState = NotProcessed
 
   def drop(): Unit = debugRewriteState = Dropped
@@ -32,4 +33,7 @@ trait DeclarationImpl[G] { this: Declaration[G] =>
       case CoercingRewriter.IncoercibleText(e, m) => Seq(TypeErrorText(e, m))
       case CoercingRewriter.IncoercibleExplanation(e, m) => Seq(TypeErrorExplanation(e, m))
     }
+
+  override def enterCheckContextDeclarationStack(context: CheckContext[G]): Seq[Declaration[G]] =
+    this +: context.declarationStack
 }

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

@@ -1,16 +1,16 @@
 package vct.col.ast.declaration.category
 
+import vct.col.ast.declaration.DeclarationImpl
 import vct.col.ast.util.Declarator
 import vct.col.ast.{Applicable, Declaration, Node, Type, Variable}
 import vct.col.check.CheckContext
 
-trait ApplicableImpl[G] extends Declarator[G] { this: Applicable[G] =>
+trait ApplicableImpl[G] extends DeclarationImpl[G] with Declarator[G] { this: Applicable[G] =>
   def args: Seq[Variable[G]]
   def returnType: Type[G]
   def body: Option[Node[G]]
 
   override def declarations: Seq[Declaration[G]] = args
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    super.enterCheckContext(context).withApplicable(this)
+  override def enterCheckContextCurrentApplicable(context: CheckContext[G]): Option[Applicable[G]] = Some(this)
 }

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

@@ -1,5 +1,6 @@
 package vct.col.ast.declaration.global
 
+import vct.col.ast.declaration.DeclarationImpl
 import vct.col.ast.{Class, Declaration, Endpoint, EndpointGuard, EndpointName, Node, SeqAssign, SeqProg}
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
@@ -19,7 +20,7 @@ object SeqProgImpl {
     })
 }
 
-trait SeqProgImpl[G] extends Declarator[G] with SeqProgOps[G] { this: SeqProg[G] =>
+trait SeqProgImpl[G] extends DeclarationImpl[G] with Declarator[G] with SeqProgOps[G] { this: SeqProg[G] =>
   override def declarations: Seq[Declaration[G]] = args ++ endpoints ++ decls
 
   override def layout(implicit ctx: Ctx): Doc =
@@ -30,8 +31,9 @@ trait SeqProgImpl[G] extends Declarator[G] with SeqProgOps[G] { this: SeqProg[G]
       "}"
     ))
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    super.enterCheckContext(context)
-      .withSeqProg(this)
-      .withCurrentParticipatingEndpoints(endpoints)
+  override def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] =
+    context.withCurrentParticipatingEndpoints(endpoints)
+
+  override def enterCheckContextCurrentSeqProg(context: CheckContext[G]): Option[SeqProg[G]] =
+    Some(this)
 }

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

@@ -0,0 +1,14 @@
+package vct.col.ast.expr.context
+
+import vct.col.ast.{Declaration, ThisDeclaration}
+import vct.col.ast.expr.ExprImpl
+import vct.col.check.{CheckContext, CheckError, ThisOutsideScopeError}
+import vct.col.ref.Ref
+
+trait ThisDeclarationImpl[G] extends ExprImpl[G] { this: ThisDeclaration[G] =>
+  def cls: Ref[G, _ <: Declaration[G]]
+
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    if(!context.declarationStack.contains(cls.decl)) super.check(context) ++ Seq(ThisOutsideScopeError(this))
+    else super.check(context)
+}

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

@@ -4,7 +4,7 @@ import vct.col.ast.{TModel, ThisModel, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.ThisModelOps
 
-trait ThisModelImpl[G] extends ThisModelOps[G] { this: ThisModel[G] =>
+trait ThisModelImpl[G] extends ThisDeclarationImpl[G] with ThisModelOps[G] { this: ThisModel[G] =>
   override def t: Type[G] = TModel(cls)
 
   override def precedence: Int = Precedence.ATOMIC

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

@@ -3,8 +3,9 @@ package vct.col.ast.expr.context
 import vct.col.ast.{TClass, ThisObject, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.ThisObjectOps
+import vct.col.check.{CheckContext, CheckError}
 
-trait ThisObjectImpl[G] extends ThisObjectOps[G] { this: ThisObject[G] =>
+trait ThisObjectImpl[G] extends ThisDeclarationImpl[G] with ThisObjectOps[G] { this: ThisObject[G] =>
   override def t: Type[G] = TClass(cls)
 
   override def precedence: Int = Precedence.ATOMIC

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

@@ -4,7 +4,7 @@ import vct.col.ast.{TAnyClass, TSeqProg, ThisSeqProg, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.ast.ops.ThisSeqProgOps
 
-trait ThisSeqProgImpl[G] extends ThisSeqProgOps[G] { this: ThisSeqProg[G] =>
+trait ThisSeqProgImpl[G] extends ThisDeclarationImpl[G] with ThisSeqProgOps[G] { this: ThisSeqProg[G] =>
   override def t: Type[G] = TSeqProg(cls)
 
   override def precedence: Int = Precedence.ATOMIC

src/col/vct/col/ast/family/location/FieldLocationImpl.scala

@@ -1,10 +1,15 @@
 package vct.col.ast.family.location
 
-import vct.col.ast.FieldLocation
+import vct.col.ast.{FieldLocation, Final}
 import vct.col.print._
 import vct.col.ast.ops.FieldLocationOps
+import vct.col.check.{CheckContext, CheckError, FinalPermission}
+
+trait FieldLocationImpl[G] extends FieldLocationOps[G] with LocationImpl[G] { this: FieldLocation[G] =>
+  override def check(context: CheckContext[G]): Seq[CheckError] =
+    if(field.decl.flags.collectFirst { case Final() => () }.nonEmpty) Seq(FinalPermission(this)) ++ super.check(context)
+    else super.check(context)
 
-trait FieldLocationImpl[G] extends FieldLocationOps[G] { this: FieldLocation[G] =>
   override def layout(implicit ctx: Ctx): Doc =
     obj.bind(Precedence.POSTFIX) <> "." <> ctx.name(field)
 }

src/col/vct/col/ast/family/location/LocationImpl.scala

@@ -1,9 +1,13 @@
 package vct.col.ast.family.location
 
+import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.{AmbiguousLocation, ArrayLocation, FieldLocation, HeapVariableLocation, InstancePredicateLocation, Location, ModelLocation, PointerLocation, PredicateLocation, SilverFieldLocation, Type}
 import vct.col.ast.ops.LocationFamilyOps
+import vct.col.check.{CheckContext, CheckError}
+
+trait LocationImpl[G] extends NodeFamilyImpl[G] with LocationFamilyOps[G] { this: Location[G] =>
+  override def check(context: CheckContext[G]): Seq[CheckError] = super.check(context)
 
-trait LocationImpl[G] extends LocationFamilyOps[G] { this: Location[G] =>
   def t: Type[G] = {
     this match {
       case FieldLocation(obj, field) => field.decl.t

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

@@ -1,7 +1,7 @@
 package vct.col.ast.family.parregion
 
 import vct.col.ast.util.Declarator
-import vct.col.ast.{Declaration, Expr, Local, ParBlock, Starall, Variable}
+import vct.col.ast.{Declaration, Expr, Local, Node, ParBlock, Starall, Variable}
 import vct.col.check.CheckContext
 import vct.col.origin.{Blame, ReceiverNotInjective}
 import vct.col.print._
@@ -21,8 +21,14 @@ trait ParBlockImpl[G] extends ParRegionImpl[G] with Declarator[G] with ParBlockO
     })
   }
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    context.copy(roScopes = context.scopes.size, roScopeReason = Some(this)).withScope(declarations)
+  override def enterCheckContextRoScopes(context: CheckContext[G]): Int =
+    context.scopes.size
+
+  override def enterCheckContextRoScopeReason(context: CheckContext[G]): Option[Node[G]] =
+    Some(this)
+
+  override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] =
+    context.withScope(declarations)
 
   override def layout(implicit ctx: Ctx): Doc = {
     val header = Group(Text("par") <+> ctx.name(decl) <>

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

@@ -1,6 +1,6 @@
 package vct.col.ast.family.parregion
 
-import vct.col.ast.ParRegion
+import vct.col.ast.{Node, ParRegion}
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.check.{CheckContext, CheckError}
 import vct.col.origin.{Blame, ParPreconditionFailed}
@@ -9,6 +9,9 @@ import vct.col.ast.ops.ParRegionFamilyOps
 trait ParRegionImpl[G] extends NodeFamilyImpl[G] with ParRegionFamilyOps[G] { this: ParRegion[G] =>
   def blame: Blame[ParPreconditionFailed]
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    context.copy(roScopes = context.scopes.size, roScopeReason = Some(this))
+  override def enterCheckContextRoScopes(context: CheckContext[G]): Int =
+    context.scopes.size
+
+  override def enterCheckContextRoScopeReason(context: CheckContext[G]): Option[Node[G]] =
+    Some(this)
 }

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

@@ -46,8 +46,30 @@ trait NodeImpl[G] extends Show { this: Node[G] =>
   def serialize(decls: Map[Declaration[G], Long]): scalapb.GeneratedMessage
   def serializeFamily(decls: Map[Declaration[G], Long]): scalapb.GeneratedMessage
 
-  def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-    context
+  final def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
+    CheckContext(
+      enterCheckContextScopes(context),
+      enterCheckContextUndeclared(context),
+      enterCheckContextRoScopes(context),
+      enterCheckContextRoScopeReason(context),
+      enterCheckContextCurrentApplicable(context),
+      enterCheckContextInPostCondition(context),
+      enterCheckContextCurrentSeqProg(context),
+      enterCheckContextCurrentReceiverEndpoint(context),
+      enterCheckContextCurrentParticipatingEndpoints(context),
+      enterCheckContextDeclarationStack(context),
+    )
+
+  def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] = context.scopes
+  def enterCheckContextUndeclared(context: CheckContext[G]): Seq[Seq[Declaration[G]]] = context.undeclared
+  def enterCheckContextRoScopes(context: CheckContext[G]): Int = context.roScopes
+  def enterCheckContextRoScopeReason(context: CheckContext[G]): Option[Node[G]] = context.roScopeReason
+  def enterCheckContextCurrentApplicable(context: CheckContext[G]): Option[Applicable[G]] = context.currentApplicable
+  def enterCheckContextInPostCondition(context: CheckContext[G]): Boolean = context.inPostCondition
+  def enterCheckContextCurrentSeqProg(context: CheckContext[G]): Option[SeqProg[G]] = context.currentSeqProg
+  def enterCheckContextCurrentReceiverEndpoint(context: CheckContext[G]): Option[Endpoint[G]] = context.currentReceiverEndpoint
+  def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] = context.currentParticipatingEndpoints
+  def enterCheckContextDeclarationStack(context: CheckContext[G]): Seq[Declaration[G]] = context.declarationStack
 
   /* Check children first, so that the check of nodes higher in the tree may depend on the type and correctness of
     subnodes */

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

@@ -8,7 +8,8 @@ import vct.col.ast.ops.ScopeOps
 
 trait ScopeImpl[G] extends ScopeOps[G] {
   this: Scope[G] =>
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
+
+  override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] =
     context.withScope(locals, toScan = Seq(body))
 
   override def layout(implicit ctx: Ctx): Doc = layoutAsBlock

src/col/vct/col/ast/statement/exceptional/EvalImpl.scala

@@ -1,18 +1,19 @@
 package vct.col.ast.statement.exceptional
 
 import vct.col.ast.statement.StatementImpl
-import vct.col.ast.{EndpointUse, Eval, MethodInvocation, Statement, ThisSeqProg}
+import vct.col.ast.{Endpoint, EndpointUse, Eval, MethodInvocation, Statement, ThisSeqProg}
 import vct.col.check.{CheckContext, CheckError, SeqProgInvocation}
 import vct.col.print.{Ctx, Doc}
 import vct.col.ast.ops.EvalOps
 
 trait EvalImpl[G] extends StatementImpl[G] with EvalOps[G] { this: Eval[G] =>
   override def layout(implicit ctx: Ctx): Doc = expr.show <> ";"
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = this match {
+  override def enterCheckContextCurrentReceiverEndpoint(context: CheckContext[G]): Option[Endpoint[G]] = this match {
     case Eval(MethodInvocation(EndpointUse(endpoint), _, _, _, _, _, _)) if context.currentSeqProg.isDefined =>
-      context.withReceiverEndpoint(endpoint.decl)
-    case _ => context
+      Some(endpoint.decl)
+    case _ =>
+      context.currentReceiverEndpoint
   }
 
   override def check(context: CheckContext[G]): Seq[CheckError] = super.check(context) ++ (context.currentSeqProg match {

src/col/vct/col/ast/statement/veymont/SeqAssignImpl.scala

@@ -1,15 +1,15 @@
 package vct.col.ast.statement.veymont
 
-import vct.col.ast.SeqAssign
+import vct.col.ast.{Endpoint, SeqAssign}
 import vct.col.ast.statement.StatementImpl
 import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
 import vct.col.print.{Ctx, Doc, Group, Text}
 import vct.col.ast.ops.SeqAssignOps
 
 trait SeqAssignImpl[G] extends StatementImpl[G] with SeqAssignOps[G] { this: SeqAssign[G] =>
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
-      context.withReceiverEndpoint(receiver.decl)
+  override def enterCheckContextCurrentReceiverEndpoint(context: CheckContext[G]): Option[Endpoint[G]] =
+    Some(receiver.decl)
 
   override def layout(implicit ctx: Ctx): Doc =
     Group(Text(ctx.name(receiver)) <> "." <> ctx.name(field) <+> ":=" <+> value.show)

src/col/vct/col/ast/statement/veymont/SeqBranchImpl.scala

@@ -12,7 +12,7 @@ trait SeqBranchImpl[G] extends StatementImpl[G] with SeqBranchOps[G] { this: Seq
   def hasUnpointed: Boolean = guards.exists { case _: UnpointedGuard[G] => true; case _ => false }
   def explicitParticipants: Seq[Endpoint[G]] = guards.collect { case EndpointGuard(Ref(endpoint), condition) => endpoint }
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = {
+  override def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] = {
     // Assume SeqProg sets participatingEndpoints
     assert(context.currentParticipatingEndpoints.isDefined)
 

src/col/vct/col/ast/statement/veymont/SeqLoopImpl.scala

@@ -12,7 +12,7 @@ trait SeqLoopImpl[G] extends StatementImpl[G] with SeqLoopOps[G] { this: SeqLoop
   def hasUnpointed: Boolean = guards.exists { case _: UnpointedGuard[G] => true; case _ => false }
   def explicitParticipants: Seq[Endpoint[G]] = guards.collect { case EndpointGuard(Ref(endpoint), condition) => endpoint }
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] = {
+  override def enterCheckContextCurrentParticipatingEndpoints(context: CheckContext[G]): Option[Set[Endpoint[G]]] = {
     // Assume SeqProg sets participatingEndpoints
     assert(context.currentParticipatingEndpoints.isDefined)
 

src/col/vct/col/ast/util/Declarator.scala

@@ -7,7 +7,7 @@ import vct.col.check.{CheckContext, DoesNotDefine, OutOfScopeError}
 trait Declarator[G] extends NodeImpl[G] { this: Node[G] =>
   def declarations: Seq[Declaration[G]]
 
-  override def enterCheckContext(context: CheckContext[G]): CheckContext[G] =
+  override def enterCheckContextScopes(context: CheckContext[G]): Seq[CheckContext.ScopeFrame[G]] =
     context.withScope(declarations)
 
   def checkDefines(defn: Declaration[G], use: Node[G]): Seq[DoesNotDefine] =