Integer-format
Fixtype of formats of (signed and unsigned) integer objects.
This is a product type introduced by fty::defprod.
Fields
- pair — uinteger+sinteger-format
Additional Requirements
The following invariant is enforced on the fields:
(uinteger-sinteger-bit-roles-wfp
(uinteger-format->bits (uinteger+sinteger-format->unsigned pair))
(sinteger-format->bits (uinteger+sinteger-format->signed pair)))
Each signed integer type has a corresponding unsigned integer type
[C17:6.2.5/6].
There are constraints between the representations of
two corresponding signed and unsigned integer types
[C17:6.2.6.2/2].
Thus, we introduce a notion for the format of
corresponding unsigned and signed integer types.
This is for signed short and unsigned short,
or for signed int and unsigned int,
etc.
This consists of a an unsigned and a signed integer format,
constrained to be well-formed relative to each other.
The reason for introducing and using
the ``intermediate'' fixtype uinteger+sinteger-format,
as opposed to directly define this integer-format fixtype
to consists of the two components of that intermediate type
is the following.
We want this integer-format fixtype to require (in :require)
the consistency between the unsigned and signed integer formats
(i.e. uinteger-sinteger-bit-roles-wfp).
But if we have two separate components,
we need separate fixers (in :reqfix for the two components:
we plan to use uinteger-bit-roles-for-sinteger-bit-roles
and sinteger-bit-roles-for-uinteger-bit-roles for that,
but we still need to prove the needed properties of those functions,
since they take a little bit of work.
Once we have the proofs,
we will eliminate the intermediate fixtype uinteger+sinteger-format
and have two components and two fixers in this fixtype here.
Subtopics
- Integer-format-fix
- Fixing function for integer-format structures.
- Integer-format-equiv
- Basic equivalence relation for integer-format structures.
- Make-integer-format
- Basic constructor macro for integer-format structures.
- Integer-format->pair
- Get the pair field from a integer-format.
- Change-integer-format
- Modifying constructor for integer-format structures.
- Integer-formatp
- Recognizer for integer-format structures.
