0b98a91 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Debraced tutorial

commit0b98a9166f6a88291b8afcb211c8972be439621b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 14:30 (15 years ago) parentb0f47e1

8 files changed+45−67

compare with master

unifiedsplit

CHANGELOG+1 tutorial/classes.tex+14−26 tutorial/idris-tutorial.pdf tutorial/interp.tex+3−4 tutorial/modules.tex+4−7 tutorial/provisional.tex+7−10 tutorial/typesfuns.tex+14−16 tutorial/views.tex+2−4

CHANGELOG+1

@@ -4,6 +4,7 @@ Complete rewrite. User visible changes:

55* New proof/tactics syntax

66* New syntax for pairs/dependent pairs

7+* Indentation-significant syntax

78* Added type classes

89* Added where clauses

910* Added case expressions, pattern matching let and lambda

tutorial/classes.tex+14−26

@@ -16,9 +16,8 @@ provides an interface for converting values to

1616

1717\begin{SaveVerbatim}{showclass}

1818

19−class Show a where {

19+class Show a where

2020 show : a -> String

21−}

2221

2322\end{SaveVerbatim}

2423\useverb{showclass}

@@ -43,10 +42,9 @@ could be defined as:

4342

4443\begin{SaveVerbatim}{shownat}

4544

46−instance Show Nat where {

45+instance Show Nat where

4746 show O = "O"

4847 show (S k) = "s" ++ show k

49−}

5048

5149Idris> show (S (S (S O)))

5250"sssO" : String

@@ -62,14 +60,12 @@ to a \texttt{String}:

6260

6361\begin{SaveVerbatim}{showvec}

6462

65−instance Show a => Show (Vect a n) where {

66− show xs = "[" ++ show' xs ++ "]" where {

63+instance Show a => Show (Vect a n) where

64+ show xs = "[" ++ show' xs ++ "]" where

6765 show' : Show a => Vect a n -> String

6866 show' VNil = ""

6967 show' (x :: VNil) = show x

7068 show' (x :: xs) = show x ++ ", " ++ show' xs

71− }

72−}

7369

7470\end{SaveVerbatim}

7571\useverb{showvec}

@@ -81,10 +77,9 @@ values for equality or inequality, with instances for all of the built-in types:

8177

8278\begin{SaveVerbatim}{eqbasic}

8379

84−class Eq a where {

80+class Eq a where

8581 (==) : a -> a -> Bool

8682 (/=) : a -> a -> Bool

87−}

8883

8984\end{SaveVerbatim}

9085\useverb{eqbasic}

@@ -95,14 +90,13 @@ For example, for an instance of \texttt{Eq} for \texttt{Nat}:

9590

9691\begin{SaveVerbatim}{eqnat}

9792

98−instance Eq Nat where {

93+instance Eq Nat where

9994 O == O = True

10095 (S x) == (S y) = x == y

10196 O == (S y) = False

10297 (S x) == O = False

10398

10499 x /= y = not (x == y)

105−}

106100

107101\end{SaveVerbatim}

108102\useverb{eqnat}

@@ -115,13 +109,12 @@ declaration, in terms of the other method:

115109

116110\begin{SaveVerbatim}{eqdefault}

117111

118−class Eq a where {

112+class Eq a where

119113 (==) : a -> a -> Bool

120114 (/=) : a -> a -> Bool

121115

122116 x /= y = not (x == y)

123117 y == y = not (x /= y)

124−}

125118

126119\end{SaveVerbatim}

127120\useverb{eqdefault}

@@ -146,7 +139,7 @@ data Ordering = LT | EQ | GT

146139

147140\begin{SaveVerbatim}{eqord}

148141

149−class Eq a => Ord a where {

142+class Eq a => Ord a where

150143 compare : a -> a -> Ordering

151144

152145 (<) : a -> a -> Bool

@@ -155,7 +148,6 @@ class Eq a => Ord a where {

155148 (>=) : a -> a -> Bool

156149 max : a -> a -> a

157150 min : a -> a -> a

158−}

159151

160152\end{SaveVerbatim}

161153\useverb{eqord}

@@ -200,10 +192,9 @@ declaration. For example:

200192

201193\begin{SaveVerbatim}{monad}

202194

203−class Monad (m : Set -> Set) where {

195+class Monad (m : Set -> Set) where

204196 return : a -> m a

205197 (>>=) : m a -> (a -> m b) -> m b

206−}

207198

208199\end{SaveVerbatim}

209200\useverb{monad}

@@ -225,12 +216,11 @@ We can also define an instance for \texttt{Maybe}, as follows:

225216

226217\begin{SaveVerbatim}{maybemonad}

227218

228−instance Monad Maybe where {

219+instance Monad Maybe where

229220 return = Just

230221

231222 Nothing >>= k = Nothing

232223 (Just x) >>= k = k x

233−}

234224

235225\end{SaveVerbatim}

236226\useverb{maybemonad}

@@ -242,10 +232,9 @@ Using this we can, for example, define a function which adds two

242232\begin{SaveVerbatim}{maybeadd}

243233

244234m_add : Maybe Int -> Maybe Int -> Maybe Int

245−m_add x y = do { x' <- x -- Extract value from x

246− y' <- y -- Extract value from y

247− return (x' + y') -- Add them

248− }

235+m_add x y = do x' <- x -- Extract value from x

236+ y' <- y -- Extract value from y

237+ return (x' + y') -- Add them

249238

250239\end{SaveVerbatim}

251240\useverb{maybeadd}

@@ -273,10 +262,9 @@ general, and applies to anything which is an instance of \texttt{MonadPlus}:

273262

274263\begin{SaveVerbatim}{monadplus}

275264

276−class Monad m => MonadPlus (m : Set -> Set) where {

265+class Monad m => MonadPlus (m : Set -> Set) where

277266 mplus : m a -> m a -> m a

278267 mzero : m a

279−}

280268

281269\end{SaveVerbatim}

282270\useverb{monadplus}

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/interp.tex+3−4

@@ -320,10 +320,9 @@ on user input:

320320\begin{SaveVerbatim}{factmain}

321321

322322main : IO ()

323−main = do { putStr "Enter a number: "

324− x <- getLine

325− print (interp [] fact (prim__strToInt x))

326− }

323+main = do putStr "Enter a number: "

324+ x <- getLine

325+ print (interp [] fact (prim__strToInt x))

327326

328327\end{SaveVerbatim}

329328\useverb{factmain}

tutorial/modules.tex+4−7

@@ -40,9 +40,8 @@ module main

4040import btree

4141

4242main : IO ()

43−main = do { let t = toTree [1,8,2,7,9,3]

44− print (toList t)

45− }

43+main = do let t = toTree [1,8,2,7,9,3]

44+ print (toList t)

4645

4746\end{SaveVerbatim}

4847\codefig{bstmain}{Binary Tree main program}

@@ -147,15 +146,13 @@ the same module:

147146

148147module foo

149148

150−namespace x {

149+namespace x

151150 test : Int -> Int

152151 test x = x * 2

153−}

154152

155−namespace y {

153+namespace y

156154 test : String -> String

157155 test x = x ++ x

158−}

159156

160157\end{SaveVerbatim}

161158\useverb{nsfoo}

tutorial/provisional.tex+7−10

@@ -252,10 +252,9 @@ provisional definition in the odd case:

252252

253253natToBin : (n:Nat) -> Binary n

254254natToBin O = bEnd

255−natToBin (S k) with parity k {

255+natToBin (S k) with (parity k)

256256 natToBin (S (j + j)) | even = bI (natToBin j)

257257 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

258−}

259258

260259\end{SaveVerbatim}

261260\useverb{ntbdef}

@@ -283,12 +282,11 @@ outputs it in binary.

283282\begin{SaveVerbatim}{binmain}

284283

285284main : IO ()

286−main = do { putStr "Enter a number: "

287− x <- getLine

288− let n = prim__strToInt x

289− let b = natToBin (fromInteger n)

290− print b

291− }

285+main = do putStr "Enter a number: "

286+ x <- getLine

287+ let n = prim__strToInt x

288+ let b = natToBin (fromInteger n)

289+ print b

292290

293291\end{SaveVerbatim}

294292\useverb{binmain}

@@ -298,11 +296,10 @@ For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary

298296

299297\begin{SaveVerbatim}{showbin}

300298

301−instance Show (Binary n) where {

299+instance Show (Binary n) where

302300 show (bO x) = show x ++ "0"

303301 show (bI x) = show x ++ "1"

304302 show bEnd = ""

305−}

306303

307304\end{SaveVerbatim}

308305\useverb{showbin}

tutorial/typesfuns.tex+14−16

@@ -196,16 +196,18 @@ accumulates the new, reversed list, and which does not need to be visible global

196196\begin{SaveVerbatim}{revwhere}

197197

198198rev : List a -> List a

199−rev xs = revAcc [] xs where {

199+rev xs = revAcc [] xs where

200200 revAcc : List a -> List a -> List a

201201 revAcc acc [] = acc

202202 revAcc acc (x :: xs) = revAcc (x :: acc) xs

203−}

204203

205204\end{SaveVerbatim}

206205\useverb{revwhere}

207206

208207\noindent

208+Indentation is significant --- functions in the \texttt{where} block must be indented

209+further than the outer function.

210+

209211\textbf{Scope:}

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

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

@@ -450,11 +452,10 @@ ordering of any implicit arguments which can appear within the block:

450452

451453\begin{SaveVerbatim}{elemusing}

452454

453−using (x:a, y:a, xs:Vect a n) {

455+using (x:a, y:a, xs:Vect a n)

454456 data Elem : a -> (Vect a n) -> Set where

455457 here : Elem x (x :: xs)

456458 | there : Elem x xs -> Elem x (y :: xs)

457−}

458459

459460\end{SaveVerbatim}

460461\useverb{elemusing}

@@ -543,10 +544,9 @@ operations with \texttt{do} notation:

543544\begin{SaveVerbatim}{greet}

544545

545546greet : IO ()

546−greet = do { putStr "What is your name? "

547− name <- getLine

548− putStrLn ("Hello " ++ name)

549− }

547+greet = do putStr "What is your name? "

548+ name <- getLine

549+ putStrLn ("Hello " ++ name)

550550

551551\end{SaveVerbatim}

552552\useverb{greet}

@@ -554,9 +554,10 @@ greet = do { putStr "What is your name? "

554554\noindent

555555The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type

556556\texttt{IO a}, and

557−puts the result, of type \texttt{a} into the variabel \texttt{x}.

557+puts the result, of type \texttt{a} into the variable \texttt{x}.

558558In this case, \texttt{getLine} returns an \texttt{IO String},

559−so \texttt{name} has type \texttt{String}.

559+so \texttt{name} has type \texttt{String}. Indentation is significant --- each

560+statement in the do block must begin in the same column.

560561The \texttt{return} operation allows us to inject a value directly into an IO

561562operation:

562563

@@ -847,9 +848,8 @@ notation. with allows pattern matching on intermediate values:

847848

848849\begin{SaveVerbatim}{vfiltercons}

849850

850−filter p (x :: xs) with filter p xs {

851+filter p (x :: xs) with (filter p xs)

851852 | (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs')

852−}

853853

854854\end{SaveVerbatim}

855855\useverb{vfiltercons}

@@ -932,9 +932,8 @@ The following function, for example, splits a string into two at a given charact

932932\begin{SaveVerbatim}{split}

933933

934934splitAt : Char -> String -> (String, String)

935−splitAt c x = case break (== c) x of {

935+splitAt c x = case break (== c) x of

936936 (x, y) => (x, strTail y)

937− }

938937

939938\end{SaveVerbatim}

940939\useverb{split}

@@ -953,10 +952,9 @@ looks up an index and returns a default value if the index is out of bounds:

953952\begin{SaveVerbatim}{listlookup}

954953

955954lookup_default : Nat -> List a -> a -> a

956−lookup_default i xs def = case list_lookup i xs of {

955+lookup_default i xs def = case list_lookup i xs of

957956 Nothing => def

958957 | Just x => x

959− }

960958

961959\end{SaveVerbatim}

962960\useverb{listlookup}

tutorial/views.tex+2−4

@@ -36,10 +36,9 @@ a vector filter function, defined as follows:

3636

3737filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

3838filter p [] = ( _ ** [] )

39−filter p (x :: xs) with filter p xs {

39+filter p (x :: xs) with (filter p xs)

4040 | ( _ ** xs' )

4141 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

42−}

4342

4443\end{SaveVerbatim}

4544\useverb{vfilterdef}

@@ -86,10 +85,9 @@ to write a function which converts a natural number to a list of binary digits

8685

8786natToBin : Nat -> List Bool

8887natToBin O = Nil

89−natToBin k with parity k {

88+natToBin k with (parity k)

9089 natToBin (j + j) | even = False :: natToBin j

9190 natToBin (S (j + j)) | odd = True :: natToBin j

92−}

9391

9492\end{SaveVerbatim}

9593\useverb{natToBin}