Remove the ending
We recursively process all the statements and blocks.
When we encounter a loop,
we use atj-remove-ending-continue
to remove all its ending
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.
Function:
(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:
(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:
(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:
(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)