|
|
|---|
|
|
|
|---|
Types used by ATJ for code generation.
In order to make the generated Java code more efficient and idiomatic,
ATJ uses types that correspond to both ACL2 predicates and Java types.
These ATJ types are used only when
For example, consider a unary ACL2 function
whose guard is or implies stringp,
and the corresponding Java method generated by ATJ.
Since under the assumption of guard satisfaction
this method will always be called
with an
In general, establishing the narrower input and output types for a Java method generated from an ACL2 function may involve arbitrarily hard theorem proving: (i) proving that the guard implies that the inputs of the ACL2 function satisfy the ACL2 predicates corresponding to the input types, and (ii) proving that the guard implies that the outputs of the ACL2 function satisfy the ACL2 predicates corresponding to the output types; the number of outputs of an ACL2 function is greater than 1 if the function returns an mv value; otherwise the number of outputs is 1. Since we do not want ATJ to attempt any theorem proving, we provide a macro atj-main-function-type to perform those theorem proving tasks under user control and to record the input and output types of ACL2 functions in a table, and we have ATJ look up types in this table. Note that these types are different from ACL2's built-in types used for typeset reasoning, ACL2's tau system types, and our ACL2 model of Java types.
With a table of the types of the involved ACL2 functions in hand
(the table being constructed via calls of atj-main-function-type),
ATJ performs a type analysis of the ACL2 terms in function bodies
before translating them to Java;
this analysis is part of ATJ's pre-translation steps.
Generally speaking,
ATJ compares the type inferred for an actual argument of a function
(this type is inferred by analyzing terms recursively)
with the type of the corresponding formal argument of the function
(this type is retrieved from the table of function types):
if they differ, ATJ inserts code to convert from the former to the latter,
unless the former is a subtype of (including equal to) the latter in Java.
The conversion may be a type cast,
e.g. to convert from
The ATJ type information stored in the table
determines/specifies the input and output types of the Java methods
generated for the corresponding ACL2 functions.
In general, there may be different possible choices of types
for certain ACL2 functions:
different choices will lead to different Java code.
For instance,
if a function's guard implies that an argument satisfies integerp,
that function's argument can be assigned
a type corresponding to
In some cases, ACL2 functions return outputs of narrower types
when given inputs of narrower types.
Prime examples are the arithmetic operations
binary-+, binary-*, and unary--.
All of their input and output types are
the type corresponding to ACL2-numberp,
based on their guards:
this can be recorded via atj-main-function-type.
Based on these types, the corresponding Java methods
will take and return
However, due to well-known closure properties,
binary-+, like binary-+ and unary--,
maps rationalp inputs to rationalp outputs,
and integerp inputs to integerp outputs.
This means that we could generate three overloaded methods
for each such ACL2 function:
one with
This is not limited to primitive arithmetic operations.
Any ACL2 function may have the property of
returning outputs of narrower types when given inputs of narrower types.
Even if the output types are not narrower,
the internal computations may be more efficient on narrower inputs,
e.g. the cast in the example above can be avoided
when that call of
Thus, we provide another macro, atj-other-function-type, to record additional input and output types for ACL2 functions. ATJ makes use of these additional types to generate multiple overloaded methods for single ACL2 functions. In general, via these two macros, each ACL2 function may have more than one input/output type associated with it (where an input/output type is a full function type, consisting of zero or more input types and one or more output types): (i) a primary (`main') input/output type, provable from the guards as described above; and (ii) zero or more secondary (`other') input/output types. The secondary input types are narrower than the primary ones, but do not have to be provable from the guard; what must be proved, via a theorem generated by atj-other-function-type, is that the guard and the input types imply the output type.
The atj-main-function-type and atj-other-function-type actually attempt to verify the theorems only if the function is in logic mode (whether it is guard-verified or not). If the function is in program mode, there is no attempt to verify theorems (as it is impossible to do so with program-mode functions), and the macros succeed. This should be no more troubling than running program-mode or guard-unverified code.
The above is just an overview of the use of types by ATJ. More details are in the documentation of their implementation and of the code generation functions that use them.