		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-tailrec-elimination

Atj-elim-tailrec-in-jstatems+jblocks

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 continue.

Since we only apply this post-translation step to tail-recursive methods, we know that recursive calls may only appear as return expressions; otherwise, the call would not be tail-recursive. Thus, we only need to look for return statements whose expression is a recursive call, and replace such statements as outlined above.

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.

Definitions and Theorems

Function: atj-elim-tailrec-in-jstatem

(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: atj-elim-tailrec-in-jblock

(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: return-type-of-atj-elim-tailrec-in-jstatem.new-block

(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: return-type-of-atj-elim-tailrec-in-jblock.new-block

(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)

Subtopics

Atj-elim-tailrec-in-jstatem
Atj-elim-tailrec-in-jblock