		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-cast

Validate a cast expression, given the type denoted by the type name and the type of the argument expression.

Signature
(valid-cast expr type-cast type-arg) → (mv erp type1)
Arguments: expr — Guard (exprp expr).; type-cast — Guard (typep type-cast).; type-arg — Guard (typep type-arg).
Returns: type1 — Type (typep type1).

The type name must denote the void type or a scalar type [C:6.5.4/2]. The expression must have scalar type [C:6.5.4/2]. Since scalar types involve pointers, we perform array-to-pointer and function-to-pointer conversions. The result is the type denoted by the type name.

Definitions and Theorems

Function: valid-cast

(defun valid-cast (expr type-cast type-arg)
 (declare (xargs :guard (and (exprp expr)
                             (typep type-cast)
                             (typep type-arg))))
 (declare (xargs :guard (expr-case expr :cast)))
 (let ((__function__ 'valid-cast))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((when (or (type-case type-cast :unknown)
               (type-case type-arg :unknown)))
     (retok (type-unknown)))
    (type1-arg (type-fpconvert (type-apconvert type-cast)))
    ((unless (or (type-case type-cast :void)
                 (type-scalarp type-cast)))
     (reterr
      (msg
       "In the cast expression ~x0, ~
                      the cast type is ~x1."
       (expr-fix expr)
       (type-fix type-cast))))
    ((unless (type-scalarp type1-arg))
     (reterr
      (msg
       "In the cast expression ~x0, ~
                      the argument expression has type ~x1."
       (expr-fix expr)
       (type-fix type-arg)))))
   (retok (type-fix type-cast)))))

Theorem: typep-of-valid-cast.type1

(defthm typep-of-valid-cast.type1
  (b* (((mv acl2::?erp ?type1)
        (valid-cast expr type-cast type-arg)))
    (typep type1))
  :rule-classes :rewrite)

Theorem: valid-cast-of-expr-fix-expr

(defthm valid-cast-of-expr-fix-expr
  (equal (valid-cast (expr-fix expr)
                     type-cast type-arg)
         (valid-cast expr type-cast type-arg)))

Theorem: valid-cast-expr-equiv-congruence-on-expr

(defthm valid-cast-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-cast expr type-cast type-arg)
                  (valid-cast expr-equiv type-cast type-arg)))
  :rule-classes :congruence)

Theorem: valid-cast-of-type-fix-type-cast

(defthm valid-cast-of-type-fix-type-cast
  (equal (valid-cast expr (type-fix type-cast)
                     type-arg)
         (valid-cast expr type-cast type-arg)))

Theorem: valid-cast-type-equiv-congruence-on-type-cast

(defthm valid-cast-type-equiv-congruence-on-type-cast
  (implies (type-equiv type-cast type-cast-equiv)
           (equal (valid-cast expr type-cast type-arg)
                  (valid-cast expr type-cast-equiv type-arg)))
  :rule-classes :congruence)

Theorem: valid-cast-of-type-fix-type-arg

(defthm valid-cast-of-type-fix-type-arg
  (equal (valid-cast expr type-cast (type-fix type-arg))
         (valid-cast expr type-cast type-arg)))

Theorem: valid-cast-type-equiv-congruence-on-type-arg

(defthm valid-cast-type-equiv-congruence-on-type-arg
  (implies (type-equiv type-arg type-arg-equiv)
           (equal (valid-cast expr type-cast type-arg)
                  (valid-cast expr type-cast type-arg-equiv)))
  :rule-classes :congruence)