		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-remove-continue

Atj-remove-ending-continue

Remove any ending continue statements from a block that forms a loop body.

Signature
(atj-remove-ending-continue block) → new-block
Arguments: block — Guard (jblockp block).
Returns: new-block — Type (jblockp new-block), given the guard.

This is called on bodies of loops (which are blocks). It removes any ending continue, including the ones inside the branches of ending ifs, recursively.

If the block is empty, we return it unchanged. If the block ends with continue, we return the block without that last statement. If the block ends with if (with or without else), we recursively process the branch(es).

We prove that the size of the new block is not greater than the size of the original block. This is used to prove the termination of atj-remove-continue-in-jstatem and atj-remove-continue-in-jblock.

Definitions and Theorems

Function: atj-remove-ending-continue

(defun atj-remove-ending-continue (block)
 (declare (xargs :guard (jblockp block)))
 (let ((__function__ 'atj-remove-ending-continue))
  (declare (ignorable __function__))
  (b* (((when (endp block)) nil)
       (last-statem (car (last block)))
       (butlast-block (butlast block 1)))
   (case (jstatem-kind last-statem)
    (:continue butlast-block)
    (:if
     (append
          butlast-block
          (list (jstatem-if (jstatem-if->test last-statem)
                            (atj-remove-ending-continue
                                 (jstatem-if->then last-statem))))))
    (:ifelse
     (append
      butlast-block
      (list
        (jstatem-ifelse (jstatem-ifelse->test last-statem)
                        (atj-remove-ending-continue
                             (jstatem-ifelse->then last-statem))
                        (atj-remove-ending-continue
                             (jstatem-ifelse->else last-statem))))))
    (otherwise block)))))

Theorem: jblockp-of-atj-remove-ending-continue

(defthm jblockp-of-atj-remove-ending-continue
  (implies (and (jblockp block))
           (b* ((new-block (atj-remove-ending-continue block)))
             (jblockp new-block)))
  :rule-classes :rewrite)

Theorem: atj-remove-ending-continue-does-not-increase-size-lemma-2

(defthm atj-remove-ending-continue-does-not-increase-size-lemma-2
 (implies
  (and (consp block)
       (jstatem-case (car (last block))
                     :ifelse))
  (equal
     (jblock-count block)
     (+ 5 (jblock-count (butlast block 1))
        (jblock-count (jstatem-ifelse->then (car (last block))))
        (jblock-count (jstatem-ifelse->else (car (last block))))))))

Theorem: atj-remove-ending-continue-does-not-increase-size

(defthm atj-remove-ending-continue-does-not-increase-size
  (b* nil
    (<= (jblock-count (atj-remove-ending-continue block))
        (jblock-count block)))
  :rule-classes :linear)