Generate the body of the new function,
when
(expdata-gen-new-fn-body-nonpred old$ arg-surjmaps res-surjmaps new$ wrld) → new-body
If
First we transform any recursive calls via
The `else' branch should use quoted
Function:
(defun expdata-gen-new-fn-body-nonpred (old$ arg-surjmaps res-surjmaps new$ wrld) (declare (xargs :guard (and (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (expdata-pos-surjmap-alistp res-surjmaps) (symbolp new$) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-new-fn-body-nonpred)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (m (number-of-results old$ wrld)) (old-body (if (non-executablep old$ wrld) (unwrapped-nonexec-body old$ wrld) (ubody old$ wrld))) (old-body-with-new-rec-calls (expdata-xform-rec-calls old-body old$ arg-surjmaps res-surjmaps new$)) (old-body-with-back-of-x1...xn (expdata-gen-subst-x1...xn-with-back-of-x1...xn old-body-with-new-rec-calls old$ arg-surjmaps wrld)) (newp-of-x1...xn (expdata-gen-newp-of-terms x1...xn arg-surjmaps)) (newp-of-x1...xn-conj (conjoin newp-of-x1...xn)) (then-branch (cond ((endp res-surjmaps) old-body-with-back-of-x1...xn) ((endp (cdr res-surjmaps)) (apply-fn-into-ifs (expdata-surjmap->forth (cdar res-surjmaps)) old-body-with-back-of-x1...xn)) (t (b* ((y1...ym (expdata-gen-result-vars old$ m)) (forth-of-y1...ym (expdata-gen-forth-of-terms y1...ym res-surjmaps))) (make-mv-let-call 'mv y1...ym :all old-body-with-back-of-x1...xn (fcons-term 'mv forth-of-y1...ym)))))) (else-branch (if (> m 1) (fcons-term 'mv (repeat m nil)) nil))) (cond ((not (recursivep old$ nil wrld)) then-branch) ((equal newp-of-x1...xn-conj *t*) then-branch) (t (cons 'if (cons (cons 'mbt$ (cons newp-of-x1...xn-conj 'nil)) (cons then-branch (cons else-branch 'nil)))))))))