Atj-input-processing
Input processing performed by atj.
See input processing for general background.
As part of input processing,
we collect the names of all the ACL2 functions to be translated to Java,
as determined by fn1, ..., fnp.
As we do that,
we also check that they satisfy the constraints
stated in the user documentation.
This collection and checking of the ACL2 functions
is realized via a worklist algorithm.
The worklist is initialized with fn1, ..., fnp.
At each step, a function fn is taken from the worklist and processed.
If fn satisfies all the necessary constraints,
it is added to a list of collected functions (which is initially empty);
otherwise, we stop with an error.
If fn is defined,
we collect the functions that occur in its defining body
and add them to the worklist,
except for those that are already in the worklist or in the collected list
(so that we do not process the same function twice).
Note that by adding fn to the collected list
before examining the functions that occur in its defining body,
we ensure termination in the presence of
(singly or mutually) recursive functions.
We proceed like this until the worklist is empty (or an error occurs).
If there are no errors, at the end
we will have checked all the functions
transitively called by fn1, ..., fnp,
and the collected list will contain all the functions
that must be translated to Java.
This is the basic algorithm, but there are some complications,
described in the following.
A complication arises from
calls of return-last whose first argument is 'acl2::mbe1-raw,
which are calls of mbe in translated form.
As explained in the user documentation,
when the :guards input of ATJ is nil,
the Java code generated by ATJ executes ``in the logic'',
and in particular executes the :logic parts of mbes;
when instead the :guards input of ATJ is t,
the Java code generated by ATJ assumes the satisfaction of the guards,
and in particular executes the :exec parts of mbes.
Thus, when we recursively collect the functions
from the body of a defined function,
when we encounter these calls of return-last,
we selectively descend into the :logic or :exec part
(based on the value of the :guards input),
ignoring the other part.
Another complication arises from
calls of return-last whose first argument is 'acl2::progn,
which are calls of prog2$ and progn$ in translated form.
As explained in the documentation,
code is generated from the last argument only,
but the other arguments must be checked to satisfy constraints as well.
Thus, we use two worklists and two collected lists:
one worklist and one collected list for the functions
for which Java code must be generated;
and one worklist and one collected list for the functions
that must be only checked to satisfy the constraints.
At the end of the algorithm,
the first collected list is used to generate Java code,
while the second collected list is discarded;
however, this second collected list is used during the algorithm,
to keep track of the functions already checked
that do not appear in the worklists or in the first collected list.
The function fn is always taken from the first worklist,
unless this worklist is empty, in which case it is taken from the second:
in other words, the first worklist is processed first,
and then the second one;
the algorithm terminates when both worklists are empty.
Yet another complication arises from
calls of functions in
*atj-jprim-fns* and *atj-jprimarr-fns*,
which are translated directly to suitable Java constructs
when :deep is nil and :guards is t.
Under these conditions, when fn is taken from a worklist,
its defining body is not examined;
i.e. it is treated like a natively implemented function,
which it is in some sense.
Further details and complications of the worklist algorithm
are explained in the implementing functions.
Subtopics
- Atj-collect-fns-in-term
- Collect all the functions in a term,
in the course of the worklist algorithm.
- Atj-worklist-iterate
- Worklist algorithm iteration.
- Atj-process-test
- Process a test from the :tests input.
- Atj-process-inputs
- Process the inputs to atj.
- Atj-process-test-input-jprim-value
- Process a Java primitive input, or part of an input,
of a test for a function call.
- Atj-process-output-subdir
- Process the subdirectories specified by
the :output-dir and :java-package inputs.
- Atj-process-test-input
- Process the input of a test for a function call.
- Atj-process-output-dir
- Process the :output-dir input.
- Atj-process-test-input-jprim-values
- Lift atj-process-test-input-jprim-value to lists.
- Atj-fns-to-translate
- Collect the names of all the ACL2 functions to be translated to Java,
checking that they satisfy all the necessary constraints.
- Atj-process-test-inputs
- Lift atj-process-test-input to lists.
- Atj-process-tests
- Process the :tests input.
- Atj-process-targets
- Process the fn1, ..., fnp inputs.
- Atj-process-no-aij-types
- Process the :no-aij-types input.
- Atj-pkgs-to-translate
- Collect all the ACL2 packages to be translated to Java.
- Atj-process-java-class
- Process the :java-class input.
- Atj-process-java-package
- Process the :java-package input.
- *atj-default-java-class*
- Default Java class name to use if :java-class is nil.
- *atj-allowed-options*
- Keyword options accepted by atj.
