Defbytetype
A macro for defining integer subrange types.
The "byte types" defined by DEFBYTETYPE correspond to the Common
Lisp concept of a "byte", that is, an integer with a fixed number of bits.
We extend the Common Lisp concept to allow signed bytes.
Example:
(DEFBYTETYPE WORD 32 :SIGNED)
Defines a new integer type of 32-bit signed integers, recognized by
(WORD-P i).
General Form:
(DEFBYTETYPE name size s/u &key saturating-coercion)
The argument name should be a symbol, size should be a constant
expression (suitable for DEFCONST) for a positive integer, s/u is
either :SIGNED or :UNSIGNED, saturating-coercion should be a symbol (default
NIL).
Each data type defined by DEFBYTETYPE produces a number of events:
- A constant *<name>-MAX*, set to the maximum value of the type.
- A constant *<name>-MIN*, set to the minimum value of the type.
- A predicate, (<pred> x), that recognizes either (UNSIGNED-BYTE-P
size x) or (SIGNED-BYTE-P size x), depending on whether s/u
was :UNSIGNED or :SIGNED respectively. This predicate is DISABLED. The name of
the predicate will be <name>-p.
- A coercion function, (<name> i), that coerces any object i to the
correct type by LOGHEAD and LOGEXT for unsigned and signed integers
respectively. This function is DISABLED.
- A lemma showing that the coercion function actually does the correct
coercion.
- A lemma that reduces calls of the coercion function when its argument
satisfies the predicate.
- A forward chaining lemma from the predicate to the appropriate type
information.
- If :SATURATING-COERCION is specified, the value of this keyword argument
should be a symbol. A function of this name will be defined to provide a
saturating coercion. `Saturation' in this context means that values outside of
the legal range for the type are coerced to the type by setting them to the
nearest legal value, which will be either the minimum or maximum value of the
type. This function will be DISABLEd, and a lemma will be generated that proves
that this function returns the correct type. Note that
the :SATURATING-COERCION option is only valid for :SIGNED types.
- A theory named <name>-THEORY that includes the lemmas and the
DEFUN-TYPE/EXEC-THEORY of the functions.
