Process an
(isodata-process-arg/res-list-iso arg/res-list-iso k old$ verify-guards$ arg-isomaps res-isomaps names-to-avoid ctx state) → (mv erp result state)
The
Function:
(defun isodata-process-arg/res-list-iso-add-args (args isomap arg-isomaps) (declare (xargs :guard (and (symbol-listp args) (isodata-isomapp isomap) (isodata-symbol-isomap-alistp arg-isomaps)))) (let ((__function__ 'isodata-process-arg/res-list-iso-add-args)) (declare (ignorable __function__)) (cond ((endp args) arg-isomaps) (t (isodata-process-arg/res-list-iso-add-args (cdr args) isomap (acons (car args) isomap arg-isomaps))))))
Theorem:
(defthm isodata-symbol-isomap-alistp-of-isodata-process-arg/res-list-iso-add-args (implies (and (symbol-listp args) (isodata-isomapp isomap) (isodata-symbol-isomap-alistp arg-isomaps)) (b* ((new-arg-isomaps (isodata-process-arg/res-list-iso-add-args args isomap arg-isomaps))) (isodata-symbol-isomap-alistp new-arg-isomaps))) :rule-classes :rewrite)
Function:
(defun isodata-process-arg/res-list-iso-add-ress (ress isomap res-isomaps) (declare (xargs :guard (and (pos-listp ress) (isodata-isomapp isomap) (isodata-pos-isomap-alistp res-isomaps)))) (let ((__function__ 'isodata-process-arg/res-list-iso-add-ress)) (declare (ignorable __function__)) (cond ((endp ress) res-isomaps) (t (isodata-process-arg/res-list-iso-add-ress (cdr ress) isomap (acons (car ress) isomap res-isomaps))))))
Theorem:
(defthm isodata-pos-isomap-alistp-of-isodata-process-arg/res-list-iso-add-ress (implies (and (pos-listp ress) (isodata-isomapp isomap) (isodata-pos-isomap-alistp res-isomaps)) (b* ((new-res-isomaps (isodata-process-arg/res-list-iso-add-ress ress isomap res-isomaps))) (isodata-pos-isomap-alistp new-res-isomaps))) :rule-classes :rewrite)
Function:
(defun isodata-process-arg/res-list-iso (arg/res-list-iso k old$ verify-guards$ arg-isomaps res-isomaps names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (posp k) (symbolp old$) (booleanp verify-guards$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbol-listp names-to-avoid)))) (let ((__function__ 'isodata-process-arg/res-list-iso)) (declare (ignorable __function__)) (b* (((er &) (ensure-tuple$ arg/res-list-iso 2 (msg "The ~n0 component of the second input" (list k)) t nil)) (arg/res-list (first arg/res-list-iso)) (iso (second arg/res-list-iso)) ((er (list args ress)) (isodata-process-arg/res-list arg/res-list k old$ ctx state)) (arg-overlap (intersection-eq args (strip-cars arg-isomaps))) ((when arg-overlap) (er-soft+ ctx t nil "The ~n0 component of the second input includes ~&1, ~ which are also present in the preceding components. ~ This violates the disjointness requirement." (list k) arg-overlap)) (res-overlap (intersection$ ress (strip-cars res-isomaps))) ((when res-overlap) (er-soft+ ctx t nil "The ~n0 component of the second input includes ~ the ~s1 ~&2, ~ which ~s3 also present in the preceding components. ~ This violates the disjointness requirement." (list k) (if (= (len res-overlap) 1) "result with index" "results with indices") res-overlap (if (= (len res-overlap) 1) "is" "are"))) ((er (list isomap names-to-avoid)) (isodata-process-iso iso k old$ verify-guards$ names-to-avoid ctx state)) (arg-isomaps (isodata-process-arg/res-list-iso-add-args args isomap arg-isomaps)) (res-isomaps (isodata-process-arg/res-list-iso-add-ress ress isomap res-isomaps))) (value (list arg-isomaps res-isomaps names-to-avoid)))))