		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Eval-cast

Evaluate a type cast on a value.

Signature
(eval-cast tyname arg) → val
Arguments: tyname — Guard (tynamep tyname).; arg — Guard (valuep arg).
Returns: val — Type (value-resultp val).

For now we only support casts between integer types. None involving pointers.

We reject casts to void, because a scalar type is required [C17:6.5.4/2].

Definitions and Theorems

Function: eval-cast

(defun eval-cast (tyname arg)
  (declare (xargs :guard (and (tynamep tyname) (valuep arg))))
  (let ((__function__ 'eval-cast))
    (declare (ignorable __function__))
    (b* ((type (tyname-to-type tyname))
         ((unless (type-nonchar-integerp type))
          (error (list :cast-not-supported :to type)))
         ((unless (value-integerp arg))
          (error (list :cast-not-supported
                       :from (value-fix arg))))
         (err (error (list :cast-undefined
                           :from (value-fix arg)
                           :to type)))
         (val (convert-integer-value arg type))
         ((when (errorp val)) err))
      val)))

Theorem: value-resultp-of-eval-cast

(defthm value-resultp-of-eval-cast
  (b* ((val (eval-cast tyname arg)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-cast-of-tyname-fix-tyname

(defthm eval-cast-of-tyname-fix-tyname
  (equal (eval-cast (tyname-fix tyname) arg)
         (eval-cast tyname arg)))

Theorem: eval-cast-tyname-equiv-congruence-on-tyname

(defthm eval-cast-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (eval-cast tyname arg)
                  (eval-cast tyname-equiv arg)))
  :rule-classes :congruence)

Theorem: eval-cast-of-value-fix-arg

(defthm eval-cast-of-value-fix-arg
  (equal (eval-cast tyname (value-fix arg))
         (eval-cast tyname arg)))

Theorem: eval-cast-value-equiv-congruence-on-arg

(defthm eval-cast-value-equiv-congruence-on-arg
  (implies (value-equiv arg arg-equiv)
           (equal (eval-cast tyname arg)
                  (eval-cast tyname arg-equiv)))
  :rule-classes :congruence)