		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-member

Validate a member expression, given the type of the sub-expression.

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

The argument type must be a structure or union type [C:6.5.2.3/1]. Since a pointer type is not allowed here, there is no need to convert arrays or functions to pointers.

For now we only have one type for structures and one type for unions. We cannot look up the member type, so we return the unknown type.

Definitions and Theorems

Function: valid-member

(defun valid-member (expr type-arg)
 (declare (xargs :guard (and (exprp expr) (typep type-arg))))
 (declare (xargs :guard (expr-case expr :member)))
 (let ((__function__ 'valid-member))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((when (type-case type-arg :unknown))
     (retok (type-unknown)))
    ((unless (or (type-case type-arg :struct)
                 (type-case type-arg :union)))
     (reterr
      (msg
       "In the member expression ~x0, ~
                      the sub-expression has type ~x1."
       (expr-fix expr)
       (type-fix type-arg)))))
   (retok (type-unknown)))))

Theorem: typep-of-valid-member.type

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

Theorem: valid-member-of-expr-fix-expr

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

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

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

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

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

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

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