Apply the usual arithmetic conversions to two arithmetic values [C:6.3.1.8].
This is the dynamic counterpart of uaconvert-types. See the documentation of that function for details. Here we actually convert the values; we do not merely compute the common type.
We convert the types of the values, obtaining the type of the new values. Then we convert each value to the new type. In our current model all the arithmetic values are integer values, so we use the integer conversions; if/when we add other arithmetic values, we will generalize this to arithmetic conversions.
This function never returns error: the usual arithmetic converesions always work. To show this, we need to show that convert-integer-value never returns errors when used to promote values, which we do via rules about convert-integer-value.
Theorem:
(defthm uaconvert-values-not-error-lemma (implies (and (value-arithmeticp val) (type-arithmeticp type)) (and (valuep (convert-integer-value val (uaconvert-types (type-of-value val) type))) (valuep (convert-integer-value val (uaconvert-types type (type-of-value val)))))))
Function:
(defun uaconvert-values (val1 val2) (declare (xargs :guard (and (valuep val1) (valuep val2)))) (declare (xargs :guard (and (value-arithmeticp val1) (value-arithmeticp val2)))) (let ((__function__ 'uaconvert-values)) (declare (ignorable __function__)) (b* ((type (uaconvert-types (type-of-value val1) (type-of-value val2))) (new-val1 (convert-integer-value val1 type)) (new-val2 (convert-integer-value val2 type))) (mv (value-fix new-val1) (value-fix new-val2)))))
Theorem:
(defthm valuep-of-uaconvert-values.new-val1 (b* (((mv ?new-val1 ?new-val2) (uaconvert-values val1 val2))) (valuep new-val1)) :rule-classes :rewrite)
Theorem:
(defthm valuep-of-uaconvert-values.new-val2 (b* (((mv ?new-val1 ?new-val2) (uaconvert-values val1 val2))) (valuep new-val2)) :rule-classes :rewrite)
Theorem:
(defthm type-of-value-of-uaconvert-values (implies (and (value-arithmeticp val1) (value-arithmeticp val2)) (b* (((mv new-val1 new-val2) (uaconvert-values val1 val2)) (type (uaconvert-types (type-of-value val1) (type-of-value val2)))) (and (equal (type-of-value new-val1) type) (equal (type-of-value new-val2) type)))))
Theorem:
(defthm value-arithmeticp-of-uaconvert-values (implies (and (value-arithmeticp val1) (value-arithmeticp val2)) (b* (((mv ?new-val1 ?new-val2) (uaconvert-values val1 val2))) (and (value-arithmeticp new-val1) (value-arithmeticp new-val2)))))
Theorem:
(defthm value-promoted-arithmeticp-of-uaconvert-values (b* (((mv newval1 newval2) (uaconvert-values val1 val2))) (implies (and (value-arithmeticp val1) (value-arithmeticp val2)) (and (value-promoted-arithmeticp newval1) (value-promoted-arithmeticp newval2)))))
Theorem:
(defthm value-integerp-of-uaconvert-values (implies (and (value-integerp val1) (value-integerp val2)) (b* (((mv ?new-val1 ?new-val2) (uaconvert-values val1 val2))) (and (value-integerp new-val1) (value-integerp new-val2)))))
Theorem:
(defthm uaconvert-values-of-value-fix-val1 (equal (uaconvert-values (value-fix val1) val2) (uaconvert-values val1 val2)))
Theorem:
(defthm uaconvert-values-value-equiv-congruence-on-val1 (implies (value-equiv val1 val1-equiv) (equal (uaconvert-values val1 val2) (uaconvert-values val1-equiv val2))) :rule-classes :congruence)
Theorem:
(defthm uaconvert-values-of-value-fix-val2 (equal (uaconvert-values val1 (value-fix val2)) (uaconvert-values val1 val2)))
Theorem:
(defthm uaconvert-values-value-equiv-congruence-on-val2 (implies (value-equiv val2 val2-equiv) (equal (uaconvert-values val1 val2) (uaconvert-values val1 val2-equiv))) :rule-classes :congruence)