		Search-engine friendly clone of the ACL2 documentation.

Floating-point-converts

Sse-cvt-fp1-to-fp2-special

Check whether the operand is SNaN or QNaN and then return corresponding result. Also handle the infinities.

Signature
(sse-cvt-fp1-to-fp2-special kind sign implicit frac frac-width1 exp-width2 frac-width2) → (mv * * * * * *)
Arguments: frac — Guard (natp frac).; frac-width1 — Guard (posp frac-width1).; exp-width2 — Guard (posp exp-width2).; frac-width2 — Guard (posp frac-width2).

Definitions and Theorems

Function: sse-cvt-fp1-to-fp2-special

(defun sse-cvt-fp1-to-fp2-special
       (kind sign implicit
             frac frac-width1 exp-width2 frac-width2)
 (declare (type (unsigned-byte 1) sign)
          (type (unsigned-byte 1) implicit))
 (declare (xargs :guard (and (natp frac)
                             (posp frac-width1)
                             (posp exp-width2)
                             (posp frac-width2))))
 (let ((__function__ 'sse-cvt-fp1-to-fp2-special))
  (declare (ignorable __function__))
  (let ((invalid (eq kind 'snan)))
   (cond
       ((eq kind 'snan)
        (let ((exp-width exp-width2)
              (frac-width frac-width2)
              (nan-frac-bits
                   (ash (part-select frac
                                     :low 0
                                     :high (nfix (- frac-width1 2)))
                        (- frac-width2 frac-width1))))
          (flag-make-special-bp 'qnan
                                nan-frac-bits sign invalid)))
       ((or (eq kind 'qnan) (eq kind 'indef))
        (let ((exp-width exp-width2)
              (frac (ash frac (- frac-width2 frac-width1))))
          (mv t sign (fp-max-exp exp-width)
              implicit frac invalid)))
       ((eq kind 'inf)
        (let ((exp-width exp-width2)
              (frac-width frac-width2))
          (flag-make-special-bp 'inf
                                0 sign invalid)))
       (t (mv nil 0 0 0 0 invalid))))))

Theorem: integerp-sse-cvt-fp1-to-fp2-special-1

(defthm integerp-sse-cvt-fp1-to-fp2-special-1
  (implies
       (integerp sign)
       (integerp (mv-nth 1
                         (sse-cvt-fp1-to-fp2-special
                              kind sign implicit frac
                              frac-width1 exp-width2 frac-width2))))
  :rule-classes :type-prescription)

Theorem: integerp-sse-cvt-fp1-to-fp2-special-2

(defthm integerp-sse-cvt-fp1-to-fp2-special-2
 (integerp
  (mv-nth
   2
   (sse-cvt-fp1-to-fp2-special kind sign implicit frac
                               frac-width1 exp-width2 frac-width2)))
 :rule-classes :type-prescription)

Theorem: integerp-sse-cvt-fp1-to-fp2-special-3

(defthm integerp-sse-cvt-fp1-to-fp2-special-3
  (implies
       (integerp implicit)
       (integerp (mv-nth 3
                         (sse-cvt-fp1-to-fp2-special
                              kind sign implicit frac
                              frac-width1 exp-width2 frac-width2))))
  :rule-classes :type-prescription)

Theorem: integerp-sse-cvt-fp1-to-fp2-special-4

(defthm integerp-sse-cvt-fp1-to-fp2-special-4
 (integerp
  (mv-nth
   4
   (sse-cvt-fp1-to-fp2-special kind sign implicit frac
                               frac-width1 exp-width2 frac-width2)))
 :rule-classes :type-prescription)