Remove any ending
This is called on bodies of loops (which are blocks).
It removes any ending
If the block is empty, we return it unchanged.
If the block ends with
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.
Function:
(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:
(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:
(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:
(defthm atj-remove-ending-continue-does-not-increase-size (b* nil (<= (jblock-count (atj-remove-ending-continue block)) (jblock-count block))) :rule-classes :linear)