		Search-engine friendly clone of the ACL2 documentation.

Atj-code-generation

Atj-post-translation

Post-translation performed by ATJ, as part of code generation.

As mentioned in atj-code-generation, after translating ACL2 to Java, ATJ performs a Java-to-Java post-translation. Currently, this post-translation consists of the following steps. These steps only apply to the shallow embedding approach.

We fold return statements into if branches. See here.
We eliminate tail recursions, replacing them with loops. See here.
We lift tests from conditionals to loops. See here.
We eliminate unnecessary continues from loops. See here.
We eliminate calls of the Java primitive array writing methods. See here.
We simplify conditional expressions with true or false tests. See here.

Subtopics

Atj-post-translation-remove-array-write-calls: Post-translation step: remove calls of the array writing methods.
Atj-post-translation-cache-const-methods: Post-translation step: cache constant methods in static final fields.
Atj-post-translation-tailrec-elimination: Post-translation step: eliminate tail recursions in favor of loops.
Atj-post-translation-fold-returns: Post-translation step: folding of returns into ifs.
Atj-post-translate-body: Post-translate a Java method body generated from an ACL2 function.
Atj-post-translation-lift-loop-tests: Post-translation step: lifting to loop tests.
Atj-post-translation-simplify-conds: Post-translation step: simplify conditional expressions.
Atj-post-translate-jcbody-elements: Post-translate a list of Java class body elements.
Atj-post-translation-remove-continue: Post-translation step: remove unnecessary continue statements.