		Search-engine friendly clone of the ACL2 documentation.

Flexible-array-member-removal

Remove-flexible-array-member

Remove the flexible array member, if the value is a structure and has such a member.

Signature
(remove-flexible-array-member val) → new-val
Arguments: val — Guard (valuep val).
Returns: new-val — Type (valuep new-val).

Our model of structure values includes a flag indicating whether a structure has a flexible array member or not, which we consult to determine whether the last member should be removed (in fact, the flag is part of the model of structure values exactly to support this operation in a simple and clear way). Besides removing the member, we clear the flag, because the structure no longer has the flexible array member. It should be an invariant that, if the flag is set, the structure has at least two members: thus, removing a flexible array member never fails, and results in a new structure value that still has at least one member, as required by the invariant captured in values. However, our current model of values does not capture the previously mentioned variant, i.e. that if the flag is set there are at least two members. Thus, this ACL2 function may receive an input structure value with the flag set and with just one member; in order to avoid returning errors and maintain the other invariant, in this case we just clear the flag without removing members. This should never happen, and we plan to add this other invariant to values, and to remove this special case from this ACL2 function.

Definitions and Theorems

Function: remove-flexible-array-member

(defun remove-flexible-array-member (val)
  (declare (xargs :guard (valuep val)))
  (let ((__function__ 'remove-flexible-array-member))
    (declare (ignorable __function__))
    (if (flexible-array-member-p val)
        (b* ((members (value-struct->members val))
             ((unless (consp (cdr members)))
              (change-value-struct val
                                   :flexiblep nil))
             (new-members (butlast members 1)))
          (change-value-struct val
                               :members new-members
                               :flexiblep nil))
      (value-fix val))))

Theorem: valuep-of-remove-flexible-array-member

(defthm valuep-of-remove-flexible-array-member
  (b* ((new-val (remove-flexible-array-member val)))
    (valuep new-val))
  :rule-classes :rewrite)

Theorem: remove-flexible-array-member-when-absent

(defthm remove-flexible-array-member-when-absent
  (implies (not (flexible-array-member-p val))
           (equal (remove-flexible-array-member val)
                  (value-fix val))))

Theorem: type-of-value-of-remove-flexible-array-member

(defthm type-of-value-of-remove-flexible-array-member
  (equal (type-of-value (remove-flexible-array-member val))
         (type-of-value val)))

Theorem: remove-flexible-array-member-of-value-fix-val

(defthm remove-flexible-array-member-of-value-fix-val
  (equal (remove-flexible-array-member (value-fix val))
         (remove-flexible-array-member val)))

Theorem: remove-flexible-array-member-value-equiv-congruence-on-val

(defthm remove-flexible-array-member-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (remove-flexible-array-member val)
                  (remove-flexible-array-member val-equiv)))
  :rule-classes :congruence)