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.
+ (optionally) binds it to \lam{bndr}. If bndr is wild, \refdef{wild
+ binders} it is left out. 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
\stopdesc
Using this set of types, all types in basic Haskell can be represented.
-
\todo{Overview of polymorphism with more examples (or move examples
- here)}.
+ here)}
\section[sec:prototype:statetype]{State annotations in Haskell}
As noted in \in{section}[sec:description:stateann], Cλash needs some
(state) variables} and \emph{substate variables}, which will be
defined in the rules themselves.
+ These rules describe everything that can be done with state
+ variables and state-containing variables. Everything else is
+ invalid.
+
\startdesc{State variables can appear as an argument.}
\startlambda
avg = λi.λspacked. ...
\stopbuffer
\placeexample[][ex:AccStateVHDL]{\VHDL\ generated for acc from \in{example}[ex:AvgState]}
- {\typebuffer[AccStateVHDL]}
+ {\typebuffervhdl{AccStateVHDL}}
\placeexample[][ex:AvgStateVHDL]{\VHDL\ generated for avg from \in{example}[ex:AvgState]}
- {\typebuffer[AvgStateVHDL]}
+ {\typebuffervhdl{AvgStateVHDL}}
% \subsection{Initial state}
% How to specify the initial state? Cannot be done inside a hardware
% function, since the initial state is its own state argument for the first