Generate the body of the new function,
when
(isodata-gen-new-fn-body-pred old$ arg-isomaps res-isomaps new$ wrld) → new-body
If
First we transform any recursive calls via
Function:
(defun isodata-gen-new-fn-body-pred (old$ arg-isomaps res-isomaps new$ wrld) (declare (xargs :guard (and (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp new$) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-fn-body-pred)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (old-body (if (non-executablep old$ wrld) (unwrapped-nonexec-body old$ wrld) (ubody old$ wrld))) (old-body-with-new-rec-calls (isodata-xform-rec-calls old-body old$ arg-isomaps res-isomaps new$)) (old-body-with-back-of-x1...xn (isodata-gen-subst-x1...xn-with-back-of-x1...xn old-body-with-new-rec-calls old$ arg-isomaps wrld)) (newp-of-x1...xn (isodata-gen-newp-of-terms x1...xn arg-isomaps)) (newp-of-x1...xn-conj (conjoin newp-of-x1...xn))) (if (equal newp-of-x1...xn-conj *t*) old-body-with-back-of-x1...xn (conjoin2 (cons 'mbt$ (cons newp-of-x1...xn-conj 'nil)) old-body-with-back-of-x1...xn)))))