\stoplambda
Again, the transformation does not apply to this lambda abstraction, so we
- look at its body. For brevity, we'll put the case statement on one line from
+ look at its body. For brevity, we'll put the case expression on one line from
now on.
\startlambda
\stopframedtext
}
- \defref{beta-reduction}
\subsubsection[sec:normalization:beta]{β-reduction}
β-reduction is a well known transformation from lambda calculus, where it is
the main reduction step. It reduces applications of lambda abstractions,
\stoptrans
\todo{Check the subscripts of this transformation}
- Note that this transformation applies to case statements with any
+ Note that this transformation applies to case expressions with any
scrutinee. If the scrutinee is a complex expression, this might result
in duplicate hardware. An extra condition to only apply this
transformation when the scrutinee is already simple (effectively
\in{section}[sec:transformation:caseremoval].
\subsubsection[sec:transformation:caseremoval]{Case removal}
- This transform removes any case statements with a single alternative and
+ This transform removes any case expression with a single alternative and
only wild binders.
- These "useless" case statements are usually leftovers from case simplification
+ These "useless" case expressions are usually leftovers from case simplification
on extractor case (see the previous example).
\starttrans
transformations will probably need updating to handle them in all
cases.
- \subsection{Normalization of stateful descriptions}
+ \subsection[sec:normalization:stateproblems]{Normalization of stateful descriptions}
Currently, the intended normal form definition\refdef{intended
normal form definition} offers enough freedom to describe all
valid stateful descriptions, but is not limiting enough. It is
matching, causing a state input to be unpacked multiple times or
be unpacked and repacked only in some of the code paths.
- \todo{example?}
-
Without going into detail about the exact problems (of which
there are probably more than have shown up so far), it seems
unlikely that these problems can be solved entirely by just
of course mean that the intended normal form definition must be
extended as well to be more specific about how state handling
should look like in normal form.
+ \in{Section}[sec:prototype:statelimits] already contains a
+ tight description of the limitations on the use of state
+ variables, which could be adapted into the intended normal form.
\section[sec:normalization:properties]{Provable properties}
When looking at the system of transformations outlined above, there are a