From fde1216f42fccc4cb8b8f0cddceafdbe27cce9e4 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Wed, 11 Dec 2024 16:46:05 +0100 Subject: [PATCH] Get started on intersect --- .../declaration/singular/EndpointImpl.scala | 2 +- .../ast/unsorted/CommTargetEndpointImpl.scala | 4 +-- .../ast/unsorted/CommunicateTargetImpl.scala | 13 +++++++++ src/col/vct/col/ast/unsorted/CtExprImpl.scala | 3 +- .../vct/col/serialize/SerializeOrigin.scala | 2 +- src/main/vct/main/stages/Transformation.scala | 1 - .../EncodeChorBranchUnanimity.scala | 28 +++++++++++++++++++ .../EncodeEndpointInequalities.scala | 2 +- 8 files changed, 48 insertions(+), 7 deletions(-) diff --git a/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala b/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala index 33819305d..694c83232 100644 --- a/src/col/vct/col/ast/declaration/singular/EndpointImpl.scala +++ b/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]]) diff --git a/src/col/vct/col/ast/unsorted/CommTargetEndpointImpl.scala b/src/col/vct/col/ast/unsorted/CommTargetEndpointImpl.scala index b844cf99d..92d02dd84 100644 --- a/src/col/vct/col/ast/unsorted/CommTargetEndpointImpl.scala +++ b/src/col/vct/col/ast/unsorted/CommTargetEndpointImpl.scala @@ -9,7 +9,7 @@ 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 @@ -17,7 +17,7 @@ trait CommTargetEndpointImpl[G] 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() } } diff --git a/src/col/vct/col/ast/unsorted/CommunicateTargetImpl.scala b/src/col/vct/col/ast/unsorted/CommunicateTargetImpl.scala index b200be6d7..3c82a78b1 100644 --- a/src/col/vct/col/ast/unsorted/CommunicateTargetImpl.scala +++ b/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 } diff --git a/src/col/vct/col/ast/unsorted/CtExprImpl.scala b/src/col/vct/col/ast/unsorted/CtExprImpl.scala index 758969534..bb4370e8b 100644 --- a/src/col/vct/col/ast/unsorted/CtExprImpl.scala +++ b/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 diff --git a/src/col/vct/col/serialize/SerializeOrigin.scala b/src/col/vct/col/serialize/SerializeOrigin.scala index de2e59c39..8e4a01afe 100644 --- a/src/col/vct/col/serialize/SerializeOrigin.scala +++ b/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, { diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index c7a02fb03..a234b4fac 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/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, diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala index 5a89c21e8..fc765709b 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala +++ b/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) + } } diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala index bb5701f7c..b951039f2 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodeEndpointInequalities.scala +++ b/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 =>