float-b

(defun install-df-basic-primitives
  (state)
  (declare (xargs :mode :program))
  (if (global-val 'boot-strap-pass-2 (w state))
    state
    (set-w 'extension
      (install-df-basic-primitives-1 *df-basic-primitives*
        (w state))
      state)))

(defun to-df?-fn
  (x)
  (declare (xargs :guard t))
  (let ((x (cond ((and (consp x)
            (consp (cdr x))
            (null (cddr x))
            (eq (car x) 'quote)
            (acl2-numberp (cadr x))) (cadr x))
         (t x))))
    (cond ((acl2-numberp x) (cond ((dfp x) `(to-df ,X)) (t x)))
      ((and (symbolp x)
         (legal-constantp1 x)
         (not (member-eq x '(t nil)))) `(let ((c ,X))
          (assert$ (dfp c) (to-df c))))
      (t x))))

(defun to-df?-args
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((endp lst) nil)
    (t (cons (to-df?-fn (car lst)) (to-df?-args (cdr lst))))))

(defun defun-df-events
  (fn-name macro-name formals rest)
  (declare (xargs :guard (and (symbolp macro-name) (symbolp fn-name))))
  (let ((dfp-thm-name (packn-pos (list 'dfp- fn-name) fn-name)) (rationalp-thm-name (packn-pos (list 'rationalp- fn-name) fn-name)))
    `((defun ,FN-NAME
       ,FORMALS
       ,@(AND FORMALS `((DECLARE (TYPE DOUBLE-FLOAT ,@FORMALS))))
       ,@REST) (defthm ,DFP-THM-NAME (dfp (,FN-NAME ,@FORMALS)))
      (defthm ,RATIONALP-THM-NAME
        (rationalp (,FN-NAME ,@FORMALS))
        :rule-classes :type-prescription)
      ,@(AND MACRO-NAME
       `((DEFMACRO ,MACRO-NAME ,FORMALS
           (CONS ',FN-NAME (TO-DF?-ARGS (LIST ,@FORMALS))))
         ,(IF (EQ MACRO-NAME 'DF-LOG)
              `(TABLE UNTRANS-TABLE ',FN-NAME '(,MACRO-NAME))
              `(ADD-MACRO-FN ,MACRO-NAME ,FN-NAME))
         (VALUE-TRIPLE ',MACRO-NAME))))))

(defun df<-fn
  (x y)
  (declare (type double-float x y))
  (< (from-df x) (from-df y)))

(defun df=-fn
  (x y)
  (declare (type double-float x y))
  (= (from-df x) (from-df y)))

(defun df/=-fn
  (x y)
  (declare (type double-float x y))
  (/= (from-df x) (from-df y)))

(defun df0 nil (declare (xargs :guard t)) (to-df 0))

(defun df1 nil (declare (xargs :guard t)) (to-df 1))

(defun df-minus-1 nil (declare (xargs :guard t)) (to-df -1))

(defun df-function-sigs
  (flg)
  (declare (xargs :guard t))
  `((df-expt-fn (x y) (or (df< 0 x) (and (df= 0 x) (df< 0 y)))) (df-exp-fn (x))
    (df-sqrt-fn (x) (df<= 0 x))
    (binary-df-log (x y) (and (df< 0 x) (df<= 0 y)))
    (unary-df-log (x) (df< 0 x))
    (df-abs-fn (x))
    (df-sin-fn (x))
    (df-cos-fn (x))
    (df-tan-fn (x)
      (not (df= (,(IF FLG
     'CONSTRAINED-DF-COS-FN
     'DF-COS-FN) x)
          0)))
    (df-asin-fn (x) (df<= (df-abs-fn x) 1))
    (df-acos-fn (x) (df<= (df-abs-fn x) 1))
    (df-atan-fn (x))
    (df-sinh-fn (x))
    (df-cosh-fn (x))
    (df-tanh-fn (x)
      (not (df= (,(IF FLG
     'CONSTRAINED-DF-COSH-FN
     'DF-COSH-FN) x)
          0)))
    (df-asinh-fn (x))
    (df-acosh-fn (x) (df<= 1 x))
    (df-atanh-fn (x) (df< (df-abs x) 1))
    (df-pi nil)))

(defun df-macro-name
  (fn)
  (declare (type symbol fn))
  (let ((name (symbol-name fn)))
    (and (string-suffixp "-FN" name)
      (intern-in-package-of-symbol (subseq name 0 (- (length name) 3))
        fn))))

(defun df-events-1
  (sig flg)
  (declare (xargs :guard (and (<= 2 (len sig))
        (symbolp (car sig))
        (symbol-listp (cadr sig)))))
  (let* ((name (car sig)) (formals (cadr sig))
      (guard (if (consp (cddr sig))
          (caddr sig)
          t))
      (constrained-name (packn (list 'constrained- name)))
      (name (if flg
          constrained-name
          name))
      (macro-name (and (null flg) (df-macro-name name)))
      (rest `((declare (xargs :guard ,GUARD)) (to-df (non-exec (,CONSTRAINED-NAME ,@FORMALS)))))
      (events (defun-df-events name macro-name formals rest)))
    (if flg
      (cons `(local (defun ,NAME ,FORMALS 0)) (cdr events))
      events)))

(defun df-events
  (sigs flg)
  (declare (xargs :guard (and (symbol-alistp sigs)
        (all->=-len sigs 2)
        (symbol-list-listp (strip-cadrs sigs)))))
  (cond ((endp sigs) nil)
    (t (append (df-events-1 (car sigs) flg)
        (df-events (cdr sigs) flg)))))

(defun prefix-sigs-with-constrained
  (sigs)
  (declare (xargs :guard (and (alistp sigs)
        (symbol-alistp sigs)
        (true-list-listp sigs))))
  (cond ((endp sigs) nil)
    (t (cons (let* ((sig (car sigs)) (fn (car sig)) (formals (cadr sig)))
          (list (packn (list 'constrained- fn)) formals t))
        (prefix-sigs-with-constrained (cdr sigs))))))

(defun df-non-constrained-functions-events
  nil
  (declare (xargs :guard t))
  (df-events *df-function-sigs-exec* nil))

(defun df-rationalize
  (x)
  (declare (xargs :mode :logic)
    (type double-float x))
  (constrained-df-rationalize (from-df x)))

(defun rize
  (x)
  (declare (type rational x))
  (df-rationalize (to-df x)))