		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation

Atj-post-translation-remove-array-write-calls

Post-translation step: remove calls of the array writing methods.

ATJ's ACL2-to-Java translation turns calls of the ACL2 functions that model array writes into calls of corresponding Java methods that make destructive writes. This keeps the translation simple, also because the array writing methods return the (modified) array, thus maintaining a functional programming style.

However, in idiomatic Java, an array write should be an assignment, whose returned value is normally discarded by turning the assignment into a statement via an ending semicolon. The goal of this post-translation step is to suitably replace calls of the array writing methods (along with some surrounding code) into assignment expression statements. This is essentially ``inlining'' these method calls.

For now we make the following transformations in this post-translation step:

We turn assignment expression statements of the form
```
a = <array-write-method>(a, i, x);
```
into assignment expressions statements of the form
```
a[i] = x;
```
ATJ's ACL2-to-Java translation produces statements of the first kind, when translating terms of the form
```
(let (... (a (<array-write-function> a i x)) ...) ...)
```
Since the array writing method makes the assignment, the second kind of assignment is equivalent to the first one. The first one just ends up assigning (the modified) a to itself. Here `modified' refers to the content of the array, not the immutable reference that is actually in a.
Because of the single-threaded array analysis, the Java variable a on the left-hand side should be the same as the first argument of the method call (when this is a variable at all), because the single-threadedness should ensure that array variables can be reused.
We turn return statements of the form
```
return <array-write-method>(a, i, x);
```
(where a is a variable) into two-statement blocks of the form
```
a[i] = x;
return a;
```
ATJ's ACL2-to-Java translation produces statements of the first kind, when a function ends its execution with a call of the form (<array-write-function> a i x). The array write method destructively updates the array and returns it. Thus, we can ``inline'' the method call here.

The two cases above are not the only kind of occurrences of the array writing methods in the Java code produced by ATJ's ACL2-to-Java translation. Other kinds of occurrences will be handled in the future.

Subtopics

Atj-remove-array-write-call-returns-in-jstatems+jblocks: Replace return statements of array write method calls with assignments to the array components and return statements of the updated arrays.
Atj-remove-array-write-call-in-asg: Replace an assignment of an array write method call with the corresponding assignment to the array component.
Atj-remove-array-write-call-asgs-in-jstatems+jblocks: Replace assignments of array write method calls with the corresponding assignments to the array components.
Atj-remove-array-write-call-return: 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.
Atj-remove-array-write-calls: Remove array write method calls from a block.
Atj-ensure-no-array-write-calls: Ensure that there are no calls of array write methods in a block.
*atj-primarray-write-method-names*: List of names of the methods to write to Java primitive arrays.