		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Promote-value

Apply the integer promotions to a value [C17:6.3.1.1/2].

Signature
(promote-value val) → promoted-val
Arguments: val — Guard (valuep val).
Returns: promoted-val — Type (valuep promoted-val).

This is the dynamic counterpart of promote-type. See the documentation of that function for details. Here we actually convert values; we do not merely compute a promoted type.

We promote the type of the value, obtaining the type of the new value. If the starting value is an integer one, in which case the promoted type is also an integer one, we convert the value to the promoted type. The other case, i.e. that the starting value is not an integer one, cannot happens under the guard, given that in our current model all the arithmetic values are integer values. But if/when we extend our model with more arithmetic values, then this code does not have to change.

This function never returns error: promotion always works. 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.

Definitions and Theorems

Theorem: promote-value-not-error-lemma

(defthm promote-value-not-error-lemma
 (implies
  (value-integerp val)
  (valuep
       (convert-integer-value val
                              (promote-type (type-of-value val))))))

Function: promote-value

(defun promote-value (val)
  (declare (xargs :guard (valuep val)))
  (declare (xargs :guard (value-arithmeticp val)))
  (let ((__function__ 'promote-value))
    (declare (ignorable __function__))
    (b* ((type (promote-type (type-of-value val))))
      (if (value-integerp val)
          (convert-integer-value val type)
        (value-fix val)))))

Theorem: valuep-of-promote-value

(defthm valuep-of-promote-value
  (b* ((promoted-val (promote-value val)))
    (valuep promoted-val))
  :rule-classes :rewrite)

Theorem: type-of-value-of-promote-value

(defthm type-of-value-of-promote-value
  (equal (type-of-value (promote-value val))
         (promote-type (type-of-value val))))

Theorem: value-arithmeticp-of-promote-value

(defthm value-arithmeticp-of-promote-value
  (equal (value-arithmeticp (promote-value val))
         (value-arithmeticp val)))

Theorem: value-promoted-arithmeticp-of-promote-value

(defthm value-promoted-arithmeticp-of-promote-value
  (equal (value-promoted-arithmeticp (promote-value val))
         (value-arithmeticp val)))

Theorem: value-integerp-of-promote-value

(defthm value-integerp-of-promote-value
  (equal (value-integerp (promote-value val))
         (value-integerp val)))

Theorem: promote-value-of-value-fix-val

(defthm promote-value-of-value-fix-val
  (equal (promote-value (value-fix val))
         (promote-value val)))

Theorem: promote-value-value-equiv-congruence-on-val

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