Apply the usual arithmetic conversions to two arithmetic types [C:6.3.1.8].
These determine a common type from the two types, which is also the type of the result of a binary operator applied to operands of the two types.
Function:
(defun uaconvert-types (type1 type2) (declare (xargs :guard (and (typep type1) (typep type2)))) (declare (xargs :guard (and (type-arithmeticp type1) (type-arithmeticp type2)))) (let ((__function__ 'uaconvert-types)) (declare (ignorable __function__)) (b* ((type1 (promote-type type1)) (type2 (promote-type type2)) ((acl2::fun (irr-type)) (ec-call (type-fix :irrelevant)))) (case (type-kind type1) (:sllong (case (type-kind type2) (:sllong (type-sllong)) (:slong (type-sllong)) (:sint (type-sllong)) (:ullong (type-ullong)) (:ulong (if (>= (sllong-max) (ulong-max)) (type-sllong) (type-ullong))) (:uint (if (>= (sllong-max) (uint-max)) (type-sllong) (type-ullong))) (t (prog2$ (impossible) (irr-type))))) (:slong (case (type-kind type2) (:sllong (type-sllong)) (:slong (type-slong)) (:sint (type-slong)) (:ullong (type-ullong)) (:ulong (type-ulong)) (:uint (if (>= (slong-max) (uint-max)) (type-slong) (type-ulong))) (t (prog2$ (impossible) (irr-type))))) (:sint (case (type-kind type2) (:sllong (type-sllong)) (:slong (type-slong)) (:sint (type-sint)) (:ullong (type-ullong)) (:ulong (type-ulong)) (:uint (type-uint)) (t (prog2$ (impossible) (irr-type))))) (:ullong (case (type-kind type2) (:sllong (type-ullong)) (:slong (type-ullong)) (:sint (type-ullong)) (:ullong (type-ullong)) (:ulong (type-ullong)) (:uint (type-ullong)) (t (prog2$ (impossible) (irr-type))))) (:ulong (case (type-kind type2) (:sllong (if (>= (sllong-max) (ulong-max)) (type-sllong) (type-ullong))) (:slong (type-ulong)) (:sint (type-ulong)) (:ullong (type-ullong)) (:ulong (type-ulong)) (:uint (type-ulong)) (t (prog2$ (impossible) (irr-type))))) (:uint (case (type-kind type2) (:sllong (if (>= (sllong-max) (uint-max)) (type-sllong) (type-ullong))) (:slong (if (>= (slong-max) (uint-max)) (type-slong) (type-ulong))) (:sint (type-uint)) (:ullong (type-ullong)) (:ulong (type-ulong)) (:uint (type-uint)) (t (prog2$ (impossible) (irr-type))))) (t (prog2$ (impossible) (irr-type)))))))
Theorem:
(defthm typep-of-uaconvert-types (b* ((type (uaconvert-types type1 type2))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm type-arithmeticp-of-uaconvert-types (equal (type-arithmeticp (uaconvert-types type1 type2)) (and (type-arithmeticp type1) (type-arithmeticp type2))))
Theorem:
(defthm type-integerp-of-uaconvert-types (implies (and (type-arithmeticp type1) (type-arithmeticp type2)) (equal (type-integerp (uaconvert-types type1 type2)) (and (type-integerp type1) (type-integerp type2)))))
Theorem:
(defthm type-nonchar-integerp-of-uaconvert-types (implies (and (type-integerp type1) (type-integerp type2)) (b* ((?type (uaconvert-types type1 type2))) (type-nonchar-integerp type))))
Theorem:
(defthm type-kind-of-uaconvert-types-not-schar (not (equal (type-kind (uaconvert-types type1 type2)) :schar)))
Theorem:
(defthm type-kind-of-uaconvert-types-not-uchar (not (equal (type-kind (uaconvert-types type1 type2)) :uchar)))
Theorem:
(defthm type-kind-of-uaconvert-types-not-sshort (not (equal (type-kind (uaconvert-types type1 type2)) :sshort)))
Theorem:
(defthm type-kind-of-uaconvert-types-not-ushort (not (equal (type-kind (uaconvert-types type1 type2)) :ushort)))
Theorem:
(defthm uaconvert-types-when-same (implies (and (type-arithmeticp type1) (type-arithmeticp type2) (type-equiv type1 type2)) (equal (uaconvert-types type1 type2) (promote-type type1))))
Theorem:
(defthm uaconvert-types-symmetry (implies (and (type-arithmeticp type1) (type-arithmeticp type2)) (equal (uaconvert-types type1 type2) (uaconvert-types type2 type1))))
Theorem:
(defthm uaconvert-types-of-type-fix-type1 (equal (uaconvert-types (type-fix type1) type2) (uaconvert-types type1 type2)))
Theorem:
(defthm uaconvert-types-type-equiv-congruence-on-type1 (implies (type-equiv type1 type1-equiv) (equal (uaconvert-types type1 type2) (uaconvert-types type1-equiv type2))) :rule-classes :congruence)
Theorem:
(defthm uaconvert-types-of-type-fix-type2 (equal (uaconvert-types type1 (type-fix type2)) (uaconvert-types type1 type2)))
Theorem:
(defthm uaconvert-types-type-equiv-congruence-on-type2 (implies (type-equiv type2 type2-equiv) (equal (uaconvert-types type1 type2) (uaconvert-types type1 type2-equiv))) :rule-classes :congruence)