		Search-engine friendly clone of the ACL2 documentation.

Atj-code-generation

Atj-pre-translation

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

As mentioned in atj-code-generation, prior to generating Java code, ATJ performs an ACL2-to-ACL2 pre-translation. Currently, this pre-translation consists of the following steps. The first three steps apply to both the deep and the shallow embedding; the others apply only to the shallow embedding.

We remove return-last. See atj-pre-translation-remove-return-last.
We remove dead if branches. See atj-pre-translation-remove-dead-if-branches.
We remove the unused lambda-bound variables. See atj-pre-translation-unused-vars.
We remove the trivial lambda-bound variables. See atj-pre-translation-trivial-vars.
We replace list calls with mv calls in functions that return multiple results. See atj-pre-translation-multiple-values.
We check (on the ACL2 code translated to Java) that the generated Java code does not use AIJ types. See atj-pre-translation-no-aij-types-analysis.
We annotate terms with ATJ type information. See atj-pre-translation-type-annotation.
We perform a single-threadedness analysis of the Java primitive arrays, but only if :guards is t. See atj-pre-translation-array-analysis.
We mark the lambda-bound variables that can be reused and destructively updated in Java. See atj-pre-translation-var-reuse.
We rename variables so that their names are valid Java variable names and so that different variables with the same name are renamed apart, unless they have been marked for reuse in the previous step. See atj-pre-translation-var-renaming.
We replace calls of the form (if a b nil) with calls of the form (and a b). See atj-pre-translation-conjunctions.
We replace calls of the form (if a a b) with calls of the form (or a b). See atj-pre-translation-disjunctions.

Subtopics

Atj-pre-translation-array-analysis: Pre-translation step performed by ATJ: single-threadedness analysis of Java primitive arrays.
Atj-pre-translation-type-annotation: Pre-translation step performed by ATJ: addition of type annotations.
Atj-pre-translation-var-reuse: Pre-translation step performed by ATJ: marking of reusable lambda-bound variables.
Atj-pre-translate: Pre-translate the formal parameters and body of an ACL2 function definition.
Atj-pre-translation-multiple-values: Pre-translation step performed by ATJ: replacement of list calls with mv calls.
Atj-pre-translation-no-aij-types-analysis: Pre-translation step performed by ATJ: analysis for the :no-aij-types option.
Atj-pre-translation-var-renaming: Pre-translation step performed by ATJ: renaming of the ACL2 variables.
Atj-pre-translation-remove-return-last: Pre-translation step performed by ATJ: removal of return-last.
Atj-pre-translation-disjunctions: Pre-translation step performed by ATJ: replacement of (if a a b) calls with or calls.
Atj-pre-translation-trivial-vars: Pre-translation step performed by ATJ: removal of all the trivial lambda-bound variables.
Atj-pre-translation-conjunctions: Pre-translation step performed by ATJ: replacement of (if a b nil) calls with and calls.
Atj-pre-translation-unused-vars: Pre-translation step performed by ATJ: removal of all the unused lambda-bound variables.
Atj-pre-translation-remove-dead-if-branches: Pre-translation step performed by ATJ: removal of dead if branches.