Focus/minimization functionality

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

@@ -696,6 +696,7 @@ final class Function[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val threadLocal: Boolean = false,
+    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]
@@ -709,6 +710,7 @@ final class Procedure[G](
     val inline: Boolean = false,
     val pure: Boolean = false,
     val vesuv_entry: Boolean = false,
+    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]
@@ -723,6 +725,7 @@ final class Predicate[G](
     val body: Option[Expr[G]],
     val threadLocal: Boolean = false,
     val inline: Boolean = false,
+    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)
@@ -760,6 +763,7 @@ final class InstanceFunction[G](
     val contract: ApplicableContract[G],
     val inline: Boolean,
     val threadLocal: Boolean = false,
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[ContractedFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractFunction[G]
@@ -773,6 +777,7 @@ final class Constructor[G](
     val body: Option[Statement[G]],
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
+    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]
@@ -785,6 +790,7 @@ final class InstanceMethod[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val pure: Boolean = false,
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractMethod[G]
@@ -796,6 +802,7 @@ final class InstancePredicate[G](
     val body: Option[Expr[G]],
     val threadLocal: Boolean = false,
     val inline: Boolean = false,
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractPredicate[G]
@@ -817,6 +824,7 @@ final class InstanceOperatorFunction[G](
     val contract: ApplicableContract[G],
     val inline: Boolean,
     val threadLocal: Boolean = false,
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[ContractedFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractFunction[G]
@@ -829,6 +837,7 @@ final class InstanceOperatorMethod[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val pure: Boolean = false,
+    val filter: FilterMode[G] = NeutralFilterMode[G](),
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends ClassDeclaration[G]
     with AbstractMethod[G]
@@ -898,8 +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]
+    extends FilterApplicable[G] with InlineableApplicableImpl[G]
 sealed trait AbstractPredicate[G]
     extends InlineableApplicable[G] with AbstractPredicateImpl[G]
 sealed trait ContractApplicable[G]
@@ -910,6 +921,16 @@ sealed trait AbstractMethod[G]
     extends ContractApplicable[G] with AbstractMethodImpl[G]
 sealed trait Field[G] extends FieldImpl[G]
 
+@family
+sealed trait FilterMode[G] extends NodeFamily[G] with FilterModeImpl[G]
+case class Include[G]()(implicit val o: Origin = DiagnosticOrigin)
+    extends FilterMode[G] with IncludeImpl[G]
+case class Exclude[G]()(implicit val o: Origin = DiagnosticOrigin)
+    extends FilterMode[G] with ExcludeImpl[G]
+// Slightly longer name here to avoid claiming the keyword "Neutral", just Option[FilterMode] can be avoided.
+case class NeutralFilterMode[G]()(implicit val o: Origin = DiagnosticOrigin)
+    extends FilterMode[G] with NeutralFilterModeImpl[G]
+
 @family @scopes[Variable]
 @scopes[LocalHeapVariable]
 final case class SignalsClause[G](binding: Variable[G], assn: Expr[G])(
@@ -3534,6 +3555,7 @@ final class LLVMSpecFunction[G](
     val contract: ApplicableContract[G],
     val inline: Boolean = false,
     val threadLocal: Boolean = false,
+    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/ExcludeImpl.scala

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

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

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

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/IncludeImpl.scala

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

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/typerules/CoercingRewriter.scala

@@ -364,6 +364,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case node: ApplyAnyPredicate[Pre] => coerce(node)
       case node: FoldTarget[Pre] => coerce(node)
       case node: LLVMFloatType[Pre] => node
+      case node: FilterMode[Pre] => coerce(node)
     }
 
   def preCoerce(decl: Declaration[Pre]): Declaration[Pre] = decl
@@ -2973,4 +2974,5 @@ abstract class CoercingRewriter[Pre <: Generation]()
   def coerce(node: PVLEndpointName[Pre]): PVLEndpointName[Pre] = node
   def coerce(node: EndpointName[Pre]): EndpointName[Pre] = node
 
+  def coerce(node: FilterMode[Pre]): FilterMode[Pre] = node
 }

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),
           )