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
Because of the single-threaded array analysis,
the Java variable
We turn return statements of the form
return <array-write-method>(a, i, x);
(where
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
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.