The existing code for generating a derivation tree had two performance pathologies.
Because derivations have reused subtrees (i.e. shared IDs) they are really more like DAGs then proper trees. Nonetheless the current API ignores the sharing and built a separate (Box) for each of these repeated sections of the output. By using shared ownership (Rc) for the shared IDs we can reduce the generation time and memory use for these complicated cases.
Because we generated derivation trees recursively, the stack memory usage was O(tree_depth). When dealing with complicated test cases that use larger Vs, it is quite possible to overflow the stack. There are probably ways to reduce the constant factors to make this problem even harder to come across, and I will need to investigate them if this PR is not accepted. But this PR solved the problem by simply removing the recursion.
This is a breaking change because the switch from Box to Rc is visible in our public API.
This is split up into several commits, each of one of which should be reviewable on its own.
The existing code for generating a derivation tree had two performance pathologies.
Because derivations have reused subtrees (i.e. shared IDs) they are really more like DAGs then proper trees. Nonetheless the current API ignores the sharing and built a separate (
Box
) for each of these repeated sections of the output. By using shared ownership (Rc
) for the shared IDs we can reduce the generation time and memory use for these complicated cases.Because we generated derivation trees recursively, the stack memory usage was
O(tree_depth)
. When dealing with complicated test cases that use largerV
s, it is quite possible to overflow the stack. There are probably ways to reduce the constant factors to make this problem even harder to come across, and I will need to investigate them if this PR is not accepted. But this PR solved the problem by simply removing the recursion.This is a breaking change because the switch from
Box
toRc
is visible in our public API.This is split up into several commits, each of one of which should be reviewable on its own.