		Search-engine friendly clone of the ACL2 documentation.

Values

Type-of-value

Type of a value.

Signature
(type-of-value val) → type
Arguments: val — Guard (valuep val).
Returns: type — Type (typep type).

This is straightforward, as values carry type information. For an array value, we always return an array type with a size, which is the length of the array, which is always positive.

Definitions and Theorems

Function: type-of-value

(defun type-of-value (val)
  (declare (xargs :guard (valuep val)))
  (let ((__function__ 'type-of-value))
    (declare (ignorable __function__))
    (value-case val
                :uchar (type-uchar)
                :schar (type-schar)
                :ushort (type-ushort)
                :sshort (type-sshort)
                :uint (type-uint)
                :sint (type-sint)
                :ulong (type-ulong)
                :slong (type-slong)
                :ullong (type-ullong)
                :sllong (type-sllong)
                :pointer (type-pointer val.reftype)
                :array (make-type-array :of val.elemtype
                                        :size (len val.elements))
                :struct (type-struct val.tag))))

Theorem: typep-of-type-of-value

(defthm typep-of-type-of-value
  (b* ((type (type-of-value val)))
    (typep type))
  :rule-classes :rewrite)

Theorem: type-kind-of-type-of-value

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

Theorem: type-signed-integerp-of-type-of-value

(defthm type-signed-integerp-of-type-of-value
  (equal (type-signed-integerp (type-of-value val))
         (value-signed-integerp val)))

Theorem: type-unsigned-integerp-of-type-of-value

(defthm type-unsigned-integerp-of-type-of-value
  (equal (type-unsigned-integerp (type-of-value val))
         (value-unsigned-integerp val)))

Theorem: type-integerp-of-type-of-value

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

Theorem: type-realp-of-type-of-value

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

Theorem: type-arithmeticp-of-type-of-value

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

Theorem: type-scalarp-of-type-of-value

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

Theorem: type-promoted-arithmeticp-of-type-of-value

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

Theorem: type-nonchar-integerp-of-type-of-value

(defthm type-nonchar-integerp-of-type-of-value
  (equal (type-nonchar-integerp (type-of-value val))
         (value-integerp val)))

Theorem: type-of-value-of-value-fix-val

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

Theorem: type-of-value-value-equiv-congruence-on-val

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