		Search-engine friendly clone of the ACL2 documentation.

Struct-operations

Op-struct-write

Leo struct writing operation.

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

The first 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. Furthermore, the type of the new component value must match the one of the value stored in the component, which is overwritten.

Definitions and Theorems

Function: op-struct-write

(defun op-struct-write (circval comp val)
 (declare (xargs :guard (and (valuep circval)
                             (identifierp comp)
                             (valuep val))))
 (let ((__function__ 'op-struct-write))
  (declare (ignorable __function__))
  (b* (((unless (value-case circval :struct))
        (reserrf (list :not-struct-value (value-fix circval))))
       (valmap (value-struct->components circval))
       (name+oldval (omap::assoc (identifier-fix comp)
                                 valmap))
       ((unless (consp name+oldval))
        (reserrf (list :component-not-found (identifier-fix comp))))
       (oldval (cdr name+oldval))
       ((unless (equal (type-of-value val)
                       (type-of-value oldval)))
        (reserrf (list :component-type-mismatch
                       :name (identifier-fix comp)
                       :required (type-of-value oldval)
                       :supplied (type-of-value val))))
       (new-valmap (omap::update (identifier-fix comp)
                                 (value-fix val)
                                 valmap))
       (new-circval (change-value-struct circval
                                         :components new-valmap)))
    new-circval)))

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

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

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

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

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

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

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

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

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

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

Theorem: op-struct-write-of-value-fix-val

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

Theorem: op-struct-write-value-equiv-congruence-on-val

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