Generate the term that rephrases (a generic call to) the old function in terms of the new function.
(tailrec-gen-old-as-new-term old$ test base nonrec updates a variant$ new-name$ new-formals wrld) → term
This is the right-hand side of the theorem
that relates the old function to the new function
(
This is as described in the documentation and design notes.
It varies slightly, depending on the transformation's variant.
As explained in the documentation,
for now it uses
Function:
(defun tailrec-gen-old-as-new-term (old$ test base nonrec updates a variant$ new-name$ new-formals wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp test) (pseudo-termp base) (pseudo-termp nonrec) (pseudo-term-listp updates) (symbolp a) (tailrec-variantp variant$) (symbolp new-name$) (symbol-listp new-formals) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-old-as-new-term)) (declare (ignorable __function__)) (untranslate (case variant$ ((:assoc :assoc-alt) (cons 'if (cons test (cons base (cons (subcor-var (cons a (formals old$ wrld)) (cons nonrec updates) (apply-term new-name$ new-formals)) 'nil))))) ((:monoid :monoid-alt) (subst-var base a (apply-term new-name$ new-formals))) (t (impossible))) nil wrld)))