		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-update-fns

Generate the iterated argument update function definitions.

Signature
(defarbrec-gen-update-fns x1...xn$ updates update-names$ k wrld) → (mv local-events exported-events)
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).; updates — Guard (pseudo-term-listp updates).; update-names$ — Guard (symbol-listp update-names$).; k — Guard (symbolp k).; wrld — Guard (plist-worldp wrld).
Returns: local-events — A pseudo-event-form-listp.; exported-events — A pseudo-event-form-listp.

These are the functions update*-x1, ..., update*-xn in the documentation. They correspond to the function d* in the template, where f has just one argument.

Definitions and Theorems

Function: defarbrec-gen-update-fns-aux

(defun defarbrec-gen-update-fns-aux
       (x1...xn$ updates update-names$ k i wrld)
 (declare (xargs :guard (and (symbol-listp x1...xn$)
                             (pseudo-term-listp updates)
                             (symbol-listp update-names$)
                             (symbolp k)
                             (plist-worldp wrld)
                             (integer-range-p 0 (len update-names$)
                                              i))))
 (declare (xargs :guard (equal (len updates)
                               (len update-names$))))
 (let ((__function__ 'defarbrec-gen-update-fns-aux))
  (declare (ignorable __function__))
  (b*
   ((i (mbe :logic (nfix i) :exec i))
    ((when (>= i (len update-names$)))
     (mv nil nil))
    (name (nth i update-names$))
    (xi (nth i x1...xn$))
    (formals (cons k x1...xn$))
    (updates (untranslate-lst updates nil wrld))
    (body
     (cons
      'if
      (cons
          (cons 'zp (cons k 'nil))
          (cons xi
                (cons (cons name
                            (cons (cons '1- (cons k 'nil)) updates))
                      'nil)))))
    (measure (cons 'acl2-count (cons k 'nil)))
    (hints '(("Goal" :in-theory nil)))
    (local-event
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         name
         (cons
          formals
          (cons
           (cons
            'declare
            (cons
             (cons
              'xargs
              (cons
               ':measure
               (cons
                   measure
                   (cons ':well-founded-relation
                         (cons 'o<
                               (cons ':hints (cons hints 'nil)))))))
             'nil))
           (cons body 'nil)))))
       'nil)))
    (exported-event
     (cons
      'defun
      (cons
       name
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
           (cons 'xargs
                 (cons ':measure
                       (cons measure '(:well-founded-relation o<))))
           'nil))
         (cons body 'nil))))))
    ((mv local-events exported-events)
     (defarbrec-gen-update-fns-aux
          x1...xn$ updates update-names$ k (1+ i)
          wrld)))
   (mv (cons local-event local-events)
       (cons exported-event exported-events)))))

Function: defarbrec-gen-update-fns

(defun defarbrec-gen-update-fns
       (x1...xn$ updates update-names$ k wrld)
  (declare (xargs :guard (and (symbol-listp x1...xn$)
                              (pseudo-term-listp updates)
                              (symbol-listp update-names$)
                              (symbolp k)
                              (plist-worldp wrld))))
  (declare (xargs :guard (equal (len updates)
                                (len update-names$))))
  (let ((__function__ 'defarbrec-gen-update-fns))
    (declare (ignorable __function__))
    (defarbrec-gen-update-fns-aux x1...xn$
                                  updates update-names$ k 0 wrld)))