← Back to AILP Home

Expression Pick (give)

(introduced in v0.37.7)

A pick can be used as an expression that produces a value. Each arm yields its result with give <expr>;, and the whole pick evaluates to the value given by the arm that ran.

func:failsafe = int32(tbb32:err) { exit 1i32; };
func:main = int32() {
    int32:sel = 2;
    int32:r = pick (sel) {
        (1) { give 10i32; },
        (2) { give 20i32; },
        (*) { give 0i32; }
    };
    exit r;   // exits 20
};

Note the trailing ; after the closing brace: here the pick is the right-hand side of an assignment, so the statement is the assignment, which ends with ;. (A statement pick has no trailing ; — see basics.)

give vs the statement form

Form Arm body ends with Whole pick ends with
statement pick normal statements } (no ;)
expression pick give <expr>; used in an expression, e.g. = pick(...) { ... };

give is only valid inside an expression pick. Using it in a statement pick is an error:

error: 'give' is only valid inside an expression pick

Arm-type unification

Every arm of an expression pick must give a value of the same type. The checker compares arm result types exactly; a mismatch is rejected:

int32:r = pick (sel) {
    (1) { give 10i32; },
    (*) { give "oops"; }   // error
};
error: expression pick arms yield mismatched types

The type of the whole expression is that single unified arm type.

Exhaustiveness is mandatory

An expression pick must produce a value on every path, so it must be exhaustive — there is no "fell through with no value" case. For an infinite selector domain this means a (*) arm is required; for a finite domain (enum, covered trit) full coverage suffices. A non-exhaustive expression pick is the same Non-exhaustive pick error as the statement form.

Where it can be used

An expression pick is a first-class expression: it can initialise a variable, be a call argument, or be embedded in a template literal. The IR generator allocates a result slot in the function entry block, each give stores into it, and the pick expression loads it once control rejoins.

Composes with guards

A where guard works inside an expression pick; the guarded arm still must give a value, and (as always) guarded arms do not count toward exhaustiveness, so keep a (*) arm.

(K does not model give; K tests 213–215 approximate expression picks by having each arm assign a result variable that is then exit-ed — see SEMANTIC_GAPS.md. Regressions: bug849–bug856.)