b752e2d · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -1,6 +1,8 @@

1New in 0.9.1:

2

3* dsl notation

4+* faster compilation (only compiling names which are used)

5+* auto implicits and default argument values {auto n : T}, {default val n : T}

4

6

50.1.x to 0.9.0:

70.1.x to 0.9.0:

6

8

lib/builtins.idr+3

@@ -51,6 +51,9 @@ infixr 1 $

51($) : (a -> b) -> a -> b

52f $ a = f a

53

54+cong : {f : t -> u} -> (a = b) -> f a = f b

55+cong refl = refl

56+

54data Bool = False | True

57data Bool = False | True

55

58

56boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a

59boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a

lib/prelude/list.idr+1−1

@@ -7,7 +7,7 @@ import prelude.nat

7

8%access public

9

10−infixr 7 ::

10+infixr 10 ::

11

12data List a

13 = Nil

lib/prelude/vect.idr+4−4

@@ -5,7 +5,7 @@ import prelude.fin

5

6%access public

7

8−infixr 7 ::

8+infixr 10 ::

9

10data Vect : Set -> Nat -> Set where

11 Nil : Vect a O

@@ -20,9 +20,9 @@ lookup (fS k) (x :: xs) = lookup k xs

20lookup fO [] impossible

21lookup (fS _) [] impossible

22

23−app : Vect a n -> Vect a m -> Vect a (n + m)

23+(++) : Vect a n -> Vect a m -> Vect a (n + m)

24−app [] ys = ys

24+(++) [] ys = ys

25−app (x :: xs) ys = x :: app xs ys

25+(++) (x :: xs) ys = x :: xs ++ ys

26

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

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

tutorial/examples/binary.idr+3−3

@@ -41,21 +41,21 @@ main = do putStr "Enter a number: "

41natToBin_lemma_1 = proof {

42 intro;

43 intro;

44− rewrite plusn_Sm j j;

44+ rewrite sym (plusSuccRightSucc j j);

45 trivial;

46}

47

48parity_lemma_2 = proof {

49 intro;

50 intro;

51− rewrite plusn_Sm j j;

51+ rewrite sym (plusSuccRightSucc j j);

52 trivial;

53}

54

55parity_lemma_1 = proof {

56 intro j;

57 intro;

58− rewrite plusn_Sm j j;

58+ rewrite sym (plusSuccRightSucc j j);

59 trivial;

60}

61

tutorial/examples/btree.idr+1−1

@@ -10,7 +10,7 @@ insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

10

11toList : BTree a -> List a

12toList Leaf = []

13−toList (Node l v r) = app (toList l) (v :: toList r)

13+toList (Node l v r) = toList l ++ (v :: toList r)

14

15toTree : Ord a => List a -> BTree a

16toTree [] = Leaf

tutorial/examples/letbind.idr+2−2

@@ -1,8 +1,8 @@

1module letbind

2

3mirror : List a -> List a

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

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

5− app xs xs'

5+ xs ++ xs'

6

7data Person = MkPerson String Int

8

tutorial/examples/theorems.idr+2−2

@@ -10,11 +10,11 @@ plusReduces n = refl

10

11plusReducesO : (n:Nat) -> n = plus n O

12plusReducesO O = refl

13−plusReducesO (S k) = eqRespS (plusReducesO k)

13+plusReducesO (S k) = cong (plusReducesO k)

14

15plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

16plusReducesS O m = refl

17−plusReducesS (S k) m = eqRespS (plusReducesS k m)

17+plusReducesS (S k) m = cong (plusReducesS k m)

18

19plusReducesO' : (n:Nat) -> n = plus n O

20plusReducesO' O = ?plusredO_O

tutorial/examples/views.idr+2−2

@@ -23,14 +23,14 @@ natToBin k with (parity k)

23views.parity_lemma_2 = proof {

24 intro;

25 intro;

26− rewrite plusn_Sm j j;

26+ rewrite sym (plusSuccRightSucc j j);

27 trivial;

28}

29

30views.parity_lemma_1 = proof {

31 intro;

32 intro;

33− rewrite plusn_Sm j j;

33+ rewrite sym (plusSuccRightSucc j j);

34 trivial;

35}

36

tutorial/interp.tex+1−1

@@ -339,7 +339,7 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

339$ idris interp.idr

340 ____ __ _

341 / _/___/ /____(_)____

342− / // __ / ___/ / ___/ Version 0.9.0

342+ / // __ / ___/ / ___/ Version 0.9.1

343 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

344 /___/\__,_/_/ /_/____/ Type :? for help

345

tutorial/provisional.tex+18−4

@@ -128,7 +128,9 @@ the prelude:

128

129\begin{SaveVerbatim}{plusnsm}

130

131−plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m)

131+plusSuccRightSucc : (left : Nat) -> (right : Nat) ->

132+ S (plus left right) = plus left (S right)

133+

132

134

133\end{SaveVerbatim}

135\end{SaveVerbatim}

134\useverb{plusnsm}

136\useverb{plusnsm}

@@ -149,11 +151,12 @@ After applying \texttt{intro} twice, we have:

149\useverb{prolemii}

151\useverb{prolemii}

150

152

151\noindent

153\noindent

154+Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,

152−Then we apply the \texttt{plusn\_Sm} function to \texttt{j} and \texttt{j}, giving:

155+to \texttt{j} and \texttt{j}, giving:

153

156

154\begin{SaveVerbatim}{prolemr}

157\begin{SaveVerbatim}{prolemr}

155

158

156−-views.parity_lemma_1> rewrite plusn_Sm j j

159+-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)

157

160

158 j : Nat

161 j : Nat

159 value : Parity (S (plus j (S j)))

162 value : Parity (S (plus j (S j)))

@@ -163,6 +166,17 @@ Then we apply the \texttt{plusn\_Sm} function to \texttt{j} and \texttt{j}, givi

163\end{SaveVerbatim}

166\end{SaveVerbatim}

164\useverb{prolemr}

167\useverb{prolemr}

165

168

169+\noindent

170+\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:

171+

172+\begin{SaveVerbatim}{sym}

173+

174+sym : l = r -> r = l

175+sym refl = refl

176+

177+\end{SaveVerbatim}

178+\useverb{sym}

179+

166\noindent

180\noindent

167We can complete this proof using the \texttt{trivial} tactic, which finds

181We can complete this proof using the \texttt{trivial} tactic, which finds

168\texttt{value} in the premisses. The proof of the second lemma proceeds in

182\texttt{value} in the premisses. The proof of the second lemma proceeds in

@@ -268,7 +282,7 @@ the proof proceeds in the same way:

268natToBin_lemma_1 = proof {

282natToBin_lemma_1 = proof {

269 intro;

283 intro;

270 intro;

284 intro;

271− rewrite plusn_Sm j j;

285+ rewrite sym (plusSuccRightSucc j j);

272 trivial;

286 trivial;

273}

287}

274

288

tutorial/starting.tex+3−3

@@ -82,7 +82,7 @@ environment. You should see something like the following:

82$ idris

83 ____ __ _

84 / _/___/ /____(_)____

85− / // __ / ___/ / ___/ Version 0.9.0

85+ / // __ / ___/ / ___/ Version 0.9.1

86 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

87 /___/\__,_/_/ /_/____/ Type :? for help

88

@@ -102,7 +102,7 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which

102the program is compiled to the executable \texttt{hello}.

103

104\begin{SaveVerbatim}{cmds}

105−Idris version 0.9.0

105+Idris version 0.9.1

106-------------------

107

108 Command Arguments Purpose

@@ -127,7 +127,7 @@ Idris version 0.9.0

127$ idris hello.idr

128 ____ __ _

129 / _/___/ /____(_)____

130− / // __ / ___/ / ___/ Version 0.9.0

130+ / // __ / ___/ / ___/ Version 0.9.1

131 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

132 /___/\__,_/_/ /_/____/ Type :? for help

133

tutorial/theorems.tex+5−5

@@ -69,18 +69,18 @@ on the first argument to \texttt{plus}, namely \texttt{n}.

69

70plusReducesO : (n:Nat) -> n = plus n O

71plusReducesO O = refl

72−plusReducesO (S k) = eqRespS (plusReducesO k)

72+plusReducesO (S k) = cong (plusReducesO k)

73

74\end{SaveVerbatim}

75\useverb{plusRedO}

76

77\noindent

78−\texttt{eqRespS} is a function defined in the library which states that

78+\texttt{cong} is a function defined in the library which states that

79−equality respects successor:

79+equality respects function application:

80

81\begin{SaveVerbatim}{resps}

82

83−eqRespS : m = n -> S m = S n

83+cong : {f : t -> u} -> a = b -> f a = f b

84

85\end{SaveVerbatim}

86\useverb{resps}

@@ -92,7 +92,7 @@ We can do the same for the reduction behaviour of plus on successors:

92

93plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

94plusReducesS O m = refl

95−plusReducesS (S k) m = eqRespS (plusReducesS k m)

95+plusReducesS (S k) m = cong (plusReducesS k m)

96

97\end{SaveVerbatim}

98\useverb{plusRedS}

tutorial/typesfuns.tex+15−12

@@ -194,8 +194,8 @@ accumulates the new, reversed list, and which does not need to be visible global

194

195\begin{SaveVerbatim}{revwhere}

196

197−rev : List a -> List a

197+reverse : List a -> List a

198−rev xs = revAcc [] xs where

198+reverse xs = revAcc [] xs where

199 revAcc : List a -> List a -> List a

200 revAcc acc [] = acc

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

@@ -217,8 +217,8 @@ behaviour, the \texttt{a} can be brought into scope as follows:

217

218\begin{SaveVerbatim}{revwhereb}

219

220−rev : List a -> List a

220+reverse : List a -> List a

221−rev {a} xs = revAcc [] xs where

221+reverse {a} xs = revAcc [] xs where

222 revAcc : List a -> List a -> List a

223 ...

224

@@ -262,14 +262,14 @@ combine to make a vector of length \texttt{S k}.

262We can define functions on dependent types such as \tTC{Vect} in the same way

263as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.

264The type of a function over \tTC{Vect} will describe what happens to the

265−lengths of the vectors involved. For example, \tFN{app}, defined in the

265+lengths of the vectors involved. For example, \tFN{++}, defined in the

266library, appends two \tTC{Vect}s:

267

268\begin{SaveVerbatim}{vapp}

269

270−app : Vect A n -> Vect A m -> Vect A (n + m)

270+(++) : Vect A n -> Vect A m -> Vect A (n + m)

271−app Nil ys = ys

271+(++) Nil ys = ys

272−app (x :: xs) ys = x :: app xs ys

272+(++) (x :: xs) ys = x :: xs ++ ys

273

274\end{SaveVerbatim}

275\useverb{vapp}

@@ -281,18 +281,21 @@ not hold, \Idris{} will not accept the definition. For example:

281

282\begin{SaveVerbatim}{vapperr}

283

284−app : Vect a n -> Vect a m -> Vect a (n + m)

284+(++) : Vect a n -> Vect a m -> Vect a (n + m)

285−app Nil ys = ys

285+(++) Nil ys = ys

286−app (x :: xs) ys = x :: app xs xs -- BROKEN

286+(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

287

288\end{SaveVerbatim}

289\useverb{vapperr}

290

291\begin{SaveVerbatim}{vapperrmsg}

292

293−$ idris vbroken.idr --check

293+$ idris vbroken.idr --check

294vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))

295

296+Specifically:

297+ Can't unify k with m

298+

296\end{SaveVerbatim}

299\end{SaveVerbatim}

297\begin{SaveVerbatim}{bleh}

300\begin{SaveVerbatim}{bleh}

298$

301$