VeyMont: parameterization syntax & AST changes

.git-blame-ignore-revs

@@ -2,3 +2,9 @@
 # Date: Tue May 28 19:06:33 2024 +0200
 # reformat scala sources
 7a81a51d7791bc2e407fcfc6aef24bc1d1a52850
+
+# Bob Rubbens: wanted to merge some stuff in after reformatting
+fecd37bf5922332cc449f0ef95f79b09f370aa8e
+
+# Bob Rubbens: (I think the same happened to Philip Tasche)
+97fb61d23cf04a909145ecb28946d1297d947ef4

build.sc

@@ -407,6 +407,7 @@ object vercors extends Module {
     }
     override def generatedSources = T { Seq(helpers.sources()) }
     override def moduleDeps = Seq(hre, serialize)
+    override def ivyDeps = Agg(ivy"com.lihaoyi::sourcecode:0.4.2")
 
     object test extends Tests
   }

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

@@ -246,9 +246,6 @@ final case class TEnum[G](enum: Ref[G, Enum[G]])(
 final case class TProverType[G](ref: Ref[G, ProverType[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends DeclaredType[G] with TProverTypeImpl[G]
-final case class TVeyMontChannel[G](channelType: String)(
-    implicit val o: Origin = DiagnosticOrigin
-) extends DeclaredType[G] with TVeyMontChannelImpl[G]
 
 @family
 sealed trait ParRegion[G] extends NodeFamily[G] with ParRegionImpl[G]
@@ -294,6 +291,7 @@ final case class CatchClause[G](decl: Variable[G], body: Statement[G])(
     implicit val o: Origin
 ) extends NodeFamily[G] with CatchClauseImpl[G]
 
+// TODO (RR): Unify with RangeBinder...!
 @family
 final case class IterVariable[G](
     variable: Variable[G],
@@ -3777,19 +3775,25 @@ final case class TChoreography[G](cls: Ref[G, Choreography[G]])(
 final case class TPVLChoreography[G](cls: Ref[G, PVLChoreography[G]])(
     implicit val o: Origin = DiagnosticOrigin
 ) extends DeclaredType[G] with TPVLChoreographyImpl[G]
-final case class TEndpoint[G](cls: Ref[G, Endpoint[G]])(
-    implicit val o: Origin = DiagnosticOrigin
-) extends DeclaredType[G] with TEndpointImpl[G]
 
+@scopes[Variable]
 final class PVLEndpoint[G](
     val name: String,
+    val range: Option[RangeBinder[G]],
     val cls: Ref[G, Class[G]],
     val typeArgs: Seq[Type[G]],
     val args: Seq[Expr[G]],
 )(val blame: Blame[InvocationFailure])(implicit val o: Origin)
-    extends ClassDeclaration[G] with PVLEndpointImpl[G] {
+    extends ClassDeclaration[G] with PVLEndpointImpl[G] with Declarator[G] {
   var ref: Option[PVLConstructorTarget[G]] = None
 }
+@family
+final case class RangeBinder[G](
+    binder: Variable[G],
+    low: Expr[G],
+    high: Expr[G],
+)(implicit val o: Origin)
+    extends NodeFamily[G] with RangeBinderImpl[G]
 final class PVLChoreography[G](
     val name: String,
     val declarations: Seq[ClassDeclaration[G]],
@@ -3803,11 +3807,33 @@ final class PVLChorRun[G](
 )(val blame: Blame[ChorRunFailure])(implicit val o: Origin)
     extends ClassDeclaration[G] with PVLChorRunImpl[G]
 
+// Represents naming a specific endpoint, or a subrange of endpoints. Used in endpoint expressions, communicate statements to indicate sender/receiver,
+// and in communicate statements to indicate sender/receiver inline in the message/destination location.
+/* TODO (RR): It's annoying here that we both use PVLLocal to refer to endpoint names, as well as the dedicated
+    PVLEndpointName in the case where it's syntactically clear it's an endpoint...
+ */
 @family
-case class PVLEndpointName[G](name: String)(implicit val o: Origin)
-    extends PVLEndpointNameImpl[G] with NodeFamily[G] {
+sealed trait PVLCommunicateTarget[G]
+    extends NodeFamily[G] with PVLCommunicateTargetImpl[G]
+final case class PVLCommTargetEndpoint[G](name: String)(implicit val o: Origin)
+    extends PVLCommTargetEndpointImpl[G] with PVLCommunicateTarget[G] {
+  var ref: Option[RefPVLEndpoint[G]] = None
+}
+final case class PVLCommTargetIndex[G](name: String, index: Expr[G])(
+    implicit val o: Origin
+) extends PVLCommTargetIndexImpl[G] with PVLCommunicateTarget[G] {
   var ref: Option[RefPVLEndpoint[G]] = None
 }
+final case class PVLCommTargetRange[G](name: String, range: RangeBinder[G])(
+    implicit val o: Origin
+) extends PVLCommunicateTarget[G] with PVLCommTargetRangeImpl[G] {
+  var ref: Option[RefPVLEndpoint[G]] = None
+}
+// Adapter node to also put endpoint naming inline in an expression, for communicate statements.
+// Only necessary for the pvlEndpointsRange rule in the PVL grammar
+case class PVLCommTargetExpr[G](set: PVLCommunicateTarget[G])(
+    implicit val o: Origin
+) extends Expr[G] with PVLCommTargetExprImpl[G]
 
 // 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.
@@ -3817,24 +3843,25 @@ final case class PVLCommunicateStatement[G](
     inv: Option[Expr[G]],
 )(implicit val o: Origin)
     extends Statement[G] with PVLCommunicateStatementImpl[G]
-@family
+@family @scopes[Variable]
 final class PVLCommunicate[G](
-    val receiver: Option[PVLEndpointName[G]],
+    val receiver: Option[PVLCommunicateTarget[G]],
     val target: Expr[G],
-    val sender: Option[PVLEndpointName[G]],
+    val sender: Option[PVLCommunicateTarget[G]],
     val msg: Expr[G],
 )(val blame: Blame[PVLCommunicateFailure])(implicit val o: Origin)
     extends Declaration[G] with PVLCommunicateImpl[G] {
-  var inferredSender: Option[PVLEndpoint[G]] = None
-  var inferredReceiver: Option[PVLEndpoint[G]] = None
+  var inferredSender: Option[PVLCommunicateTarget[G]] = None
+  var inferredReceiver: Option[PVLCommunicateTarget[G]] = None
 }
+@scopes[Variable]
 final case class PVLEndpointStatement[G](
-    endpoint: Option[PVLEndpointName[G]],
+    endpoint: Option[PVLCommunicateTarget[G]],
     inner: Statement[G],
 )(val blame: Blame[ChorStatementFailure])(implicit val o: Origin)
     extends Statement[G] with PVLEndpointStatementImpl[G]
 final case class PVLChorPerm[G](
-    endpoint: PVLEndpointName[G],
+    endpoint: PVLCommunicateTarget[G],
     loc: Location[G],
     perm: Expr[G],
 )(implicit val o: Origin)
@@ -3852,13 +3879,14 @@ final case class PVLMessage[G]()(implicit val o: Origin)
   var ref: Option[PVLCommunicateStatement[G]] = None
 }
 
-@family
+@family @scopes[Variable]
 final class Endpoint[G](
+    val range: Option[RangeBinder[G]],
     val cls: Ref[G, Class[G]],
     val typeArgs: Seq[Type[G]],
     val init: Expr[G],
 )(implicit val o: Origin)
-    extends Declaration[G] with EndpointImpl[G]
+    extends Declaration[G] with EndpointImpl[G] with Declarator[G]
 @scopes[Endpoint]
 @scopes[Variable]
 final class Choreography[G](
@@ -3880,20 +3908,35 @@ final case class ChorRun[G](
 @family
 final class Communicate[G](
     val invariant: Expr[G],
-    val receiver: Option[Ref[G, Endpoint[G]]],
-    val target: Expr[G],
-    val sender: Option[Ref[G, Endpoint[G]]],
+    val receiver: Option[CommunicateTarget[G]],
+    val destination: Expr[G],
+    val sender: Option[CommunicateTarget[G]],
     val msg: Expr[G],
 )(val blame: Blame[CommunicateFailure])(implicit val o: Origin)
-    extends Declaration[G] with CommunicateImpl[G]
+    extends CommunicateImpl[G] with Declaration[G]
 @scopes[Communicate]
 final case class CommunicateStatement[G](inner: Communicate[G])(
     implicit val o: Origin
 ) extends PurelySequentialStatement[G] with CommunicateStatementImpl[G]
 
-final case class EndpointName[G](ref: Ref[G, Endpoint[G]])(
+@family
+sealed trait CommunicateTarget[G]
+    extends NodeFamily[G] with CommunicateTargetImpl[G]
+case class CommTargetEndpoint[G](ref: Ref[G, Endpoint[G]])(
+    implicit val o: Origin
+) extends CommunicateTarget[G] with CommTargetEndpointImpl[G]
+case class CommTargetRange[G](ref: Ref[G, Endpoint[G]], range: RangeBinder[G])(
+    implicit val o: Origin
+) extends CommunicateTarget[G] with CommTargetRangeImpl[G]
+case class CommTargetIndex[G](ref: Ref[G, Endpoint[G]], index: Expr[G])(
+    implicit val o: Origin
+) extends CommunicateTarget[G] with CommTargetIndexImpl[G]
+
+final case class CtExpr[G](inner: CommunicateTarget[G])(implicit val o: Origin)
+    extends Expr[G] with CtExprImpl[G]
+final case class EndpointFamilyExpr[G](ref: Ref[G, Endpoint[G]])(
     implicit val o: Origin
-) extends Expr[G] with EndpointNameImpl[G]
+) extends Expr[G] with EndpointFamilyExprImpl[G]
 final case class Sender[G](ref: Ref[G, Communicate[G]])(implicit val o: Origin)
     extends Expr[G] with SenderImpl[G]
 final case class Receiver[G](ref: Ref[G, Communicate[G]])(
@@ -3906,40 +3949,25 @@ final case class ChorStatement[G](inner: Statement[G])(
     val blame: Blame[ChorStatementFailure]
 )(implicit val o: Origin)
     extends Statement[G] with ChorStatementImpl[G]
+@scopes[Variable]
 final case class EndpointStatement[G](
-    endpoint: Option[Ref[G, Endpoint[G]]],
+    endpoint: Option[CommunicateTarget[G]],
     inner: Statement[G],
 )(val blame: Blame[ChorStatementFailure])(implicit val o: Origin)
     extends Statement[G] with EndpointStatementImpl[G]
 
 final case class PVLEndpointExpr[G](
-    endpoint: PVLEndpointName[G],
+    endpoint: PVLCommunicateTarget[G],
     expr: Expr[G],
 )(implicit val o: Origin)
-    extends Expr[G] with PVLEndpointExprImpl[G]
-final case class EndpointExpr[G](endpoint: Ref[G, Endpoint[G]], expr: Expr[G])(
+    extends Expr[G] with PVLEndpointExprImpl[G] with Declarator[G]
+@scopes[Variable]
+final case class EndpointExpr[G](endpoint: CommunicateTarget[G], expr: Expr[G])(
     implicit val o: Origin
 ) extends Expr[G] with EndpointExprImpl[G]
 final case class ChorExpr[G](expr: Expr[G])(implicit val o: Origin)
     extends Expr[G] with ChorExprImpl[G]
 
-final case class VeyMontAssignExpression[G](
-    endpoint: Ref[G, Endpoint[G]],
-    assign: Statement[G],
-)(implicit val o: Origin)
-    extends Statement[G]
-    with ControlContainerStatement[G]
-    with VeyMontAssignExpressionImpl[G]
-final case class CommunicateX[G](
-    receiver: Ref[G, Endpoint[G]],
-    sender: Ref[G, Endpoint[G]],
-    chanType: Type[G],
-    assign: Statement[G],
-)(implicit val o: Origin)
-    extends Statement[G]
-    with ControlContainerStatement[G]
-    with CommunicateXImpl[G]
-
 sealed trait SilverExpr[G] extends Expr[G] with SilverExprImpl[G]
 final case class SilverDeref[G](obj: Expr[G], field: Ref[G, SilverField[G]])(
     val blame: Blame[InsufficientPermission]

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

@@ -6,9 +6,9 @@ import vct.col.ast.{
   ChorStatement,
   Choreography,
   Class,
+  CommunicateTarget,
   Declaration,
   Endpoint,
-  EndpointName,
   EndpointStatement,
   Node,
 }
@@ -21,13 +21,33 @@ import vct.col.ref.Ref
 import scala.collection.immutable.ListSet
 import vct.col.ast.ops.ChoreographyOps
 import vct.col.util.AstBuildHelpers.tt
+import vct.col.util.AstMatchHelpers.{EndpointIndex, EndpointName, EndpointRange}
+import vct.result.VerificationError.UserError
 
 object ChoreographyImpl {
+  case class OnlySingleEndpointsSupported(node: Node[_]) extends UserError {
+    override def code: String = "onlySingleEndpointsSupported"
+    override def text: String =
+      node.o.messageInContext(
+        "Only singular endpoint definitions are supported for permission generation"
+      )
+  }
+
+  // This method is _bad_ because it collects participants from a node in an unprincipled way.
+  // Instead, there should be a series of methods like this, that define it for nodes where it makes sense
+  // E.g. for a choreographies, because you can look at the endpoints directly.
+  // Maybe not for statements, because of unpointed expressions
+  // If you assume there are no unpointed expressions, and all other endpoint owner annotations are also explicit, maybe
+  //    it can make sense to define this method.
   def participants[G](node: Node[G]): ListSet[Endpoint[G]] =
     ListSet.from(node.collect {
-      case EndpointStatement(Some(Ref(endpoint)), Assign(_, _)) => Seq(endpoint)
       case EndpointName(Ref(endpoint)) => Seq(endpoint)
-      case c @ ChorStatement(_) => c.participants.toSeq
+      case node @ EndpointRange(_, _) =>
+        throw OnlySingleEndpointsSupported(node) // Seq(endpoint)
+      case node @ EndpointIndex(_, _) =>
+        throw OnlySingleEndpointsSupported(node)
+      // Seq(endpoint)
+//      case c @ ChorStatement(_) => c.participants.toSeq
     }.flatten)
 }
 
@@ -51,8 +71,8 @@ trait ChoreographyImpl[G]
 
   override def enterCheckContextCurrentParticipatingEndpoints(
       context: CheckContext[G]
-  ): Option[Set[Endpoint[G]]] =
-    context.withCurrentParticipatingEndpoints(endpoints)
+  ): Option[Set[CommunicateTarget[G]]] =
+    Some(ListSet.from(endpoints.map(_.commTarget)))
 
   override def enterCheckContextCurrentChoreography(
       context: CheckContext[G]

src/col/vct/col/ast/declaration/singular/EndpointImpl.scala

@@ -1,19 +1,61 @@
 package vct.col.ast.declaration.singular
 
 import vct.col.ast.declaration.DeclarationImpl
-import vct.col.ast.{Endpoint, TByReferenceClass, TClass, Type}
+import vct.col.ast.{
+  CommTargetEndpoint,
+  CommTargetRange,
+  CommunicateTarget,
+  Declaration,
+  Endpoint,
+  EndpointFamilyExpr,
+  RangeBinder,
+  Size,
+  TByReferenceClass,
+  TClass,
+  TInt,
+  TSeq,
+  Type,
+  Variable,
+}
 import vct.col.print._
-import vct.col.ast.ops.{EndpointFamilyOps, EndpointOps}
+import vct.col.ast.ops.{EndpointFamilyExprOps, EndpointOps}
 import vct.col.check.{CheckContext, CheckError}
+import vct.col.origin.{DiagnosticOrigin, Origin}
+import vct.col.util.AstBuildHelpers
+import vct.col.util.AstMatchHelpers.{EndpointName, EndpointRange}
+import vct.col.ast.ops.{EndpointFamilyOps, EndpointOps}
 
 trait EndpointImpl[G]
-    extends EndpointOps[G] with EndpointFamilyOps[G] with DeclarationImpl[G] {
+    extends EndpointOps[G] with DeclarationImpl[G] with EndpointFamilyOps[G] {
   this: Endpoint[G] =>
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("endpoint") <+> ctx.name(this) <+> "=" <+> init)
+    Group(
+      Text("endpoint") <+> ctx.name(this) <> range.map(_.show)
+        .getOrElse(Empty) <+> "=" <+> init <> ";"
+    )
+
+  def singleType: TClass[G] = cls.decl.classType(typeArgs)
+  def rangeType: TSeq[G] = TSeq(singleType)
 
-  def t: TClass[G] = cls.decl.classType(typeArgs)
+  override def declarations: Seq[Declaration[G]] =
+    range.map(r => Seq(r.binder)).getOrElse(Seq())
 
-  override def check(ctx: CheckContext[G]): Seq[CheckError] = super.check(ctx)
+  def isFamily: Boolean = range.nonEmpty
+  def isSingle: Boolean = !isFamily
 
+  def commTarget: CommunicateTarget[G] = {
+    implicit val o = DiagnosticOrigin
+    range match {
+      case None => CommTargetEndpoint(this.ref)
+      case Some(_) =>
+        CommTargetRange(
+          this.ref,
+          RangeBinder(
+            new Variable(TInt()),
+            AstBuildHelpers.const(0),
+            Size(EndpointFamilyExpr(this.ref)),
+          ),
+        )
+    }
+  }
 }

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

@@ -1,15 +1,7 @@
 package vct.col.ast.expr.heap.read
 
 import vct.col.ast.expr.ExprImpl
-import vct.col.ast.{
-  Deref,
-  EndpointName,
-  Expr,
-  FieldLocation,
-  TClass,
-  Type,
-  Value,
-}
+import vct.col.ast.{Deref, FieldLocation, Type, Value}
 import vct.col.check.{Check, CheckContext, CheckError, SeqProgReceivingEndpoint}
 import vct.col.print.{Ctx, Doc, Group, Precedence}
 import vct.col.ref.Ref