		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-remove-continue

Atj-remove-continue-in-jstatems+jblocks

Remove the ending continue statements in all the loops found in statements and blocks.

We recursively process all the statements and blocks. When we encounter a loop, we use atj-remove-ending-continue to remove all its ending continues (if any), and then we recursively process the resulting body in order to remove continues from any nested loops.

Currently ATJ's ACL2-to-Java translation does not generate nested loops, and none of ATJ's post-translation steps generates nested loops. However, making this post-translation step more general require only little additional effort.

Definitions and Theorems

Function: atj-remove-continue-in-jstatem

(defun atj-remove-continue-in-jstatem (statem)
 (declare (xargs :guard (jstatemp statem)))
 (let ((__function__ 'atj-remove-continue-in-jstatem))
   (declare (ignorable __function__))
   (jstatem-case
        statem :locvar statem :expr
        statem :return statem :throw statem
        :break statem :continue statem :if
        (jstatem-if statem.test
                    (atj-remove-continue-in-jblock statem.then))
        :ifelse
        (jstatem-ifelse statem.test
                        (atj-remove-continue-in-jblock statem.then)
                        (atj-remove-continue-in-jblock statem.else))
        :while
        (b* ((body (atj-remove-ending-continue statem.body)))
          (jstatem-while statem.test
                         (atj-remove-continue-in-jblock body)))
        :do
        (b* ((body (atj-remove-ending-continue statem.body)))
          (jstatem-do (atj-remove-continue-in-jblock body)
                      statem.test))
        :for
        (b* ((body (atj-remove-ending-continue statem.body)))
          (jstatem-for statem.init statem.test statem.update
                       (atj-remove-continue-in-jblock body))))))

Function: atj-remove-continue-in-jblock

(defun atj-remove-continue-in-jblock (block)
  (declare (xargs :guard (jblockp block)))
  (let ((__function__ 'atj-remove-continue-in-jblock))
    (declare (ignorable __function__))
    (cond ((endp block) nil)
          (t (cons (atj-remove-continue-in-jstatem (car block))
                   (atj-remove-continue-in-jblock (cdr block)))))))

Theorem: return-type-of-atj-remove-continue-in-jstatem.new-statem

(defthm return-type-of-atj-remove-continue-in-jstatem.new-statem
  (implies
       (and (jstatemp statem))
       (b* ((?new-statem (atj-remove-continue-in-jstatem statem)))
         (jstatemp new-statem)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-remove-continue-in-jblock.new-block

(defthm return-type-of-atj-remove-continue-in-jblock.new-block
  (implies (and (jblockp block))
           (b* ((?new-block (atj-remove-continue-in-jblock block)))
             (jblockp new-block)))
  :rule-classes :rewrite)

Subtopics

Atj-remove-continue-in-jstatem
Atj-remove-continue-in-jblock