Atj-tutorial-ACL2-environment
ATJ tutorial: Java Representation of the ACL2 Environment.
AIJ provides a Java representation of the ACL2 environment.
For the deep embedding approach, this environment consists of ACL2 package definitions and ACL2 function definitions; for the shallow embedding approach, this environment consists of package definitions only,
because in this approach functions are represented as methods
outside of AIJ.
This tutorial page may be skipped at first reading.
Representation of the ACL2 Package Definitions
AIJ represents ACL2 packages
as objects of the class Acl2Package in the simplified UML class diagram below.
An Acl2PackageName is a wrapper of java.lang.String
that enforces the restrictions of valid package names
described in defpkg.
An Acl2Package stores, in private fields,
a name and a list of 0 or more imported symbols.
A defpkg may also include a documentation string,
but this is not represented in Acl2Package.
The Acl2Package class also has a private static field
that contains all the packages defined so far,
as a java.util.Map<Acl2PackageName,Acl2Package> object.
This map is initially empty;
it is extended, one package definition at a time,
via the static method
Acl2Package.define(Acl2PackageName, List<Acl2Symbol>).
This method ensures that the first three packages defined are
"KEYWORD", "COMMON-LISP", and "ACL2",
in that order;
these are the first three packages, in that order,
that appear in the ACL2 world.
The method also checks that
"KEYWORD" and "COMMON-LISP" have empty import lists,
and that "ACL2" only imports symbols from "COMMON-LISP".
These properties, which can be easily checked in an ACL2 shell,
help guarantee the well-formedness of certain Acl2Symbol instances
that are pre-created when the class Acl2Symbol is initialized
(i.e. before any other symbol can be created).
See AIJ's Java code and Javadoc for more details.
Building of the ACL2 Package Definitions
The Java code generated by ATJ repeatedly calls the method
Acl2Package.define(Acl2PackageName, List<Acl2Symbol>)
to define all the ACL2 packages
that are known when ATJ is called to generate the Java code.
Representation of the ACL2 Function Definitions
AIJ represents ACL2 functions as decribed in atj-tutorial-ACL2-terms.
The simplified UML class diagram on that page shows that instances of Acl2DefinedFunction
have lambda expressions as definientia,
where each lambda expression consists of
zero or more formal parameters and a body.
An ACL2 function definition has additional information,
such as the guard of the function;
none of this additional information is currently present
in AIJ's Java representation.
The Acl2DefinedFunction class also has a private static field
that contains all the functions defined so far,
as a java.util.Map<Acl2Symbol, Acl2DefinedFunction> object.
This map is initially empty;
it is extended, one function definition at a time,
via the instance method
Acl2NamedFunction.define(Acl2Symbol[], Acl2Term),
which is abstract in the public class Acl2NamedFunction
and implemented in the non-public class Acl2DefinedFunction.
Objects of Acl2NamedFunction are interned,
i.e. there is a unique instance for each function name:
this is ensured by the public factory method
Acl2NamedFunction.make(Acl2Symbol),
which is the only way for code external to AIJ
to build Acl2NamedFunction objects.
Thus, calling the instance method
Acl2NamedFunction.define(Acl2Symbol[], Acl2Term)
always defines that unique instance;
the method sets the private instance field definiens.
Building of the ACL2 Function Definitions
In the deep embedding approach, the Java code generated by ATJ repeatedly
builds Acl2NamedFunction instances
via Acl2NamedFunction.make(Acl2Symbol)
for all the ACL2 defined functions to be translated to Java,
and defines each such function by calling
Acl2NamedFunction.define(Acl2Symbol[], Acl2Term)
on those instances.
The ATJ-generated code also uses Acl2NamedFunction.make(Acl2Symbol)
to build function names as part of the ACL2 terms
that form the bodies of defined functions;
there is just one instance for each name, as explained above,
to which the definition is attached.
The ATJ-generated code also builds Acl2NamedFunction instances
for functions that are implemented natively in Java
(e.g. for the ACL2 primitive functions, which have no definition),
i.e. for instances of the Acl2NativeFunction class.
The factory method Acl2NamedFunction.make(Acl2Symbol)
knows which function symbols have native Java implementations
and accordingly returns
either Acl2NativeFunction or Acl2DefinedFunction instances.
The ATJ-generated code calls
Acl2NamedFunction.define(Acl2Symbol[], Acl2Term)
only on instances of Acl2DefinedFunction;
ATJ also knows which ACL2 functions have native Java implementations
(the implementing method in Acl2NativeFunction
of Acl2NamedFunction.define(Acl2Symbol[], Acl2Term)
throws an exception).
Previous: Java Representation of the ACL2 Terms
Next: Native Java Implementations of ACL2 Functions
