		Search-engine friendly clone of the ACL2 documentation.

Array-operations

Value-array-write

Write an element to an array.

Signature
(value-array-write index elem array) → new-array
Arguments: index — Guard (natp index).; elem — Guard (valuep elem).; array — Guard (valuep array).
Returns: new-array — Type (value-resultp new-array).

If the index is too large, it is an error.

If the type of the new element does not match the array type, it is an error.

Prior to storing the value, we remove its flexible array member, if any. See remove-flexible-array-member.

Definitions and Theorems

Function: value-array-write

(defun value-array-write (index elem array)
 (declare (xargs :guard (and (natp index)
                             (valuep elem)
                             (valuep array))))
 (declare (xargs :guard (value-case array :array)))
 (let ((__function__ 'value-array-write))
  (declare (ignorable __function__))
  (b* ((index (nfix index))
       ((unless (< index (value-array->length array)))
        (error (list :array-write-index
                     index (value-fix array))))
       ((unless (equal (type-of-value elem)
                       (value-array->elemtype array)))
        (error (list :array-write-mistype
                     :required (value-array->elemtype array)
                     :supplied (type-of-value elem))))
       (new-elements (update-nth index
                                 (remove-flexible-array-member elem)
                                 (value-array->elements array))))
    (change-value-array array
                        :elements new-elements))))

Theorem: value-resultp-of-value-array-write

(defthm value-resultp-of-value-array-write
  (b* ((new-array (value-array-write index elem array)))
    (value-resultp new-array))
  :rule-classes :rewrite)

Theorem: value-kind-of-value-array-write

(defthm value-kind-of-value-array-write
  (b* ((?new-array (value-array-write index elem array)))
    (implies (not (errorp new-array))
             (equal (value-kind new-array) :array))))

Theorem: value-array-write-of-nfix-index

(defthm value-array-write-of-nfix-index
  (equal (value-array-write (nfix index)
                            elem array)
         (value-array-write index elem array)))

Theorem: value-array-write-nat-equiv-congruence-on-index

(defthm value-array-write-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (value-array-write index elem array)
                  (value-array-write index-equiv elem array)))
  :rule-classes :congruence)

Theorem: value-array-write-of-value-fix-elem

(defthm value-array-write-of-value-fix-elem
  (equal (value-array-write index (value-fix elem)
                            array)
         (value-array-write index elem array)))

Theorem: value-array-write-value-equiv-congruence-on-elem

(defthm value-array-write-value-equiv-congruence-on-elem
  (implies (value-equiv elem elem-equiv)
           (equal (value-array-write index elem array)
                  (value-array-write index elem-equiv array)))
  :rule-classes :congruence)

Theorem: value-array-write-of-value-fix-array

(defthm value-array-write-of-value-fix-array
  (equal (value-array-write index elem (value-fix array))
         (value-array-write index elem array)))

Theorem: value-array-write-value-equiv-congruence-on-array

(defthm value-array-write-value-equiv-congruence-on-array
  (implies (value-equiv array array-equiv)
           (equal (value-array-write index elem array)
                  (value-array-write index elem array-equiv)))
  :rule-classes :congruence)