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

CHANGELOG+1

compare with master

unifiedsplit

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

4

5* New proof/tactics syntax

6* New syntax for pairs/dependent pairs

7+* Indentation-significant syntax

7* Added type classes

8* Added type classes

8* Added where clauses

9* Added where clauses

9* Added case expressions, pattern matching let and lambda

10* Added case expressions, pattern matching let and lambda

tutorial/classes.tex+14−26

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

16

17\begin{SaveVerbatim}{showclass}

18

19−class Show a where {

19+class Show a where

20 show : a -> String

21−}

22

21

23\end{SaveVerbatim}

22\end{SaveVerbatim}

24\useverb{showclass}

23\useverb{showclass}

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

43

42

44\begin{SaveVerbatim}{shownat}

43\begin{SaveVerbatim}{shownat}

45

44

46−instance Show Nat where {

45+instance Show Nat where

47 show O = "O"

46 show O = "O"

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

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

49−}

50

48

51Idris> show (S (S (S O)))

49Idris> show (S (S (S O)))

52"sssO" : String

50"sssO" : String

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

62

60

63\begin{SaveVerbatim}{showvec}

61\begin{SaveVerbatim}{showvec}

64

62

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

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

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

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

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

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

68 show' VNil = ""

66 show' VNil = ""

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

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

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

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

71− }

72−}

73

69

74\end{SaveVerbatim}

70\end{SaveVerbatim}

75\useverb{showvec}

71\useverb{showvec}

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

81

77

82\begin{SaveVerbatim}{eqbasic}

78\begin{SaveVerbatim}{eqbasic}

83

79

84−class Eq a where {

80+class Eq a where

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

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

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

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

87−}

88

83

89\end{SaveVerbatim}

84\end{SaveVerbatim}

90\useverb{eqbasic}

85\useverb{eqbasic}

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

95

90

96\begin{SaveVerbatim}{eqnat}

91\begin{SaveVerbatim}{eqnat}

97

92

98−instance Eq Nat where {

93+instance Eq Nat where

99 O == O = True

94 O == O = True

100 (S x) == (S y) = x == y

95 (S x) == (S y) = x == y

101 O == (S y) = False

96 O == (S y) = False

102 (S x) == O = False

97 (S x) == O = False

103

98

104 x /= y = not (x == y)

99 x /= y = not (x == y)

105−}

106

100

107\end{SaveVerbatim}

101\end{SaveVerbatim}

108\useverb{eqnat}

102\useverb{eqnat}

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

115

109

116\begin{SaveVerbatim}{eqdefault}

110\begin{SaveVerbatim}{eqdefault}

117

111

118−class Eq a where {

112+class Eq a where

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

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

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

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

121

115

122 x /= y = not (x == y)

116 x /= y = not (x == y)

123 y == y = not (x /= y)

117 y == y = not (x /= y)

124−}

125

118

126\end{SaveVerbatim}

119\end{SaveVerbatim}

127\useverb{eqdefault}

120\useverb{eqdefault}

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

146

139

147\begin{SaveVerbatim}{eqord}

140\begin{SaveVerbatim}{eqord}

148

141

149−class Eq a => Ord a where {

142+class Eq a => Ord a where

150 compare : a -> a -> Ordering

143 compare : a -> a -> Ordering

151

144

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

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

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

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

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

156 max : a -> a -> a

149 max : a -> a -> a

157 min : a -> a -> a

150 min : a -> a -> a

158−}

159

151

160\end{SaveVerbatim}

152\end{SaveVerbatim}

161\useverb{eqord}

153\useverb{eqord}

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

200

192

201\begin{SaveVerbatim}{monad}

193\begin{SaveVerbatim}{monad}

202

194

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

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

204 return : a -> m a

196 return : a -> m a

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

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

206−}

207

198

208\end{SaveVerbatim}

199\end{SaveVerbatim}

209\useverb{monad}

200\useverb{monad}

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

225

216

226\begin{SaveVerbatim}{maybemonad}

217\begin{SaveVerbatim}{maybemonad}

227

218

228−instance Monad Maybe where {

219+instance Monad Maybe where

229 return = Just

220 return = Just

230

221

231 Nothing >>= k = Nothing

222 Nothing >>= k = Nothing

232 (Just x) >>= k = k x

223 (Just x) >>= k = k x

233−}

234

224

235\end{SaveVerbatim}

225\end{SaveVerbatim}

236\useverb{maybemonad}

226\useverb{maybemonad}

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

242\begin{SaveVerbatim}{maybeadd}

232\begin{SaveVerbatim}{maybeadd}

243

233

244m_add : Maybe Int -> Maybe Int -> Maybe Int

234m_add : Maybe Int -> Maybe Int -> Maybe Int

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

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

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

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

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

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

248− }

249

238

250\end{SaveVerbatim}

239\end{SaveVerbatim}

251\useverb{maybeadd}

240\useverb{maybeadd}

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

273

262

274\begin{SaveVerbatim}{monadplus}

263\begin{SaveVerbatim}{monadplus}

275

264

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

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

277 mplus : m a -> m a -> m a

266 mplus : m a -> m a -> m a

278 mzero : m a

267 mzero : m a

279−}

280

268

281\end{SaveVerbatim}

269\end{SaveVerbatim}

282\useverb{monadplus}

270\useverb{monadplus}

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/interp.tex+3−4

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

320\begin{SaveVerbatim}{factmain}

321

322main : IO ()

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

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

324− x <- getLine

324+ x <- getLine

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

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

326− }

327

326

328\end{SaveVerbatim}

327\end{SaveVerbatim}

329\useverb{factmain}

328\useverb{factmain}

tutorial/modules.tex+4−7

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

40import btree

41

42main : IO ()

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

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

44− print (toList t)

44+ print (toList t)

45− }

46

45

47\end{SaveVerbatim}

46\end{SaveVerbatim}

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

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

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

147

146

148module foo

147module foo

149

148

150−namespace x {

149+namespace x

151 test : Int -> Int

150 test : Int -> Int

152 test x = x * 2

151 test x = x * 2

153−}

154

152

155−namespace y {

153+namespace y

156 test : String -> String

154 test : String -> String

157 test x = x ++ x

155 test x = x ++ x

158−}

159

156

160\end{SaveVerbatim}

157\end{SaveVerbatim}

161\useverb{nsfoo}

158\useverb{nsfoo}

tutorial/provisional.tex+7−10

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

252

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

254natToBin O = bEnd

255−natToBin (S k) with parity k {

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

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

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

258−}

259

258

260\end{SaveVerbatim}

259\end{SaveVerbatim}

261\useverb{ntbdef}

260\useverb{ntbdef}

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

283\begin{SaveVerbatim}{binmain}

282\begin{SaveVerbatim}{binmain}

284

283

285main : IO ()

284main : IO ()

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

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

287− x <- getLine

286+ x <- getLine

288− let n = prim__strToInt x

287+ let n = prim__strToInt x

289− let b = natToBin (fromInteger n)

288+ let b = natToBin (fromInteger n)

290− print b

289+ print b

291− }

292

290

293\end{SaveVerbatim}

291\end{SaveVerbatim}

294\useverb{binmain}

292\useverb{binmain}

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

298

296

299\begin{SaveVerbatim}{showbin}

297\begin{SaveVerbatim}{showbin}

300

298

301−instance Show (Binary n) where {

299+instance Show (Binary n) where

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

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

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

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

304 show bEnd = ""

302 show bEnd = ""

305−}

306

303

307\end{SaveVerbatim}

304\end{SaveVerbatim}

308\useverb{showbin}

305\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

196\begin{SaveVerbatim}{revwhere}

197

198rev : List a -> List a

199−rev xs = revAcc [] xs where {

199+rev xs = revAcc [] xs where

200 revAcc : List a -> List a -> List a

201 revAcc acc [] = acc

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

203−}

204

203

205\end{SaveVerbatim}

204\end{SaveVerbatim}

206\useverb{revwhere}

205\useverb{revwhere}

207

206

208\noindent

207\noindent

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

209+further than the outer function.

210+

209\textbf{Scope:}

211\textbf{Scope:}

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

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

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

213clause (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:

450

452

451\begin{SaveVerbatim}{elemusing}

453\begin{SaveVerbatim}{elemusing}

452

454

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

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

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

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

455 here : Elem x (x :: xs)

457 here : Elem x (x :: xs)

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

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

457−}

458

459

459\end{SaveVerbatim}

460\end{SaveVerbatim}

460\useverb{elemusing}

461\useverb{elemusing}

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

543\begin{SaveVerbatim}{greet}

544\begin{SaveVerbatim}{greet}

544

545

545greet : IO ()

546greet : IO ()

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

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

547− name <- getLine

548+ name <- getLine

548− putStrLn ("Hello " ++ name)

549+ putStrLn ("Hello " ++ name)

549− }

550

551\end{SaveVerbatim}

552\useverb{greet}

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

554\noindent

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

556\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}.

558In 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.

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

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

561operation:

562operation:

562

563

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

847

848

848\begin{SaveVerbatim}{vfiltercons}

849\begin{SaveVerbatim}{vfiltercons}

849

850

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

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

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

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

852−}

853

854\end{SaveVerbatim}

855\useverb{vfiltercons}

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

932\begin{SaveVerbatim}{split}

933

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

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

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

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

937− }

938

937

939\end{SaveVerbatim}

938\end{SaveVerbatim}

940\useverb{split}

939\useverb{split}

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

953\begin{SaveVerbatim}{listlookup}

952\begin{SaveVerbatim}{listlookup}

954

953

955lookup_default : Nat -> List a -> a -> a

954lookup_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

957 Nothing => def

956 Nothing => def

958 | Just x => x

957 | Just x => x

959− }

960

958

961\end{SaveVerbatim}

959\end{SaveVerbatim}

962\useverb{listlookup}

960\useverb{listlookup}

tutorial/views.tex+2−4

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

36

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

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

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

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

40 | ( _ ** xs' )

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

42−}

43

42

44\end{SaveVerbatim}

43\end{SaveVerbatim}

45\useverb{vfilterdef}

44\useverb{vfilterdef}

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

86

85

87natToBin : Nat -> List Bool

86natToBin : Nat -> List Bool

88natToBin O = Nil

87natToBin O = Nil

89−natToBin k with parity k {

88+natToBin k with (parity k)

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

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

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

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

92−}

93

91

94\end{SaveVerbatim}

92\end{SaveVerbatim}

95\useverb{natToBin}

93\useverb{natToBin}