e62b7ea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pattern matching lambda, plus tutorial update

commite62b7ea2c9a1b0bfd54d3b7ca7d1ab7bf2e05ca1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 00:42 (15 years ago) parent67c5734

4 files changed+71−8

compare with master

unifiedsplit

src/Idris/Parser.hs+17−5 tutorial/classes.tex+6−1 tutorial/examples/letbind.idr+12 tutorial/typesfuns.tex+36−2

src/Idris/Parser.hs+17−5

@@ -621,11 +621,23 @@ pTSig syn = do lchar ':'

621621 sc <- pExpr syn

622622 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

623623

624−pLambda syn = do lchar '\\';

625− xt <- tyOptDeclList syn

626− symbol "=>"

627− sc <- pExpr syn

628− return (bindList PLam xt sc)

624+pLambda syn = try (do lchar '\\';

625+ xt <- tyOptDeclList syn

626+ symbol "=>"

627+ sc <- pExpr syn

628+ return (bindList PLam xt sc))

629+ <|> (do lchar '\\'

630+ ps <- sepBy (do fc <- pfc

631+ e <- pSimpleExpr syn

632+ return (fc, e)) (lchar ',')

633+ symbol "=>"

634+ sc <- pExpr syn

635+ return (pmList (zip [0..] ps) sc))

636+ where pmList [] sc = sc

637+ pmList ((i, (fc, x)) : xs) sc

638+ = PLam (MN i "lamp") Placeholder

639+ (PCase fc (PRef fc (MN i "lamp"))

640+ [(x, (pmList xs sc))])

629641

630642pLet syn = try (do reserved "let"; n <- pName;

631643 ty <- option Placeholder (do lchar ':'; pExpr' syn)

tutorial/classes.tex+6−1

@@ -140,6 +140,11 @@ which inherits method from \texttt{Eq} as well as defining some of its own:

140140

141141data Ordering = LT | EQ | GT;

142142

143+\end{SaveVerbatim}

144+\useverb{ord}

145+

146+\begin{SaveVerbatim}{eqord}

147+

143148class Eq a => Ord a where {

144149 compare : a -> a -> Ordering;

145150

@@ -152,7 +157,7 @@ class Eq a => Ord a where {

152157}

153158

154159\end{SaveVerbatim}

155−\useverb{ord}

160+\useverb{eqord}

156161

157162The \texttt{Ord} class allows us to compare two values and determine their ordering.

158163Only the \texttt{compare} method is required; every other method has a default definition.

tutorial/examples/letbind.idrnew file+12

@@ -0,0 +1,12 @@

1+module letbind;

3+mirror : List a -> List a;

4+mirror xs = let xs' = rev xs in

5+ app xs xs';

7+data Person = MkPerson String Int;

9+showPerson : Person -> String;

10+showPerson p = let MkPerson name age = p in

11+ name ++ " is " ++ show age ++ " years old";

12+

tutorial/typesfuns.tex+36−2

@@ -109,6 +109,10 @@ e.g. (::). Infix operators can use any of the symbols:

109109\end{SaveVerbatim}

110110\useverb{infixsyms}

111111

112+\begin{SaveVerbatim}{argh}

113+$

114+\end{SaveVerbatim}

115+

112116\subsection{Functions}

113117

114118Functions are implemented by pattern matching, again using a similar syntax to

@@ -196,6 +200,34 @@ rev xs = revAcc [] xs where {

196200Any names which are visible in the outer scope are also visible in the \texttt{where}

197201clause (unless they have been redefined, such as \texttt{xs} here).

198202

203+\subsubsection*{\texttt{let} bindings}

204+

205+Intermediate values can be calculated using \texttt{let} bindings:

206+

207+\begin{SaveVerbatim}{letb}

208+

209+mirror : List a -> List a;

210+mirror xs = let xs' = rev xs in

211+ app xs xs';

212+

213+\end{SaveVerbatim}

214+\useverb{letb}

215+

216+\noindent

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:

219+

220+\begin{SaveVerbatim}{letp}

221+

222+data Person = MkPerson String Int;

223+

224+showPerson : Person -> String;

225+showPerson p = let MkPerson name age = p in

226+ name ++ " is " ++ show age ++ " years old";

227+

228+\end{SaveVerbatim}

229+\useverb{letp}

230+

199231\subsection{Dependent Types}

200232

201233\subsubsection{Vectors}

@@ -625,12 +657,13 @@ to use an anonymous function:

625657\end{SaveVerbatim}

626658\useverb{lam1}

627659

660+\noindent

628661The notation \texttt{$\backslash$x => val} constructs an anonymous function

629662which takes one argument, \texttt{x} and returns the expression \texttt{val}.

630663Anonymous functions may take several arguments, separated by commas, e.g.

631664\texttt{$\backslash$x, y, z => val}. Arguments may also be given explicit

632−types, e.g. \texttt{$\backslash$x : Int => x * 2}.

633−

665+types, e.g. \texttt{$\backslash$x : Int => x * 2}, and can pattern match,

666+e.g. \texttt{$\backslash$ (x, y) => x + y}.

634667We could also use an operator section:

635668

636669\begin{SaveVerbatim}{sec1}

@@ -641,6 +674,7 @@ We could also use an operator section:

641674\end{SaveVerbatim}

642675\useverb{sec1}

643676

677+\noindent

644678\texttt{(*2)} is shorthand for a function which multiplies a number by 2. It expands to

645679\texttt{$\backslash$x => x * 2}.

646680Similarly, \texttt{(2*)} would expand to \texttt{$\backslash$x => 2 * x}.