Basic constructor macro for integer-format structures.
(make-integer-format [:pair <pair>])
This is the usual way to construct integer-format structures. It simply conses together a structure with the specified fields.
This macro generates a new integer-format structure from scratch. See also change-integer-format, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-integer-format (&rest args) (std::make-aggregate 'integer-format args '((:pair)) 'make-integer-format nil))
Function:
(defun integer-format (pair) (declare (xargs :guard (uinteger+sinteger-formatp pair))) (declare (xargs :guard (uinteger-sinteger-bit-roles-wfp (uinteger-format->bits (uinteger+sinteger-format->unsigned pair)) (sinteger-format->bits (uinteger+sinteger-format->signed pair))))) (let ((__function__ 'integer-format)) (declare (ignorable __function__)) (b* ((pair (mbe :logic (uinteger+sinteger-format-fix pair) :exec pair))) (let ((pair (mbe :logic (if (uinteger-sinteger-bit-roles-wfp (uinteger-format->bits (uinteger+sinteger-format->unsigned pair)) (sinteger-format->bits (uinteger+sinteger-format->signed pair))) pair (make-uinteger+sinteger-format :unsigned (make-uinteger-format :bits (list (uinteger-bit-role-value 0) (uinteger-bit-role-value 1)) :traps nil) :signed (make-sinteger-format :bits (list (sinteger-bit-role-value 0) (sinteger-bit-role-sign)) :signed (signed-format-twos-complement) :traps nil))) :exec pair))) (list (cons 'pair pair))))))