		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-lift-loop-tests

Atj-lift-loop-test

Lift an if test to the enclosing loop.

Signature
(atj-lift-loop-test block) → new-block
Arguments: block — Guard (jblockp block).
Returns: new-block — Type (jblockp new-block), given the guard.

If the block is a loop of the form described here, we transform into the equivalent code also described here. We do it only once, not recursively, because ATJ's ACL2-to-Java translation currently does not generate nested loops.

Definitions and Theorems

Function: atj-lift-loop-test

(defun atj-lift-loop-test (block)
  (declare (xargs :guard (jblockp block)))
  (let ((__function__ 'atj-lift-loop-test))
    (declare (ignorable __function__))
    (b* (((mv matchp test return body)
          (atj-check-liftable-loop-test block))
         ((unless matchp) block))
      (append (jblock-while test body)
              (jblock-return return)))))

Theorem: jblockp-of-atj-lift-loop-test

(defthm jblockp-of-atj-lift-loop-test
  (implies (and (jblockp block))
           (b* ((new-block (atj-lift-loop-test block)))
             (jblockp new-block)))
  :rule-classes :rewrite)