		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-lift-loop-tests

Atj-check-liftable-loop-test

Check if a Java block is a while (true) ... loop with an if body whose test can be lifted to the loop.

Signature
(atj-check-liftable-loop-test block) → (mv yes/no test return body)
Arguments: block — Guard (jblockp block).
Returns: yes/no — Type (booleanp yes/no).; test — Type (jexprp test).; return — Type (jexprp return).; body — Type (jblockp body).

This checks if a block has one of the two forms described here. If it does, we return its components, i.e. the test expression, the return expression, and the block that will become the body of the new loop (i.e. the `then' or `else' branch that is not a return. The returned test expression is the one that will become the test of the new loop: thus, it is either the same as the if or its logical negation, depending on which branch is the return.

If the first result of this function is nil, the other results have irrelevant values.

Definitions and Theorems

Function: atj-check-liftable-loop-test

(defun atj-check-liftable-loop-test (block)
  (declare (xargs :guard (jblockp block)))
  (let ((__function__ 'atj-check-liftable-loop-test))
    (declare (ignorable __function__))
    (b* (((fun (fail))
          (mv nil (jexpr-name "")
              (jexpr-name "")
              nil))
         ((unless (= (len block) 1)) (fail))
         (statem (car block))
         ((unless (jstatem-case statem :while))
          (fail))
         (while-test (jstatem-while->test statem))
         (while-body (jstatem-while->body statem))
         ((unless (equal while-test (jexpr-literal-true)))
          (fail))
         ((unless (= (len while-body) 1)) (fail))
         (statem (car while-body))
         ((unless (jstatem-case statem :ifelse))
          (fail))
         (test (jstatem-ifelse->test statem))
         (then (jstatem-ifelse->then statem))
         (else (jstatem-ifelse->else statem))
         ((mv then-return-p return)
          (atj-check-single-return-with-expr then))
         ((when then-return-p)
          (mv t (negate-boolean-jexpr test)
              return else))
         ((mv else-return-p return)
          (atj-check-single-return-with-expr else))
         ((when else-return-p)
          (mv t test return then)))
      (fail))))

Theorem: booleanp-of-atj-check-liftable-loop-test.yes/no

(defthm booleanp-of-atj-check-liftable-loop-test.yes/no
  (b* (((mv ?yes/no
            ?test common-lisp::?return acl2::?body)
        (atj-check-liftable-loop-test block)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-check-liftable-loop-test.test

(defthm jexprp-of-atj-check-liftable-loop-test.test
  (b* (((mv ?yes/no
            ?test common-lisp::?return acl2::?body)
        (atj-check-liftable-loop-test block)))
    (jexprp test))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-check-liftable-loop-test.return

(defthm jexprp-of-atj-check-liftable-loop-test.return
  (b* (((mv ?yes/no
            ?test common-lisp::?return acl2::?body)
        (atj-check-liftable-loop-test block)))
    (jexprp return))
  :rule-classes :rewrite)

Theorem: jblockp-of-atj-check-liftable-loop-test.body

(defthm jblockp-of-atj-check-liftable-loop-test.body
  (b* (((mv ?yes/no
            ?test common-lisp::?return acl2::?body)
        (atj-check-liftable-loop-test block)))
    (jblockp body))
  :rule-classes :rewrite)