		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-decompose-recursive-branch

Decompose the recursive branch of the target function into its components, as described in the documentation.

Signature
(tailrec-decompose-recursive-branch old$ rec-branch ctx state) → (mv erp result state)
Arguments: old$ — Guard (symbolp old$).; rec-branch — Guard (pseudo-termp rec-branch).
Returns: result — A tuple (nonrec<x1,...,xn> (... update-xi<x1...,xn> ...) combine<q,r> q r), whose components are described in the documentation, satisfying (typed-tuplep pseudo-termp pseudo-term-listp pseudo-termp symbolp symbolp result).

Definitions and Theorems

Function: tailrec-decompose-recursive-branch

(defun tailrec-decompose-recursive-branch
       (old$ rec-branch ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-termp rec-branch))))
 (let ((__function__ 'tailrec-decompose-recursive-branch))
  (declare (ignorable __function__))
  (b*
   ((rec-calls (all-calls (list old$)
                          rec-branch nil nil))
    (rec-calls (remove-duplicates-equal rec-calls))
    ((when (/= (len rec-calls) 1))
     (er-soft+
      ctx t nil
      "After translation and LET expansion, ~
                   the recursive branch ~x0 of the target function ~x1 ~
                   must not contain different calls to ~x1."
      rec-branch old$))
    (rec-call (car rec-calls))
    ((when (equal rec-call rec-branch))
     (er-soft+ ctx t nil
               "The target function ~x0 is already tail-recursive."
               old$))
    (updates (fargs rec-call))
    (formals (formals old$ (w state)))
    (r (genvar old$ "R" nil formals))
    (q (genvar old$ "Q" nil formals))
    (combine-nonrec (subst-expr r rec-call rec-branch))
    ((er &)
     (ensure-term-not-call-of$
      combine-nonrec 'if
      (msg
       "After translation and LET expansion, ~
                      and after replacing the calls to ~x0 ~
                      with a fresh variable ~x1, ~
                      the recursive branch ~x2 of the target function ~x0"
       old$ r combine-nonrec)
      t nil))
    ((mv found nonrec combine)
     (tailrec-find-nonrec-term combine-nonrec combine-nonrec r q))
    ((unless found)
     (er-soft+
      ctx t nil
      "Unable to decompose the recursive branch ~x0 ~
                   of the target function ~x1."
      rec-branch old$)))
   (value (list nonrec updates combine q r)))))