Apply the integer promotions to an arithmetic type [C:6.3.1.1/2].
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
The plain
Function:
(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:
(defthm typep-of-promote-type (b* ((promoted-type (promote-type type))) (typep promoted-type)) :rule-classes :rewrite)
Theorem:
(defthm type-arithmeticp-of-promote-type (equal (type-arithmeticp (promote-type type)) (type-arithmeticp type)))
Theorem:
(defthm type-promoted-arithmeticp-of-promote-type (equal (type-promoted-arithmeticp (promote-type type)) (type-arithmeticp type)))
Theorem:
(defthm type-integerp-of-promote-type (equal (type-integerp (promote-type type)) (type-integerp type)))
Theorem:
(defthm type-nonchar-integerp-of-promote-type (implies (type-nonchar-integerp type) (type-nonchar-integerp (promote-type type))))
Theorem:
(defthm promote-type-when-not-type-integerp (implies (not (type-integerp type)) (equal (promote-type type) (type-fix type))))
Theorem:
(defthm type-kind-of-promote-type-not-schar (not (equal (type-kind (promote-type type)) :schar)))
Theorem:
(defthm type-kind-of-promote-type-not-uchar (not (equal (type-kind (promote-type type)) :uchar)))
Theorem:
(defthm type-kind-of-promote-type-not-sshort (not (equal (type-kind (promote-type type)) :sshort)))
Theorem:
(defthm type-kind-of-promote-type-not-ushort (not (equal (type-kind (promote-type type)) :ushort)))
Theorem:
(defthm promote-type-of-type-fix-type (equal (promote-type (type-fix type)) (promote-type type)))
Theorem:
(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)