Eliminate all the tail-recursive calls in a method's statement or block.
We recursively traverse the statements and blocks
and replace each call of the given method name
with a parallel assignment to the method parameters
followed by a
Since we only apply this post-translation step to tail-recursive methods,
we know that recursive calls may only appear as
Since a single statement may be replaced by a block, we systematically turn statements into blocks (often singletons), and handle the transformation of blocks appropriately.
Function:
(defun atj-elim-tailrec-in-jstatem (statem method-params method-name) (declare (xargs :guard (and (jstatemp statem) (jparam-listp method-params) (stringp method-name)))) (let ((__function__ 'atj-elim-tailrec-in-jstatem)) (declare (ignorable __function__)) (jstatem-case statem :locvar (list statem) :expr (list statem) :return (atj-elim-tailrec-in-return statem.expr? method-params method-name) :throw (list statem) :break (list statem) :continue (list statem) :if (jblock-if statem.test (atj-elim-tailrec-in-jblock statem.then method-params method-name)) :ifelse (jblock-ifelse statem.test (atj-elim-tailrec-in-jblock statem.then method-params method-name) (atj-elim-tailrec-in-jblock statem.else method-params method-name)) :while (jblock-while statem.test (atj-elim-tailrec-in-jblock statem.body method-params method-name)) :do (jblock-do (atj-elim-tailrec-in-jblock statem.body method-params method-name) statem.test) :for (jblock-for statem.init statem.test statem.update (atj-elim-tailrec-in-jblock statem.body method-params method-name)))))
Function:
(defun atj-elim-tailrec-in-jblock (block method-params method-name) (declare (xargs :guard (and (jblockp block) (jparam-listp method-params) (stringp method-name)))) (let ((__function__ 'atj-elim-tailrec-in-jblock)) (declare (ignorable __function__)) (cond ((endp block) nil) (t (append (atj-elim-tailrec-in-jstatem (car block) method-params method-name) (atj-elim-tailrec-in-jblock (cdr block) method-params method-name))))))
Theorem:
(defthm return-type-of-atj-elim-tailrec-in-jstatem.new-block (implies (jstatemp statem) (b* ((?new-block (atj-elim-tailrec-in-jstatem statem method-params method-name))) (jblockp new-block))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-elim-tailrec-in-jblock.new-block (implies (jblockp block) (b* ((?new-block (atj-elim-tailrec-in-jblock block method-params method-name))) (jblockp new-block))) :rule-classes :rewrite)