		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation

Atj-post-translation-lift-loop-tests

Post-translation step: lifting to loop tests.

The tail recursion elimination step produces method bodies of the form while (true) { ... }. When the body of the while is an if one of whose branches is a return, then it is possible to lift the if tests to the loop test, moving the return after the loop.

More precisely, if the method body has the form

while (true) {
    if (<test>) {
        return <expr>;
    } else {
        ...
    }
}

it can be turned into

while (!<test>) {
    ...
}
return <expr>;

Simillarly, if the method body has the form

while (true) {
    if (<test>) {
        ....
    } else {
        return <expr>;
    }
}

it can be turned into

while (<test>) {
    ...
}
return <expr>;

This post-translation step performs these transformations, which produce more idiomatic looping code. It should be possible to extend the scope of this post-translation step, e.g. to cases in which the return is preceded by some statements.

Subtopics

Atj-check-liftable-loop-test: Check if a Java block is a while (true) ... loop with an if body whose test can be lifted to the loop.
Atj-check-single-return-with-expr: Check if a Java block consists of a single return with an expression.
Atj-lift-loop-test: Lift an if test to the enclosing loop.