		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-alpha-component-terms

Generate the terms of the components of the result of \alpha.

Signature
(tailrec-gen-alpha-component-terms alpha-name old$ wrld) → terms
Arguments: alpha-name — Guard (symbolp alpha-name).; old$ — Guard (symbolp old$).; wrld — Guard (plist-worldp wrld).
Returns: terms — A pseudo-term-listp.

These are the terms (nth 0 (alpha x1 ... xn)), ... (nth n-1 (alpha x1 ... xn)).

The recursion constructs the terms in reverse order, with i going from n down to 1, exiting when it reaches 0.

Definitions and Theorems

Function: tailrec-gen-alpha-component-terms-aux

(defun tailrec-gen-alpha-component-terms-aux
       (i alpha-name formals terms)
  (declare (xargs :guard (and (natp i)
                              (symbolp alpha-name)
                              (symbol-listp formals)
                              (pseudo-term-listp terms))))
  (let ((__function__ 'tailrec-gen-alpha-component-terms-aux))
    (declare (ignorable __function__))
    (if (zp i)
        terms
      (b* ((i-1 (1- i))
           (term (cons 'nth
                       (cons (cons 'quote (cons i-1 'nil))
                             (cons (cons alpha-name formals)
                                   'nil)))))
        (tailrec-gen-alpha-component-terms-aux
             i-1 alpha-name
             formals (cons term terms))))))

Function: tailrec-gen-alpha-component-terms

(defun tailrec-gen-alpha-component-terms (alpha-name old$ wrld)
  (declare (xargs :guard (and (symbolp alpha-name)
                              (symbolp old$)
                              (plist-worldp wrld))))
  (let ((__function__ 'tailrec-gen-alpha-component-terms))
    (declare (ignorable __function__))
    (b* ((formals (formals old$ wrld))
         (n (len formals)))
      (tailrec-gen-alpha-component-terms-aux
           n alpha-name formals nil))))