@@ -200,33 +200,6 @@ rev xs = revAcc [] xs where {
200Any names which are visible in the outer scope are also visible in the \texttt{where}
200Any names which are visible in the outer scope are also visible in the \texttt{where}
201clause (unless they have been redefined, such as \texttt{xs} here).
201clause (unless they have been redefined, such as \texttt{xs} here).
203−\subsubsection*{\texttt{let} bindings}
205−Intermediate values can be calculated using \texttt{let} bindings:
207−\begin{SaveVerbatim}{letb}
209−mirror : List a -> List a;
210−mirror xs = let xs' = rev xs in
217−We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
218−fields from a record as follows, as well as by pattern matching at the top level:
220−\begin{SaveVerbatim}{letp}
222−data Person = MkPerson String Int;
224−showPerson : Person -> String;
225−showPerson p = let MkPerson name age = p in
226− name ++ " is " ++ show age ++ " years old";
231\subsection{Dependent Types}
204\subsection{Dependent Types}
@@ -294,9 +267,11 @@ app (x :: xs) ys = x :: app xs xs; -- BROKEN
294$ idris vbroken.idr --check
267$ idris vbroken.idr --check
295vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
268vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
271+\begin{SaveVerbatim}{bleh}
297\end{SaveVerbatim}
273\end{SaveVerbatim}
298\useverb{vapperrmsg}
274\useverb{vapperrmsg}
301This error message suggests that there is a length mismatch between two vectors
276This error message suggests that there is a length mismatch between two vectors
302--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
277--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
@@ -699,8 +674,8 @@ bounds error:
700list_lookup : Nat -> List a -> Maybe a;
675list_lookup : Nat -> List a -> Maybe a;
701list_lookup _ Nil = Nothing;
676list_lookup _ Nil = Nothing;
702−list_lookup O (Cons x xs) = Just x;
677+list_lookup O (x :: xs) = Just x;
703−list_lookup (S k) (Cons x xs) = list_lookup k xs;
678+list_lookup (S k) (x :: xs) = list_lookup k xs;
705\end{SaveVerbatim}
680\end{SaveVerbatim}
706\useverb{lookuplist}
681\useverb{lookuplist}
@@ -839,3 +814,98 @@ filter p (x :: xs) with filter p xs {
840We will see more on \texttt{with} notation later.
815We will see more on \texttt{with} notation later.
817+\subsection{More Expressions}
819+\subsubsection*{\texttt{let} bindings}
821+Intermediate values can be calculated using \texttt{let} bindings:
823+\begin{SaveVerbatim}{letb}
825+mirror : List a -> List a;
826+mirror xs = let xs' = rev xs in
833+We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
834+fields from a record as follows, as well as by pattern matching at the top level:
836+\begin{SaveVerbatim}{letp}
838+data Person = MkPerson String Int;
840+showPerson : Person -> String;
841+showPerson p = let MkPerson name age = p in
842+ name ++ " is " ++ show age ++ " years old";
847+\subsubsection*{\texttt{case} expressions}
849+Another way of inspecting intermediate values of \emph{simple} types
850+is to use a \texttt{case} expression.
851+The following function, for example, splits a string into two at a given character:
853+\begin{SaveVerbatim}{split}
855+splitAt : Char -> String -> (String, String);
856+splitAt c x = case break (== c) x of {
857+ (x, y) => (x, strTail y)
864+\texttt{break} is a library function which breaks a string into a pair of strings
865+at the point where the given function is no longer true. We then deconstruct the
866+pair it returns, and remove the first character of the second string.
868+A \texttt{case} expression can match several cases, for example, to inspect an
869+intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
870+looks up an index in a list, returning \texttt{Nothing} if the index is out
871+of bounds. We can use this to write \texttt{lookup\_default}, which
872+looks up an index and returns a default value if the index is out of bounds:
874+\begin{SaveVerbatim}{listlookup}
876+lookup_default : Nat -> List a -> a -> a;
877+lookup_default i xs def = case list_lookup i xs of {
886+If the index is in bounds, we get the value at that index, otherwise we get
889+\begin{SaveVerbatim}{deftest}
891+*usefultypes> lookup_default 2 [3,4,5,6] (-1)
893+*usefultypes> lookup_default 4 [3,4,5,6] (-1)
900+\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
901+of intermediate expressions to avoid the need to write auxiliary functions, and is
902+also used internally to implement pattern matching \texttt{let} and lambda bindings.
903+It will \emph{only} work if:
906+\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
907+value of the same type.
908+\item The type of the result is ``known''. i.e. the type of the expression can be
909+determined \emph{without} type checking the \texttt{case}-expression itself.