A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java

TL;DR

This paper presents a code generator that translates ACL2 functional code into Java, producing imperative and object-oriented features, and demonstrates that the generated Java code maintains performance close to the original ACL2 code.

Contribution

It introduces a novel shallow embedding-based translation approach from ACL2 to Java, extending previous deep embedding methods and enabling recognition of Java constructs within ACL2.

Findings

Generated Java code is not much slower than ACL2 code.

The generator can recognize and translate ACL2 representations of Java constructs.

The approach extends previous deep embedding methods with a shallow embedding technique.

Abstract

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.