b752e2d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Made tutorial and examples consistent with latest library

commitb752e2dc0f3c259033f6177f1bda49d357a9acc6 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 26 Jan 2012, 17:01 (15 years ago) parentcfc12ba

14 files changed+62−40

compare with master

unifiedsplit

CHANGELOG+2 lib/builtins.idr+3 lib/prelude/list.idr+1−1 lib/prelude/vect.idr+4−4 tutorial/examples/binary.idr+3−3 tutorial/examples/btree.idr+1−1 tutorial/examples/letbind.idr+2−2 tutorial/examples/theorems.idr+2−2 tutorial/examples/views.idr+2−2 tutorial/interp.tex+1−1 tutorial/provisional.tex+18−4 tutorial/starting.tex+3−3 tutorial/theorems.tex+5−5 tutorial/typesfuns.tex+15−12

CHANGELOG+2

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

11New in 0.9.1:

33* 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}

570.1.x to 0.9.0:

lib/builtins.idr+3

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

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

5252f $ a = f a

5353

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

55+cong refl = refl

56+

5457data Bool = False | True

5558

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

lib/prelude/list.idr+1−1

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

88%access public

10−infixr 7 ::

10+infixr 10 ::

1111

1212data List a

1313 = Nil

lib/prelude/vect.idr+4−4

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

66%access public

8−infixr 7 ::

8+infixr 10 ::

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

1111 Nil : Vect a O

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

2020lookup fO [] impossible

2121lookup (fS _) [] impossible

2222

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

24−app [] ys = ys

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

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

24+(++) [] ys = ys

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

2626

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

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

tutorial/examples/binary.idr+3−3

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

4141natToBin_lemma_1 = proof {

4242 intro;

4343 intro;

44− rewrite plusn_Sm j j;

44+ rewrite sym (plusSuccRightSucc j j);

4545 trivial;

4646}

4747

4848parity_lemma_2 = proof {

4949 intro;

5050 intro;

51− rewrite plusn_Sm j j;

51+ rewrite sym (plusSuccRightSucc j j);

5252 trivial;

5353}

5454

5555parity_lemma_1 = proof {

5656 intro j;

5757 intro;

58− rewrite plusn_Sm j j;

58+ rewrite sym (plusSuccRightSucc j j);

5959 trivial;

6060}

6161

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)

1010

1111toList : BTree a -> List a

1212toList Leaf = []

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

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

1414

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

1616toTree [] = Leaf

tutorial/examples/letbind.idr+2−2

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

11module letbind

33mirror : List a -> List a

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

5− app xs xs'

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

5+ xs ++ xs'

77data Person = MkPerson String Int

tutorial/examples/theorems.idr+2−2

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

1010

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

1212plusReducesO O = refl

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

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

1414

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

1616plusReducesS O m = refl

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

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

1818

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

2020plusReducesO' O = ?plusredO_O

tutorial/examples/views.idr+2−2

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

2323views.parity_lemma_2 = proof {

2424 intro;

2525 intro;

26− rewrite plusn_Sm j j;

26+ rewrite sym (plusSuccRightSucc j j);

2727 trivial;

2828}

2929

3030views.parity_lemma_1 = proof {

3131 intro;

3232 intro;

33− rewrite plusn_Sm j j;

33+ rewrite sym (plusSuccRightSucc j j);

3434 trivial;

3535}

3636

tutorial/interp.tex+1−1

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

339339$ idris interp.idr

340340 ____ __ _

341341 / _/___/ /____(_)____

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

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

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

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

345345

tutorial/provisional.tex+18−4

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

128128

129129\begin{SaveVerbatim}{plusnsm}

130130

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+

132134

133135\end{SaveVerbatim}

134136\useverb{plusnsm}

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

149151\useverb{prolemii}

150152

151153\noindent

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

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

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

153156

154157\begin{SaveVerbatim}{prolemr}

155158

156−-views.parity_lemma_1> rewrite plusn_Sm j j

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

157160

158161 j : Nat

159162 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

163166\end{SaveVerbatim}

164167\useverb{prolemr}

165168

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+

166180\noindent

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

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

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

268282natToBin_lemma_1 = proof {

269283 intro;

270284 intro;

271− rewrite plusn_Sm j j;

285+ rewrite sym (plusSuccRightSucc j j);

272286 trivial;

273287}

274288

tutorial/starting.tex+3−3

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

8282$ idris

8383 ____ __ _

8484 / _/___/ /____(_)____

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

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

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

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

8888

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

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

103103

104104\begin{SaveVerbatim}{cmds}

105−Idris version 0.9.0

105+Idris version 0.9.1

106106-------------------

107107

108108 Command Arguments Purpose

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

127127$ idris hello.idr

128128 ____ __ _

129129 / _/___/ /____(_)____

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

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

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

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

133133

tutorial/theorems.tex+5−5

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

6969

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

7171plusReducesO O = refl

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

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

7373

7474\end{SaveVerbatim}

7575\useverb{plusRedO}

7676

7777\noindent

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

79−equality respects successor:

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

79+equality respects function application:

8080

8181\begin{SaveVerbatim}{resps}

8282

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

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

8484

8585\end{SaveVerbatim}

8686\useverb{resps}

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

9292

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

9494plusReducesS O m = refl

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

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

9696

9797\end{SaveVerbatim}

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

194194

195195\begin{SaveVerbatim}{revwhere}

196196

197−rev : List a -> List a

198−rev xs = revAcc [] xs where

197+reverse : List a -> List a

198+reverse xs = revAcc [] xs where

199199 revAcc : List a -> List a -> List a

200200 revAcc acc [] = acc

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

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

217217

218218\begin{SaveVerbatim}{revwhereb}

219219

220−rev : List a -> List a

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

220+reverse : List a -> List a

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

222222 revAcc : List a -> List a -> List a

223223 ...

224224

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

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

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

264264The 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

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

267267

268268\begin{SaveVerbatim}{vapp}

269269

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

271−app Nil ys = ys

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

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

271+(++) Nil ys = ys

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

273273

274274\end{SaveVerbatim}

275275\useverb{vapp}

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

281281

282282\begin{SaveVerbatim}{vapperr}

283283

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

285−app Nil ys = ys

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

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

285+(++) Nil ys = ys

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

287287

288288\end{SaveVerbatim}

289289\useverb{vapperr}

290290

291291\begin{SaveVerbatim}{vapperrmsg}

292292

293−$ idris vbroken.idr --check

293+$ idris vbroken.idr --check

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

295295

296+Specifically:

297+ Can't unify k with m

298+

296299\end{SaveVerbatim}

297300\begin{SaveVerbatim}{bleh}

298301$