Atj-tutorial-ACL2-terms
ATJ tutorial: Java Representation of the ACL2 Terms.
For the deep embedding approach, AIJ provides a Java representation of the ACL2 terms.
Since ACL2 terms are also ACL2 values,
in principle the Java representation of the ACL2 values provided by AIJ could be used to represent the ACL2 terms as well.
However, it is more convenient to use
a more specialized representation,
described in this tutorial page.
This tutorial page may be skipped at first reading.
ACL2 Translated Terms
The set of ACL2 translated terms consists of
(i) variables,
which are symbols,
(ii) quoted constants,
which are lists (quote value) where value is a value,
and (iii) function applications,
which are lists (fn arg1 ... argn)
where fn is a function
and arg1, ..., argn are zero or more terms.
A function fn used in a term is
(i) a named function,
which is a symbol,
or (ii) a lambda expression,
which is a list (lambda (var1 ... varm) body)
where var1, ..., varm are zero or more symbols
and body is a term,
whose free variables are all among var1, ..., varm
(i.e. lambda expressions are always closed).
Java Classes
AIJ represents ACL2 terms in a manner similar to ACL2 values,
as objects of class Acl2Term and its subclasses in the simplified UML class diagram below.
Functions are represented
as objects of class Acl2Function and its subclasses
in the same diagram.
The classes with subclasses are abstract,
while classes without subclasses are concrete.
All these classes are public, except Acl2DefinedFunction.
The information about the represented ACL2 terms (and functions)
is stored in private fields.
Acl2Variable is a wrapper of Acl2Symbol, and
Acl2QuotedConstant is a wrapper of Acl2Value;
these wrappers place Acl2Symbol and Acl2Value
into the class hierarchy of Acl2Term,
given that Java does not support multiple class inheritance
(e.g. Acl2Symbol could not be
both a subclass of Acl2Value and a subclass of Acl2Term).
An Acl2FunctionCall stores
an Acl2Function and zero or more Acl2Terms.
An Acl2LambdaExpression stores
zero or more Acl2Variables and an Acl2Term.
Acl2NamedFunction is a wrapper of Acl2Symbol,
placing Acl2Symbol into the class hierarchy of Acl2Function.
AIJ's Java representation of named functions
differentiates between native and defined functions.
An Acl2DefinedFunction stores a definition
consisting of zero or more formal parameters (Acl2Symbols)
and of a body (an Acl2Term),
which are put together into a lambda expression
(as in a higher-order equality (equal fn (lambda ...))).
An Acl2NativeFunction represents an ACL2 function
that is implemented natively via Java code, not via (a Java representation of) an ACL2 definiens.
Here `native' is with respect to ACL2, not Java;
it has nothing to do with JNI. There is an instance of Acl2NativeFunction
for each ACL2 primitive function: these could not be instances of Acl2DefinedFunction,
because they have no ACL2 definition.
There are also instances of Acl2NativeFunction
for other built-in ACL2 functions,
and more may be added in the future,
particularly for execution efficiency.
Java Factory and Getter Methods
The classes for ACL2 terms (and functions) provide
public static factory methods to build instances of these classes,
but no public Java constructors,
similarly to the classes for ACL2 values. In the deep embedding approach, the Java code generated by ATJ
uses these factory methods to build the terms in the definientia
of the ACL2 functions that are being translated to Java.
Note that since Acl2QuotedConstant wraps Acl2Value,
the ATJ-generated Java code also uses
the factory methods of the classes of ACL2 values.
The classes for ACL2 terms (and functions) do not provide
getter methods to extract information,
unlike the classes for the ACL2 values.
The reason is that code external to AIJ
(including the code generated by ATJ)
only needs to build terms, not unbuild them.
In contrast, code external to AIJ,
and to ATJ-generated code,
may need to unbuild the results obtained by evaluating
calls of ACL2 functions.
More Information
For more details on AIJ's implementation and API of ACL2 terms,
see the Javadoc in AIJ's Java code.
Previous: Deep Embedding Approach
Next: Java Representation of the ACL2 Environment
