|
|
|---|
|
|
|
|---|
Pre-translation step performed by ATJ: removal of all the unused lambda-bound variables.
This is done in both the deep and shallow embedding approach.
We remove all the lambda-bound variables, and corresponding actual arguments, that are not actually used in the body of the lambda expression. This way, we avoid calculating and assigning actual arguments that are then discarded. Recall that ATJ checks that the ACL2 code to be translated to Java is free of side effects: thus, this removal is safe and semantics-preserving.
This is accomplished via the remove-unused-vars system utility. No other code is needed to do this in ATJ.