Jtype
Java types [JLS14:4].
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :prim → jtype-prim
- :class → jtype-class
- :array → jtype-array
We capture all eight primitive types.
We use ACL2 strings to capture not only single type identifiers,
but also dot-separated sequences with package names and type identifiers:
the latter have dots in the ACL2 strings.
This also accommodates types with type arguments,
by using < and > in the ACL2 strings.
Since the Java grammar defines InterfaceType as ClassType,
we use :class for both class and interface types;
this is consistent with similar terminology in Java
(e.g. a `class file' may define an interface.)
We capture array types via a natural recursive structure,
by wrapping the component type.
Subtopics
- Jtype-case
- Case macro for the different kinds of jtype structures.
- Jtypep
- Recognizer for jtype structures.
- Jtype-fix
- Fixing function for jtype structures.
- Jtype-equiv
- Basic equivalence relation for jtype structures.
- Jtype-count
- Measure for recurring over jtype structures.
- Jtype-prim
- Jtype-class
- Jtype-array
- Jtype-kind
- Get the kind (tag) of a jtype structure.