		Search-engine friendly clone of the ACL2 documentation.

Structure-operations

Value-struct-read

Read a member of a structure.

Signature
(value-struct-read name struct) → val
Arguments: name — Guard (identp name).; struct — Guard (valuep struct).
Returns: val — Type (value-resultp val).

We look up the members in order; given that the members have distinct names (see value), the search order is immaterial.

Definitions and Theorems

Function: value-struct-read-aux

(defun value-struct-read-aux (name members)
  (declare (xargs :guard (and (identp name)
                              (member-value-listp members))))
  (let ((__function__ 'value-struct-read-aux))
    (declare (ignorable __function__))
    (b* (((when (endp members))
          (error (list :member-not-found (ident-fix name))))
         ((member-value member) (car members))
         ((when (equal member.name (ident-fix name)))
          member.value))
      (value-struct-read-aux name (cdr members)))))

Theorem: value-resultp-of-value-struct-read-aux

(defthm value-resultp-of-value-struct-read-aux
  (b* ((val (value-struct-read-aux name members)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: value-struct-read-aux-when-member-type-lookup

(defthm value-struct-read-aux-when-member-type-lookup
  (implies (equal memtypes
                  (member-types-of-member-values memvals))
           (b* ((type (member-type-lookup name memtypes))
                (val (value-struct-read-aux name memvals)))
             (implies (typep type)
                      (and (valuep val)
                           (equal (type-of-value val) type))))))

Theorem: value-struct-read-aux-of-ident-fix-name

(defthm value-struct-read-aux-of-ident-fix-name
  (equal (value-struct-read-aux (ident-fix name)
                                members)
         (value-struct-read-aux name members)))

Theorem: value-struct-read-aux-ident-equiv-congruence-on-name

(defthm value-struct-read-aux-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (value-struct-read-aux name members)
                  (value-struct-read-aux name-equiv members)))
  :rule-classes :congruence)

Theorem: value-struct-read-aux-of-member-value-list-fix-members

(defthm value-struct-read-aux-of-member-value-list-fix-members
 (equal (value-struct-read-aux name (member-value-list-fix members))
        (value-struct-read-aux name members)))

Theorem: value-struct-read-aux-member-value-list-equiv-congruence-on-members

(defthm
 value-struct-read-aux-member-value-list-equiv-congruence-on-members
 (implies (member-value-list-equiv members members-equiv)
          (equal (value-struct-read-aux name members)
                 (value-struct-read-aux name members-equiv)))
 :rule-classes :congruence)

Function: value-struct-read

(defun value-struct-read (name struct)
  (declare (xargs :guard (and (identp name) (valuep struct))))
  (declare (xargs :guard (value-case struct :struct)))
  (let ((__function__ 'value-struct-read))
    (declare (ignorable __function__))
    (value-struct-read-aux name (value-struct->members struct))))

Theorem: value-resultp-of-value-struct-read

(defthm value-resultp-of-value-struct-read
  (b* ((val (value-struct-read name struct)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: value-struct-read-of-ident-fix-name

(defthm value-struct-read-of-ident-fix-name
  (equal (value-struct-read (ident-fix name)
                            struct)
         (value-struct-read name struct)))

Theorem: value-struct-read-ident-equiv-congruence-on-name

(defthm value-struct-read-ident-equiv-congruence-on-name
  (implies (ident-equiv name name-equiv)
           (equal (value-struct-read name struct)
                  (value-struct-read name-equiv struct)))
  :rule-classes :congruence)

Theorem: value-struct-read-of-value-fix-struct

(defthm value-struct-read-of-value-fix-struct
  (equal (value-struct-read name (value-fix struct))
         (value-struct-read name struct)))

Theorem: value-struct-read-value-equiv-congruence-on-struct

(defthm value-struct-read-value-equiv-congruence-on-struct
  (implies (value-equiv struct struct-equiv)
           (equal (value-struct-read name struct)
                  (value-struct-read name struct-equiv)))
  :rule-classes :congruence)