Atj-test-value
Fixtype of values used for
inputs and outputs in user-specified ATJ tests.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :acl2 → atj-test-value-ACL2
- :jboolean → atj-test-value-jboolean
- :jchar → atj-test-value-jchar
- :jbyte → atj-test-value-jbyte
- :jshort → atj-test-value-jshort
- :jint → atj-test-value-jint
- :jlong → atj-test-value-jlong
- :jboolean[] → atj-test-value-jboolean[]
- :jchar[] → atj-test-value-jchar[]
- :jbyte[] → atj-test-value-jbyte[]
- :jshort[] → atj-test-value-jshort[]
- :jint[] → atj-test-value-jint[]
- :jlong[] → atj-test-value-jlong[]
The Java methods generated by ATJ manipulate three kinds of values:
- Objects of the AIJ classes that represent ACL2 values,
e.g. Acl2Integer.
These correspond to the :acl2 ATJ types, e.g. :ainteger.
- Java primitive values,
which correspond to the ATJ :jprim types.
These values are used only in the shallow embedding with guards.
- Java primitive arrays,
which correspond to the ATJ :jprimarr types.
These arrays are only used in the shallow embedding with guards.
Thus, when generating tests for the generated Java methods,
the input and output values of the tests may be
of these three different kinds.
So we introduce a type for these three kinds of values,
with each of the last two kinds having six sub-kinds each.
The :acl2 values may be anything,
while the j... values are restricted to (our model of)
Java primitive values and Java primitive arrays,
excluding float and double values and arrays,
because we only have an abstract model of those for now
and thus ATJ does not support
the generation of tests involving float and double.
Subtopics
- Atj-test-value-fix
- Fixing function for atj-test-value structures.
- Atj-test-value-case
- Case macro for the different kinds of atj-test-value structures.
- Atj-test-valuep
- Recognizer for atj-test-value structures.
- Atj-test-value-equiv
- Basic equivalence relation for atj-test-value structures.
- Atj-test-value-kind
- Get the kind (tag) of a atj-test-value structure.
- Atj-test-value-ACL2
- Atj-test-value-jshort[]
- Atj-test-value-jshort
- Atj-test-value-jlong[]
- Atj-test-value-jlong
- Atj-test-value-jint[]
- Atj-test-value-jint
- Atj-test-value-jchar[]
- Atj-test-value-jchar
- Atj-test-value-jbyte[]
- Atj-test-value-jbyte
- Atj-test-value-jboolean[]
- Atj-test-value-jboolean
