		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Struct-member-lookup

Look up a member in a structure type in the tag environment.

Signature
(struct-member-lookup tag mem tagenv) → type
Arguments: tag — Guard (identp tag).; mem — Guard (identp mem).; tagenv — Guard (tag-envp tagenv).
Returns: type — Type (type-resultp type).

We first look up the tag, ensuring we find a structure type. Then we look for the member in the structure type, returning its type if successful. We propagate errors.

This is used to check member expressions, both the . kind and the -> kind.

Definitions and Theorems

Function: struct-member-lookup

(defun struct-member-lookup (tag mem tagenv)
  (declare (xargs :guard (and (identp tag)
                              (identp mem)
                              (tag-envp tagenv))))
  (let ((__function__ 'struct-member-lookup))
    (declare (ignorable __function__))
    (b* ((info (tag-env-lookup tag tagenv))
         ((when (tag-info-option-case info :none))
          (reserrf (list :struct-not-found (ident-fix tag)
                         (tag-env-fix tagenv))))
         (info (tag-info-option-some->val info))
         ((unless (tag-info-case info :struct))
          (reserrf (list :tag-not-struct (ident-fix tag)
                         info)))
         (members (tag-info-struct->members info))
         (type (member-type-lookup mem members))
         ((when (type-option-case type :none))
          (reserrf (list :member-not-found (ident-fix tag)
                         (ident-fix mem)
                         members))))
      (type-option-some->val type))))

Theorem: type-resultp-of-struct-member-lookup

(defthm type-resultp-of-struct-member-lookup
  (b* ((type (struct-member-lookup tag mem tagenv)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: struct-member-lookup-of-ident-fix-tag

(defthm struct-member-lookup-of-ident-fix-tag
  (equal (struct-member-lookup (ident-fix tag)
                               mem tagenv)
         (struct-member-lookup tag mem tagenv)))

Theorem: struct-member-lookup-ident-equiv-congruence-on-tag

(defthm struct-member-lookup-ident-equiv-congruence-on-tag
  (implies (ident-equiv tag tag-equiv)
           (equal (struct-member-lookup tag mem tagenv)
                  (struct-member-lookup tag-equiv mem tagenv)))
  :rule-classes :congruence)

Theorem: struct-member-lookup-of-ident-fix-mem

(defthm struct-member-lookup-of-ident-fix-mem
  (equal (struct-member-lookup tag (ident-fix mem)
                               tagenv)
         (struct-member-lookup tag mem tagenv)))

Theorem: struct-member-lookup-ident-equiv-congruence-on-mem

(defthm struct-member-lookup-ident-equiv-congruence-on-mem
  (implies (ident-equiv mem mem-equiv)
           (equal (struct-member-lookup tag mem tagenv)
                  (struct-member-lookup tag mem-equiv tagenv)))
  :rule-classes :congruence)

Theorem: struct-member-lookup-of-tag-env-fix-tagenv

(defthm struct-member-lookup-of-tag-env-fix-tagenv
  (equal (struct-member-lookup tag mem (tag-env-fix tagenv))
         (struct-member-lookup tag mem tagenv)))

Theorem: struct-member-lookup-tag-env-equiv-congruence-on-tagenv

(defthm struct-member-lookup-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (struct-member-lookup tag mem tagenv)
                  (struct-member-lookup tag mem tagenv-equiv)))
  :rule-classes :congruence)