- This transformation only applies to the entire body of a
- function instead of any subexpression in a function. This is
- achieved by the contexts, like \lam{x = E}, though this is
- strictly not correct (you could read this as "if there is any
- function \lam{x} that binds \lam{E}, any \lam{E} can be
- transformed, while we only mean the \lam{E} that is bound by
- \lam{x}).
-
- Note that the return value is not simplified if its not
- representable. Otherwise, this would cause a direct loop with
- the inlining of unrepresentable bindings. If the return value is
- not representable because it has a function type, η-abstraction
- should make sure that this transformation will eventually apply.
- If the value is not representable for other reasons, the
- function result itself is not representable, meaning this
- function is not translatable anyway.
+ The basic idea of this transformation is to take the body of a
+ function and bind it with a let expression (so the body of that let
+ expression becomes a variable reference that can be used as the output
+ port). If the body of the function happens to have lambda abstractions
+ at the top level (which is allowed by the intended normal
+ form\refdef{intended normal form definition}), we take the body of the
+ inner lambda instead. If that happens to be a let expression already
+ (which is allowed by the intended normal form), we take the body of
+ that let (which is not allowed to be anything but a variable reference
+ according the the intended normal form).
+
+ This transformation uses the context conditions in a special way.
+ These contexts, like \lam{x = λv1 ... λvn.E}, are above the dotted
+ line and provide a condition on the environment (\ie\ they require a
+ certain top level binding to be present). These ensure that
+ expressions are only transformed when they are in the functions
+ \quote{return value} directly. This means the context conditions have
+ to interpreted in the right way: not \quote{if there is any function
+ \lam{x} that binds \lam{E}, any \lam{E} can be transformed}, but we
+ mean only the \lam{E} that is bound by \lam{x}).
+
+ Be careful when reading the transformations: Not the entire function
+ from the context is transformed, just a part of it.
+
+ Note that the return value is not simplified if it is not representable.
+ Otherwise, this would cause a loop with the inlining of
+ unrepresentable bindings in
+ \in{section}[sec:normalization:nonrepinline]. If the return value is
+ not representable because it has a function type, η-expansion should
+ make sure that this transformation will eventually apply. If the
+ value is not representable for other reasons, the function result
+ itself is not representable, meaning this function is not translatable
+ anyway.