Aij-atj-paper
ACL2-2018 Workshop paper on AIJ and ATJ.
The ACL2-2018 Workshop paper on AIJ and ATJ provides an overview of AIJ and ATJ,
along with some performance measurements.
The presentation of the Workshop talk is available here.
As AIJ and ATJ are being extended and improved over time,
some of the contents of the paper and presentation are becoming outdated.
This manual provides up-to-date information about AIJ and ATJ.
The following differences exist
between the current version of AIJ and ATJ
and the version described in the paper and presentation:
- The Java class Acl2Constant
has been renamed to Acl2QuotedConstant.
- The Java class Acl2Cons
has been renamed to Acl2ConsPair.
- The Java class Acl2FunctionApplication
has been renamed to Acl2FunctionCall.
- AIJ's evaluator has been extended
to recognize a ``pseudo-function'' or
and to execute it non-strictly,
as an optimized version of an if
whose test and `then' branch are the same.
Accordingly, ATJ has been extended
to recognize translated terms of the form (if a a b)
and to generate Java code to represent them as (or a b).
- The Java representation of ACL2 variables
has been optimized to include numeric indices
derived from the position of variables
in the lists of parameters
in named function definitions and lambda expressions.
These indices are set in the body of each function definition
as the function definition is added to
the Java representation of the ACL2 environment.
The AIJ evaluator has been optimized to use
Java arrays of ACL2 values as bindings,
instead of hash maps from ACL2 symbols to values,
enabling faster lookup of variables in bindings.
- The Java representation of ACL2 named functions
has been changed to consist of native and defined functions.
The former have a native Java implementation,
while the latter have a definition
in the Java representation of the ACL2 environment.
All the ACL2 primitive functions are represented as native functions,
the ``pseudo-function'' or is represented like that as well,
and other built-in ACL2 functions could be represented like that as well
in the future.
Each native function has its own unique Java class and instance:
its application to values is now handled via Java's dynamic dispatch
rather than by cases analysis, thus optimizing evaluation.
Each defined function has its own unique instance as well
(so, all the ACL2 named functions are interned),
and its representation includes its definition,
so that evaluation no longer needs to
look up the function definition in the environment,
resulting in increased execution speed.
- The Java class Acl2Environment has been eliminated.
The information about the function definitions
is now stored directly with the function themselves.
The information about the package definitions
is now stored directly into instances of a Java class Acl2Package
that has been added for this purpose;
this class also contains the information about the package witness name.
- The package witness name,
i.e. the content of the *pkg-witness-name* constant,
is now stored in a final static field,
which therefore no longer needs to be initialized
by code external to AIJ.
The consistency of this Java value with the actual ACL2 value
is checked via an assertion in a newly added community book
kestrel/java/aij/assumptions.lisp.
- The return types of some of the native Java implementation methods
of the ACL2 primitive functions in AIJ
have been made more precise than the general type Acl2Value,
e.g. now the method for equal returns Acl2Symbol.
- Some native Java implementations of ACL2 primitive functions
have been optimized.
- Public static methods have been added
to execute the native implementations of ACL2 functions
from outside AIJ.
This is in support of the shallow embedding approach (see below).
- Some variant native implementations of ACL2 functions
have been added that assume the satisfaction of the guards.
This is in support of the shallow embedding approach (see below)
when assuming that the guards are satisfied (see below).
- AIJ has been extended with the ability to validate statically that
all the function calls reference existing functions
and have a number of arguments that matches the function arity.
AIJ provides a new public API method
to validate all the currently defined functions.
AIJ can thus avoid these checks at run time,
resulting in increased execution speed.
- ATJ has been extended with a facility to generate Java code
to execute tests that compare
results obtained via evaluation in ACL2
with results obtained via evaluation in AIJ.
- ATJ has been extended with a facility to generate Java code
according to a shallow embedding approach,
in addition to the deep embedding approach described in the paper.
- ATJ has been extended with a facility to generate Java code
assuming that all the guards are satisfied.
This facility is available for
both the deep and shallow embedding approaches.
The last two bullet points above provide a major extension of ATJ,
which produces much more readable and efficient Java code,
including Java code that manipulates Java primitive types and arrays.
