Atj-post-translation-tailrec-elimination
Post-translation step:
eliminate tail recursions in favor of loops.
It is well-known that tail recursions can be turned into loops;
this process is often called `tail recursion elimination'.
This post-translation step does that,
by surrounding the body of a tail-recursive method
in a while (true) { ... } loop,
and replacing each recursive call with a continue
preceded by an assignment to the method's parameters
of the values passed to the recursive call.
We remark that the assignment to the method's parameters
is an instance of destructive updates,
which is idiomatic in Java.
It seems better to realize this as a post-translation step,
rather than as part of the ACL2-to-Java translation,
which is already fairly complicated.
Subtopics
- Atj-make-parallel-asg
- Generate a block that performs a parallel assignment
of the given expressions to the given variables.
- Atj-elim-tailrec-in-jstatems+jblocks
- Eliminate all the tail-recursive calls in a method's
statement or block.
- Atj-parallel-asg-depgraph
- Calculate a dependency graph for a parallel assignment.
- Atj-elim-tailrec-in-return
- Eliminate any tail-recursive call in a return statement.
- Atj-serialize-parallel-asg
- Generate a block that performs a parallel assignment
of the given expressions to the given variables,
according to the supplied serialization.
- Atj-elim-tailrec
- Turn the body of a tail-recursive method into a loop.
- Atj-elim-tailrec-gen-block
- Generate the block for eliminating tail recursion.
