Atj-java-primitive-arrays
ATJ's representation of Java primitive arrays and operations on them.
In order to have ATJ generate Java code
that manipulates Java primitive arrays,
we use an approach similar to the one for Java primitive values. We use ACL2 functions that correspond to
the Java primitive arrays and operations on them:
when ATJ encounters these specific ACL2 functions,
it translates them to corresponding Java constructs
that operate on Java primitive arrays;
this happens only when :deep is nil and :guards is t.
The discussion in atj-java-primitives
about derivations targeting
the ACL2 functions that represent Java primitive values
applies to Java primitive arrays as well.
As discussed in atj-java-primitive-array-model,
currently the ACL2 functions that represent Java primitive arrays
are part of ATJ, but (perhaps some generalization of them) could be
part of the language formalization at some point.
Subtopics
- Atj-jprimarr-new-init-fn-to-ptype
- Map an ACL2 function that models
a Java primitive array constructor with initializer
to the corresponding primitive type.
- Atj-jprimarr-conv-tolist-fn-to-ptype
- Map an array-to-list conversion function
to the corresponding Java primitive type.
- Atj-jprimarr-conv-fromlist-fn-to-ptype
- Map a list-to-array conversion function
to the corresponding Java primitive type.
- Atj-jprimarr-conv-fromlist-fn-p
- Recognizer the ACL2 function symbols that model
the conversions to Java primitive arrays from ACL2 lists.
- Atj-jprimarr-write-fn-p
- Recognizer the ACL2 function symbols that model
the writing of components from Java primitive arrays.
- Atj-jprimarr-new-len-fn-p
- Recognizer the ACL2 function symbols that model
the creation of Java primitive arrays from lengths.
- Atj-jprimarr-new-init-fn-p
- Recognizer the ACL2 function symbols that model
the creation of Java primitive arrays from components.
- Atj-jprimarr-conv-tolist-fn-p
- Recognizer the ACL2 function symbols that model
the conversions from Java primitive arrays to ACL2 lists.
- *atj-jprimarr-new-init-fns*
- List of (the names of) the ACL2 functions that model
the creation of Java primitive arrays from components.
- Atj-jprimarr-read-fn-p
- Recognizer the ACL2 function symbols that model
the reading of components from Java primitive arrays.
- Atj-jprimarr-length-fn-p
- Recognizer the ACL2 function symbols that model
the retrieval of lengths of Java primitive arrays.
- Atj-jprimarr-fn-p
- Recognize the ACL2 function symbols that model
Java primitive array operations.
- *atj-jprimarr-fns*
- List of (the names of) the ACL2 functions that model
Java primitive array operations.
- *atj-jprimarr-write-fns*
- List of (the names of) the ACL2 functions that model
the writing of components of Java primitive arrays.
- *atj-jprimarr-read-fns*
- List of (the names of) the ACL2 functions that model
the reading of components of Java primitive arrays.
- *atj-jprimarr-new-len-fns*
- List of (the names of) the ACL2 functions that model
the creation of Java primitive arrays from lengths.
- *atj-jprimarr-length-fns*
- List of (the names of) the ACL2 functions that model
the retrieval of lengths of Java primitive arrays.
- *atj-jprimarr-conv-tolist-fns*
- List of (the names of) the ACL2 functions that model
the conversion from Java primitive arrays to ACL2 lists.
- *atj-jprimarr-conv-fromlist-fns*
- List of (the names of) the ACL2 functions that model
the conversion to Java primitive arrays from ACL2 lists.
- Atj-types-for-java-primitive-arrays
- ATJ types for the Java primitive array operations.
