		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Promote-type

Apply the integer promotions to an arithmetic type [C17:6.3.1.1/2].

Signature
(promote-type type) → promoted-type
Arguments: type — Guard (typep type).
Returns: promoted-type — Type (typep promoted-type).

These are the static counterpart of the integer promotions that are applied to values: statically, they are applied to types.

These only modify the character and short types; all the other types are unchanged.

If int can represent all the values of the original type, the promotion is to int: this is always the case for signed char and signed short, but not necessarily for char (which may be signed or not), unsigned char, and unsigned short. In the unlikely but allowed case that a byte consists of 16 bits and that int also consists of 16 bits, some unsigned char values are not representable in int. Otherwise, the promotion is to unsigned int.

The plain char type is not supported for now. It will be soon.

Definitions and Theorems

Function: promote-type

(defun promote-type (type)
 (declare (xargs :guard (typep type)))
 (declare (xargs :guard (type-arithmeticp type)))
 (let ((__function__ 'promote-type))
  (declare (ignorable __function__))
  (case (type-kind type)
   (:char
    (prog2$ (raise "Internal error: plain char type not supported.")
            (type-sint)))
   (:schar (type-sint))
   (:uchar (if (<= (uchar-max) (sint-max))
               (type-sint)
             (type-uint)))
   (:sshort (type-sint))
   (:ushort (if (<= (ushort-max) (sint-max))
                (type-sint)
              (type-uint)))
   (t (type-fix type)))))

Theorem: typep-of-promote-type

(defthm typep-of-promote-type
  (b* ((promoted-type (promote-type type)))
    (typep promoted-type))
  :rule-classes :rewrite)

Theorem: type-arithmeticp-of-promote-type

(defthm type-arithmeticp-of-promote-type
  (equal (type-arithmeticp (promote-type type))
         (type-arithmeticp type)))

Theorem: type-promoted-arithmeticp-of-promote-type

(defthm type-promoted-arithmeticp-of-promote-type
  (equal (type-promoted-arithmeticp (promote-type type))
         (type-arithmeticp type)))

Theorem: type-integerp-of-promote-type

(defthm type-integerp-of-promote-type
  (equal (type-integerp (promote-type type))
         (type-integerp type)))

Theorem: type-nonchar-integerp-of-promote-type

(defthm type-nonchar-integerp-of-promote-type
  (implies (type-nonchar-integerp type)
           (type-nonchar-integerp (promote-type type))))

Theorem: promote-type-when-not-type-integerp

(defthm promote-type-when-not-type-integerp
  (implies (not (type-integerp type))
           (equal (promote-type type)
                  (type-fix type))))

Theorem: type-kind-of-promote-type-not-schar

(defthm type-kind-of-promote-type-not-schar
  (not (equal (type-kind (promote-type type))
              :schar)))

Theorem: type-kind-of-promote-type-not-uchar

(defthm type-kind-of-promote-type-not-uchar
  (not (equal (type-kind (promote-type type))
              :uchar)))

Theorem: type-kind-of-promote-type-not-sshort

(defthm type-kind-of-promote-type-not-sshort
  (not (equal (type-kind (promote-type type))
              :sshort)))

Theorem: type-kind-of-promote-type-not-ushort

(defthm type-kind-of-promote-type-not-ushort
  (not (equal (type-kind (promote-type type))
              :ushort)))

Theorem: promote-type-of-type-fix-type

(defthm promote-type-of-type-fix-type
  (equal (promote-type (type-fix type))
         (promote-type type)))

Theorem: promote-type-type-equiv-congruence-on-type

(defthm promote-type-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (promote-type type)
                  (promote-type type-equiv)))
  :rule-classes :congruence)