cakeml
cakeml copied to clipboard
Add Constructed Product Result Optimisation to CakeML
Functions frequently return values as tuples. At present, returning a tuple in CakeML will always produce heap allocation, which is pointless in cases where the caller immediately pattern matches on the tuple and only uses the content rather than the tuple itself.
This PR is about implementing a form of Constructed Product Result optimisation for CakeML. The analysis would identify functions, e.g. foo
, that always return something of a specific tuple shape, e.g. (x, y, z)
, transform each such function into two functions:
-
foo_mv
same as the originalfoo
but returns multiple valuesx, y, z
wherefoo
returned(x, y, z)
-
foo
is now justfoo args = let x, y, z = foo_mv args in (x, y, z)
There would be an inlining phase that attempts to inline foo
functions as aggressively as possible so that the tuple allocation can be dead-code eliminated.
I propose that this PR is implemented after PR #837, and that BVI and DataLang are adjusted to allow multiple return values. The new optimisations, i.e. foo_mv
introduction and foo
inlining, could then be BVI-to-BVI optimisations.