Skip to content

Commit

Permalink
Chapters/Float.lhs: \edcomm{}s.
Browse files Browse the repository at this point in the history
  • Loading branch information
WolframKahl committed Jun 7, 2017
1 parent bb4866b commit 720a9b9
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions Chapters/Float.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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.

Expand All @@ -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
Expand Down

0 comments on commit 720a9b9

Please sign in to comment.