← Back to AILP Home

Optional blocks

Both completion clauses are optional. A when may have a then block, an end block, both, or neither. When the selected completion path has no block, the loop simply falls through to the statement after the when.

then only

when (i < 3i32) {
    i = i + 1i32;
} then {
    result = 2i32;   // runs on clean exit
}
// on a break, control falls through with result unchanged

A then-only when runs the block on a clean exit and falls through on a break (or zero iterations).

end only

when (i < 3i32) {
    i = i + 1i32;
    if (done) { break; }
} end {
    result = 3i32;   // runs on a break OR zero iterations
}
// on a clean exit, control falls through with result unchanged

An end-only when runs the block on a short-circuit and falls through on a clean exit.

Bare when

when (i < 3i32) {
    i = i + 1i32;
}
// no completion block — behaves exactly like `while (i < 3i32) { ... }`

A when with neither clause is indistinguishable from a while loop. There is no reason to prefer it stylistically; reach for when only when you actually use then or end.

Observing the fall-through

Because a fall-through leaves your variables untouched, seed a sentinel before the loop so the final value distinguishes "the block ran" from "fell through":

int32:result = 5i32;     // sentinel: 5 means "fell through"
when (cond) {
    // ...
} then {
    result = 2i32;       // 2 means "clean exit"
}
exit result;             // 2 if clean, 5 if it broke / zero-iterated

This is the pattern the v0.39.x regression tests use: a distinct seed value per slice makes each completion path observable through the process exit code.