← Back to AILP Home

Guards (where)

(introduced in v0.37.6)

A where clause attaches a boolean condition to an arm. The arm matches only when its pattern matches and the guard expression is true.

func:failsafe = int32(tbb32:err) { exit 1i32; };
func:main = int32() {
    int32:x = 7;
    pick (x) {
        (n) where n > 10 { exit 2i32; },
        (n) where n > 5  { exit 1i32; },
        (*)              { exit 0i32; }
    }
    exit 0i32;
};

With x == 7 the first guard (n > 10) is false, the second (n > 5) is true, so the program exits 1.

Syntax

(pattern) where <bool-expr> { body }

The guard goes between the pattern and the body. Any pattern bindings (like n above) are in scope inside the guard expression.

Guards and exhaustiveness

A guarded arm might not match even when its pattern does — the guard could be false. The exhaustiveness checker therefore ignores guarded arms when deciding whether the pick is total. In practice this means a pick that uses guards almost always needs a (*) arm (or an unguarded arm) to cover the "every guard was false" case:

error: Non-exhaustive pick statement. Missing cases: ... (guarded arms do not count toward exhaustiveness)

Guards disable jump tables

Because a guard has to be evaluated at runtime, a pick with any guarded arm is lowered to a compare-chain rather than a jump table (see integer dispatch). This is a behaviour-neutral performance detail.

Guards in expression picks

A where guard composes with the expression form: a guarded arm in an expression pick still must give a value, and the guard is evaluated before the give.

(K does not model where guards; K tests 211–212 approximate guard true/false control flow with an inner pick on the guard's truth value — see SEMANTIC_GAPS.md.)