Atj-java-primitives
Representation of Java primitive types and operations for ATJ.
In order to have ATJ generate Java code
that manipulates Java primitive values,
we use ACL2 functions that correspond to
the Java primitive values and operations:
when ATJ encounters these specific ACL2 functions,
it translates them to corresponding Java constructs
that operate on primitive types;
this happens only when :deep is nil and :guards is t.
When deriving a Java implementation from a specification,
where ATJ is used as the last step of the derivation,
the steps just before the last one can refine the ACL2 code
to use the aforementioned ACL2 functions,
ideally using APT transformations,
so that ATJ can produce Java code
that operates on primitive values where needed.
Such refinement steps could perhaps be somewhat automated,
and incorporated into a code generation step that actually encompasses
some APT transformation steps
before the final ATJ code generation step.
The natural place for the aforementioned ACL2 functions
that correspond to Java primitive values and operations is the language formalization that is being developed.
So ATJ recognizes those functions from the language formalization,
and translates them to Java code that manipulates Java primitive values.
Note that here `primitive' refers to
Java primitive types, values, and operations.
It has nothing to do with the ACL2 primitive functions.
Subtopics
- Atj-jprim-deconstr-fn-to-ptype
- Map an ACL2 function that models a Java primitive deconstructor
to the corresponding Java primitive type.
- Atj-jprim-constr-fn-to-ptype
- Map an ACL2 function that models a Java primitive constructor
to the corresponding Java primitive type.
- Atj-jprim-deconstr-fn-p
- Recognize the ACL2 function symbols that model
the deconstruction of Java primitive types.
- *atj-jprim-binop-fns*
- List of (the names of) the ACL2 functions that model
Java primitive binary operations.
- Atj-jprim-unop-fn-p
- Recognize the ACL2 function symbols that model
the Java primitive unary operations.
- Atj-jprim-conv-fn-p
- Recognize the ACL2 function symbols that model
the Java primitive conversions.
- Atj-jprim-constr-fn-p
- Recognize the ACL2 function symbols that model
the construction of Java primitive types.
- Atj-jprim-binop-fn-p
- Recognize the ACL2 function symbols that model
the Java primitive binary operations.
- Atj-jprim-fn-p
- Recognize the ACL2 function symbols that model
the Java primitive value constructions, operations, and conversions.
- *atj-jprim-deconstr-fns*
- List of (the names of) the ACL2 functions that model
the deconstruction of Java primitive values.
- *atj-jprim-conv-fns*
- List of (the names of) the ACL2 functions that model
Java primitive conversions.
- *atj-jprim-constr-fns*
- List of (the names of) the ACL2 functions that model
the construction of Java primitive values.
- *atj-jprim-unop-fns*
- List of (the names of) the ACL2 functions that model
Java primitive unary operations.
- *atj-jprim-fns*
- List of (the names of) the ACL2 functions that model
Java primitive value constructions and operations.
- Atj-types-for-java-primitives
- ATJ types for the Java primitive constructors and operations.
