Refinement with multi-field predicates

Area: Refinement & types Teaches: a refinement predicate is an ordinary boolean expression — it can read several fields and combine them with &&/||, comparisons, and string equality. Prerequisites: refinement (iff/where). Run: ox build examples/multi_field_refinement && ox run-scenario examples/multi_field_refinement

A single iff refinement classifies a Person by two fields at once:

pub type ActiveAdult <: Person iff {
    self.age >= 18 && self.status == "active"
};

ActiveAdult is the subset of people who are both adults and active. The predicate is evaluated per individual at query time against that individual’s declared fields — no membership is stored.

Running it

The scenario registers four people; only those satisfying both conjuncts are classified:

alice  age=25  status="active"    → ActiveAdult
bob    age=12  status="active"    → not (fails age >= 18)
carol  age=30  status="inactive"  → not (fails status == "active")
dave   age=45  status="active"    → ActiveAdult

so active_adults returns 2 rows (alice, dave) out of the 4 in all_people.

This example is compiled and run in CI; its runtime behaviour is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Refinement with multi-field predicates and logical operators.

mod people;

people.ar

//! Refinement with multi-field predicates and logical operators.
//!
//! Demonstrates:
//!   * Refinement using `&&` and `||`
//!   * Multiple fields in a single predicate
//!   * Comparison operators (`>=`, `<`, `==`)
//!
//! Expected runtime behavior — the refinement predicate is evaluated
//! per individual against the individual's declared field values:
//!
//!   alice  age=25  status="active"   →  ✓ ActiveAdult
//!   bob    age=12  status="active"   →  ✗ (too young)
//!   carol  age=30  status="inactive" →  ✗ (wrong status)
//!   dave   age=45  status="active"   →  ✓ ActiveAdult

pub type Person {
    mut age: Int,
    mut status: String,
}

pub type ActiveAdult <: Person iff { self.age >= 18 && self.status == "active" };

pub mutate register(p: Person, age: Int, status: String) {
    insert iof(p, Person);
    update p: Person set { age = age, status = status }
}

pub query all_people() -> Person;
pub query active_adults() -> ActiveAdult;