		Search-engine friendly clone of the ACL2 documentation.

Struct-operations

Op-struct-read

Leo struct reading operation.

Signature
(op-struct-read circval comp) → result
Arguments: circval — Guard (valuep circval).; comp — Guard (identifierp comp).
Returns: result — Type (value-resultp result).

The value must be a struct value, otherwise it is an error. The struct value must have a component with the given name, otherwise it is an error.

Definitions and Theorems

Function: op-struct-read

(defun op-struct-read (circval comp)
 (declare (xargs :guard (and (valuep circval)
                             (identifierp comp))))
 (let ((__function__ 'op-struct-read))
   (declare (ignorable __function__))
   (b*
     (((unless (value-case circval :struct))
       (reserrf (list :not-struct-value (value-fix circval))))
      (valmap (value-struct->components circval))
      (name+val (omap::assoc (identifier-fix comp)
                             valmap))
      ((unless (consp name+val))
       (reserrf (list :component-not-found (identifier-fix comp)))))
     (cdr name+val))))

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

(defthm value-resultp-of-op-struct-read
  (b* ((result (op-struct-read circval comp)))
    (value-resultp result))
  :rule-classes :rewrite)

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

(defthm op-struct-read-of-value-fix-circval
  (equal (op-struct-read (value-fix circval)
                         comp)
         (op-struct-read circval comp)))

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

(defthm op-struct-read-value-equiv-congruence-on-circval
  (implies (value-equiv circval circval-equiv)
           (equal (op-struct-read circval comp)
                  (op-struct-read circval-equiv comp)))
  :rule-classes :congruence)

Theorem: op-struct-read-of-identifier-fix-comp

(defthm op-struct-read-of-identifier-fix-comp
  (equal (op-struct-read circval (identifier-fix comp))
         (op-struct-read circval comp)))

Theorem: op-struct-read-identifier-equiv-congruence-on-comp

(defthm op-struct-read-identifier-equiv-congruence-on-comp
  (implies (identifier-equiv comp comp-equiv)
           (equal (op-struct-read circval comp)
                  (op-struct-read circval comp-equiv)))
  :rule-classes :congruence)