Atj-type
Fixtype of all the ATJ types.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :acl2 → atj-type-ACL2
- :jprim → atj-type-jprim
- :jprimarr → atj-type-jprimarr
These are used for code generation, as explained in atj-types.
Currently ATJ uses types for:
- ACL2 integers, rationals, numbers,
characters, strings, symbols, booleans
cons pairs, and all values,
whose fixtype is atj-atype.
With the exception of the type of booleans,
these all correspond to the AIJ public class types for ACL2 values.
- Java primitive values and arrays.
More types may be added in the future.
Each ATJ type denotes
(i) an ACL2 predicate (see atj-type-to-pred) and
(ii) a Java type (see atj-type-to-jitype).
It is not the case that
just the :acl2 types denote ACL2 types
and just the :jprim and :jprimarr types denote Java types:
each type denotes both an ACL2 type and a Java type.
The distinction is just that
the :acl2 types denote built-in ACL2 types,
which are therefore independent from Java
(even though they have a Java representation, in AIJ),
while the :jprim and :jprimarr types are Java-specific.
Subtopics
- Atj-typep
- Recognizer for atj-type structures.
- Atj-type-case
- Case macro for the different kinds of atj-type structures.
- Atj-type-fix
- Fixing function for atj-type structures.
- Atj-type-equiv
- Basic equivalence relation for atj-type structures.
- Atj-type-jprimarr
- Atj-type-jprim
- Atj-type-ACL2
- Atj-type-kind
- Get the kind (tag) of a atj-type structure.
