		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Truncated-integer-sin/cos-table-fn

Helper for SIN/COS-TABLE-FN.

Note that this function has special code for 0, \pi/2, \pi, and \frac{3}{2}\pi. The convergence of the series at these points is problematic in the context of truncation (vs. rounding).

Definitions and Theorems

Function: truncated-integer-sin/cos-table-fn

(defun truncated-integer-sin/cos-table-fn
       (sin/cos i n pie itr scale)
 (declare
      (xargs :guard (and (or (eq sin/cos :sin) (eq sin/cos :cos))
                         (integerp i)
                         (<= 0 i)
                         (integerp n)
                         (<= 0 n)
                         (<= i n)
                         (rationalp pie)
                         (integerp itr)
                         (<= 0 itr)
                         (rationalp scale))))
 (cond
  ((zp (- n i)) nil)
  (t
   (let ((i/n (/ i n)))
     (cons (cons i
                 (case sin/cos
                   (:sin (case i/n
                           ((0 1/2) 0)
                           (1/4 (truncate scale 1))
                           (3/4 (truncate scale -1))
                           (t (truncated-integer-sin (* 2 pie i/n)
                                                     itr scale))))
                   (t (case i/n
                        (0 (truncate scale 1))
                        ((1/4 3/4) 0)
                        (1/2 (truncate scale -1))
                        (t (truncated-integer-cos (* 2 pie i/n)
                                                  itr scale))))))
           (truncated-integer-sin/cos-table-fn sin/cos (1+ i)
                                               n pie itr scale))))))