Replace a return statement of an array write method call with an assignment to the array component followed by a return statement of the updated array.
This performs the second transformation described in atj-post-translation-remove-array-write-calls.
This function turns a single statement into a block of one or two statements. If there is no actual transformation, the output block is a singleton containing the input statement. If there is a transformation, the output block consists of two statements.
Function:
(defun atj-remove-array-write-call-return (statem) (declare (xargs :guard (jstatemp statem))) (let ((__function__ 'atj-remove-array-write-call-return)) (declare (ignorable __function__)) (b* ((no-change (list (jstatem-fix statem))) ((unless (jstatem-case statem :return)) no-change) (expr? (jstatem-return->expr? statem)) ((unless expr?) no-change) (expr expr?) ((unless (jexpr-case expr :method)) no-change) (method-name (jexpr-method->name expr)) ((unless (member-equal method-name *atj-primarray-write-method-names*)) no-change) (args (jexpr-method->args expr)) ((unless (= (len args) 3)) (prog2$ (raise "Internal error: ~ the call ~x0 of an array write method ~ has the wrong number of arguments." expr) no-change)) (array (first args)) ((unless (jexpr-case array :name)) no-change) (index (second args)) (component (third args))) (list (jstatem-expr (jexpr-binary (jbinop-asg) (jexpr-array array index) component)) (jstatem-return array)))))
Theorem:
(defthm jblockp-of-atj-remove-array-write-call-return (b* ((block (atj-remove-array-write-call-return statem))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-atj-remove-array-write-call-return (b* ((block (atj-remove-array-write-call-return statem))) (consp block)) :rule-classes :type-prescription)
Theorem:
(defthm atj-remove-array-write-call-return-of-jstatem-fix-statem (equal (atj-remove-array-write-call-return (jstatem-fix statem)) (atj-remove-array-write-call-return statem)))
Theorem:
(defthm atj-remove-array-write-call-return-jstatem-equiv-congruence-on-statem (implies (jstatem-equiv statem statem-equiv) (equal (atj-remove-array-write-call-return statem) (atj-remove-array-write-call-return statem-equiv))) :rule-classes :congruence)