		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-new-fn-body

Generate the body of the new function.

Signature
(parteval-gen-new-fn-body old$ static$ new-name$ case wrld) → new-body
Arguments: old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; new-name$ — Guard (symbolp new-name$).; case — Guard (member case '(1 2 3)).; wrld — Guard (plist-worldp wrld).
Returns: new-body — A pseudo-termp.

In case 1, we replace each yj with cj in the body of old.

In case 2, we replace each recursive call of old with a call of new with the static arguments removed, and then we replace each yj with cj.

In case 3, we call old with each yj replaced with cj.

Definitions and Theorems

Function: parteval-gen-new-fn-body

(defun parteval-gen-new-fn-body (old$ static$ new-name$ case wrld)
  (declare (xargs :guard (and (symbolp old$)
                              (symbol-alistp static$)
                              (symbolp new-name$)
                              (member case '(1 2 3))
                              (plist-worldp wrld))))
  (let ((__function__ 'parteval-gen-new-fn-body))
    (declare (ignorable __function__))
    (case case
      (1 (fsublis-var static$ (ubody old$ wrld)))
      (2 (b* ((body (ubody old$ wrld))
              (body (parteval-transform-rec-calls-in-term
                         body old$ new-name$ (strip-cars static$)
                         wrld))
              (body (fsublis-var static$ body)))
           body))
      (3 (fsublis-var static$
                      (cons old$ (formals old$ wrld))))
      (t (impossible)))))