← Back to AILP Home

Nested Picks

An arm body is an ordinary block, so it may contain another pick. Nesting is how you dispatch on a second dimension once the first has been resolved.

func:failsafe = int32(tbb32:err) { exit 1i32; };
func:main = int32() {
    int32:major = 1;
    int32:minor = 2;
    pick (major) {
        (1) {
            pick (minor) {
                (1) { exit 11i32; },
                (2) { exit 12i32; },
                (*) { exit 19i32; }
            }
        },
        (*) { exit 99i32; }
    }
    exit 0i32;
};

Each pick is independent

The inner pick has its own exhaustiveness obligation, its own arm labels, and its own catch-all. The outer and inner picks share nothing except the variables in scope.

Tagged-payload inner picks

A common pattern is to match an enum variant in the outer pick, bind its payload, then pick on that payload:

enum:Msg = { Quit, Move(int32) };
func:failsafe = int32(tbb32:_code) { exit 1i32; };
func:main = int32() {
    Msg:m = Msg.Move(2);
    pick (m) {
        (Msg.Move(d)) {
            pick (d) {
                (1) { exit 1i32; },
                (2) { exit 2i32; },
                (*) { exit 9i32; }
            }
        },
        (Msg.Quit) { exit 0i32; }
    }
    exit 0i32;
};

fall is scoped to the nearest pick

A fall <label>; inside the inner pick targets the inner pick's labels only. There is no way to fall from an inner arm out into an outer arm — use a shared variable and let the outer pick re-dispatch if you need that effect. An unknown label is reported as ARIA-PICK-004 against the enclosing pick.

(K test 214 approximates a nested statement pick writing a result variable.)