论文标题
基于ACL2浅嵌入Java中的ACL2的复杂Java代码生成器
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
论文作者
论文摘要
本文介绍了一个代码生成器，该代码生成器将ACL2构造转换为相应的Java构造，根据Java中ACL2的浅嵌入。从纯粹的功能性ACL2代码开始，生成的Java代码表现出必要的和面向对象的功能，例如破坏性更新，循环和过载。从ACL2到Java的总体翻译相当精心设计，包括几个ACL2至ACL2前翻译步骤，ACL2- java适当的翻译步骤以及几个Java-to Java to-Java后翻译步骤。实验表明，生成的Java代码不比ACL2代码慢得多。代码生成器还可以识别某些Java构建体的ACL2表示，并转化为Java，它可以根据ACL2中Java的浅嵌入（即以另一种方式）来预测代码生成方法。该代码生成器基于ACL2的ACL2深入嵌入Java中的ACL2的简单Java代码生成器，并显着扩展了Java代码生成器。
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.
