Replace return statements of array write method calls with assignments to the array components and return statements of the updated arrays.
When a block is empty, we return the empty block unchanged.
When a block is a singleton,
we use atj-remove-array-write-call-return
on the (only) statement in the block and return the resulting block,
which is either the initial block or a two-statement block
(see atj-remove-array-write-call-return).
In the first case, we recursively process the (singleton) block,
because the statement may be an
Processing a statement means processing the blocks inside it. Note that the return statements that return array write method calls are replaced as part of block processing (see above).
Function:
(defun atj-remove-array-write-call-returns-in-jstatem (statem) (declare (xargs :guard (jstatemp statem))) (let ((__function__ 'atj-remove-array-write-call-returns-in-jstatem)) (declare (ignorable __function__)) (jstatem-case statem :locvar (jstatem-fix statem) :expr (jstatem-fix statem) :return (jstatem-fix statem) :throw (jstatem-fix statem) :break (jstatem-fix statem) :continue (jstatem-fix statem) :if (jstatem-if statem.test (atj-remove-array-write-call-returns-in-jblock statem.then)) :ifelse (jstatem-ifelse statem.test (atj-remove-array-write-call-returns-in-jblock statem.then) (atj-remove-array-write-call-returns-in-jblock statem.else)) :while (jstatem-while statem.test (atj-remove-array-write-call-returns-in-jblock statem.body)) :do (jstatem-do (atj-remove-array-write-call-returns-in-jblock statem.body) statem.test) :for (jstatem-for statem.init statem.test statem.update (atj-remove-array-write-call-returns-in-jblock statem.body)))))
Function:
(defun atj-remove-array-write-call-returns-in-jblock (block) (declare (xargs :guard (jblockp block))) (let ((__function__ 'atj-remove-array-write-call-returns-in-jblock)) (declare (ignorable __function__)) (b* (((when (endp block)) nil) ((when (endp (cdr block))) (b* ((statem (car block)) (new-block (atj-remove-array-write-call-return statem))) (if (consp (cdr new-block)) new-block (list (atj-remove-array-write-call-returns-in-jstatem statem)))))) (cons (atj-remove-array-write-call-returns-in-jstatem (car block)) (atj-remove-array-write-call-returns-in-jblock (cdr block))))))
Theorem:
(defthm return-type-of-atj-remove-array-write-call-returns-in-jstatem.new-statem (b* ((?new-statem (atj-remove-array-write-call-returns-in-jstatem statem))) (jstatemp new-statem)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-remove-array-write-call-returns-in-jblock.new-block (b* ((?new-block (atj-remove-array-write-call-returns-in-jblock block))) (jblockp new-block)) :rule-classes :rewrite)
Theorem:
(defthm atj-remove-array-write-call-returns-in-jstatem-of-jstatem-fix-statem (equal (atj-remove-array-write-call-returns-in-jstatem (jstatem-fix statem)) (atj-remove-array-write-call-returns-in-jstatem statem)))
Theorem:
(defthm atj-remove-array-write-call-returns-in-jblock-of-jblock-fix-block (equal (atj-remove-array-write-call-returns-in-jblock (jblock-fix block)) (atj-remove-array-write-call-returns-in-jblock block)))
Theorem:
(defthm atj-remove-array-write-call-returns-in-jstatem-jstatem-equiv-congruence-on-statem (implies (jstatem-equiv statem statem-equiv) (equal (atj-remove-array-write-call-returns-in-jstatem statem) (atj-remove-array-write-call-returns-in-jstatem statem-equiv))) :rule-classes :congruence)
Theorem:
(defthm atj-remove-array-write-call-returns-in-jblock-jblock-equiv-congruence-on-block (implies (jblock-equiv block block-equiv) (equal (atj-remove-array-write-call-returns-in-jblock block) (atj-remove-array-write-call-returns-in-jblock block-equiv))) :rule-classes :congruence)