|
|
|---|
|
|
|
|---|
Code generation performed by ATJ.
We generate Java abstract syntax, which we then pretty-print to files.
We translate ACL2 values, terms, and lambda expressions to Java expressions ``preceded by'' Java blocks. By this we mean that the relevant code generation functions generally return a Java block and a Java expression, such that the block must be executed before the expression. That is, the Java block provides the necessary code to ``prepare'' the evaluation of the Java expression. The Java block may include Java expressions and blocks that are recursively generated.
To illustrate this concept, consider the generation of a Java expression to build the Java representation of an ACL2 cons pair. In some circumstances, since the pair may be a large binary tree, we prefer not to generate a large Java expression. Instead, we generate a Java block that sets a local variable to be the car, a Java block that sets another local variable to be the cdr, and then a Java expression that builds the pair from those two variables. The two blocks are concatenated, resulting in a block and an expression for the cons pair in question. But the expressions assigned to the two local variables may in turn need to be built that way, recursively. This recursion ends when an atom value is reached. A similar strategy is used to build Java representations of ACL2 terms and lambda expressions, which have a recursive structure analogously to cons pairs.
As special cases, some of these code generation functions may return just Java expressions and no blocks, since they would always return empty blocks.
These code generation functions keep track of the next local variables to use via numeric indices that are threaded through the functions. The indices are appended to the base names for the local variables in order to guarantee the uniqueness of the local variables.
The
The code generation process consists of a pre-translation from ACL2 to ACL2, followed by a translation from ACL2 to Java, followed by a post-translation from Java to Java. The pre-translation turns the ACL2 code into a form that is closer to the target Java code, thus making the translation simpler. The correctness of the pre-translation can be formally proved within ACL2, without involving (the semantics of) Java; however, some of the proofs may need to be based on an an evaluation semantics of ACL2, rather than just a logical semantics. The post-translation makes some improvements directly on the Java code, making it more efficient and idiomatic.