		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

Fast-logext16

Optimized implementation of 16-bit sign-extension.

Signature
(fast-logext16 x) → *
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: fast-logext16$inline

(defun fast-logext16$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'fast-logext16))
    (declare (ignorable __function__))
    (mbe :logic (logext 16 x)
         :exec (the (signed-byte 16)
                    (- (the (unsigned-byte 16)
                            (logxor (the (unsigned-byte 16)
                                         (logand 65535 x))
                                    (the (unsigned-byte 16) 32768)))
                       32768)))))