Generate the block for eliminating tail recursion.
(atj-elim-tailrec-gen-block arg-exprs method-params) → block
This is called by atj-elim-tailrec-in-return.
When we encounter a tail-recursive call of the method
in a
Function:
(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:
(defthm jblockp-of-atj-elim-tailrec-gen-block (b* ((block (atj-elim-tailrec-gen-block arg-exprs method-params))) (jblockp block)) :rule-classes :rewrite)