		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-tailrec-elimination

Atj-elim-tailrec-gen-block

Generate the block for eliminating tail recursion.

Signature
(atj-elim-tailrec-gen-block arg-exprs method-params) → block
Arguments: arg-exprs — Guard (jexpr-listp arg-exprs).; method-params — Guard (jparam-listp method-params).
Returns: block — Type (jblockp block).

This is called by atj-elim-tailrec-in-return. When we encounter a tail-recursive call of the method in a return statement, we generate a block consisting of (1) a parallel assignment of the call's actual arguments to the method's parameters, and (2) a continue statement.

Definitions and Theorems

Function: atj-elim-tailrec-gen-block

(defun atj-elim-tailrec-gen-block (arg-exprs method-params)
 (declare (xargs :guard (and (jexpr-listp arg-exprs)
                             (jparam-listp method-params))))
 (let ((__function__ 'atj-elim-tailrec-gen-block))
  (declare (ignorable __function__))
  (b*
   ((names (jparam-list->names method-params))
    (types (jparam-list->types method-params))
    ((unless (= (len names) (len arg-exprs)))
     (raise
      "Internal error: ~
                call of tail-recursive method has ~x0 parameters ~
                but is called with ~x1 arguments."
      (len names)
      (len arg-exprs))))
   (append (atj-make-parallel-asg names types arg-exprs)
           (jblock-continue)))))

Theorem: jblockp-of-atj-elim-tailrec-gen-block

(defthm jblockp-of-atj-elim-tailrec-gen-block
  (b* ((block (atj-elim-tailrec-gen-block arg-exprs method-params)))
    (jblockp block))
  :rule-classes :rewrite)