		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))))))