Filtering...

float-raw

float-raw
other
(in-package "ACL2")
df-signal?macro
(defmacro df-signal? (form op) (declare (ignore op)) form)
defun-df-binarymacro
(defmacro defun-df-binary
  (name op)
  (let ((body `(df-signal? (,OP (the double-float x) (the double-float y))
         ,OP)))
    `(progn (defun ,NAME
        (x y)
        (declare (type double-float x y))
        (the double-float ,BODY)))))
defun-df-unarymacro
(defmacro defun-df-unary
  (name op)
  (let ((body `(df-signal? (,OP (the double-float x)) ,OP)))
    `(progn (defun ,NAME
        (x)
        (declare (type double-float x))
        (the double-float ,BODY)))))
other
(defun-df-binary binary-df+ +)
other
(defun-df-binary binary-df* *)
other
(defun-df-binary binary-df/ /)
other
(defun-df-binary binary-df-log log)
other
(defun-df-binary df-expt-fn expt)
other
(defun-df-unary unary-df- -)
other
(defun-df-unary unary-df/ /)
other
(defun-df-unary df-exp-fn exp)
other
(defun-df-unary df-sqrt-fn sqrt)
other
(defun-df-unary unary-df-log log)
other
(defun-df-unary df-abs-fn abs)
other
(defun-df-unary df-sin-fn sin)
other
(defun-df-unary df-cos-fn cos)
other
(defun-df-unary df-tan-fn tan)
other
(defun-df-unary df-asin-fn asin)
other
(defun-df-unary df-acos-fn acos)
other
(defun-df-unary df-atan-fn atan)
other
(defun-df-unary df-sinh-fn sinh)
other
(defun-df-unary df-cosh-fn cosh)
other
(defun-df-unary df-tanh-fn tanh)
other
(defun-df-unary df-asinh-fn asinh)
other
(defun-df-unary df-acosh-fn acosh)
other
(defun-df-unary df-atanh-fn atanh)
df-pifunction
(defun df-pi nil pi)
df-stringfunction
(defun df-string
  (x)
  (the string
    (cond ((typep x 'double-float) (let* ((s (princ-to-string x)) (p1 (position #\E s))
            (p2 (and (not p1) (position #\e s)))
            (p (or p1 p2)))
          (cond ((and p (not (member (char s (1+ p)) '(#\+ #\-)))) (cond (p1 (concatenate 'string
                    (subseq s 0 (1+ p1))
                    "+"
                    (subseq s (1+ p1) (length s))))
                (t (concatenate 'string
                    (subseq s 0 p2)
                    "E+"
                    (subseq s (1+ p2) (length s))))))
            (p2 (concatenate 'string
                (subseq s 0 p2)
                "E"
                (subseq s (1+ p2) (length s))))
            (t s))))
      (t (error "~s called on non-df value, ~s" 'df-string x) ""))))
make-dffunction
(defun make-df
  (x)
  (cond ((typep x 'double-float) x)
    ((rationalp x) (let ((xf (to-df x)))
        (and (= xf x) xf)))
    (t nil)))
defun-df-*1*-unarymacro
(defmacro defun-df-*1*-unary
  (fn &rest more-guard-conjuncts)
  `(defun-*1* ,FN
    (x)
    (the rational
      (let ((xf (make-df x)))
        (cond ((and xf
             ,@(AND MORE-GUARD-CONJUNCTS
       `((LET ((X XF))
           ,@MORE-GUARD-CONJUNCTS)))) (rational (,FN xf)))
          (t (gv ,FN
              (x)
              ,(COND ((EQ FN 'UNARY-DF-) `(DF-ROUND (FUNCALL ',(*1*-SYMBOL 'UNARY--) X)))
       ((EQ FN 'UNARY-DF/) `(DF-ROUND (FUNCALL ',(*1*-SYMBOL 'UNARY-/) X)))
       (T `(,(PACKN (LIST 'CONSTRAINED- FN)) X))))))))))
defun-df-*1*-binarymacro
(defmacro defun-df-*1*-binary
  (fn &rest more-guard-conjuncts)
  `(defun-*1* ,FN
    (x y)
    (the rational
      (let ((xf (make-df x)) (yf (make-df y)))
        (declare (type (or double-float null) xf yf))
        (cond ((and xf
             yf
             ,@(AND MORE-GUARD-CONJUNCTS
       `((LET ((X XF) (Y YF))
           (DECLARE (IGNORABLE X Y))
           ,@MORE-GUARD-CONJUNCTS)))) (rational (,FN xf yf)))
          (t (gv ,FN
              (x y)
              ,(COND ((EQ FN 'BINARY-DF+) `(DF-ROUND (FUNCALL ',(*1*-SYMBOL 'BINARY-+) X Y)))
       ((EQ FN 'BINARY-DF*) `(DF-ROUND (FUNCALL ',(*1*-SYMBOL 'BINARY-*) X Y)))
       ((EQ FN 'BINARY-DF/)
        `(DF-ROUND
          (FUNCALL ',(*1*-SYMBOL 'BINARY-*) X
                   (FUNCALL ',(*1*-SYMBOL 'UNARY-/) Y))))
       (T `(,(PACKN (LIST 'CONSTRAINED- FN)) X Y))))))))))
other
(defun-*1* from-df
  (x)
  (cond ((typep x 'double-float) (rational x))
    ((dfp x) x)
    (t (gv from-df (x) x))))
other
(defun-*1* dfp (x) (dfp x))
other
(defconstant rational-pi (rational pi))
other
(defun-*1* df-pi nil rational-pi)
other
(defun-*1* to-df
  (x)
  (rational (cond ((typep x 'double-float) (rational x))
      ((rationalp x) (rational (to-df x)))
      (t (gv to-df (x) (constrained-to-df x))))))
other
(defun-*1* df-string
  (x)
  (cond ((typep x 'double-float) (df-string x))
    ((rationalp x) (df-string (to-df x)))
    (t (gv df-string (x) (constrained-df-string x)))))
defun-df-*1*-from-function-sigsmacro
(defmacro defun-df-*1*-from-function-sigs
  nil
  (cons 'progn
    (loop with
      tmp
      for
      tuple
      in
      *df-function-sigs-exec*
      as
      fn
      =
      (car tuple)
      as
      args
      =
      (cadr tuple)
      when
      (setq tmp
        (cond ((null args) nil)
          ((null (cdr args)) `(defun-df-*1*-unary ,FN ,@(CDDR TUPLE)))
          ((null (cddr args)) `(defun-df-*1*-binary ,FN ,@(CDDR TUPLE)))
          (t (error "Unexpected: ~s has ~s arguments, ~
                                        which is more than 2."
              fn
              (length args)))))
      collect
      tmp)))
other
(defun-df-*1*-from-function-sigs)
other
(defun-df-*1*-unary unary-df-)
other
(defun-df-*1*-unary unary-df/)
other
(defun-df-*1*-unary df-rationalize)
other
(defun-df-*1*-binary binary-df+)
other
(defun-df-*1*-binary binary-df*)
other
(defun-df-*1*-binary binary-df/ (not (= y 0)))