		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-fconst

Validate a floating constant.

Signature
(valid-fconst fconst) → type
Arguments: fconst — Guard (fconstp fconst).
Returns: type — Type (typep type).

A floating constant is always valid: [C:6.4.4.2] states no restrictions, except for a recommended practice to provide a diagnostic message in certain cases, which also instructs to proceed with compilation nonetheless, suggesting that it should be only a warning, not an error.

The type is determined solely by the suffix, including its absence [C:6.4.4.2/4].

Definitions and Theorems

Function: valid-fconst

(defun valid-fconst (fconst)
  (declare (xargs :guard (fconstp fconst)))
  (let ((__function__ 'valid-fconst))
    (declare (ignorable __function__))
    (b* ((suffix? (fconst-case fconst
                               :dec fconst.suffix?
                               :hex fconst.suffix?)))
      (cond ((not suffix?) (type-double))
            ((or (fsuffix-case suffix? :locase-f)
                 (fsuffix-case suffix? :upcase-f))
             (type-float))
            ((or (fsuffix-case suffix? :locase-l)
                 (fsuffix-case suffix? :upcase-l))
             (type-ldouble))
            (t (prog2$ (impossible) (irr-type)))))))

Theorem: typep-of-valid-fconst

(defthm typep-of-valid-fconst
  (b* ((type (valid-fconst fconst)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-fconst-of-fconst-fix-fconst

(defthm valid-fconst-of-fconst-fix-fconst
  (equal (valid-fconst (fconst-fix fconst))
         (valid-fconst fconst)))

Theorem: valid-fconst-fconst-equiv-congruence-on-fconst

(defthm valid-fconst-fconst-equiv-congruence-on-fconst
  (implies (fconst-equiv fconst fconst-equiv)
           (equal (valid-fconst fconst)
                  (valid-fconst fconst-equiv)))
  :rule-classes :congruence)