A representation of C integers in ACL2.

This is part of the shallow embedding.

We define a representation of
the C standard signed and unsigned integer values,
except

For each C integer type covered by our representation, we define the C values as wrappers of ACL2 integers in appropriate ranges. We also define lists of these C values, and some operations between these lists and lists of ACL2 integers in the corresponding ranges.

For the unsigned types, we also introduce ACL2 functions to turn ACL2 integers into values of those types by reducing them modulo one plus the maximum value of the type. These functions are used to define certain C integer conversions and operations, which are modular for unsigned integer types.

This representation of C integers in ACL2 should be treated like
abstract data types whose definition is opaque.
Consider the representation of `ucharp` does not matter.
What matters is that the set of ACL2 values that satisfy that predicate
is isomorphic to the set of ACL2 integers
that satisfy `uchar-integerp`;
the isomorphisms between the two sets are
`integer-from-uchar` and `uchar-from-integer`.
The fixer `uchar-fix` should be treated opaquely too.
There should be sufficient theorems
that capture the isomorphism property
and that support reasoning about these C integers in ACL2
independently from their representation.
On the other hand, `uchar-integerp` is not opaque:
it is a known set of ACL2 integers, and that matters for reasoning.
As a practical issue, `uchar-integerp-alt-def`,
which as the name suggests is like an alternative definition,
is generally more convenient than the actual definition,
because the latter involves powers of two and bit sizes,
while the alternate definition involves minima and maxima.
As another practical issue, it is generally unnecessary
to enable the fixer `uchar-integer-fix`,
which exposes `uchar-integerp`,
which therefore needs to be enabled anyways;
there is a theorem that simplifies away `uchar-integer-fix`
when `uchar-integerp` holds,
so enabling `uchar-integerp-alt-def` should normally suffice.
Even with the aforementioned isomorphisms disabled,
their executable counterparts are enabled (per ACL2's defaults),
exposing the internal representation in some constant cases;
we may consider keeping those executable counterparts disabled too.

- Def-integer-values
- Event to generate the model of the values of a C integer type.
- Ushort-list-from-integer-list
- Lift
`ushort`to lists. - Ullong-list-from-integer-list
- Lift
`ullong`to lists. - Sshort-list-from-integer-list
- Lift
`sshort`to lists. - Sllong-list-from-integer-list
- Lift
`sllong`to lists. - Integer-list-from-ushort-list
- Lift
`integer-from-ushort`to lists. - Integer-list-from-ullong-list
- Lift
`integer-from-ullong`to lists. - Integer-list-from-sshort-list
- Lift
`integer-from-sshort`to lists. - Integer-list-from-sllong-list
- Lift
`integer-from-sllong`to lists. - Ulong-list-from-integer-list
- Lift
`ulong`to lists. - Uchar-list-from-integer-list
- Lift
`uchar`to lists. - Slong-list-from-integer-list
- Lift
`slong`to lists. - Schar-list-from-integer-list
- Lift
`schar`to lists. - Integer-list-from-ulong-list
- Lift
`integer-from-ulong`to lists. - Integer-list-from-uchar-list
- Lift
`integer-from-uchar`to lists. - Integer-list-from-slong-list
- Lift
`integer-from-slong`to lists. - Integer-list-from-schar-list
- Lift
`integer-from-schar`to lists. - Uint-list-from-integer-list
- Lift
`uint`to lists. - Sint-list-from-integer-list
- Lift
`sint`to lists. - Integer-list-from-uint-list
- Lift
`integer-from-uint`to lists. - Integer-list-from-sint-list
- Lift
`integer-from-sint`to lists. - Cinteger
- Fixtype of all the supported C integer types.
- Ullongp
- Recognizer of values of type
unsigned long long . - Ucharp
- Recognizer of values of type
unsigned char . - Sintp
- Recognizer of values of type
signed int . - Ushortp
- Recognizer of values of type
unsigned short . - Ulongp
- Recognizer of values of type
unsigned long . - Uintp
- Recognizer of values of type
unsigned int . - Sllongp
- Recognizer of values of type
signed long long . - Slongp
- Recognizer of values of type
signed long . - Sshortp
- Recognizer of values of type
signed short . - Scharp
- Recognizer of values of type
signed char . - Integer-from-sshort
- Accessor for values of type
signed short . - Integer-from-sllong
- Accessor for values of type
signed long long . - Integer-from-sint
- Accessor for values of type
signed int . - Integer-from-slong
- Accessor for values of type
signed long . - Integer-from-schar
- Accessor for values of type
signed char . - Integer-type-to-fixtype
- Name of the fixtype of the values of a C integer type.
- Integer-from-ushort
- Accessor for values of type
unsigned short . - Integer-from-ullong
- Accessor for values of type
unsigned long long . - Integer-from-uchar
- Accessor for values of type
unsigned char . - Integer-from-cinteger
- ACL2 integer corresponding to the C integer.
- Integer-from-ulong
- Accessor for values of type
unsigned long . - Integer-from-uint
- Accessor for values of type
unsigned int . - Def-integer-values-loop
- Events to generate the models of the values of some C integer types.
- Sint-from-integer
- Constructor for values of type
signed int . - Sint
- Fixtype of values of type
signed int . - Fixtype-to-integer-type
- Integer type corresponding to a fixtype name, if any.
- Uchar-from-integer
- Constructor for values of type
unsigned char . - Ushort-from-integer-mod
- Reduce modularly ACL2 integers to values of type
unsigned short . - Ushort-from-integer
- Constructor for values of type
unsigned short . - Ulong-from-integer-mod
- Reduce modularly ACL2 integers to values of type
unsigned long . - Ulong-from-integer
- Constructor for values of type
unsigned long . - Ullong-from-integer-mod
- Reduce modularly ACL2 integers to values of type
unsigned long long . - Ullong-from-integer
- Constructor for values of type
unsigned long long . - Uchar-from-integer-mod
- Reduce modularly ACL2 integers to values of type
unsigned char . - Sshort-from-integer
- Constructor for values of type
signed short . - Slong-from-integer
- Constructor for values of type
signed long . - Sllong-from-integer
- Constructor for values of type
signed long long . - Schar-from-integer
- Constructor for values of type
signed char . - Uint-from-integer-mod
- Reduce modularly ACL2 integers to values of type
unsigned int . - Uint-from-integer
- Constructor for values of type
unsigned int . - Uchar
- Fixtype of values of type
unsigned char . - Schar
- Fixtype of values of type
signed char . - Ushort
- Fixtype of values of type
unsigned short . - Ulong
- Fixtype of values of type
unsigned long . - Ullong
- Fixtype of values of type
unsigned long long . - Sshort
- Fixtype of values of type
signed short . - Slong
- Fixtype of values of type
signed long . - Sllong
- Fixtype of values of type
signed long long . - Ullong-fix
- Fixer for values of type
unsigned long long . - Uint
- Fixtype of values of type
unsigned int . - Uchar-fix
- Fixer for values of type
unsigned char . - Sint-fix
- Fixer for values of type
signed int . - Ushort-fix
- Fixer for values of type
unsigned short . - Ulong-fix
- Fixer for values of type
unsigned long . - Uint-fix
- Fixer for values of type
unsigned int . - Sshort-fix
- Fixer for values of type
signed short . - Slong-fix
- Fixer for values of type
signed long . - Sllong-fix
- Fixer for values of type
signed long long . - Schar-fix
- Fixer for values of type
signed char . - Ushort-list
- Fixtype of lists of values of type
unsigned short . - Ulong-list
- Fixtype of lists of values of type
unsigned long . - Ullong-list
- Fixtype of lists of values of type
unsigned long long . - Uint-list
- Fixtype of lists of values of type
unsigned int . - Uchar-list
- Fixtype of lists of values of type
unsigned char . - Sshort-list
- Fixtype of lists of values of type
signed short . - Slong-list
- Fixtype of lists of values of type
signed long . - Sllong-list
- Fixtype of lists of values of type
signed long long . - Sint-list
- Fixtype of lists of values of type
signed int . - Schar-list
- Fixtype of lists of values of type
signed char . - Integer-type-to/from-fixtype-theorems
- Inversion theorems about the mappings between integer types and fixtype symbols.
- *nonchar-integer-fixtypes*
- List of the fixtype names of
the (supported) C integer types except plain
char .