		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-find-nonrec-term-in-term/terms

Decompose combine<nonrec<x1,...,xn>,r> into nonrec<x1,...,xn> and combine<q,r>, as described in the documentation.

Definitions and Theorems

Function: tailrec-find-nonrec-term

(defun tailrec-find-nonrec-term (combine-nonrec term-to-try r q)
  (declare (xargs :guard (and (pseudo-termp combine-nonrec)
                              (pseudo-termp term-to-try)
                              (symbolp r)
                              (symbolp q))))
  (let ((__function__ 'tailrec-find-nonrec-term))
    (declare (ignorable __function__))
    (b* (((mv found combine)
          (tailrec-check-nonrec-conditions
               combine-nonrec term-to-try r q))
         ((when found)
          (mv t term-to-try combine))
         ((when (or (variablep term-to-try)
                    (fquotep term-to-try)))
          (mv nil nil nil)))
      (tailrec-find-nonrec-terms combine-nonrec (fargs term-to-try)
                                 r q))))

Function: tailrec-find-nonrec-terms

(defun tailrec-find-nonrec-terms (combine-nonrec terms-to-try r q)
 (declare (xargs :guard (and (pseudo-termp combine-nonrec)
                             (pseudo-term-listp terms-to-try)
                             (symbolp r)
                             (symbolp q))))
 (let ((__function__ 'tailrec-find-nonrec-terms))
  (declare (ignorable __function__))
  (cond
   ((endp terms-to-try) (mv nil nil nil))
   (t
     (b*
       (((mv found nonrec combine)
         (tailrec-find-nonrec-term combine-nonrec (car terms-to-try)
                                   r q))
        ((when found) (mv t nonrec combine)))
       (tailrec-find-nonrec-terms combine-nonrec (cdr terms-to-try)
                                  r q))))))

Subtopics

Tailrec-find-nonrec-term: Find the maximal and leftmost subterm of term-to-try that satisfies the conditions for nonrec<x1,...,xn> described in the documentation.
Tailrec-find-nonrec-terms: Find the maximal and leftmost subterm of terms-to-try that satisfies the conditions for nonrec<x1,...,xn> described in the documentation.