		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-update-names

Process the :update-names input.

Signature
(defarbrec-process-update-names update-names fn$ x1...xn$ ctx state) → (mv erp update-names$ state)
Arguments: fn$ — Guard (symbolp fn$).; x1...xn$ — Guard (symbol-listp x1...xn$).
Returns: update-names$ — A symbol-listp.

Return the names to use for the iterated argument update functions, in the same order as the function's formal arguments.

Definitions and Theorems

Function: defarbrec-process-update-names-aux

(defun defarbrec-process-update-names-aux
       (symbols fn$ xi...xn$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp symbols)
                             (symbolp fn$)
                             (symbol-listp xi...xn$))))
 (let ((__function__ 'defarbrec-process-update-names-aux))
  (declare (ignorable __function__))
  (b*
   (((when (endp symbols)) (value nil))
    (symbol (car symbols))
    ((er &)
     (ensure-symbol-new-event-name$
      symbol
      (msg
       "The name ~x0 of ~
                         the iterated argument update function for ~
                         the ~x1 argument of ~x2, ~
                         determined (perhaps by default) by ~
                         the :UPDATE-NAMES input,"
       symbol (car xi...xn$)
       fn$)
      t nil)))
   (defarbrec-process-update-names-aux (cdr symbols)
                                       fn$ (cdr xi...xn$)
                                       ctx state))))

Theorem: null-of-defarbrec-process-update-names-aux.nothing

(defthm null-of-defarbrec-process-update-names-aux.nothing
  (b* (((mv ?erp ?nothing ?state)
        (defarbrec-process-update-names-aux
             symbols fn$ xi...xn$ ctx state)))
    (null nothing))
  :rule-classes :rewrite)

Function: defarbrec-process-update-names

(defun defarbrec-process-update-names
       (update-names fn$ x1...xn$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn$)
                             (symbol-listp x1...xn$))))
 (let ((__function__ 'defarbrec-process-update-names))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol-list$ update-names
                                   "The :UPDATE-NAMES input" t nil))
    (symbols (or update-names
                 (defarbrec-default-update-names x1...xn$ fn$)))
    ((er &)
     (ensure-list-has-no-duplicates$
          symbols
          "The list of symbols supplied as the :UPDATE-NAMES input"
          t nil))
    ((when (/= (len symbols) (len x1...xn$)))
     (er-soft+
      ctx t nil
      "The length of the list of symbols ~
                   supplied as the :UPDATE-NAME input ~
                   must be equal to the arity of the function ~x0."
      fn$))
    ((er &)
     (defarbrec-process-update-names-aux
          symbols fn$ x1...xn$ ctx state))
    ((er &)
     (ensure-value-is-not-in-list$
      fn$ symbols
      (if
       (= 1 (len symbols))
       (msg
        "the name ~x0 of ~
                          the iterated argument update function, ~
                          determined (perhaps by default) by ~
                          the :UPDATE-NAMES input"
        (car symbols))
       (msg
        "any of the names ~&0 of ~
                        the iterated argument update functions, ~
                        determined (perhaps by default) by ~
                        the :UPDATE-NAMES input"
        symbols))
      (msg "The name ~x0 of the function to generate"
           fn$)
      t nil)))
   (value symbols))))