From 5b4c3842143c22fc97264bd1acabc9e094d241c0 Mon Sep 17 00:00:00 2001 From: Natalie Perna Date: Thu, 1 Jun 2017 10:41:01 -0400 Subject: [PATCH] Rough and short cross-call-floating description attempt. --- Chapters/Conclusion.lhs | 2 ++ Chapters/Float.lhs | 16 +++++++++------- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/Chapters/Conclusion.lhs b/Chapters/Conclusion.lhs index 970502a..40bb0dd 100755 --- a/Chapters/Conclusion.lhs +++ b/Chapters/Conclusion.lhs @@ -31,6 +31,8 @@ In our implementations of projection inlining and case squashing, it was noted t Further testing of the projection inlining optimisation on a greater variety of Agda codebases is also a necessary next step before it can be safely integrated with a stable release branch of the compiler. +\edcomm{NP}{Floating cases that don't have lets} + \section{Closing Remarks} \label{sec:closing_remarks} diff --git a/Chapters/Float.lhs b/Chapters/Float.lhs index 2dec37c..f4bc3ba 100755 --- a/Chapters/Float.lhs +++ b/Chapters/Float.lhs @@ -18,10 +18,18 @@ Pattern let floating combines the benefits of pattern lets, described in section \section{Implementation} -There are a couple of implementation-specific details of interest when implementing pattern let floating. Firstly, the |floatPLet| function will only float pattern lets which occur in multiple branches, and they are floated to the least join point of those branches. +There are a couple of implementation-specific details of interest when implementing pattern let floating. Firstly, in order to float pattern lets, we first convert the |TTerm|s into a variant data type using named variables for ease of expression manipulation. Then the entire expression tree is recursed over, floating all $\lambda$ bindings to the top of the expression and accumulating a list of variables in each definition is accumulated. + +The |floatPatterns| function will only float pattern lets which occur in multiple branches, and they are floated to the least join point of those branches. Further, it is worth noting that pattern let occurrences are duplicated at join points, indicating that identical pattern lets have ``met'' there, and are then later simplified away with the |squashFloatings| function. +\subsection{Next Steps} + +Our goal is to further expand the pattern let floating optimisation such that they can not only be floated up expressions, but also across function calls. By floating pattern lets across function calls, we can avoid even more duplicated computation through sharing. + +This feature can be implemented by splitting the pattern lets at the root of functions into separate pattern lets and a body. By creating secondary functions that take the variables bound by pattern lets and make them explicit arguments to a separate function, we can abstract the patterns across function calls. + \section{Application} As readers may have noticed inspecting Figure~\ref{fig:Triangle_genplet} in the preceding chapter, there are 4 pattern let bindings for the same \texttt{v2} variable within the \texttt{d4788} function. This is a perfect opportunity for floating pattern lets, to create sharing where there formerly was none. @@ -34,9 +42,3 @@ As readers may have noticed inspecting Figure~\ref{fig:Triangle_genplet} in the \end{figure} Figure~\ref{fig:Triangle_float} shows the result of applying @--float-plet@ to this compilation, resulting in the \texttt{v2} bindings floating above the shared function call. - -\section{Next Steps} - -Our goal is to further expand the pattern let floating optimisation such that they can not only be floated up expressions, but also across function calls. By floating pattern lets across function calls, we can avoid even more duplicated computation through sharing. - -\edcomm{NP}{Future work: floating cases that don't have lets}