		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-memberp

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

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

The type of the sub-expression is calculated (recursively) by valid-expr.

The argument type must be a pointer to a structure or union type [C17:6.5.2.3/2]. We need to convert arrays to pointers, and then we just check that we have the (one) pointer type; we will refine this when we refine our type system. We do not conver functions to pointers, because that would result into a pointer to function, which is not a pointer to structure or union as required; thus, by leaving function types unchanged, we reject them here.

Since we cannot yet look up members in structure and union types, we return the unknown type.

Definitions and Theorems

Function: valid-memberp

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

Theorem: typep-of-valid-memberp.type

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

Theorem: valid-memberp-of-expr-fix-expr

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

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

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

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

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

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

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