From 720a9b9487fe616ea548337998e2ecf09b6b2c11 Mon Sep 17 00:00:00 2001 From: Wolfram Kahl Date: Tue, 6 Jun 2017 22:17:20 -0400 Subject: [PATCH] Chapters/Float.lhs: \edcomm{}s. --- Chapters/Float.lhs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Chapters/Float.lhs b/Chapters/Float.lhs index b624bbb..22b130f 100755 --- a/Chapters/Float.lhs +++ b/Chapters/Float.lhs @@ -28,6 +28,7 @@ In combination with our option: --cross-call-float float pattern bindings across function calls \end{verbatim} +\edinsert{WK}{that is currently under development,} bindings can also be shared across function calls. \section{Logical Representation} @@ -95,7 +96,7 @@ let f@(g@(h,i),j@(k,l)) = RHS in \end{spec} %} -We are further expanding 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. +We are \edinsert{WK}{currently working on} further expanding 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 is 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. @@ -113,7 +114,9 @@ The @--abstract-plet@ feature is necessary to split functions into two, with the \newpage -In Figure~\ref{fig:pullback_cross} we can see the result of cross-call floating on the \AgdaModule{Pullback} module. Notice that without cross-call floating, a single call to \texttt{du78} would result in two unshared calls to \texttt{du58}, one via \texttt{du60} and one via \texttt{du70}. With cross-call floating, \texttt{du78} calls \texttt{du58} only once, then passes the results via the additional parameters to \texttt{dv78}, which in turn shares the values with both \texttt{dv60} and \texttt{dv70}. +In Figure~\ref{fig:pullback_cross} we can see the result of cross-call floating on the \AgdaModule{Pullback} module. +\edcomm{WK}{Consider moving this down, to make the sequence here the same as in ``Usage''.} +Notice that without cross-call floating, a single call to \texttt{du78} would result in two unshared calls to \texttt{du58}, one via \texttt{du60} and one via \texttt{du70}. With cross-call floating, \texttt{du78} calls \texttt{du58} only once, then passes the results via the additional parameters to \texttt{dv78}, which in turn shares the values with both \texttt{dv60} and \texttt{dv70}. \begin{figure}[h] \centering