		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Convert-integer-value

Convert an integer value to an integer type [C:6.3.1.3].

Signature
(convert-integer-value val type) → newval
Arguments: val — Guard (valuep val).; type — Guard (typep type).
Returns: newval — Type (value-resultp newval).

We extract the underlying mathematical (i.e. ACL2) integer from the value, and we attempt to contruct an integer value of the new type from it. If the new type is unsigned, the mathematical integer is reduced modulo one plus the maximum value of the unsigned type [C:6.3.1.3/2]; this always works, i.e. no error is ever returned. If the new type is signed, there are two cases [C:6.3.1.3/3]: if the mathematical integer fits in the type, we return a value of that type with that integer; otherwise, we return an error.

We do not yet support conversions to the plain char type; this restriction is expressed by the guard. However, we prefer to keep the name of this function more general, in anticipation for extending it to those two types.

We prove a theorem showing that converting a value to its type is a no-op, i.e. it leaves the value unchanged.

We prove a theorem saying that conversions to unsigned types never yields errors.

We also prove two theorems saying that converting signed chars and signed shorts to signed ints never yields errors, as well as two theorems saying that converting unsigned chars and unsigned shorts to signed ints, provided the range of the latter includes the ranges of the former, never yields errors.

These last four theorems are relevant to the use of integer conversions in promote-value, to show that that function never yields errors; however, they are more general theorems about integer conversions. Also the first two theorems mentioned above are in fact relevant to showing that promote-value yields no error, but they are clearly more general in nature.

Definitions and Theorems

Function: convert-integer-value

(defun convert-integer-value (val type)
 (declare (xargs :guard (and (valuep val) (typep type))))
 (declare (xargs :guard (and (value-integerp val)
                             (type-nonchar-integerp type))))
 (let ((__function__ 'convert-integer-value))
  (declare (ignorable __function__))
  (b* ((mathint (value-integer->get val)))
    (cond ((type-unsigned-integerp type)
           (value-integer (mod mathint (1+ (integer-type-max type)))
                          type))
          ((integer-type-rangep mathint type)
           (value-integer mathint type))
          (t (error (list :out-of-range (value-fix val)
                          (type-fix type))))))))

Theorem: value-resultp-of-convert-integer-value

(defthm value-resultp-of-convert-integer-value
  (b* ((newval (convert-integer-value val type)))
    (value-resultp newval))
  :rule-classes :rewrite)

Theorem: type-of-value-of-convert-integer-value

(defthm type-of-value-of-convert-integer-value
  (implies (type-nonchar-integerp type)
           (b* ((?newval (convert-integer-value val type)))
             (implies (not (errorp newval))
                      (equal (type-of-value newval)
                             (type-fix type))))))

Theorem: value-kind-of-convert-integer-value

(defthm value-kind-of-convert-integer-value
  (b* ((?newval (convert-integer-value val type)))
    (implies (and (not (errorp newval))
                  (type-nonchar-integerp type))
             (equal (value-kind newval)
                    (type-kind type)))))

Theorem: value-integerp-of-convert-integer-value

(defthm value-integerp-of-convert-integer-value
  (implies (type-nonchar-integerp type)
           (b* ((?newval (convert-integer-value val type)))
             (implies (not (errorp newval))
                      (value-integerp newval)))))

Theorem: convert-integer-value-to-type-of-value

(defthm convert-integer-value-to-type-of-value
  (implies (and (value-integerp val)
                (equal type (type-of-value val)))
           (equal (convert-integer-value val type)
                  (value-fix val))))

Theorem: valuep-of-convert-integer-value-to-unsigned

(defthm valuep-of-convert-integer-value-to-unsigned
  (implies (type-unsigned-integerp type)
           (valuep (convert-integer-value val type))))

Theorem: valuep-of-convert-integer-value-from-schar-to-sint

(defthm valuep-of-convert-integer-value-from-schar-to-sint
  (implies (value-case val :schar)
           (valuep (convert-integer-value val (type-sint)))))

Theorem: valuep-of-convert-integer-value-from-schar-to-slong

(defthm valuep-of-convert-integer-value-from-schar-to-slong
  (implies (value-case val :schar)
           (valuep (convert-integer-value val (type-slong)))))

Theorem: valuep-of-convert-integer-value-from-schar-to-sllong

(defthm valuep-of-convert-integer-value-from-schar-to-sllong
  (implies (value-case val :schar)
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-sshort-to-sint

(defthm valuep-of-convert-integer-value-from-sshort-to-sint
  (implies (value-case val :sshort)
           (valuep (convert-integer-value val (type-sint)))))

Theorem: valuep-of-convert-integer-value-from-sshort-to-slong

(defthm valuep-of-convert-integer-value-from-sshort-to-slong
  (implies (value-case val :sshort)
           (valuep (convert-integer-value val (type-slong)))))

Theorem: valuep-of-convert-integer-value-from-sshort-to-sllong

(defthm valuep-of-convert-integer-value-from-sshort-to-sllong
  (implies (value-case val :sshort)
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-sint-to-slong

(defthm valuep-of-convert-integer-value-from-sint-to-slong
  (implies (value-case val :sint)
           (valuep (convert-integer-value val (type-slong)))))

Theorem: valuep-of-convert-integer-value-from-sint-to-sllong

(defthm valuep-of-convert-integer-value-from-sint-to-sllong
  (implies (value-case val :sint)
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-slong-to-sllong

(defthm valuep-of-convert-integer-value-from-slong-to-sllong
  (implies (value-case val :slong)
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-uchar-to-sint

(defthm valuep-of-convert-integer-value-from-uchar-to-sint
  (implies (and (value-case val :uchar)
                (<= (uchar-max) (sint-max)))
           (valuep (convert-integer-value val (type-sint)))))

Theorem: valuep-of-convert-integer-value-from-uchar-to-slong

(defthm valuep-of-convert-integer-value-from-uchar-to-slong
  (implies (and (value-case val :uchar)
                (<= (uchar-max) (slong-max)))
           (valuep (convert-integer-value val (type-slong)))))

Theorem: valuep-of-convert-integer-value-from-uchar-to-sllong

(defthm valuep-of-convert-integer-value-from-uchar-to-sllong
  (implies (and (value-case val :uchar)
                (<= (uchar-max) (sllong-max)))
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-ushort-to-sint

(defthm valuep-of-convert-integer-value-from-ushort-to-sint
  (implies (and (value-case val :ushort)
                (<= (ushort-max) (sint-max)))
           (valuep (convert-integer-value val (type-sint)))))

Theorem: valuep-of-convert-integer-value-from-ushort-to-slong

(defthm valuep-of-convert-integer-value-from-ushort-to-slong
  (implies (and (value-case val :ushort)
                (<= (ushort-max) (slong-max)))
           (valuep (convert-integer-value val (type-slong)))))

Theorem: valuep-of-convert-integer-value-from-ushort-to-sllong

(defthm valuep-of-convert-integer-value-from-ushort-to-sllong
  (implies (and (value-case val :ushort)
                (<= (ushort-max) (sllong-max)))
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-uint-to-slong

(defthm valuep-of-convert-integer-value-from-uint-to-slong
  (implies (and (value-case val :uint)
                (<= (uint-max) (slong-max)))
           (valuep (convert-integer-value val (type-slong)))))

Theorem: valuep-of-convert-integer-value-from-uint-to-sllong

(defthm valuep-of-convert-integer-value-from-uint-to-sllong
  (implies (and (value-case val :uint)
                (<= (uint-max) (sllong-max)))
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: valuep-of-convert-integer-value-from-ulong-to-sllong

(defthm valuep-of-convert-integer-value-from-ulong-to-sllong
  (implies (and (value-case val :ulong)
                (<= (ulong-max) (sllong-max)))
           (valuep (convert-integer-value val (type-sllong)))))

Theorem: convert-integer-value-of-value-fix-val

(defthm convert-integer-value-of-value-fix-val
  (equal (convert-integer-value (value-fix val)
                                type)
         (convert-integer-value val type)))

Theorem: convert-integer-value-value-equiv-congruence-on-val

(defthm convert-integer-value-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (convert-integer-value val type)
                  (convert-integer-value val-equiv type)))
  :rule-classes :congruence)

Theorem: convert-integer-value-of-type-fix-type

(defthm convert-integer-value-of-type-fix-type
  (equal (convert-integer-value val (type-fix type))
         (convert-integer-value val type)))

Theorem: convert-integer-value-type-equiv-congruence-on-type

(defthm convert-integer-value-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (convert-integer-value val type)
                  (convert-integer-value val type-equiv)))
  :rule-classes :congruence)