|
|
|---|
|
|
|
|---|
ATJ tutorial: Deep and Shallow Embedding Approaches.
This tutorial page provides an introduction to the main code generation options provided by ATJ, namely the choice between the deep and shallow embedding approach.
Translating ACL2 to Java involves not only representing the ACL2 values in Java but also representing the ACL2 language constructs (function definitions, conditionals, etc.) in Java in some way so that they can be executed in Java. There are generally two approaches to representing a language in another language: deep embedding and shallow embedding. ATJ supports both.
In the deep embedding approach, both the syntax and (evaluation) semantics of ACL2 are represented explicitly in Java. There are Java data structures that correspond to the ACL2 language constructs, and there is Java code that executes these constructs consistently with ACL2's semantics. In other words, there is an interpreter of the ACL2 language written in the Java language.
In the shallow embedding approach, there is no such explicit representation of ACL2's syntax and (evaluation) semantics in Java. Instead, the ACL2 constructs are mapped to Java constructs in a way that Java's semantics corresponds to ACL2's semantics.
Compilers and code generators normally follow the shallow embedding approach. ATJ's initial version supported the deep embedding approach, because of its simplicity and assurance. ATJ's later versions added the shallow embedding approach, which provides more readable and performant Java code. The shallow embedding is the preferred approach, but support for the deep embedding has been retained and there are no plans to remove it.
In the following manual pages, first we describe the deep embedding approach, because it is simple and because some of the concepts also apply to the shallow embedding approach.
Previous: Java Representation of the ACL2 Values
Next: Deep Embedding Approach