Fold
If the block ends with the pattern described here, we replace it with the equivalent code also described here, recursively.
Function:
(defun atj-fold-returns (block) (declare (xargs :guard (jblockp block))) (let ((__function__ 'atj-fold-returns)) (declare (ignorable __function__)) (b* (((mv matchp pre-block test-expr then-block then-expr else-block else-expr) (atj-check-foldable-return block)) ((unless matchp) block) (then-return (jstatem-return then-expr)) (else-return (jstatem-return else-expr)) (new-then-block (append then-block (list then-return))) (new-else-block (append else-block (list else-return))) (new-then-block (atj-fold-returns new-then-block)) (new-else-block (atj-fold-returns new-else-block)) (if-block (list (jstatem-ifelse test-expr new-then-block new-else-block))) (new-block (append pre-block if-block))) new-block)))
Theorem:
(defthm jblockp-of-atj-fold-returns (implies (and (jblockp block)) (b* ((new-block (atj-fold-returns block))) (jblockp new-block))) :rule-classes :rewrite)