\definetyping[lambda][option=LAM,style=sans]
\definetype[lam][option=LAM,style=sans]
+\installprettytype [TRANS] [TRANS]
+\definetyping[trans][option=TRANS,style=normal,before=,after=]
+
% An (invisible) frame to hold a lambda expression
\define[1]\lamframe{
% Put a frame around lambda expressions, so they can have multiple
number of conclusions (below the horizontal line). The details of using
this notation are still a bit fuzzy, so comments are welcom.
+TODO: Formally describe the "apply to every (sub)expression" in terms of
+rules with full transformations in the conditions.
+
\subsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
β-reduction and function inlining below, all function-typed expressions should
be lambda abstractions or global identifiers.
-\transform{η-abstraction}
-{
-\lam{E :: * -> *}
-
-\lam{E} is not the first argument of an application.
-
-\lam{E} is not a lambda abstraction.
-
-\lam{x} is a variable that does not occur free in E.
-
-\conclusion
-
-\trans{E}{λx.E x}
-}
+\starttrans
+E \lam{E :: * -> *}
+-------------- \lam{E} is not the first argument of an application.
+λx.E x \lam{E} is not a lambda abstraction.
+ \lam{x} is a variable that does not occur free in \lam{E}.
+\stoptrans
\startbuffer[from]
foo = λa -> case a of
hardware translation is available, because its actual definition is not
translatable. A user-defined function is any other function.
+\starttrans
+x = E
+~
+x Y0 ... Yi ... Yn \lam{Y_i} is not of a runtime representable type
+--------------------------------------------- \lam{Y_i} is not a local variable reference
+x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn . \lam{f0 ... fm} = free local vars of \lam{Y_i}
+ E y0 ... yi-1 Yi yi+1 ... yn
+~
+x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn
+\stoptrans
+
\transform{Argument propagation}
{
\lam{x} is a global variable, bound to a user-defined function