Atj-implementation
Implementation of atj.
The implementation functions have formal parameters
consistently named as follows:
- state is the ACL2 state.
- ctx is the context used for errors.
- args is the list of all the inputs to atj,
before being processed.
The type of this formal parameter is just true-listp
because its elements may be any values.
- targets is the list (fn1 ... fnp) of inputs to atj,
before being processed.
The type of this formal parameter is just true-listp
because its elements may be any values.
- targets$ is the result of processing targets.
It is identical to targets,
but has a type implied by its successful validation,
performed when it is processed.
- deep,
guards,
java-package,
java-class,
output-dir,
tests, and
verbose
are the homonymous inputs to atj,
before being processed.
These formal parameters have no types because they may be any values.
- deep$,
guards$,
java-package$,
java-class$,
tests$, and
verbose$
are the results of processing
the homonymous inputs (without the $) to atj.
Some are identical to the corresponding inputs,
but they have types implied by their successful validation,
performed when they are processed.
- output-file$ and output-file-test$
are the results of processing output-dir.
- output-subdir is the directory
where the Java files are generated,
which is output-dir or a subdirectory of it,
based on java-package.
- test$ is an element of tests$.
- pkgs is the list of names of all the currently known ACL2 packages,
in chronological order.
- fns-to-translate is the list of ACL2 functions
to be translated to Java.
- fns-by-pkg consists of fns-to-translate,
plus all the ACL2 functions natively implemented in AIJ
(which currently are the ACL2 primitive functions)
organized as an alist from ACL2 package names to
the non-empty lists of the functions in the respective packages.
See atj-code-generation.
- avars-by-name consists of all the free and bound variables
that appear in the ACL2 function definition
for which code is being generated.
These variables are organized as an alist from symbol names
to the variables with the respective names.
See atj-code-generation.
- jvar-value-base,
jvar-term-base, and
jvar-lambda-base
are the base names of the Java local variables to use
to construct ACL2 values,
deeply embedded ACL2 terms,
and deeply embedded ACL2 lambda expressions.
See atj-code-generation.
- jvar-result-base is the base name of the Java local variable to use
to store the results of arguments of non-strict ACL2 functions.
- jvar-value-index,
jvar-term-index, and
jvar-lambda-index
are the indices of the next Java local variables to use
to construct ACL2 values,
deeply embedded ACL2 terms,
and deeply embedded ACL2 lambda expressions.
See atj-code-generation.
- jvar-result-index is the index of the next Java local variable to use
to store the results of arguments of non-strict ACL2 functions.
- indices is an alist from symbols to positive integers,
which associates to each ACL2 variable the next index to use
to disambiguate a new instance of that variable from previous instances.
This is used when renaming ACL2 variables to their Java names,
in the shallow embedding approach.
See atj-code-generation.
- renaming-new and renaming-old
are alists from symbols to symbols,
which associate to each ACL2 variable its Java name
(i.e. the name of the Java variable generated from this ACL2 variable).
The former is used for the variables marked as `new',
while the latter is used for the variables marked as `old'.
This is used when renaming ACL2 variables to their Java names,
in the shallow embedding approach.
See atj-code-generation.
- pkg-class-names is an alist from strings to strings,
which associates to each package name in the keys of fns-by-pkg
the name of the corresponding Java class name.
This is used in the shallow embedding approach.
See atj-code-generation.
- fn-method-names is an alist from strings to strings,
which associates to each function name in fns-to-translate
the name of the corresponding Java method name.
This is used in the shallow embedding approach.
See atj-code-generation.
- mv-class-names is a list of strings consisting of
the names of all the generated mv classes.
This is used in the shallow embedding approach.
See atj-code-generation.
- curr-pkg is the name of the ACL2 package of the ACL2 function
for which Java code is being generated.
The parameters of implementation functions that are not listed above
are described in, or clear from, those functions' documentation.
Subtopics
- Atj-types
- Types used by ATJ for code generation.
- Atj-java-primitive-array-model
- ATJ's model of Java primitive arrays.
- Atj-java-abstract-syntax
- An abstract syntax of Java for ATJ's implementation.
- Atj-input-processing
- Input processing performed by atj.
- Atj-java-pretty-printer
- A pretty-printer for the abstract syntax of Java,
for ATJ's implementation.
- Atj-code-generation
- Code generation performed by ATJ.
- Atj-java-primitives
- Representation of Java primitive types and operations for ATJ.
- Atj-java-primitive-arrays
- ATJ's representation of Java primitive arrays and operations on them.
- Atj-type-macros
- User-level macros to verify and record ATJ types.
- Atj-java-syntax-operations
- Operations on the Java abstract syntax used by ATJ.
- Atj-fn
- Process the inputs and generate the Java file(s).
- Atj-library-extensions
- Library extensions for atj.
- Atj-java-input-types
- Java input types generated by ATJ.
- Atj-test-structures
- Structures that store user-specified ATJ tests.
- Aij-notions
- AIJ notions used by ATJ.
- Atj-macro-definition
- Definition of the atj macro.
