cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Add Constructed Product Result Optimisation to CakeML

Open myreen opened this issue 3 years ago • 0 comments

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 original foo but returns multiple values x, y, z where foo returned (x, y, z)
  • foo is now just foo 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.

myreen avatar Sep 24 '21 13:09 myreen