		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Value-integer

Turn a mathematical (i.e. ACL2) integer into a C integer value.

Signature
(value-integer mathint type) → val
Arguments: mathint — Guard (integerp mathint).; type — Guard (typep type).
Returns: val — Type (valuep val).

The type of the C integer value is passed as parameter to this function.

We exclude the plain char type for now, because our model of values does not yet include plain char.

We require, in the guard, the integer to be representable in the range of the integer type.

Definitions and Theorems

Function: value-integer

(defun value-integer (mathint type)
  (declare (xargs :guard (and (integerp mathint) (typep type))))
  (declare (xargs :guard (and (type-nonchar-integerp type)
                              (integer-type-rangep mathint type))))
  (let ((__function__ 'value-integer))
    (declare (ignorable __function__))
    (b* ((mathint (ifix mathint)))
      (case (type-kind type)
        (:uchar (value-uchar mathint))
        (:schar (value-schar mathint))
        (:ushort (value-ushort mathint))
        (:sshort (value-sshort mathint))
        (:uint (value-uint mathint))
        (:sint (value-sint mathint))
        (:ulong (value-ulong mathint))
        (:slong (value-slong mathint))
        (:ullong (value-ullong mathint))
        (:sllong (value-sllong mathint))
        (t (value-fix (impossible)))))))

Theorem: valuep-of-value-integer

(defthm valuep-of-value-integer
  (b* ((val (value-integer mathint type)))
    (valuep val))
  :rule-classes :rewrite)

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

(defthm type-of-value-of-value-integer
  (implies (type-nonchar-integerp type)
           (equal (type-of-value (value-integer mathint type))
                  (type-fix type))))

Theorem: value-kind-of-value-integer

(defthm value-kind-of-value-integer
  (implies (type-nonchar-integerp type)
           (equal (value-kind (value-integer mathint type))
                  (type-kind type))))

Theorem: value-integerp-of-value-integer

(defthm value-integerp-of-value-integer
  (implies (type-nonchar-integerp type)
           (value-integerp (value-integer mathint type))))

Theorem: value-integer-of-ifix-mathint

(defthm value-integer-of-ifix-mathint
  (equal (value-integer (ifix mathint) type)
         (value-integer mathint type)))

Theorem: value-integer-int-equiv-congruence-on-mathint

(defthm value-integer-int-equiv-congruence-on-mathint
  (implies (acl2::int-equiv mathint mathint-equiv)
           (equal (value-integer mathint type)
                  (value-integer mathint-equiv type)))
  :rule-classes :congruence)

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

(defthm value-integer-of-type-fix-type
  (equal (value-integer mathint (type-fix type))
         (value-integer mathint type)))

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

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