• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
          • Bitops/merge
          • Bitops-compatibility
          • Bitops-books
          • Logbitp-reasoning
          • Bitops/signed-byte-p
          • Fast-part-select
          • Bitops/integer-length
          • Bitops/extra-defs
          • Install-bit
          • Trailing-0-count
          • Bitops/defaults
          • Logbitp-mismatch
          • Trailing-1-count
          • Bitops/rotate
          • Bitops/equal-by-logbitp
          • Bitops/ash-bounds
          • Bitops/fast-logrev
          • Limited-shifts
          • Bitops/part-select
          • Bitops/parity
          • Bitops/saturate
          • Bitops/part-install
          • Bitops/logbitp-bounds
          • Bitops/ihsext-basics
          • Bitops/fast-rotate
            • Fast-rotate
              • Rotate-left-9
              • Rotate-left-8
              • Rotate-left-65
              • Rotate-left-64
              • Rotate-left-33
              • Rotate-left-32
              • Rotate-left-17
              • Rotate-left-16
              • Rotate-right-65
              • Rotate-right-64
              • Rotate-right-33
              • Rotate-right-32
              • Rotate-right-17
              • Rotate-right-16
              • Rotate-right-9
              • Rotate-right-8
          • Bitops/fast-logext
          • Bitops/ihs-extensions
        • Bv
        • Ihs
        • Rtl
      • Algebra
    • Testing-utilities
  • Bitops/fast-rotate

Fast-rotate

fast-rotate-left is logically identical to rotate-left and fast-rotate-right is logically identical to rotate-right.

fast-rotate-left and fast-rotate-right are actually macros. Generally, they expand into a call of rotate-left and rotate-right respectively. But in the common cases where n is explicitly 8, 16, 32, or 64, they instead expand into a call of a specialized, inlined function.

Macro: fast-rotate-left

(defmacro fast-rotate-left (x width places)
  (cond ((eql width 8)
         (cons 'rotate-left-8
               (cons x (cons places 'nil))))
        ((eql width 9)
         (cons 'rotate-left-9
               (cons x (cons places 'nil))))
        ((eql width 16)
         (cons 'rotate-left-16
               (cons x (cons places 'nil))))
        ((eql width 17)
         (cons 'rotate-left-17
               (cons x (cons places 'nil))))
        ((eql width 32)
         (cons 'rotate-left-32
               (cons x (cons places 'nil))))
        ((eql width 33)
         (cons 'rotate-left-33
               (cons x (cons places 'nil))))
        ((eql width 64)
         (cons 'rotate-left-64
               (cons x (cons places 'nil))))
        ((eql width 65)
         (cons 'rotate-left-65
               (cons x (cons places 'nil))))
        (t (cons 'rotate-left
                 (cons x (cons width (cons places 'nil)))))))

Macro: fast-rotate-right

(defmacro fast-rotate-right (x width places)
  (cond ((eql width 8)
         (cons 'rotate-right-8
               (cons x (cons places 'nil))))
        ((eql width 9)
         (cons 'rotate-right-9
               (cons x (cons places 'nil))))
        ((eql width 16)
         (cons 'rotate-right-16
               (cons x (cons places 'nil))))
        ((eql width 17)
         (cons 'rotate-right-17
               (cons x (cons places 'nil))))
        ((eql width 32)
         (cons 'rotate-right-32
               (cons x (cons places 'nil))))
        ((eql width 33)
         (cons 'rotate-right-33
               (cons x (cons places 'nil))))
        ((eql width 64)
         (cons 'rotate-right-64
               (cons x (cons places 'nil))))
        ((eql width 65)
         (cons 'rotate-right-65
               (cons x (cons places 'nil))))
        (t (cons 'rotate-right
                 (cons x (cons width (cons places 'nil)))))))

Subtopics

Rotate-left-9
Rotate-left-8
Rotate-left-65
Rotate-left-64
Rotate-left-33
Rotate-left-32
Rotate-left-17
Rotate-left-16
Rotate-right-65
Rotate-right-64
Rotate-right-33
Rotate-right-32
Rotate-right-17
Rotate-right-16
Rotate-right-9
Rotate-right-8