		Search-engine friendly clone of the ACL2 documentation.

Atc-types

Positive-to-iconst

Turn a positive integer into an integer constant.

Signature
(positive-to-iconst pos) → iconst
Arguments: pos — Guard (posp pos).
Returns: iconst — Type (iconstp iconst).

We always generate a decimal constant of the smallest type that can represent it. We cause an internal error if the integer is too large even for unsigned long long. This is never expected to happen, given expected invariants that hold when this function is called.

Definitions and Theorems

Function: positive-to-iconst

(defun positive-to-iconst (pos)
  (declare (xargs :guard (posp pos)))
  (let ((__function__ 'positive-to-iconst))
    (declare (ignorable __function__))
    (cond ((<= pos (sint-max))
           (make-iconst :value pos
                        :base (iconst-base-dec)
                        :unsignedp nil
                        :length (iconst-length-none)))
          ((<= pos (uint-max))
           (make-iconst :value pos
                        :base (iconst-base-dec)
                        :unsignedp t
                        :length (iconst-length-none)))
          ((<= pos (slong-max))
           (make-iconst :value pos
                        :base (iconst-base-dec)
                        :unsignedp nil
                        :length (iconst-length-long)))
          ((<= pos (ulong-max))
           (make-iconst :value pos
                        :base (iconst-base-dec)
                        :unsignedp t
                        :length (iconst-length-long)))
          ((<= pos (sllong-max))
           (make-iconst :value pos
                        :base (iconst-base-dec)
                        :unsignedp nil
                        :length (iconst-length-llong)))
          ((<= pos (ullong-max))
           (make-iconst :value pos
                        :base (iconst-base-dec)
                        :unsignedp t
                        :length (iconst-length-llong)))
          (t (prog2$ (raise "Internal error: ~x0 too large." pos)
                     (ec-call (iconst-fix :irrelevant)))))))

Theorem: iconstp-of-positive-to-iconst

(defthm iconstp-of-positive-to-iconst
  (b* ((iconst (positive-to-iconst pos)))
    (iconstp iconst))
  :rule-classes :rewrite)