Atj-tutorial-ACL2-values
ATJ tutorial: Java Representation of the ACL2 Values.
In order to translate from ACL2 to Java,
there must be a Java representation of the ACL2 values. AIJ provides a default representation,
described in this tutorial page.
More advanced representations are discussed later.
ACL2 Values
The set of values of the ACL2 evaluation semantics
is the union of the sets depicted below:
(i) integers, recognized by integerp;
(ii) ratios, i.e. rationals that are not integers,
with no built-in recognizer
(the term `ratio' is used in Section 2.1.2 of the Common Lisp specification);
(iii) complex rationals, recognized by complex-rationalp;
(iv) characters, recognized by characterp;
(v) strings, recognized by stringp;
(vi) symbols, recognized by symbolp; and
(vii) cons pairs, recognized by consp.
Integers and ratios form the rationals, recognized by rationalp.
Rationals and complex rationals form the Gaussian rationals,
which are all the numbers in ACL2,
recognized by ACL2-numberp
(this discussion does not apply to ACL2(r)).
The logical semantics of ACL2 allows additional values called `bad atoms',
and consequently cons pairs
that may contain them directly or indirectly;
however, such values cannot be constructed in evaluation.
Java Classes
AIJ represents ACL2 values
as immutable objects of class Acl2Value and its subclasses
in the simplified UML class diagram below.
Each class in the diagram, except Acl2PackageName,
corresponds to a set
in the picture of ACL2 values above.
The subset relationships in that picture
match the inheritance relationships in the UML diagram below.
The sets of values that are unions of other sets of values
correspond to abstract classes;
the other sets correspond to concrete classes.
All these classes are public,
except for the package-private ones for ratios and complex rationals:
ratios and complex rationals are built indirectly via AIJ's API,
by building
rationals that are not integers and numbers that are not rationals.
The information about the represented ACL2 values
is stored in fields of the non-abstract classes.
Acl2Integer stores
the numeric value as a java.math.BigInteger.
Acl2Ratio stores
the numerator and denominator as Acl2Integers,
in reduced form
(i.e. their greatest common divisor is 1
and the denominator is greater than 1).
Acl2ComplexRational stores
the real and imaginary parts as Acl2Rationals.
Acl2Character stores
the 8-bit code of the character as a char below 256.
Acl2String stores
the codes and order of the characters as a java.lang.String
whose chars are all below 256.
Acl2Symbol stores
the symbol's package name as a Acl2PackageName
(a wrapper of java.lang.String
that enforces the ACL2 constraints on package names)
and the symbol's name as a Acl2String.
Acl2ConsPair stores the component Acl2Values.
All these fields are private,
thus encapsulating the internal representation choices
and enabling their localized modification.
ACL2 numbers, strings, and symbols have no preset limits,
but the underlying Lisp runtime may run out of memory.
Their Java representations (e.g. java.math.BigInteger)
have very large limits,
whose exceedance could be regarded as running out of memory.
If needed, the Java representations could be changed
to overcome the current limits
(e.g. by using lists of java.math.BigIntegers).
Java Factory and Getter Methods
The public classes for ACL2 values and package names
in the UML diagram above
provide public static factory methods to build objects of these classes.
For example, Acl2Character.make(char)
returns a Acl2Character with the supplied argument as code,
throwing an exception if the argument is above 255.
As another example, Acl2ConsPair.make(Acl2Value,Acl2Value)
returns a Acl2ConsPair with the supplied arguments as components.
Some classes provide overloaded variants,
e.g. Acl2Integer.make(int)
and Acl2Integer.make(java.math.BigInteger).
All these classes provide no public Java constructors,
thus encapsulating the details of object creation and re-use,
which is essentially transparent to external code
because these objects are immutable.
The public classes for ACL2 values in the UML diagram above
provide public instance getter methods
to unbuild (i.e. extract information from) instances of these classes.
For example, Acl2Character.getJavaChar()
returns the code of the character
as a char that is always below 256.
As another example,
Acl2ConsPair.getCar() and Acl2ConsPair.getCdr()
return the component Acl2Values of the cons pair.
Some classes provide variants,
e.g. Acl2Integer.getJavaInt()
(which throws an exception if the integer does not fit in an int)
and Acl2Integer.getJavaBigInteger().
Thus, AIJ provides a public API to
build and unbuild Java representations of ACL2 values:
the API consists of the factory and getter methods described above.
When talking about AIJ,
this tutorial calls `build' and `unbuild'
what is often called `construct' and `destruct' in functional programming,
because in object-oriented programming the latter terms
may imply object allocation and deallocation,
which is not necessarily what the AIJ API does.
More Information
For more details on AIJ's implementation and API of ACL2 values,
see the Javadoc in AIJ's Java code.
Previous: About the Simplified UML Class Diagrams
Next: Deep and Shallow Embedding Approaches
