  This paper describes a code generator that translates ACL2 constructs to
corresponding Java constructs, according to a shallow embedding of ACL2 in
Java. Starting from purely functional ACL2 code, the generated Java code
exhibits imperative and object-oriented features like destructive updates,
loops, and overloading. The overall translation from ACL2 to Java is fairly
elaborate, consisting of several ACL2-to-ACL2 pre-translation steps, an
ACL2-to-Java proper translation step, and several Java-to-Java post-translation
steps. Experiments suggest that the generated Java code is not much slower than
the ACL2 code. The code generator can also recognize, and translate to Java,
ACL2 representations of certain Java constructs, forerunning a code generation
approach based on a shallow embedding of Java in ACL2 (i.e. going the other
way). This code generator builds upon, and significantly extends, a simple Java
code generator for ACL2 based on a deep embedding of ACL2 in Java.
