		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-transform-rec-args

Transform the arguments of a recursive call of old.

Signature
(parteval-transform-rec-args rec-args yj...ym rem-formals) → new-rec-args
Arguments: rec-args — Arguments of a recursive call of old.
Guard (pseudo-term-listp rec-args).; yj...ym — Guard (symbol-listp yj...ym).; rem-formals — Formals that haven't been removed yet.
Guard (symbol-listp rem-formals).
Returns: new-rec-args — A pseudo-term-listp.

This applies to case 2 in the reference documentation. Each call of old is replaced with a call of new with the static arguments removed. This code performs the removal of these arguments.

Definitions and Theorems

Function: parteval-transform-rec-args

(defun parteval-transform-rec-args (rec-args yj...ym rem-formals)
 (declare (xargs :guard (and (pseudo-term-listp rec-args)
                             (symbol-listp yj...ym)
                             (symbol-listp rem-formals))))
 (let ((__function__ 'parteval-transform-rec-args))
  (declare (ignorable __function__))
  (cond
   ((endp yj...ym) rec-args)
   (t
     (b* ((yj (car yj...ym))
          (pos (position-eq yj rem-formals))
          (rec-args (append (take pos rec-args)
                            (nthcdr (1+ pos) rec-args))))
       (parteval-transform-rec-args rec-args (cdr yj...ym)
                                    (remove-eq yj rem-formals)))))))