Atj-tutorial-deep
ATJ tutorial: Deep Embedding Approach.
This tutorial page describes and exemplifies
most aspects of using ATJ with the deep embedding approach.
Other aspects are described in subsequent pages.
Even though, as noted in atj-tutorial-deep-shallow,
the shallow embedding approach is generally preferred over the deep one,
some of the concepts common to the two approaches are discussed here.
So, if this tutorial page is skipped at first reading,
it may be necessary to come back to it
while reading the pages on the shallow embedding approach.
AIJ's Role
AIJ not only provides a default Java representation of the ACL2 values: it is a deep embedding of ACL2 in Java; more precisely, a deep embedding of the
executable, side-effect-free, non-stobj-accessing
subset of the ACL2 language without guards
(see atj-tutorial-background).
AIJ includes a Java representation of the ACL2 terms (in translated form)
and a Java representation of the ACL2 environment, consisting of function definitions and package definitions. AIJ also includes a Java implementation of the ACL2 primitive functions, and an ACL2 evaluator written in Java.
Besides an API to build and unbuild ACL2 values, AIJ also provides
an API to build an ACL2 environment
(i.e. to build ACL2 function and package definitions),
and an API to evaluate calls of ACL2 primitive and defined functions
without checking guards.
External Java code could use this whole API as follows
(see picture below):
- Build the ACL2 environment:
- Define the ACL2 packages of interest,
both built-in and user-defined,
in the order in which they appear in the ACL2 world.
- Define the ACL2 functions of interest,
both built-in and user-defined (except the primitive ones),
in any order.
- Evaluate ACL2 function calls:
- Build the name of the ACL2 function to call,
as well as zero or more ACL2 values to pass as arguments,
via the factory methods of the value classes.
- Call the Acl2NamedFunction.call(Acl2Value[]) method
on the function name with the (array of) arguments.
- Unbuild the returned Acl2Value as needed to inspect and use it,
using the getter methods of the value classes.
ATJ's Role
ATJ automates the first part of the protocol described above,
namely the building of the ACL2 environment
(see picture below).
ATJ generates Java code
that uses the AIJ API to build the ACL2 environment
and that provides a wrapper API
for external Java code to evaluate ACL2 function calls.
The external Java code must still directly use the AIJ API
to build and unbuild ACL2 values
passed to and received from function calls.
Example of Generated Code
For example, consider the following factorial function:
(defun fact (n)
(declare (xargs :guard (natp n)))
(if (zp n)
1
(* n (fact (1- n)))))To generate Java code for that function,
include ATJ via
(include-book "kestrel/java/atj/atj" :dir :system)
and call ATJ via
(java::atj fact :deep t :guards nil)
where :deep t specifies the deep embedding approach
and :guards nil specifies not to assume the guards' satisfaction
(more on this in atj-tutorial-deep-guards).
As conveyed by the message shown on the screen by ATJ,
two Java files, Acl2Code.java and Acl2CodeEnvironment.java,
are generated,
in the current directory (by default).
(If the files already exist, they are overwritten.)
Opening the Acl2Code.java file reveals that it contains
a single Java public class called Acl2Code.
The file imports all the (public) AIJ classes.
The Acl2Code class starts with a static initializer that calls
the static build() method
of the class Acl2CodeEnvironment,
which is in the file Acl2CodeEnvironment.java,
as can be seen by opening that file.
The Acl2CodeEnvironment class starts with
a package-private static method build()
that calls a number of methods to define ACL2 packages
and a number of methods to define ACL2 functions;
it also calls an AIJ method to validate the well-formedness of
all the function calls in the constructed ACL2 function definitions,
but the details of this are not discussed here.
The packages are all the known ones in the ACL2 world
at the time that ATJ is called:
the method names are derived from the package names,
as should be apparent.
The functions are fact and all the ones
called directly or indirectly by fact,
except for the primitive functions. In this case, the functions are
fact, zp, and not:
- fact calls zp, which calls not.
- fact also calls * and 1-,
but these are macros whose expansions call
the primitive functions binary-* and binary-+.
- zp also calls the primitive function if,
and the macro <=, whose expansion calls not
and the primitive function <.
- not calls the primitive function if.
ATJ looks at the translated bodies of the functions,
where macros, and also named constants, are expanded already.
The build() method is followed by
the (private) methods that it calls.
The package definition methods
build the packages' import lists (some quite long)
and pass them to the AIJ method to define packages;
the code that builds the import lists is generated by ATJ,
based on the results of pkg-imports on the known packages.
The function definition methods
build the functions' names, formal parameters, and bodies,
and pass them to the AIJ method to define functions;
the code that builds formal parameters and bodies is generated by ATJ,
based on the formals and unnormalized-body properties
of the function symbols.
The details of all these methods are unimportant here.
Back to the Acl2Code class,
after the static initializer,
there are two public methods,
which form the API to the ATJ-generated Java code
illustrated in the picture above.
The initialize() method has an empty body,
but its purpose is to ensure the initialization of the class,
and therefore the execution of the static initializer,
which defines all the ACL2 packages and functions of interest.
(In the embedding, the static initializer could be avoided,
putting the call of build() directly in initialize().
But in the shallow embedding, as explained in later tutorial pages,
the static initializer is needed,
and so the same is done in the deep embedding for uniformity.)
The call(Acl2Symbol, Acl2Value[]) method
evaluates an ACL2 function call,
by invoking the relevant AIJ method (the details are unimportant here).
Example of External Code
External Java code must call initialize()
not only before calling call(Acl2Symbol, Acl2Value[]),
but also before using AIJ's API to build
the Acl2Symbol and Acl2Values
to pass to call(Acl2Symbol, Acl2Value[]).
The reason is that the building of Acl2Symbols
depends on the definitions of the known packages being in place,
just as in ACL2.
The following is a simple example of external Java code
that uses the ATJ-generated code and AIJ:
import edu.kestrel.acl2.aij.*;
public class Test {
public static void main(String[] args)
throws Acl2UndefinedPackageException {
Acl2Code.initialize();
Acl2Symbol function = Acl2Symbol.make("ACL2", "FACT");
Acl2Value argument = Acl2Integer.make(100);
Acl2Value[] arguments = new Acl2Value[]{argument};
Acl2Value result = Acl2Code.call(function, arguments);
System.out.println("Result: " + result + ".");
}
}This code initializes the ACL2 environment,
creates the function symbol `acl2::fact',
creates a singleton array of arguments with the ACL2 integer 100,
calls the factorial function,
and prints the resulting value.
(AIJ's API includes toString() methods
to convert ACL2 values to Java strings.)
The Acl2UndefinedPackageException must be declared
because call(Acl2Symbol, Acl2Value[]) may throw it in general,
even though it will not in this case.
Example of Compiling and Running the Code
If the code above is in a file Test.java
in the same directory where Acl2Code.java was generated,
it can be compiled via
javac -cp [books]/kestrel/java/aij/java/out/artifacts/AIJ_jar/AIJ.jar \
Acl2Code.java Acl2CodeEnvironment.java Test.javawhere [books]/... must be replaced with
a proper path to the AIJ jar file
(see the documentation of AIJ for instructions on how to obtain that jar file).
After compiling, the code can be run via
java -cp [books]/kestrel/java/aij/java/out/artifacts/AIJ_jar/AIJ.jar:. \
Testwhere again [books]/... must be replaced with a proper path.
A fairly large number will be printed on the screen.
Some ACL2 code has just been run in Java.
Java Stack Space Considerations
If the 100 passed to the factorial function call
is increased to a sufficiently large value,
the execution of the Java code will result in a stack overflow
(this is just the JVM running out of stack memory;
it has nothing to do with type unsafety and security exploits).
This is unavoidable, because in the deep embedding approach
the ACL2 functions are evaluated via AIJ's recursive interpreter. Note also that recursive method calls in the JVM
may not be as efficiently implemented as recursive function calls in Lisp,
given that Java is an imperative language
and thus loops are the preferred way to repeat computations.
This stack overflow issue may be mitigated
by passing a larger stack size to the JVM,
via the -Xss option to the java command.
For example,
java -cp [books]/kestrel/java/aij/java/out/artifacts/AIJ_jar/AIJ.jar:. \
-Xss1G \
Testruns the factorial program with 1 GiB of stack space,
which should be larger than the default.
Previous: Deep and Shallow Embedding Approaches
Next: Java Representation of the ACL2 Terms
