Atj-tutorial-evaluator
ATJ tutorial: ACL2 Evaluator Written in Java.
For the deep embedding approach, AIJ provides an ACL2 evaluator written in Java.
For ease of exposition and understanding,
we first describe
(key aspects of) the initial implementation of the evaluator
(as it was in earlier versions of AIJ),
and then we describe how the current implementation
is obtained by optimizing the initial one.
This tutorial page may be skipped at first reading.
Java Methods
The evaluator is realized via
the implementing methods of the abstract methods
Acl2Term.eval(Acl2Value[]) and Acl2Function.apply(Acl2Value[]);
The implementing methods are
in subclasses of Acl2Term and Acl2Function.
Recall that all these classes provide the Java representation of ACL2 terms.
Initial Implementation
In early versions of AIJ,
the eval methods in Acl2Term and subclasses
took a java.lang.Map<Acl2Symbol, Acl2Value> as argument,
instead of an Acl2Value[] as in the current version of AIJ.
Such a map was a binding of variables (i.e. symbols) to values,
with respect to which quoted constants, variables, and function calls
were evaluated:
- Evaluating a quoted constant returned its value,
independently from the binding of variables to values.
- Evaluating a variable returned the value associated to the variable,
which was looked up in the binding.
- Evaluating a function call caused
first the recursive evaluation of all the arguments of the call,
and then the application of the function to the resulting values.
(See below.)
The apply methods in Acl2Function and subclasses
take an Acl2Value[] argument in all versions of AIJ.
The array is the sequence of values to apply the function to.
Function application proceeded as follows in early versions of AIJ:
- Applying a lambda expression returned the result of
recursively evaluating the body of the lambda expression
with a binding of the parameters of the lambda expressions
to the argument values.
(Recall that lambda expressions are always closed
in ACL2 translated terms,
so each lambda expression body is evaluated in a new binding.)
- Applying a natively implemented function returned the result of executing the native Java implementation
on the argument values.
- Applying a function with an ACL2 definition returned the result of
recursively evaluating the body of the function
with a binding of the parameters of the function
to the argument values.
This simple and typical evaluation algorithm worked,
but the evaluation of each variable involved a map lookup.
The use of hash maps made this lookup essentially constant-time,
but still a relatively large constant.
Current Implementation
The current version of AIJ uses
a more optimized approach for variable lookup,
described below.
Each Acl2Variable instance includes
a numeric index, in a private field.
The index is initially -1 (when the object is created),
which means that it is not set yet.
When AIJ's public API is used to provide a function definition
(which is added to the Java representation of the ACL2 environment), AIJ sets all the indices in the Acl2Variables
that occur in the definiens of the function.
The setting of indices starts with the parameters of the function:
the 0-based position of each parameter in the parameter list
is the value to which all the occurrences of that variable are set
in the body of the function;
however, when a lambda expression is encountered,
the variables in its body are given indices
based on the parameters of the lambda expression,
ignoring the outer indices
(recall that lambda expressions are always closed
in ACL2 translated terms).
In assigning these indices,
AIJ ensures that the definiens of the function is well-formed,
e.g. that the body does not include free variables that are not parameters.
Because the same ACL2 variable
may have different indices in different contexts,
the Acl2Term instances passed to AIJ to define functions
must not share any Acl2Variable instances;
AIJ throws an exception if, during the index setting recursion,
it encounters an Acl2Variable whose index is already set.
Given these variable indices, a binding of variables to values
can be represented as a map from indices (i.e. natural numbers) to values
instead of a map from symbols to values.
But a map from indices to values can be represented as an array,
and that is why the eval methods of Acl2Term and subclasses
take an Acl2Value[] as argument:
that argument is still a binding of variables to values,
but the variables are represented by indices.
An array access is much faster than a hash map access.
The evaluation algorithm on terms is still the one described above,
except that the bindings are represented as arrays instead of maps.
The evaluation of terms is mutually recursive with
the application of functions to values.
This ACL2 evaluation is in the logic:
guards are completely ignored,
and in fact not even currently represented in AIJ.
More Information
See the AIJ code and Javadoc for more details on the ACL2 evaluator.
Previous: Native Java Implementations of ACL2 Functions
Next: Customization Options for Generated Code
