Eliminate any tail-recursive call in a
(atj-elim-tailrec-in-return expr? method-params method-name) → block
This is called by atj-elim-tailrec-in-jstatem
when a
If the expression is a call of the method,
we return a block consisting of
(1) a parallel assignment of the call's actual arguments
to the method's parameters, and
(2) a
If the expression is a right-associated conditional conjunction
if (expr1 && (expr2 && (... && exprN-1)...)) { <parallel-asg> continue; } else { return false; }
In all other cases,
we return a block consisting of the single
Function:
(defun atj-elim-tailrec-in-return (expr? method-params method-name) (declare (xargs :guard (and (maybe-jexprp expr?) (jparam-listp method-params) (stringp method-name)))) (let ((__function__ 'atj-elim-tailrec-in-return)) (declare (ignorable __function__)) (b* (((unless (jexprp expr?)) (list (jstatem-return nil))) (expr expr?)) (cond ((and (jexpr-case expr :method) (equal (jexpr-method->name expr) method-name)) (atj-elim-tailrec-gen-block (jexpr-method->args expr) method-params)) ((and (jexpr-case expr :binary) (jbinop-case (jexpr-binary->op expr) :condand)) (b* ((exprs (unmake-right-assoc-condand expr)) ((unless (>= (len exprs) 2)) (raise "Internal error: ~ expression ~x0 has fewer than 2 conjuncts." exprs) (ec-call (jblock-fix :irrelevant))) (rightmost (car (last exprs))) (others (butlast exprs 1)) ((unless (and (jexpr-case rightmost :method) (equal (jexpr-method->name rightmost) method-name))) (list (jstatem-return expr?)))) (jblock-ifelse (make-right-assoc-condand others) (atj-elim-tailrec-gen-block (jexpr-method->args rightmost) method-params) (jblock-return (jexpr-literal-false))))) (t (list (jstatem-return expr?)))))))
Theorem:
(defthm jblockp-of-atj-elim-tailrec-in-return (b* ((block (atj-elim-tailrec-in-return expr? method-params method-name))) (jblockp block)) :rule-classes :rewrite)