Process an
(expdata-process-arg/res-list arg/res-list k old$ ctx state) → (mv erp result state)
If the processing is successful,
the
Function:
(defun expdata-process-arg/res-list-aux (arg/res-list x1...xn m err-msg-preamble ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbol-listp arg/res-list) (symbol-listp x1...xn) (posp m) (msgp err-msg-preamble)))) (let ((__function__ 'expdata-process-arg/res-list-aux)) (declare (ignorable __function__)) (b* (((when (endp arg/res-list)) (value (list nil nil))) (arg/res (car arg/res-list)) ((when (member-eq arg/res x1...xn)) (b* (((er (list args ress)) (expdata-process-arg/res-list-aux (cdr arg/res-list) x1...xn m err-msg-preamble ctx state))) (value (list (cons arg/res args) ress)))) ((er j) (expdata-process-res arg/res m err-msg-preamble ctx state)) ((er (list args ress)) (expdata-process-arg/res-list-aux (cdr arg/res-list) x1...xn m err-msg-preamble ctx state))) (value (list args (cons j ress))))))
Function:
(defun expdata-process-arg/res-list (arg/res-list k old$ ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (posp k) (symbolp old$)))) (let ((__function__ 'expdata-process-arg/res-list)) (declare (ignorable __function__)) (b* ((wrld (w state)) (x1...xn (formals old$ wrld)) (m (number-of-results old$ wrld)) (err-msg-part (if (= m 1) (msg "must be either a formal argument of ~x0, ~ or the keyword @(':RESULT'), or the keyword @(':RESULT1')." old$) (msg "must be either a formal argument of ~x0, ~ or a keyword :RESULTj where j is ~ a positive integer not exceeding ~ the number of results ~x1 of ~x0." old$ m)))) (if (atom arg/res-list) (if (member-eq arg/res-list x1...xn) (value (list (list arg/res-list) nil)) (b* ((err-msg-preamble (msg "Since the ~n0 ARG/RES-LIST component ~ of the second input ~ is not a list, it ~@1" (list k) err-msg-part)) ((er j) (expdata-process-res arg/res-list m err-msg-preamble ctx state))) (value (list nil (list j))))) (b* (((er &) (ensure-value-is-symbol-list$ arg/res-list (msg "Since the ~n0 ARG/RES component of the second input ~ is not an atom, it" (list k)) t nil)) ((er &) (ensure-list-has-no-duplicates$ arg/res-list (msg "The list ~x0 that is ~ the ~n1 ARG/RES-LIST component of the second input" arg/res-list (list k)) t nil)) (err-msg-preamble (msg "Each element ~ of the ~n0 ARG/RES-LIST component ~ of the second input ~ must be ~@1" (list k) err-msg-part))) (expdata-process-arg/res-list-aux arg/res-list x1...xn m err-msg-preamble ctx state))))))