		Search-engine friendly clone of the ACL2 documentation.

Fast-part-select

Fast-part-extend

Optimized function for selecting a signed bit range from a big integer.

Signature
(fast-part-extend x width low) → *
Arguments: x — Guard (integerp x).; width — Guard (posp width).; low — Guard (natp low).

This is the same as fast-part-select, but it returns a sign-extended range instead of a zero-extended one. Its implementation is more efficient than applying logext to the result of fast-part-select.

Definitions and Theorems

Function: fast-part-extend$inline

(defun fast-part-extend$inline (x width low)
  (declare (type integer x)
           (type (integer 0 *) width)
           (type (integer 0 *) low))
  (declare (xargs :guard (and (integerp x)
                              (posp width)
                              (natp low))))
  (declare (xargs :split-types t))
  (let ((__function__ 'fast-part-extend))
    (declare (ignorable __function__))
    (mbe :logic
         (logext width
                 (part-select-width-low x (pos-fix width)
                                        low))
         :exec
         (b* ((width (lposfix width))
              (low (lnfix low))
              (low-slice (ash low -5))
              (low-omit (logand 31 low))
              (high (+ -1 low width))
              (high-slice (ash high -5))
              (high-omit (- 31 (logand 31 high)))
              (slices (+ 1 (- high-slice low-slice))))
           (fast-pext x
                      low-slice slices low-omit high-omit)))))