		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-dec-core-fconst

Print a decimal core floating constant.

Signature
(print-dec-core-fconst fconst pstate) → new-pstate
Arguments: fconst — Guard (dec-core-fconstp fconst).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

For an integer one, we ensure that there is at least one digit. For a fractional one, the check is performed in print-dec-frac-const.

Definitions and Theorems

Function: print-dec-core-fconst

(defun print-dec-core-fconst (fconst pstate)
 (declare (xargs :guard (and (dec-core-fconstp fconst)
                             (pristatep pstate))))
 (let ((__function__ 'print-dec-core-fconst))
  (declare (ignorable __function__))
  (dec-core-fconst-case
   fconst :frac
   (b* ((pstate (print-dec-frac-const fconst.significand pstate))
        (pstate (print-dec-expo-option fconst.expo? pstate)))
     pstate)
   :int
   (b*
    (((unless fconst.significand)
      (raise
       "Misusage error: ~
                      the integer decimal core floating constant ~
                      has no digits in the significand.")
      (pristate-fix pstate))
     (pstate (print-dec-digit-achars fconst.significand pstate))
     (pstate (print-dec-expo fconst.expo pstate)))
    pstate))))

Theorem: pristatep-of-print-dec-core-fconst

(defthm pristatep-of-print-dec-core-fconst
  (b* ((new-pstate (print-dec-core-fconst fconst pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-dec-core-fconst

(defthm pristate->gcc-of-print-dec-core-fconst
  (b* ((?new-pstate (print-dec-core-fconst fconst pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-dec-core-fconst-of-dec-core-fconst-fix-fconst

(defthm print-dec-core-fconst-of-dec-core-fconst-fix-fconst
  (equal (print-dec-core-fconst (dec-core-fconst-fix fconst)
                                pstate)
         (print-dec-core-fconst fconst pstate)))

Theorem: print-dec-core-fconst-dec-core-fconst-equiv-congruence-on-fconst

(defthm
   print-dec-core-fconst-dec-core-fconst-equiv-congruence-on-fconst
  (implies (dec-core-fconst-equiv fconst fconst-equiv)
           (equal (print-dec-core-fconst fconst pstate)
                  (print-dec-core-fconst fconst-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-dec-core-fconst-of-pristate-fix-pstate

(defthm print-dec-core-fconst-of-pristate-fix-pstate
  (equal (print-dec-core-fconst fconst (pristate-fix pstate))
         (print-dec-core-fconst fconst pstate)))

Theorem: print-dec-core-fconst-pristate-equiv-congruence-on-pstate

(defthm print-dec-core-fconst-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-dec-core-fconst fconst pstate)
                  (print-dec-core-fconst fconst pstate-equiv)))
  :rule-classes :congruence)