Make range binder leaking work

src/col/vct/col/ast/lang/pvl/PVLCommunicateStatementImpl.scala

@@ -1,9 +1,35 @@
 package vct.col.ast.lang.pvl
 
-import vct.col.ast.PVLCommunicateStatement
+import vct.col.ast.{
+  PVLCommTargetRange,
+  PVLCommunicateStatement,
+  RangeBinder,
+  Variable,
+}
 import vct.col.ast.ops.PVLCommunicateStatementOps
+import vct.col.ast.statement.StatementImpl
+import vct.col.check.{Check, CheckContext, CheckError}
 
-trait PVLCommunicateStatementImpl[G] extends PVLCommunicateStatementOps[G] {
+trait PVLCommunicateStatementImpl[G]
+    extends PVLCommunicateStatementOps[G] with StatementImpl[G] {
   this: PVLCommunicateStatement[G] =>
   // override def layout(implicit ctx: Ctx): Doc = ???
+
+  def rangeBinder: Option[Variable[G]] = {
+    // TODO (RR): Take inference into account here somehow?
+    comm.sender match {
+      case Some(PVLCommTargetRange(_, RangeBinder(v, _, _))) => Some(v)
+      case _ => None
+    }
+  }
+
+  // TODO (RR): This allows nodes[i := i .. i], which should instead be an error
+  override def enterCheckContextScopes(
+      context: CheckContext[G]
+  ): Seq[CheckContext.ScopeFrame[G]] = {
+    rangeBinder match {
+      case Some(v) => context.withScope(Seq(v))
+      case None => context.scopes
+    }
+  }
 }

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

@@ -1,18 +1,28 @@
 package vct.col.ast.statement.veymont
 
+import hre.data.BitString
 import vct.col.ast.declaration.DeclarationImpl
 import vct.col.ast.{
+  CommTargetRange,
   Communicate,
   CommunicateTarget,
+  CtExpr,
   Endpoint,
+  Expr,
+  Message,
   Node,
+  RangeBinder,
   TClass,
   Type,
+  Variable,
 }
 import vct.col.check.{CheckContext, CheckError, SeqProgParticipant}
 import vct.col.print.{Ctx, Doc, Group, Nest, Text}
 import vct.col.ref.Ref
 import vct.col.ast.ops.{CommunicateFamilyOps, CommunicateOps}
+import vct.result.VerificationError.UserError
+
+import scala.collection.immutable.{AbstractSeq, LinearSeq}
 
 trait CommunicateImpl[G]
     extends DeclarationImpl[G]
@@ -43,16 +53,54 @@ trait CommunicateImpl[G]
       case _ => Nil
     }
 
+  case class TooManyRangeBinders(ex1: Node[_], ex2: Node[_]) extends UserError {
+    override def code: String = "tooManyRangeBinders"
+    override def text: String =
+      vct.result.Message.messagesInContext(
+        (
+          ex1.o,
+          "Only one range binder allowed, but two detected. For example here, and...",
+        ),
+        (ex2.o, "... here."),
+      )
+  }
+
+  def rangeBinder(node: Node[G]): Option[Variable[G]] =
+    node match {
+      case CommTargetRange(_, RangeBinder(v, _, _)) => Some(v)
+      case e: Expr[G] =>
+        e.collect { case CtExpr(CommTargetRange(_, RangeBinder(v, _, _))) =>
+            v
+          } match {
+          case Seq(v) => Some(v)
+          case Seq() => None
+          case xs => throw TooManyRangeBinders(xs.head, xs(1))
+        }
+      case _ => None
+    }
+
+  def rangeBinders: Seq[Variable[G]] =
+    receiver.flatMap(rangeBinder).toSeq ++ sender.flatMap(rangeBinder).toSeq ++
+      rangeBinder(destination).toSeq ++ rangeBinder(msg).toSeq
+
   override def checkContextRecursor[T](
       context: CheckContext[G],
       f: (CheckContext[G], Node[G]) => T,
-  ): Seq[T] =
-    subnodes match {
-      case invariant +: rest =>
-        f(context.withCommunicateInvariant(this), invariant) +:
-          rest.map(f(enterCheckContext(context), _))
-      case _ => ???
-    }
+  ): Seq[T] = {
+    val ctxRangeBinder = context.copy(scopes = context.withScope(rangeBinders))
+    receiver.map(f(ctxRangeBinder, _)).toSeq ++ sender.map(f(ctxRangeBinder, _))
+      .toSeq ++ Seq(
+      f(context.withCommunicateInvariant(this), invariant),
+      f(ctxRangeBinder, destination),
+      f(ctxRangeBinder, msg),
+    )
+//    subnodes match {
+//      case invariant +: rest =>
+//        f(context.withCommunicateInvariant(this), invariant) +:
+//          rest.map(f(enterCheckContext(context), _))
+//      case _ => ???
+//    }
+  }
 
   def participants: Seq[CommunicateTarget[G]] = sender.toSeq ++ receiver.toSeq
 

src/col/vct/col/resolve/Resolve.scala

@@ -481,7 +481,12 @@ case object ResolveReferences extends LazyLogging {
         ctx.copy(currentThis = Some(RefPVLChoreography(chor)))
           .declare(chor.args).declare(chor.declarations)
       case comm: PVLCommunicateStatement[G] =>
-        ctx.copy(currentCommunicate = Some(comm))
+        // TODO (RR): This allows nodes[i := i .. i], which should instead be an error
+        (comm.comm.sender match {
+          case Some(PVLCommTargetRange(_, RangeBinder(v, _, _))) =>
+            ctx.declare(Seq(v))
+          case _ => ctx
+        }).copy(currentCommunicate = Some(comm))
       case method: JavaMethod[G] =>
         ctx.copy(currentResult = Some(RefJavaMethod(method)))
           .copy(inStaticJavaContext =

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

@@ -364,6 +364,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case node: FoldTarget[Pre] => coerce(node)
       case node: PVLCommTargetRange[Pre] => coerce(node)
       case node: RangeBinder[Pre] => coerce(node)
+      case node: PVLCommunicateTarget[Pre] => coerce(node)
       case node: CommunicateTarget[Pre] => coerce(node)
     }