1 \chapter{Normalization}
3 % A helper to print a single example in the half the page width. The example
4 % text should be in a buffer whose name is given in an argument.
6 % The align=right option really does left-alignment, but without the program
7 % will end up on a single line. The strut=no option prevents a bunch of empty
8 % space at the start of the frame.
10 \framed[offset=1mm,align=right,strut=no]{
11 \setuptyping[option=LAM,style=sans,before=,after=]
13 \setuptyping[option=none,style=\tttf]
18 % A transformation example
19 \definefloat[example][examples]
20 \setupcaption[example][location=top] % Put captions on top
22 \define[3]\transexample{
23 \placeexample[here]{#1}
24 \startcombination[2*1]
25 {\example{#2}}{Original program}
26 {\example{#3}}{Transformed program}
30 %\define[3]\transexampleh{
31 %% \placeexample[here]{#1}
32 %% \startcombination[1*2]
33 %% {\example{#2}}{Original program}
34 %% {\example{#3}}{Transformed program}
38 The first step in the core to VHDL translation process, is normalization. We
39 aim to bring the core description into a simpler form, which we can
40 subsequently translate into VHDL easily. This normal form is needed because
41 the full core language is more expressive than VHDL in some areas and because
42 core can describe expressions that do not have a direct hardware
45 TODO: Describe core properties not supported in VHDL, and describe how the
46 VHDL we want to generate should look like.
49 The transformations described here have a well-defined goal: To bring the
50 program in a well-defined form that is directly translatable to hardware,
51 while fully preserving the semantics of the program.
53 This {\em normal form} is again a Core program, but with a very specific
54 structure. A function in normal form has nested lambda's at the top, which
55 produce a let expression. This let expression binds every function application
56 in the function and produces a simple identifier. Every bound value in
57 the let expression is either a simple function application or a case
58 expression to extract a single element from a tuple returned by a
61 An example of a program in canonical form would be:
64 -- All arguments are an inital lambda
66 -- There are nested let expressions at top level
68 -- Unpack the state by coercion
69 s = sp :: (Word, Word)
70 -- Extract both registers from the state
71 r1 = case s of (fst, snd) -> fst
72 r2 = case s of (fst, snd) -> snd
73 -- Calling some other user-defined function.
75 -- Conditional connections
87 -- Packing the state by coercion
88 sp' = s' :: State (Word, Word)
89 -- Pack our return value
97 \italic{normal} = \italic{lambda}
98 \italic{lambda} = λvar.\italic{lambda} (representable(typeof(var)))
100 \italic{toplet} = let \italic{binding} in \italic{toplet}
101 | letrec [\italic{binding}] in \italic{toplet}
102 | var (representable(typeof(var)), fvar(var))
103 \italic{binding} = var = \italic{rhs} (representable(typeof(rhs)))
104 -- State packing and unpacking by coercion
105 | var0 = var1 :: State ty (fvar(var1))
106 | var0 = var1 :: ty (var0 :: State ty) (fvar(var1))
107 \italic{rhs} = userapp
110 | case var of C a0 ... an -> ai (fvar(var))
112 | case var of (fvar(var))
113 DEFAULT -> var0 (fvar(var0))
114 C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, fvar(resvar))
115 \italic{userapp} = \italic{userfunc}
116 | \italic{userapp} {userarg}
117 \italic{userfunc} = var (tvar(var))
118 \italic{userarg} = var (fvar(var))
119 \italic{builtinapp} = \italic{builtinfunc}
120 | \italic{builtinapp} \italic{builtinarg}
121 \italic{builtinfunc} = var (bvar(var))
122 \italic{builtinarg} = \italic{coreexpr}
125 -- TODO: Define tvar, fvar, typeof, representable
126 -- TODO: Limit builtinarg further
128 -- TODO: There can still be other casts around (which the code can handle,
129 e.g., ignore), which still need to be documented here.
131 -- TODO: Note about the selector case. It just supports Bit and Bool
132 currently, perhaps it should be generalized in the normal form?
134 When looking at such a program from a hardware perspective, the top level
135 lambda's define the input ports. The value produced by the let expression is
136 the output port. Most function applications bound by the let expression
137 define a component instantiation, where the input and output ports are mapped
138 to local signals or arguments. Some of the others use a builtin
139 construction (\eg the \lam{case} statement) or call a builtin function
140 (\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
143 \subsection{Normal definition}
144 Formally, the normal form is a core program obeying the following
145 constraints. TODO: Update this section, this is probably not completely
146 accurate or relevant anymore.
148 \startitemize[R,inmargin]
149 %\item All top level binds must have the form $\expr{\bind{fun}{lamexpr}}$.
150 %$fun$ is an identifier that will be bound as a global identifier.
151 %\item A $lamexpr$ has the form $\expr{\lam{arg}{lamexpr}}$ or
152 %$\expr{letexpr}$. $arg$ is an identifier which will be bound as an $argument$.
153 %\item[letexpr] A $letexpr$ has the form $\expr{\letexpr{letbinds}{retexpr}}$.
154 %\item $letbinds$ is a list with elements of the form
155 %$\expr{\bind{res}{appexpr}}$ or $\expr{\bind{res}{builtinexpr}}$, where $res$ is
156 %an identifier that will be bound as local identifier. The type of the bound
157 %value must be a $hardware\;type$.
158 %\item[builtinexpr] A $builtinexpr$ is an expression that can be mapped to an
159 %equivalent VHDL expression. Since there are many supported forms for this,
160 %these are defined in a separate table.
161 %\item An $appexpr$ has the form $\expr{fun}$ or $\expr{\app{appexpr}{x}}$,
162 %where $fun$ is a global identifier and $x$ is a local identifier.
163 %\item[retexpr] A $retexpr$ has the form $\expr{x}$ or $\expr{tupexpr}$, where $x$ is a local identifier that is bound as an $argument$ or $result$. A $retexpr$ must
164 %be of a $hardware\;type$.
165 %\item A $tupexpr$ has the form $\expr{con}$ or $\expr{\app{tupexpr}{x}}$,
166 %where $con$ is a tuple constructor ({\em e.g.} $(,)$ or $(,,,)$) and $x$ is
168 %\item A $hardware\;type$ is a type that can be directly translated to
169 %hardware. This includes the types $Bit$, $SizedWord$, tuples containing
170 %elements of $hardware\;type$s, and will include others. This explicitely
171 %excludes function types.
174 TODO: Say something about uniqueness of identifiers
176 \subsection{Builtin expressions}
177 A $builtinexpr$, as defined at \in[builtinexpr] can have any of the following forms.
179 \startitemize[m,inmargin]
181 %$tuple\_extract=\expr{\case{t}{\alt{\app{con}{x_0\;x_1\;..\;x_n}}{x_i}}}$,
182 %where $t$ can be any local identifier, $con$ is a tuple constructor ({\em
183 %e.g.} $(,)$ or $(,,,)$), $x_0$ to $x_n$ can be any identifier, and $x_i$ can
184 %be any of $x_0$ to $x_n$. A case expression must have a $hardware\;type$.
185 %\item TODO: Many more!
188 \section{Transform passes}
190 In this section we describe the actual transforms. Here we're using
191 the core language in a notation that resembles lambda calculus.
193 Each of these transforms is meant to be applied to every (sub)expression
194 in a program, for as long as it applies. Only when none of the
195 expressions can be applied anymore, the program is in normal form. We
196 hope to be able to prove that this form will obey all of the constraints
197 defined above, but this has yet to happen (though it seems likely that
200 Each of the transforms will be described informally first, explaining
201 the need for and goal of the transform. Then, a formal definition is
202 given, using a familiar syntax from the world of logic. Each transform
203 is specified as a number of conditions (above the horizontal line) and a
204 number of conclusions (below the horizontal line). The details of using
205 this notation are still a bit fuzzy, so comments are welcom.
207 TODO: Formally describe the "apply to every (sub)expression" in terms of
208 rules with full transformations in the conditions.
210 \subsection{η-abstraction}
211 This transformation makes sure that all arguments of a function-typed
212 expression are named, by introducing lambda expressions. When combined with
213 β-reduction and function inlining below, all function-typed expressions should
214 be lambda abstractions or global identifiers.
218 -------------- \lam{E} is not the first argument of an application.
219 λx.E x \lam{E} is not a lambda abstraction.
220 \lam{x} is a variable that does not occur free in \lam{E}.
224 foo = λa -> case a of
230 foo = λa.λx -> (case a of
235 \transexample{η-abstraction}{from}{to}
237 \subsection{Extended β-reduction}
238 This transformation is meant to propagate application expressions downwards
239 into expressions as far as possible. In lambda calculus, this reduction
240 is known as β-reduction, but it is of course only defined for
241 applications of lambda abstractions. We extend this reduction to also
242 work for the rest of core (case and let expressions).
264 For lambda expressions:
277 b = (let y = 3 in add y) 2
287 b = let y = 3 in add y 2
292 \transexample{Extended β-reduction}{from}{to}
294 \subsection{Let derecursification}
295 This transformation is meant to make lets non-recursive whenever possible.
296 This might allow other optimizations to do their work better. TODO: Why is
299 \subsection{Let flattening}
300 This transformation puts nested lets in the same scope, by lifting the
301 binding(s) of the inner let into a new let around the outer let. Eventually,
302 this will cause all let bindings to appear in the same scope (they will all be
303 in scope for the function return value).
305 Note that this transformation does not try to be smart when faced with
306 recursive lets, it will just leave the lets recursive (possibly joining a
307 recursive and non-recursive let into a single recursive let). The let
308 rederursification transformation will do this instead.
311 letnonrec x = (let bindings in M) in N
312 ------------------------------------------
313 let bindings in (letnonrec x = M) in N
319 x = (let bindings in M)
323 ------------------------------------------
342 b = let c = 3 in a + c
363 \transexample{Let flattening}{from}{to}
365 \subsection{Empty let removal}
366 This transformation is simple: It removes recursive lets that have no bindings
367 (which usually occurs when let derecursification removes the last binding from
376 \subsection{Simple let binding removal}
377 This transformation inlines simple let bindings (\eg a = b).
379 This transformation is not needed to get into normal form, but makes the
380 resulting VHDL a lot shorter.
406 \subsection{Unused let binding removal}
407 This transformation removes let bindings that are never used. Usually,
408 the desugarer introduces some unused let bindings.
410 This normalization pass should really be unneeded to get into normal form
411 (since ununsed bindings are not forbidden by the normal form), but in practice
412 the desugarer or simplifier emits some unused bindings that cannot be
413 normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
414 this transformation makes the resulting VHDL a lot shorter.
418 ---------------------------- \lam{a} does not occur free in \lam{M}
429 ---------------------------- \lam{a} does not occur free in \lam{M}
437 \subsection{Non-representable binding inlining}
438 This transform inlines let bindings that have a non-representable type. Since
439 we can never generate a signal assignment for these bindings (we cannot
440 declare a signal assignment with a non-representable type, for obvious
441 reasons), we have no choice but to inline the binding to remove it.
443 If the binding is non-representable because it is a lambda abstraction, it is
444 likely that it will inlined into an application and β-reduction will remove
445 the lambda abstraction and turn it into a representable expression at the
446 inline site. The same holds for partial applications, which can be turned into
447 full applications by inlining.
449 Other cases of non-representable bindings we see in practice are primitive
450 Haskell types. In most cases, these will not result in a valid normalized
451 output, but then the input would have been invalid to start with. There is one
452 exception to this: When a builtin function is applied to a non-representable
453 expression, things might work out in some cases. For example, when you write a
454 literal \hs{SizedInt} in Haskell, like \hs{1 :: SizedInt D8}, this results in
455 the following core: \lam{fromInteger (smallInteger 10)}, where for example
456 \lam{10 :: GHC.Prim.Int\#} and \lam{smallInteger 10 :: Integer} have
457 non-representable types. TODO: This/these paragraph(s) should probably become a
458 separate discussion somewhere else.
462 -------------------------- \lam{E} has a non-representable type.
473 -------------------------- \lam{E} has a non-representable type.
493 x = fromInteger (smallInteger 10)
495 (λa -> add a 1) (add 1 x)
498 \transexample{Let flattening}{from}{to}
500 \subsection{Compiler generated top level binding inlining}
503 \subsection{Scrutinee simplification}
504 This transform ensures that the scrutinee of a case expression is always
505 a simple variable reference.
510 ----------------- \lam{E} is not a local variable reference
529 \transexample{Let flattening}{from}{to}
532 \subsection{Case simplification}
533 This transformation ensures that all case expressions become normal form. This
534 means they will become one of:
536 \item An extractor case with a single alternative that picks a single field
537 from a datatype, \eg \lam{case x of (a, b) -> a}.
538 \item A selector case with multiple alternatives and only wild binders, that
539 makes a choice between expressions based on the constructor of another
540 expression, \eg \lam{case x of Low -> a; High -> b}.
545 C0 v0,0 ... v0,m -> E0
547 Cn vn,0 ... vn,m -> En
548 --------------------------------------------------- \forall i \forall j, 0 <= i <= n, 0 <= i < m (\lam{wi,j} is a wild (unused) binder)
550 v0,0 = case x of C0 v0,0 .. v0,m -> v0,0
552 v0,m = case x of C0 v0,0 .. v0,m -> v0,m
555 vn,m = case x of Cn vn,0 .. vn,m -> vn,m
559 C0 w0,0 ... w0,m -> x0
561 Cn wn,0 ... wn,m -> xn
564 TODO: This transformation specified like this is complicated and misses
565 conditions to prevent looping with itself. Perhaps we should split it here for
584 \transexample{Selector case simplification}{from}{to}
592 b = case a of (,) b c -> b
593 c = case a of (,) b c -> c
600 \transexample{Extractor case simplification}{from}{to}
602 \subsection{Case removal}
603 This transform removes any case statements with a single alternative and
606 These "useless" case statements are usually leftovers from case simplification
607 on extractor case (see the previous example).
612 ---------------------- \lam{\forall i, 0 <= i <= m} (\lam{vi} does not occur free in E)
625 \transexample{Case removal}{from}{to}
627 \subsection{Argument simplification}
628 The transforms in this section deal with simplifying application
629 arguments into normal form. The goal here is to:
632 \item Make all arguments of user-defined functions (\eg, of which
633 we have a function body) simple variable references of a runtime
634 representable type. This is needed, since these applications will be turned
635 into component instantiations.
636 \item Make all arguments of builtin functions one of:
638 \item A type argument.
639 \item A dictionary argument.
640 \item A type level expression.
641 \item A variable reference of a runtime representable type.
642 \item A variable reference or partial application of a function type.
646 When looking at the arguments of a user-defined function, we can
647 divide them into two categories:
649 \item Arguments with a runtime representable type (\eg bits or vectors).
651 These arguments can be preserved in the program, since they can
652 be translated to input ports later on. However, since we can
653 only connect signals to input ports, these arguments must be
654 reduced to simple variables (for which signals will be
655 produced). This is taken care of by the argument extraction
657 \item Non-runtime representable typed arguments.
659 These arguments cannot be preserved in the program, since we
660 cannot represent them as input or output ports in the resulting
661 VHDL. To remove them, we create a specialized version of the
662 called function with these arguments filled in. This is done by
663 the argument propagation transform.
665 Typically, these arguments are type and dictionary arguments that are
666 used to make functions polymorphic. By propagating these arguments, we
667 are essentially doing the same which GHC does when it specializes
668 functions: Creating multiple variants of the same function, one for
669 each type for which it is used. Other common non-representable
670 arguments are functions, e.g. when calling a higher order function
671 with another function or a lambda abstraction as an argument.
673 The reason for doing this is similar to the reasoning provided for
674 the inlining of non-representable let bindings above. In fact, this
675 argument propagation could be viewed as a form of cross-function
679 TODO: Check the following itemization.
681 When looking at the arguments of a builtin function, we can divide them
685 \item Arguments with a runtime representable type.
687 As we have seen with user-defined functions, these arguments can
688 always be reduced to a simple variable reference, by the
689 argument extraction transform. Performing this transform for
690 builtin functions as well, means that the translation of builtin
691 functions can be limited to signal references, instead of
692 needing to support all possible expressions.
694 \item Arguments with a function type.
696 These arguments are functions passed to higher order builtins,
697 like \lam{map} and \lam{foldl}. Since implementing these
698 functions for arbitrary function-typed expressions (\eg, lambda
699 expressions) is rather comlex, we reduce these arguments to
700 (partial applications of) global functions.
702 We can still support arbitrary expressions from the user code,
703 by creating a new global function containing that expression.
704 This way, we can simply replace the argument with a reference to
705 that new function. However, since the expression can contain any
706 number of free variables we also have to include partial
707 applications in our normal form.
709 This category of arguments is handled by the function extraction
711 \item Other unrepresentable arguments.
713 These arguments can take a few different forms:
714 \startdesc{Type arguments}
715 In the core language, type arguments can only take a single
716 form: A type wrapped in the Type constructor. Also, there is
717 nothing that can be done with type expressions, except for
718 applying functions to them, so we can simply leave type
719 arguments as they are.
721 \startdesc{Dictionary arguments}
722 In the core language, dictionary arguments are used to find
723 operations operating on one of the type arguments (mostly for
724 finding class methods). Since we will not actually evaluatie
725 the function body for builtin functions and can generate
726 code for builtin functions by just looking at the type
727 arguments, these arguments can be ignored and left as they
730 \startdesc{Type level arguments}
731 Sometimes, we want to pass a value to a builtin function, but
732 we need to know the value at compile time. Additionally, the
733 value has an impact on the type of the function. This is
734 encoded using type-level values, where the actual value of the
735 argument is not important, but the type encodes some integer,
736 for example. Since the value is not important, the actual form
737 of the expression does not matter either and we can leave
738 these arguments as they are.
740 \startdesc{Other arguments}
741 Technically, there is still a wide array of arguments that can
742 be passed, but does not fall into any of the above categories.
743 However, none of the supported builtin functions requires such
744 an argument. This leaves use with passing unsupported types to
745 a function, such as calling \lam{head} on a list of functions.
747 In these cases, it would be impossible to generate hardware
748 for such a function call anyway, so we can ignore these
751 The only way to generate hardware for builtin functions with
752 arguments like these, is to expand the function call into an
753 equivalent core expression (\eg, expand map into a series of
754 function applications). But for now, we choose to simply not
755 support expressions like these.
758 From the above, we can conclude that we can simply ignore these
759 other unrepresentable arguments and focus on the first two
763 \subsubsection{Argument simplification}
764 This transform deals with arguments to functions that
765 are of a runtime representable type. It ensures that they will all become
766 references to global variables, or local signals in the resulting VHDL.
768 TODO: It seems we can map an expression to a port, not only a signal.
769 Perhaps this makes this transformation not needed?
770 TODO: Say something about dataconstructors (without arguments, like True
771 or False), which are variable references of a runtime representable
772 type, but do not result in a signal.
774 To reduce a complex expression to a simple variable reference, we create
775 a new let expression around the application, which binds the complex
776 expression to a new variable. The original function is then applied to
781 -------------------- \lam{N} is of a representable type
782 let x = N in M x \lam{N} is not a local variable reference
790 let x = add a 1 in add x 1
793 \transexample{Argument extraction}{from}{to}
795 \subsubsection{Function extraction}
796 This transform deals with function-typed arguments to builtin functions.
797 Since these arguments cannot be propagated, we choose to extract them
798 into a new global function instead.
800 Any free variables occuring in the extracted arguments will become
801 parameters to the new global function. The original argument is replaced
802 with a reference to the new function, applied to any free variables from
803 the original argument.
805 This transformation is useful when applying higher order builtin functions
806 like \hs{map} to a lambda abstraction, for example. In this case, the code
807 that generates VHDL for \hs{map} only needs to handle top level functions and
808 partial applications, not any other expression (such as lambda abstractions or
809 even more complicated expressions).
812 M N \lam{M} is a (partial aplication of a) builtin function.
813 --------------------- \lam{f0 ... fn} = free local variables of \lam{N}
814 M x f0 ... fn \lam{N :: a -> b}
815 ~ \lam{N} is not a (partial application of) a top level function
820 map (λa . add a b) xs
834 \transexample{Function extraction}{from}{to}
836 \subsubsection{Argument propagation}
837 This transform deals with arguments to user-defined functions that are
838 not representable at runtime. This means these arguments cannot be
839 preserved in the final form and most be {\em propagated}.
841 Propagation means to create a specialized version of the called
842 function, with the propagated argument already filled in. As a simple
843 example, in the following program:
850 we could {\em propagate} the constant argument 1, with the following
858 Special care must be taken when the to-be-propagated expression has any
859 free variables. If this is the case, the original argument should not be
860 removed alltogether, but replaced by all the free variables of the
861 expression. In this way, the original expression can still be evaluated
862 inside the new function. Also, this brings us closer to our goal: All
863 these free variables will be simple variable references.
865 To prevent us from propagating the same argument over and over, a simple
866 local variable reference is not propagated (since is has exactly one
867 free variable, itself, we would only replace that argument with itself).
869 This shows that any free local variables that are not runtime representable
870 cannot be brought into normal form by this transform. We rely on an
871 inlining transformation to replace such a variable with an expression we
874 TODO: Move these definitions somewhere sensible.
876 Definition: A global variable is any variable that is bound at the
877 top level of a program. A local variable is any other variable.
879 Definition: A hardware representable type is a type that we can generate
880 a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
881 unsigned word, etc. Types that are not runtime representable notably
882 include (but are not limited to): Types, dictionaries, functions.
884 Definition: A builtin function is a function for which a builtin
885 hardware translation is available, because its actual definition is not
886 translatable. A user-defined function is any other function.
891 x Y0 ... Yi ... Yn \lam{Yi} is not of a runtime representable type
892 --------------------------------------------- \lam{Yi} is not a local variable reference
893 x' y0 ... yi-1 f0 ... fm Yi+1 ... Yn \lam{f0 ... fm} = free local vars of \lam{Yi}
895 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .
896 E y0 ... yi-1 Yi yi+1 ... yn
902 \subsection{Cast propagation / simplification}
903 This transform pushes casts down into the expression as far as possible. Since
904 its exact role and need is not clear yet, this transformation is not yet
907 \subsection{Return value simplification}
908 This transformation ensures that the return value of a function is always a
909 simple local variable reference.
911 Currently implemented using lambda simplification, let simplification, and
912 top simplification. Should change into something like the following, which
913 works only on the result of a function instead of any subexpression. This is
914 achieved by the contexts, like \lam{x = E}, though this is strictly not
915 correct (you could read this as "if there is any function \lam{x} that binds
916 \lam{E}, any \lam{E} can be transformed, while we only mean the \lam{E} that
917 is bound by \lam{x}. This might need some extra notes or something).
920 x = E \lam{E} is representable
921 ~ \lam{E} is not a lambda abstraction
922 E \lam{E} is not a let expression
923 --------------------------- \lam{E} is not a local variable reference
929 ~ \lam{E} is representable
930 E \lam{E} is not a let expression
931 --------------------------- \lam{E} is not a local variable reference
936 x = λv0 ... λvn.let ... in E
937 ~ \lam{E} is representable
938 E \lam{E} is not a local variable reference
939 ---------------------------
948 x = let x = add 1 2 in x
951 \transexample{Return value simplification}{from}{to}
953 \subsection{Example sequence}
955 This section lists an example expression, with a sequence of transforms
956 applied to it. The exact transforms given here probably don't exactly
957 match the transforms given above anymore, but perhaps this can clarify
958 the big picture a bit.
960 TODO: Update or remove this section.
978 After top-level η-abstraction:
997 After (extended) β-reduction:
1015 After return value extraction:
1034 Scrutinee simplification does not apply.
1036 After case binder wildening:
1041 a = case s of (a, _) -> a
1042 b = case s of (_, b) -> b
1043 r = case s of (_, _) ->
1046 Low -> let op' = case b of
1055 After case value simplification
1060 a = case s of (a, _) -> a
1061 b = case s of (_, b) -> b
1062 r = case s of (_, _) -> r'
1064 rl = let rll = λc.λd.c
1077 After let flattening:
1082 a = case s of (a, _) -> a
1083 b = case s of (_, b) -> b
1084 r = case s of (_, _) -> r'
1098 After function inlining:
1103 a = case s of (a, _) -> a
1104 b = case s of (_, b) -> b
1105 r = case s of (_, _) -> r'
1117 After (extended) β-reduction again:
1122 a = case s of (a, _) -> a
1123 b = case s of (_, b) -> b
1124 r = case s of (_, _) -> r'
1136 After case value simplification again:
1141 a = case s of (a, _) -> a
1142 b = case s of (_, b) -> b
1143 r = case s of (_, _) -> r'
1161 a = case s of (a, _) -> a
1162 b = case s of (_, b) -> b
1176 After let bind removal:
1181 a = case s of (a, _) -> a
1182 b = case s of (_, b) -> b
1195 Application simplification is not applicable.