← Back to AILP Home

break routing

A break inside a when body always routes the loop to its end block. This is the defining difference between then and end: then is "ran out of work", end is "stopped early", and break is the canonical early stop.

when (i < 100i32) {
    i = i + 1i32;
    if (i == 2i32) { break; }
} then {
    result = 2i32;   // skipped
} end {
    result = 3i32;   // runs: a break fired
}

It does not matter how many iterations completed before the break. As soon as the broke flag is set, the completion decision favors end:

end  ⇐  broke || !completed

break targets the innermost when

Like every loop, break; leaves the innermost enclosing loop. A break in an inner when routes the inner loop to its end; the outer when is unaffected and still completes on its own terms.

when (a < 2i32) {
    a = a + 1i32;
    when (b < 5i32) {
        b = b + 1i32;
        break;            // ends the INNER when only
    } then {
        r = r + 1i32;     // inner then: skipped
    } end {
        r = r + 10i32;    // inner end: runs each outer pass
    }
} then {
    r = r + 100i32;       // outer then: runs (outer completed cleanly)
} end {
    r = r + 1000i32;      // outer end: skipped
}
// over 2 outer iterations: 2*10 + 100 = 120

To break out of an outer when from inside an inner one, use a labeled break — see Nested when.

Loan release on the break path

The borrow checker treats the break edge like any other loop exit: loans taken in the body are released before control reaches end. A fresh borrow of the same location inside end therefore does not conflict with a body borrow:

when (i < 5i32) {
    $$m int32:rb = pair.a;   // body loan
    rb = rb + 1i32;
    i = i + 1i32;
    if (done) { break; }
} then {
    // ...
} end {
    $$m int32:re = pair.a;   // fresh loan — body loan already released
    re = re + 100i32;
}

This mirrors the loan-release-on-break behavior documented for the other loop forms in break and continue.