		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-tailrec-elimination

Atj-elim-tailrec

Turn the body of a tail-recursive method into a loop.

Signature
(atj-elim-tailrec name params body) → new-block
Arguments: name — Guard (stringp name).; params — Guard (jparam-listp params).; body — Guard (jblockp body).
Returns: new-block — Type (jblockp new-block).

This is called only on tail-recursive methods. We replace the recursive calls in the block and we surround the block with a while loop with test true; the loop is actually exited when a return is executed.

Under suitable conditions, it should be possible to generate more idiomatic while loops, with an actual continuation test instead of true, and with base cases outside the loop. However, the current form always works for all possible tail-recursive methods.

Because of the constant true continuation test in the while, it is unnecessary to have a dummy return after the loop. According to Java's static semantics, code after the loop is unreachable.

Definitions and Theorems

Function: atj-elim-tailrec

(defun atj-elim-tailrec (name params body)
 (declare (xargs :guard (and (stringp name)
                             (jparam-listp params)
                             (jblockp body))))
 (let ((__function__ 'atj-elim-tailrec))
  (declare (ignorable __function__))
  (list (make-jstatem-while
             :test (jexpr-literal-true)
             :body (atj-elim-tailrec-in-jblock body params name)))))

Theorem: jblockp-of-atj-elim-tailrec

(defthm jblockp-of-atj-elim-tailrec
  (b* ((new-block (atj-elim-tailrec name params body)))
    (jblockp new-block))
  :rule-classes :rewrite)