Get started on intersect

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

@@ -40,7 +40,7 @@ trait EndpointImpl[G]
     getRange.map(r => Seq(r.binder)).getOrElse(Seq())
 
   def isFamily: Boolean = range.nonEmpty
-  def isEndpoint: Boolean = !isFamily
+  def isSingle: Boolean = !isFamily
 
   def getRange: Option[RangeBinder[G]] =
     this.range.map(_.asInstanceOf[RangeBinder[G]])

src/col/vct/col/ast/unsorted/CommTargetEndpointImpl.scala

@@ -9,15 +9,15 @@ import vct.col.print._
 trait CommTargetEndpointImpl[G]
     extends CommTargetEndpointOps[G] with CommunicateTargetImpl[G] {
   this: CommTargetEndpoint[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+  override def layout(implicit ctx: Ctx): Doc = Text(ctx.name(ref))
 
   def endpoint: Endpoint[G] = ref.decl
 
   override def check(context: CheckContext[G]): Seq[CheckError] =
     super.check(context) ++ {
       // This is really a well-formedness requirement on the AST. Ideally it would be checked earlier, but this is not
       // possibly, as the ref might not be resolved yet.
-      require(endpoint.isEndpoint)
+      require(endpoint.isSingle)
       Seq()
     }
 }

src/col/vct/col/ast/unsorted/CommunicateTargetImpl.scala

@@ -37,5 +37,18 @@ trait CommunicateTargetImpl[G] extends CommunicateTargetFamilyOps[G] {
       case _ => ???
     }
 
+  def isSingle: Boolean =
+    this match {
+      case _: CommTargetEndpoint[G] => true
+      case _: CommTargetIndex[G] => true
+      case _ => false
+    }
+
+  def isRange: Boolean =
+    this match {
+      case _: CommTargetRange[G] => true
+      case _ => false
+    }
+
   override def check(context: CheckContext[G]): Seq[CheckError] = Nil
 }

src/col/vct/col/ast/unsorted/CtExprImpl.scala

@@ -15,7 +15,8 @@ import vct.col.util.AstMatchHelpers.{EndpointIndex, EndpointName, EndpointRange}
 
 trait CtExprImpl[G] extends CtExprOps[G] {
   this: CtExpr[G] =>
-//  override def layout(implicit ctx: Ctx): Doc = inner.layout
+  override def layout(implicit ctx: Ctx): Doc = inner.show
+  override def precedence: Int = Precedence.ATOMIC
 
   // TODO (RR): I think this is wrong, but keeping it around for a few minutes
   override def t: TClass[G] = inner.ref.decl.t

src/col/vct/col/serialize/SerializeOrigin.scala

@@ -27,7 +27,7 @@ object SerializeOrigin extends LazyLogging {
           context.inlineContext,
           context.shortPosition,
         )
-      case ser.OriginContent.Content.ReadableOrigin(_) =>
+      case ser.OriginContent.Content.ReadableOrigin(context) =>
         val path = Path.of(context.directory, context.filename)
         ReadableOrigin(fileMap.getOrElseUpdate(
           path, {

src/main/vct/main/stages/Transformation.scala

@@ -31,7 +31,6 @@ import vct.result.VerificationError.SystemError
 import vct.rewrite.adt.ImportSetCompat
 import vct.rewrite.{
   DisambiguatePredicateExpression,
-  EncodeAssertingAssuming,
   EncodeAutoValue,
   EncodeByValueClassUsage,
   EncodeRange,

src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala

@@ -4,6 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.util.ScopedStack
 import vct.col.ast._
 import vct.col.origin._
+import vct.col.ref.{Ref, DirectRef}
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
 import vct.col.util.AstBuildHelpers._
 import vct.rewrite.veymont.VeymontContext
@@ -137,4 +138,31 @@ case class EncodeChorBranchUnanimity[Pre <: Generation](enabled: Boolean)
         )
       case _ => contract.rewriteDefault()
     }
+
+  def min(a: Expr[Post], b: Expr[Post]): Expr[Post] = ???
+  def max(a: Expr[Post], b: Expr[Post]): Expr[Post] = ???
+
+  def intersect(
+      left: CommunicateTarget[Pre],
+      right: CommunicateTarget[Pre],
+  ): CommunicateTarget[Post] =
+    (left, right) match {
+      case (left, right) if left.isSingle && right.isSingle && left == right =>
+        dispatch(left)
+      case (
+            CommTargetRange(Ref(f), RangeBinder(_, fLow, fHigh)),
+            CommTargetRange(Ref(g), RangeBinder(_, gLow, gHigh)),
+          ) if f == g =>
+        implicit val o: Origin = TraceOrigin()
+        CommTargetRange[Post](
+          succ(f),
+          RangeBinder(
+            new Variable(TInt()),
+            max(fLow.rewriteDefault(), gLow.rewriteDefault()),
+            min(fHigh.rewriteDefault(), gHigh.rewriteDefault()),
+          ),
+        )
+      case (left, right) if right.isSingle => intersect(right, left)
+      case (left, right) => assert(left.isSingle && right.isRange)
+    }
 }

src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala

@@ -50,7 +50,7 @@ case class EncodeEndpointInequalities[Pre <: Generation]()
           (endpoint, targets) +: makeInequalitySets(targets)
       }
     implicit val o = chor.o
-    val singleEndpoints = chor.endpoints.filter(_.isEndpoint)
+    val singleEndpoints = chor.endpoints.filter(_.isSingle)
     foldStar(
       makeInequalitySets(singleEndpoints).flatMap { case (endpoint, others) =>
         others.map { other =>