← Back to AILP Home

Nested loops

Loops nest to any depth, and any form may nest inside any other — while-in-for, loop-in-till, and so on. The control-flow rules stay simple: bare control targets the innermost loop, labels target a named level.

Innermost by default

func:failsafe = int32(tbb32:err) {
    exit 1;
};

func:main = int32() {
    int32:count = 0i32;
    loop(0i32, 3i32, 1i32) {
        loop(0i32, 3i32, 1i32) {
            if ($ == 2i32) { break; }   // breaks the inner loop only
            count += 1i32;
        }
    }
    exit count;   // outer runs 3x, inner contributes 2 each => 6
};

A bare break; in the inner loop ends just that loop; the outer loop continues with its next iteration.

Escaping multiple levels

To leave more than one level at once, name the outer loop and break to it:

outer: loop(0i32, 3i32, 1i32) {
    loop(0i32, 3i32, 1i32) {
        if (done()) { break(outer); }   // leaves both
    }
}

See Labeled control for the full label vocabulary, including three-level nests where each break(name) / continue(name) targets a distinct level.

Mixing forms

Nesting is form-agnostic. A common pattern is a for-in over rows containing a while that consumes a row:

for row in rows {
    int32:i = 0i32;
    while (i < row_len) {
        consume(row, i);
        i += 1i32;
    }
}

Scope per level

Each loop body has its own block scope. A variable declared in an inner body is gone when the inner loop ends; declare shared state in the outer body (or the enclosing function) when both levels need it.

Next: Invariants and contracts.