Ported the whole thing, but don't have the syntax yet to test it...!

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

@@ -696,7 +696,7 @@ final class Function[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val threadLocal: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[ContractedFailure])(implicit val o: Origin)
     extends GlobalDeclaration[G] with AbstractFunction[G] with FunctionImpl[G]
 @scopes[LabelDecl]
@@ -710,7 +710,7 @@ final class Procedure[G](
     val inline: Boolean = false,
     val pure: Boolean = false,
     val vesuv_entry: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends GlobalDeclaration[G] with AbstractMethod[G] with ProcedureImpl[G]
 @scopes[LabelDecl]
@@ -725,7 +725,7 @@ final class Predicate[G](
     val body: Option[Expr[G]],
     val threadLocal: Boolean = false,
     val inline: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(implicit val o: Origin)
     extends GlobalDeclaration[G] with AbstractPredicate[G] with PredicateImpl[G]
 final class Enum[G](val constants: Seq[EnumConstant[G]])(implicit val o: Origin)
@@ -763,7 +763,7 @@ final class InstanceFunction[G](
     val contract: ApplicableContract[G],
     val inline: Boolean,
     val threadLocal: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[ContractedFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractFunction[G]
@@ -777,7 +777,7 @@ final class Constructor[G](
     val body: Option[Statement[G]],
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends ClassDeclaration[G] with AbstractMethod[G] with ConstructorImpl[G]
 @scopes[LabelDecl]
@@ -790,7 +790,7 @@ final class InstanceMethod[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val pure: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractMethod[G]
@@ -802,7 +802,7 @@ final class InstancePredicate[G](
     val body: Option[Expr[G]],
     val threadLocal: Boolean = false,
     val inline: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractPredicate[G]
@@ -824,7 +824,7 @@ final class InstanceOperatorFunction[G](
     val contract: ApplicableContract[G],
     val inline: Boolean,
     val threadLocal: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[ContractedFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractFunction[G]
@@ -837,7 +837,7 @@ final class InstanceOperatorMethod[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val pure: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractMethod[G]
@@ -907,10 +907,10 @@ final class ParInvariantDecl[G]()(implicit val o: Origin)
     extends Declaration[G] with ParInvariantDeclImpl[G]
 
 sealed trait Applicable[G] extends ApplicableImpl[G] with Declaration[G]
+sealed trait FilterApplicable[G]
+    extends Applicable[G] with FilterApplicableImpl[G]
 sealed trait InlineableApplicable[G]
-    extends Applicable[G]
-    with InlineableApplicableImpl[G]
-    with FilterApplicable[G]
+    extends FilterApplicable[G] with InlineableApplicableImpl[G]
 sealed trait AbstractPredicate[G]
     extends InlineableApplicable[G] with AbstractPredicateImpl[G]
 sealed trait ContractApplicable[G]
@@ -921,10 +921,6 @@ sealed trait AbstractMethod[G]
     extends ContractApplicable[G] with AbstractMethodImpl[G]
 sealed trait Field[G] extends FieldImpl[G]
 
-sealed trait FilterApplicable[G] {
-  def filter: FilterMode[G]
-}
-
 @family
 sealed trait FilterMode[G] extends NodeFamily[G] with FilterModeImpl[G]
 case class Include[G]()(implicit val o: Origin = DiagnosticOrigin)
@@ -3559,7 +3555,7 @@ final class LLVMSpecFunction[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val threadLocal: Boolean = false,
-    val filter: FilterMode[G] = NeutralFilterMode(),
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[ContractedFailure])(implicit val o: Origin)
     extends LLVMCallable[G]
     with AbstractFunction[G]

src/col/vct/col/ast/declaration/category/AbstractPredicateImpl.scala

@@ -1,9 +1,10 @@
 package vct.col.ast.declaration.category
 
-import vct.col.ast.{AbstractPredicate, TResource, Type}
+import vct.col.ast.{AbstractPredicate, Expr, TResource, Type}
 
 trait AbstractPredicateImpl[G] extends InlineableApplicableImpl[G] {
   this: AbstractPredicate[G] =>
+  def body: Option[Expr[G]]
   def threadLocal: Boolean
   override def returnType: Type[G] = TResource()
 }

src/col/vct/col/ast/declaration/category/FilterApplicableImpl.scala

@@ -0,0 +1,8 @@
+package vct.col.ast.declaration.category
+
+import vct.col.ast.{FilterApplicable, FilterMode}
+
+trait FilterApplicableImpl[G] extends ApplicableImpl[G] {
+  this: FilterApplicable[G] =>
+  def filter: FilterMode[G]
+}

src/col/vct/col/ast/declaration/category/InlineableApplicableImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.declaration.category
 
 import vct.col.ast.InlineableApplicable
 
-trait InlineableApplicableImpl[G] extends ApplicableImpl[G] {
+trait InlineableApplicableImpl[G] extends FilterApplicableImpl[G] {
   this: InlineableApplicable[G] =>
   def inline: Boolean
 }

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

@@ -1,10 +1,13 @@
 package vct.col.ast.unsorted
 
-import vct.col.ast.AmbiguousFoldTarget
+import vct.col.ast.{AmbiguousFoldTarget, ApplyAnyPredicate}
 import vct.col.ast.ops.AmbiguousFoldTargetOps
 import vct.col.print._
 
 trait AmbiguousFoldTargetImpl[G] extends AmbiguousFoldTargetOps[G] {
   this: AmbiguousFoldTarget[G] =>
   override def layout(implicit ctx: Ctx): Doc = target.show
+
+  // Not supported, until someone implements it
+  def apply: ApplyAnyPredicate[G] = ???
 }

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

@@ -1,11 +1,12 @@
 package vct.col.ast.unsorted
 
-import vct.col.ast.FoldTarget
+import vct.col.ast.{AbstractPredicate, ApplyAnyPredicate, FoldTarget}
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.ops.FoldTargetFamilyOps
 import vct.col.print._
 
 trait FoldTargetImpl[G] extends NodeFamilyImpl[G] with FoldTargetFamilyOps[G] {
   this: FoldTarget[G] =>
 
+  def apply: ApplyAnyPredicate[G]
 }

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

@@ -0,0 +1,10 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.NeutralFilterMode
+import vct.col.ast.ops.NeutralFilterModeOps
+import vct.col.print._
+
+trait NeutralFilterModeImpl[G] extends NeutralFilterModeOps[G] {
+  this: NeutralFilterMode[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/util/AstBuildHelpers.scala

@@ -372,19 +372,23 @@ object AstBuildHelpers {
     def rewrite(
         args: => Seq[Variable[Post]] = rewriter.variables
           .dispatch(predicate.args),
+        body: => Option[Expr[Post]] = predicate.body
+          .map((e: Expr[Pre]) => rewriter.dispatch(e)),
         inline: => Boolean = predicate.inline,
         threadLocal: => Boolean = predicate.threadLocal,
     ): AbstractPredicate[Post] =
       predicate match {
         case predicate: Predicate[Pre] =>
           predicate.rewrite(
             args = args,
+            body = body,
             inline = Some(inline),
             threadLocal = Some(threadLocal),
           )
         case predicate: InstancePredicate[Pre] =>
           predicate.rewrite(
             args = args,
+            body = body,
             inline = Some(inline),
             threadLocal = Some(threadLocal),
           )