		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-arg/res-list

Process an arg/res-list component of the surjmaps input.

Signature
(expdata-process-arg/res-list arg/res-list k old$ ctx state) → (mv erp result state)
Arguments: arg/res-list — The arg/res-listk component of surjmaps.; k — The k in arg/res-listk.
Guard (posp k).; old$ — Guard (symbolp old$).
Returns: result — A tuple (args ress) satisfying (typed-tuplep symbol-listp pos-listp result).

If the processing is successful, the args result is the list of arguments of old in arg/res-list, and the ress result is the list of 1-based indices of results of old in arg/res-list.

Definitions and Theorems

Function: expdata-process-arg/res-list-aux

(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: expdata-process-arg/res-list

(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))))))