Primitive-function-macros
Macros to formalize more concisely
ACL2 functions over the Java primitive values.
The ACL2 functions that formalize Java primitive operations and conversions
have the following structure:
they take one (if unary) or two (if binary) primitive values as arguments;
they use primitive value destructors (e.g. int-value->int)
to obtain the ``core'' values to operate upon with existing ACL2 functions;
they use existing ACL2 functions to generate the ``core'' result;
they uses primitive value constructors (e.g. int-value)
to return the result primitive value.
The only ``interesting'' part is how the core result
is calculated from the core arguments via existing ACL2 functions.
The rest is boilerplate that can be automatically generated,
which we do via macros.
We introduce two general macros:
one for unary functions, and one for binary functions.
These can generate functions over primitive values
of any combination of operand and result types,
which are all explicitly specified.
Since certain combinations of operand and result types
are shared by certain collections of primitive operations,
we also introduce more specialized macros for these combinations.
These macros also provide options
to generate certain kinds of theorems about the operations,
e.g. commutativity theorems.
Subtopics
- Def-primitive-binary
- Macro to formalize a binary ACL2 function over Java primitive values.
- Def-primitive-unary
- Macro to formalize a unary ACL2 function over Java primitive values.
- Primitive-type-destructor
- The destructor of the fixtype of the values of a primitive type.
- Primitive-type-predicate
- The recognizer of the fixtype of the values of a primitive type.
- Primitive-type-constructor
- The constructor of the fixtype of the values of a primitive type.
- Def-long=>boolean-binary
- Specialization of def-primitive-binary to
the case in which the input types are long
and the output type is boolean.
- Def-int=>boolean-binary
- Specialization of def-primitive-binary to
the case in which the input types are int
and the output type is boolean.
- Def-int-binary
- Specialization of def-primitive-binary to
the case in which input and output types are int.
- Def-float=>boolean-binary
- Specialization of def-primitive-binary to
the case in which the input types are float
and the output type is boolean.
- Def-double=>boolean-binary
- Specialization of def-primitive-binary to
the case in which the input types are double
and the output type is boolean.
- Def-long-binary
- Specialization of def-primitive-binary to
the case in which input and output types are long.
- Def-float-binary
- Specialization of def-primitive-binary to
the case in which input and output types are float.
- Def-double-binary
- Specialization of def-primitive-binary to
the case in which input and output types are double.
- Def-boolean-binary
- Specialization of def-primitive-binary to
the case in which input and output types are boolean.
- Def-long-unary
- Specialization of def-primitive-unary to
the case in which input and output types are long.
- Def-int-unary
- Specialization of def-primitive-unary to
the case in which input and output types are int.
- Def-float-unary
- Specialization of def-primitive-unary to
the case in which input and output types are float.
- Def-double-unary
- Specialization of def-primitive-unary to
the case in which input and output types are double.
- Def-boolean-unary
- Specialization of def-primitive-unary to
the case in which input and output types are boolean.
