Replace an assignment of an array write method call with the corresponding assignment to the array component.
This performs the first transformation described in atj-post-translation-remove-array-write-calls.
This is called on the top-level expression of an expression statement, i.e. an expression that is terminated by a semicolon. If the expression fits the pattern to transform, we transform it. Otherwise, we leave it unchanged.
The expression must be a simple assignment, whose left-hand-side is an expression name and whose right-hand side is a call of one of the array write methods. Furthermore, the first argument of the method call must be the same as the left-hand side expression. In Java code produced by ATJ's ACL2-to-Java translation, the expression name should always be an identifier, of a method parameter or of a local variable.
Note that we use the
Function:
(defun atj-remove-array-write-call-in-asg (expr) (declare (xargs :guard (jexprp expr))) (let ((__function__ 'atj-remove-array-write-call-in-asg)) (declare (ignorable __function__)) (b* (((unless (jexpr-case expr :binary)) (jexpr-fix expr)) (op (jexpr-binary->op expr)) ((unless (jbinop-case op :asg)) (jexpr-fix expr)) (left (jexpr-binary->left expr)) ((unless (jexpr-case left :name)) (jexpr-fix expr)) (right (jexpr-binary->right expr)) ((unless (jexpr-case right :method)) (jexpr-fix expr)) (method-name (jexpr-method->name right)) ((unless (member-equal method-name *atj-primarray-write-method-names*)) (jexpr-fix expr)) (args (jexpr-method->args right)) ((unless (= (len args) 3)) (prog2$ (raise "Internal error: ~ the call ~x0 of an array write method ~ has the wrong number of arguments." right) (ec-call (jexpr-fix :irrelevant)))) (array (first args)) ((unless (equal array left)) (prog2$ (raise "Internal error: ~ the assignment ~x0 uses different arrays." expr) (ec-call (jexpr-fix :irrelevant)))) (index (second args)) (component (third args))) (jexpr-binary (jbinop-asg) (jexpr-array array index) component))))
Theorem:
(defthm jexprp-of-atj-remove-array-write-call-in-asg (b* ((new-expr (atj-remove-array-write-call-in-asg expr))) (jexprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm atj-remove-array-write-call-in-asg-of-jexpr-fix-expr (equal (atj-remove-array-write-call-in-asg (jexpr-fix expr)) (atj-remove-array-write-call-in-asg expr)))
Theorem:
(defthm atj-remove-array-write-call-in-asg-jexpr-equiv-congruence-on-expr (implies (jexpr-equiv expr expr-equiv) (equal (atj-remove-array-write-call-in-asg expr) (atj-remove-array-write-call-in-asg expr-equiv))) :rule-classes :congruence)