Make progress on syntax & ast changes

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

@@ -3823,20 +3823,24 @@ final case class PVLEndpointName[G](name: String)(implicit val o: Origin)
   var ref: Option[RefPVLEndpoint[G]] = None
 }
 final case class PVLEndpointRange[G](
-    family: Expr[G],
+    name: String,
     binder: Variable[G],
     low: Expr[G],
     high: Expr[G],
 )(implicit val o: Origin)
-    extends PVLEndpointSet[G] with PVLEndpointRangeImpl[G]
+    extends PVLEndpointSet[G] with PVLEndpointRangeImpl[G] {
+  var ref: Option[RefPVLEndpoint[G]] = None
+}
 // Need a second one, because don't want to have one node in two node families (PVLEndpointSet and Expr)
 case class PVLEndpointRangeExpr[G](
-    family: Expr[G],
+    name: String,
     binder: Variable[G],
     low: Expr[G],
     high: Expr[G],
 )(implicit val o: Origin)
-    extends Expr[G] with PVLEndpointRangeExprImpl[G]
+    extends Expr[G] with PVLEndpointRangeExprImpl[G] {
+  var ref: Option[RefPVLEndpoint[G]] = None
+}
 
 // Resolution of invariant can depend on communicate's target/msg through \sender, \receiver, \msg. Therefore, definitions are nested like this,
 // to ensure that PVLCommunicate is fully resolved before the invariant is typechecked.

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

@@ -1239,10 +1239,12 @@ case object ResolveReferences extends LazyLogging {
                 expr.o.messageInContext("Too many endpoints possible")
               )
           }
-        comm.inferredSender = comm.sender.map(_.ref.get.decl)
-          .orElse(Some(getEndpoint(comm.msg)))
-        comm.inferredReceiver = comm.receiver.map(_.ref.get.decl)
-          .orElse(Some(getEndpoint(comm.target)))
+        comm.inferredSender =
+          ??? /* comm.sender.map(_.ref.get.decl)
+          .orElse(Some(getEndpoint(comm.msg))) */ // TODO (RR): Re-enable this ASAP
+        comm.inferredReceiver =
+          ??? /* comm.receiver.map(_.ref.get.decl)
+          .orElse(Some(getEndpoint(comm.target))) */ // TODO (RR): Re-enable this ASAP
       case sender: PVLSender[G] =>
         sender.ref = Some(
           ctx.currentCommunicate.getOrElse(throw OnlyInChannelInvariant(sender))

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

@@ -2966,4 +2966,19 @@ abstract class CoercingRewriter[Pre <: Generation]()
   def coerce(node: PVLEndpointName[Pre]): PVLEndpointName[Pre] = node
   def coerce(node: EndpointName[Pre]): EndpointName[Pre] = node
 
+  def coerce(node: PVLEndpointSet[Pre]): PVLEndpointSet[Pre] = {
+    implicit val o = node.o
+    node match {
+      case PVLEndpointName(name) => node
+      case PVLEndpointRange(name, binder, low, high) =>
+        PVLEndpointRange(name, binder, int(low), int(high))
+    }
+  }
+
+  def coerce(node: PVLFamily[Pre]): PVLFamily[Pre] = {
+    implicit val o = node.o
+    val PVLFamily(binder, low, high) = node
+    PVLFamily(binder, int(low), int(high))
+  }
+
 }

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -652,16 +652,26 @@ case class PVLToCol[G](
     }
     PVLCommunicateStatement(
       comm,
-      inv.map { case node @ ChannelInvariant0(_, inv, _) => convert(inv) },
+      inv.map { case ChannelInvariant0(_, inv, _) => convert(inv) },
     )(origin(node))
   }
 
   def convertParticipant(
       implicit participant: ParticipantContext
-  ): PVLEndpointName[G] =
+  ): PVLEndpointSet[G] =
     participant match {
       case Participant0(name, None, _) => PVLEndpointName(convert(name))
-      case Participant0(name, Some(_), _) => ???
+      case Participant0(
+            name,
+            Some(FamilyIter0(_, binder, _, _, low, _, high, _)),
+            _,
+          ) =>
+        PVLEndpointRange(
+          convert(name),
+          new Variable(TInt())(origin(binder).sourceName(convert(name))),
+          convert(low),
+          convert(high),
+        )
     }
 
   def convert(implicit stat: ForStatementListContext): Statement[G] =

test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala

@@ -2,6 +2,21 @@ package vct.test.integration.examples.veymont
 
 import vct.test.integration.helper.VeyMontSpec
 
+class TechnicalVeyMontSpec2 extends VeyMontSpec {
+  choreography(
+    desc = "Can define families",
+    pvl = """
+      class C {
+        constructor(int tid);
+      }
+      requires N > 0;
+      choreography Chor(int N) {
+        endpoints nodes[tid := 0 .. N] = C(tid);
+      }
+    """,
+  )
+}
+
 class TechnicalVeyMontSpec extends VeyMontSpec {
   choreography(
     desc = "Endpoint expressions can be nested",