Finally do something about prettyprinting. Also add endpoint expressi…

…ons around branch unanimity condition
utwente-fmt · Dec 20, 2024 · 163776b · 163776b
1 parent 661c2fc
commit 163776b
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 13 deletions.
diff --git a/src/col/vct/col/ast/unsorted/CommTargetRangeImpl.scala b/src/col/vct/col/ast/unsorted/CommTargetRangeImpl.scala
@@ -8,7 +8,7 @@ import vct.col.check.{CheckContext, CheckError}
 trait CommTargetRangeImpl[G]
     extends CommTargetRangeOps[G] with CommunicateTargetImpl[G] {
   this: CommTargetRange[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+  override def layout(implicit ctx: Ctx): Doc = Text(ctx.name(ref)) <> range
 
   override def check(context: CheckContext[G]): Seq[CheckError] =
     super.check(context) ++ {

diff --git a/src/col/vct/col/ast/unsorted/EndpointFamilyExprImpl.scala b/src/col/vct/col/ast/unsorted/EndpointFamilyExprImpl.scala
@@ -7,7 +7,8 @@ import vct.col.print._
 
 trait EndpointFamilyExprImpl[G] extends EndpointFamilyExprOps[G] {
   this: EndpointFamilyExpr[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+  override def layout(implicit ctx: Ctx): Doc = Text(ctx.name(ref))
+  override def precedence: Int = Precedence.ATOMIC
 
   override def t: Type[G] = TSeq(ref.decl.t)
 }
diff --git a/src/col/vct/col/ast/unsorted/PVLCommTargetRangeImpl.scala b/src/col/vct/col/ast/unsorted/PVLCommTargetRangeImpl.scala
@@ -11,7 +11,7 @@ import vct.col.print._
 
 trait PVLCommTargetRangeImpl[G] extends PVLCommTargetRangeOps[G] {
   this: PVLCommTargetRange[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+  override def layout(implicit ctx: Ctx): Doc = Text(name) <> range
 
   override def t: Type[G] = ref.get.decl.t
 }
diff --git a/src/col/vct/col/ast/unsorted/RangeBinderImpl.scala b/src/col/vct/col/ast/unsorted/RangeBinderImpl.scala
@@ -8,6 +8,7 @@ import vct.col.ast.ops.{RangeBinderFamilyOps, RangeBinderOps}
 trait RangeBinderImpl[G]
     extends RangeBinderOps[G] with RangeBinderFamilyOps[G] {
   this: RangeBinder[G] =>
-  // override def layout(implicit ctx: Ctx): Doc = ???
+  override def layout(implicit ctx: Ctx): Doc =
+    Text("[") <> ctx.name(binder) <+> ":=" <+> low <+> ".." <+> high <> "]"
   require(binder.t == TInt[G]())
 }
diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala
@@ -248,16 +248,16 @@ case class EncodeChorBranchUnanimity[Pre <: Generation](enabled: Boolean)
     alpha match {
       case r @ (_: CommTargetEndpoint[Pre] | _: CommTargetIndex[Pre]) =>
         partialProject(expr, r) |===| b
-      case CommTargetRange(f, RangeBinder(oldV, low, high)) =>
-        variables.scope(forall(
-          TInt(),
-          v => {
-            variables.succeedOnly(oldV, v.ref.decl)
+      case target @ CommTargetRange(f, RangeBinder(oldV, low, high)) =>
+        variables.scope {
+          val newTarget = target.rewriteDefault()
+          val v = newTarget.range.binder.get
+          EndpointExpr(
+            newTarget,
             ((dispatch(low) <= v) && (v < dispatch(high))) ==>
-              partialProject(expr, CommTargetIndex(f, oldV.get)) |===| b
-          },
-        ))
-
+              partialProject(expr, CommTargetIndex(f, oldV.get)) |===| b,
+          )
+        }
     }
   }