e62b7ea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Pattern matching lambda, plus tutorial update

e62b7eaEdwin Brady15 years ago

src/Idris/Parser.hs+17−5

compare with master

unifiedsplit

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

621 sc <- pExpr syn

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

623

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

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

625− xt <- tyOptDeclList syn

625+ xt <- tyOptDeclList syn

626− symbol "=>"

626+ symbol "=>"

627− sc <- pExpr syn

627+ sc <- pExpr syn

628− return (bindList PLam xt sc)

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))])

629

641

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

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

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

643 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:

140

141data Ordering = LT | EQ | GT;

142

143+\end{SaveVerbatim}

144+\useverb{ord}

145+

146+\begin{SaveVerbatim}{eqord}

147+

143class Eq a => Ord a where {

148class Eq a => Ord a where {

144 compare : a -> a -> Ordering;

149 compare : a -> a -> Ordering;

145

150

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

152}

157}

153

158

154\end{SaveVerbatim}

159\end{SaveVerbatim}

155−\useverb{ord}

160+\useverb{eqord}

156

161

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

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

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

163Only 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:

109\end{SaveVerbatim}

110\useverb{infixsyms}

111

112+\begin{SaveVerbatim}{argh}

113+$

114+\end{SaveVerbatim}

115+

112\subsection{Functions}

116\subsection{Functions}

113

117

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

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

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

196Any 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}

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

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

198

202

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+

199\subsection{Dependent Types}

231\subsection{Dependent Types}

200

232

201\subsubsection{Vectors}

233\subsubsection{Vectors}

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

625\end{SaveVerbatim}

657\end{SaveVerbatim}

626\useverb{lam1}

658\useverb{lam1}

627

659

660+\noindent

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

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

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

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

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

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

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

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

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

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

633−

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

634We could also use an operator section:

667We could also use an operator section:

635

668

636\begin{SaveVerbatim}{sec1}

669\begin{SaveVerbatim}{sec1}

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

641\end{SaveVerbatim}

674\end{SaveVerbatim}

642\useverb{sec1}

675\useverb{sec1}

643

676

677+\noindent

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

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

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

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

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

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