Post-translation step:
folding of
ATJ's ACL2-to-Java translation
introduces a Java local variable for every if in ACL2:
the variable is assigned in the `then' and `else' branches,
and then used in subsequent Java code.
When the subsequent Java code is simply a
... <type> <result> = null; if (...) { ... <result> = <then>; } else { ... <result> = <else>; } return <result>;
This post-translation step folds the
... if (...) { ... return <then>; } else { ... return <else>; }
In fact, it does so recursively:
if the new `then' and/or `else' branch has the same form as above
(i.e.
The function atj-gen-shallow-fndef-method,
which translates an ACL2 function to a Java method,
always produces a method body that ends with a single