-\startlambda
- case scrut of bndr
- DEFAULT -> defaultbody
- C0 bndr0,0 ... bndr0,m -> body0
- \vdots
- Cn bndrn,0 ... bndrn,m -> bodyn
-\stoplambda
-
-TODO: Define WHNF
-
- A case expression is the only way in Core to choose between values. A case
- expression evaluates its scrutinee, which should have an algebraic
- datatype, into weak head normal form (\small{WHNF}) and (optionally) binds
- it to \lam{bndr}. It then chooses a body depending on the constructor of
- its scrutinee. If none of the constructors match, the \lam{DEFAULT}
- alternative is chosen.
-
- Since we can only match the top level constructor, there can be no overlap
- in the alternatives and thus order of alternatives is not relevant (though
- the \lam{DEFAULT} alternative must appear first for implementation
- efficiency).
-
- Any arguments to the constructor in the scrutinee are bound to each of the
- binders after the constructor and are in scope only in the corresponding
- body.
-
- To support strictness, the scrutinee is always evaluated into WHNF, even
- when there is only a \lam{DEFAULT} alternative. This allows a strict
- function argument to be written like:
-
-\startlambda
-function (case argument of arg
- DEFAULT -> arg)
-\stoplambda
-
- This seems to be the only use for the extra binder to which the scrutinee
- is bound. When not using strictness annotations (which is rather pointless
- in hardware descriptions), \small{GHC} seems to never generate any code
- making use of this binder. The current prototype does not handle it
- either, which probably means that code using it would break.
-
- Note that these case statements are less powerful than the full Haskell
- case statements. In particular, they do not support complex patterns like
- in Haskell. Only the constructor of an expression can be matched, complex
- patterns are implemented using multiple nested case expressions.
-
- Case statements are also used for unpacking of algebraic datatypes, even
- when there is only a single constructor. For examples, to add the elements
- of a tuple, the following Core is generated:
-
-\startlambda
-sum = λtuple.case tuple of
- (,) a b -> a + b
-\stoplambda
-
- Here, there is only a single alternative (but no \lam{DEFAULT}
- alternative, since the single alternative is already exhaustive). When
- it's body is evaluated, the arguments to the tuple constructor \lam{(,)}
- (\eg, the elements of the tuple) are bound to \lam{a} and \lam{b}.
- \stopdesc
- \startdesc{Cast expression}
-\startlambda
-body :: targettype
-\stoplambda
- A cast expression allows you to change the type of an expression to an
- equivalent type. Note that this is not meant to do any actual work, like
- conversion of data from one format to another, or force a complete type
- change. Instead, it is meant to change between different representations
- of the same type, \eg switch between types that are provably equal (but
- look different).
-
- In our hardware descriptions, we typically see casts to change between a
- Haskell newtype and its contained type, since those are effectively
- different representations of the same type.
-
- More complex are types that are proven to be equal by the typechecker,
- but look different at first glance. To ensure that, once the typechecker
- has proven equality, this information sticks around, explicit casts are
- added. In our notation we only write the target type, but in reality a
- cast expressions carries around a \emph{coercion}, which can be seen as a
- proof of equality. TODO: Example
-
- The value of a cast is the value of its body, unchanged. The type of this
- value is equal to the target type, not the type of its body.
-
- Note that this syntax is also used sometimes to indicate that a particular
- expression has a particular type, even when no cast expression is
- involved. This is then purely informational, since the only elements that
- are explicitely typed in the Core language are the binder references and
- cast expressions, the types of all other elements are determined at
- runtime.
- \stopdesc
- \startdesc{Note}
-
- The Core language in \small{GHC} allows adding \emph{notes}, which serve
- as hints to the inliner or add custom (string) annotations to a core
- expression. These shouldn't be generated normally, so these are not
- handled in any way in the prototype.
- \stopdesc
- \startdesc{Type}
-\startlambda
-@type
-\stoplambda
- It is possibly to use a Core type as a Core expression. This is done to
- allow for type abstractions and applications to be handled as normal
- lambda abstractions and applications above. This means that a type
- expression in Core can only ever occur in the argument position of an
- application, and only if the type of the function that is applied to
- expects a type as the first argument. This happens for all polymorphic
- functions, for example, the \lam{fst} function:
-
-\startlambda
-fst :: \forall a. \forall b. (a, b) -> a
-fst = λtup.case tup of (,) a b -> a
-
-fstint :: (Int, Int) -> Int
-fstint = λa.λb.fst @Int @Int a b
-\stoplambda
+ \defref{case expression}
+ \startlambda
+ case scrutinee of bndr
+ DEFAULT -> defaultbody
+ C0 bndr0,0 ... bndr0,m -> body0
+ \vdots
+ Cn bndrn,0 ... bndrn,m -> bodyn
+ \stoplambda
+
+ A case expression is the only way in Core to choose between values. All
+ \hs{if} expressions and pattern matchings from the original Haskell
+ PRogram have been translated to case expressions by the desugarer.
+
+ A case expression evaluates its scrutinee, which should have an
+ algebraic datatype, into weak head normal form (\small{WHNF}) and
+ (optionally) binds it to \lam{bndr}. Every alternative lists a
+ single constructor (\lam{C0 ... Cn}). Based on the actual
+ constructor of the scrutinee, the corresponding alternative is
+ chosen. The binders in the chosen alternative (\lam{bndr0,0 ....
+ bndr0,m} are bound to the actual arguments to the constructor in
+ the scrutinee.
+
+ This is best illustrated with an example. Assume
+ there is an algebraic datatype declared as follows\footnote{This
+ datatype is not suported by the current Cλash implementation, but
+ serves well to illustrate the case expression}:
+
+ \starthaskell
+ data D = A Word | B Bit
+ \stophaskell
+
+ This is an algebraic datatype with two constructors, each getting
+ a single argument. A case expression scrutinizing this datatype
+ could look like the following:
+
+ \startlambda
+ case s of
+ A word -> High
+ B bit -> bit
+ \stoplambda
+
+ What this expression does is check the constructor of the
+ scrutinee \lam{s}. If it is \lam{A}, it always evaluates to
+ \lam{High}. If the constructor is \lam{B}, the binder \lam{bit} is
+ bound to the argument passed to \lam{B} and the case expression
+ evaluates to this bit.
+
+ If none of the alternatives match, the \lam{DEFAULT} alternative
+ is chosen. A case expression must always be exhaustive, \ie it
+ must cover all possible constructors that the scrutinee can have
+ (if all of them are covered explicitly, the \lam{DEFAULT}
+ alternative can be left out).
+
+ Since we can only match the top level constructor, there can be no overlap
+ in the alternatives and thus order of alternatives is not relevant (though
+ the \lam{DEFAULT} alternative must appear first for implementation
+ efficiency).
+
+ To support strictness, the scrutinee is always evaluated into
+ \small{WHNF}, even when there is only a \lam{DEFAULT} alternative. This
+ allows aplication of the strict function \lam{f} to the argument \lam{a}
+ to be written like:
+
+ \startlambda
+ f (case a of arg DEFAULT -> arg)
+ \stoplambda
+
+ According to the \GHC documentation, this is the only use for the extra
+ binder to which the scrutinee is bound. When not using strictness
+ annotations (which is rather pointless in hardware descriptions),
+ \small{GHC} seems to never generate any code making use of this binder.
+ In fact, \GHC has never been observed to generate code using this
+ binder, even when strictness was involved. Nonetheless, the prototype
+ handles this binder as expected.
+
+ Note that these case expressions are less powerful than the full Haskell
+ case expressions. In particular, they do not support complex patterns like
+ in Haskell. Only the constructor of an expression can be matched,
+ complex patterns are implemented using multiple nested case expressions.
+
+ Case expressions are also used for unpacking of algebraic datatypes, even
+ when there is only a single constructor. For examples, to add the elements
+ of a tuple, the following Core is generated:
+
+ \startlambda
+ sum = λtuple.case tuple of
+ (,) a b -> a + b
+ \stoplambda