		Search-engine friendly clone of the ACL2 documentation.

Integer-format

Make-integer-format

Basic constructor macro for integer-format structures.

Syntax

(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.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-integer-format

(defmacro make-integer-format (&rest args)
  (std::make-aggregate 'integer-format
                       args '((:pair))
                       'make-integer-format
                       nil))

Function: integer-format

(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))))))