		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-member

Check a structure member expression [C:6.5.2.3].

Signature
(check-member target-expr target-etype name tagenv) → etype
Arguments: target-expr — Guard (exprp target-expr).; target-etype — Guard (expr-typep target-etype).; name — Guard (identp name).; tagenv — Guard (tag-envp tagenv).
Returns: etype — Type (expr-type-resultp etype).

We ensure that the target has a structure type. We do not do need to do array-to-pointer conversion, because we require the type to be a structure type, which rejects both array and pointer types. We look up the structure type and its member. We return its type, and we preserve the lvalue status: if the target is an lvalue, so is the member; if the target is not an lvalue, neither is the member.

Definitions and Theorems

Function: check-member

(defun check-member (target-expr target-etype name tagenv)
 (declare (xargs :guard (and (exprp target-expr)
                             (expr-typep target-etype)
                             (identp name)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-member))
  (declare (ignorable __function__))
  (b*
   ((target-type (expr-type->type target-etype))
    (target-lvalue (expr-type->lvalue target-etype))
    ((unless (type-case target-type :struct))
     (reserrf (list :dot-target-not-struct (expr-fix target-expr))))
    (tag (type-struct->tag target-type))
    ((okf memtype)
     (struct-member-lookup tag name tagenv)))
   (make-expr-type :type memtype
                   :lvalue target-lvalue))))

Theorem: expr-type-resultp-of-check-member

(defthm expr-type-resultp-of-check-member
  (b* ((etype (check-member target-expr target-etype name tagenv)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-member-of-expr-fix-target-expr

(defthm check-member-of-expr-fix-target-expr
  (equal (check-member (expr-fix target-expr)
                       target-etype name tagenv)
         (check-member target-expr target-etype name tagenv)))

Theorem: check-member-expr-equiv-congruence-on-target-expr

(defthm check-member-expr-equiv-congruence-on-target-expr
 (implies (expr-equiv target-expr target-expr-equiv)
          (equal (check-member target-expr target-etype name tagenv)
                 (check-member target-expr-equiv
                               target-etype name tagenv)))
 :rule-classes :congruence)

Theorem: check-member-of-expr-type-fix-target-etype

(defthm check-member-of-expr-type-fix-target-etype
  (equal (check-member target-expr (expr-type-fix target-etype)
                       name tagenv)
         (check-member target-expr target-etype name tagenv)))

Theorem: check-member-expr-type-equiv-congruence-on-target-etype

(defthm check-member-expr-type-equiv-congruence-on-target-etype
 (implies (expr-type-equiv target-etype target-etype-equiv)
          (equal (check-member target-expr target-etype name tagenv)
                 (check-member target-expr
                               target-etype-equiv name tagenv)))
 :rule-classes :congruence)

Theorem: check-member-of-ident-fix-name

(defthm check-member-of-ident-fix-name
  (equal (check-member target-expr
                       target-etype (ident-fix name)
                       tagenv)
         (check-member target-expr target-etype name tagenv)))

Theorem: check-member-ident-equiv-congruence-on-name

(defthm check-member-ident-equiv-congruence-on-name
 (implies (ident-equiv name name-equiv)
          (equal (check-member target-expr target-etype name tagenv)
                 (check-member target-expr
                               target-etype name-equiv tagenv)))
 :rule-classes :congruence)

Theorem: check-member-of-tag-env-fix-tagenv

(defthm check-member-of-tag-env-fix-tagenv
  (equal (check-member target-expr
                       target-etype name (tag-env-fix tagenv))
         (check-member target-expr target-etype name tagenv)))

Theorem: check-member-tag-env-equiv-congruence-on-tagenv

(defthm check-member-tag-env-equiv-congruence-on-tagenv
 (implies (tag-env-equiv tagenv tagenv-equiv)
          (equal (check-member target-expr target-etype name tagenv)
                 (check-member target-expr
                               target-etype name tagenv-equiv)))
 :rule-classes :congruence)