628ddcb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove captions from docs

628ddcbEdwin Brady12 years ago

docs/effects/depeff.rst+2−5

compare with master

unifiedsplit

@@ -156,13 +156,11 @@ file management follows a resource usage protocol with the following

156These requirements can be expressed formally in , by creating a

157``FILE_IO`` effect parameterised over a file handle state, which is

158either empty, open for reading, or open for writing. The ``FILE_IO``

159−effect’s definition is given in Listing :ref:`eff-fileio`. Note that this

159+effect’s definition is given below. Note that this

160effect is mainly for illustrative purposes—typically we would also like

161to support random access files and better reporting of error conditions.

162

163−.. _eff-fileio:

164.. code-block:: idris

163.. code-block:: idris

165− :caption: File I/O Effect

166

164

167 module Effect.File

165 module Effect.File

168

166

@@ -200,7 +198,6 @@ we continue the protocol accordingly.

200

198

201.. _eff-readfile:

199.. _eff-readfile:

202.. code-block:: idris

200.. code-block:: idris

203− :caption: Reading a File

204

201

205 readFile : { [FILE_IO (OpenFile Read)] } Eff (List String)

202 readFile : { [FILE_IO (OpenFile Read)] } Eff (List String)

206 readFile = readAcc [] where

203 readFile = readAcc [] where

@@ -210,7 +207,7 @@ we continue the protocol accordingly.

210 then readAcc (!readLine :: acc)

207 then readAcc (!readLine :: acc)

211 else pure (reverse acc)

208 else pure (reverse acc)

212

209

213−Given a function ``readFile`` (Listing :ref:`eff-readfile`) which reads from

210+Given a function ``readFile``, above, which reads from

214an open file until reaching the end, we can write a program which opens

211an open file until reaching the end, we can write a program which opens

215a file, reads it, then displays the contents and closes it, as follows,

212a file, reads it, then displays the contents and closes it, as follows,

216correctly following the protocol:

213correctly following the protocol:

docs/effects/hangman.rst+3−4

@@ -225,8 +225,7 @@ for the game which uses the ``MYSTERY`` effect:

225The type indicates that the game must start in a running state, with

226some guesses available, and eventually reach a not-running state (i.e.

227won or lost). The only way to achieve this is by correctly following the

228−stated rules. A possible complete implementation of ``game`` is

228+stated rules.

229−presented in Listing :ref:`mword`.

230

229

231Note that the type of ``game`` makes no assumption that there are

230Note that the type of ``game`` makes no assumption that there are

232letters to be guessed in the given word (i.e. it is ``w`` rather than

231letters to be guessed in the given word (i.e. it is ``w`` rather than

@@ -267,10 +266,10 @@ generator, then pick a random ``Fin`` to index into a list of

267 Idris’s proof search mechanism find the type. This is a

266 Idris’s proof search mechanism find the type. This is a

268 limited form of type inference, but very useful in practice.

267 limited form of type inference, but very useful in practice.

269

268

269+A possible complete implementation of ``game`` is

270+presented below:

270

271

271−.. _mword:

272.. code-block:: idris

273− :caption: Mystery Word Game Implementation

274

273

275 game : { [MYSTERY (Running (S g) w), STDIO] ==>

274 game : { [MYSTERY (Running (S g) w), STDIO] ==>

276 [MYSTERY NotRunning, STDIO] } Eff ()

275 [MYSTERY NotRunning, STDIO] } Eff ()

docs/effects/impleff.rst+24−30

@@ -156,12 +156,10 @@ new effects, however.

156Summary

157~~~~~~~

158

159−Listing :ref:`eff-statedef` summarises what is required to define the

159+The following listing summarises what is required to define the

160−``STATE`` effect.

160+``STATE`` effect:

161

162−.. _eff-statedef:

163.. code-block:: idris

162.. code-block:: idris

164− :caption: Complete State Effect Definition

165

163

166 data State : Effect where

164 data State : Effect where

167 Get : { a } State a

165 Get : { a } State a

@@ -187,7 +185,7 @@ Listing :ref:`eff-statedef` summarises what is required to define the

187Console I/O

185Console I/O

188-----------

186-----------

189

187

190−Listing :ref:`eff-stdiodef` gives the definition of the ``STDIO``

188+Then listing below gives the definition of the ``STDIO``

191effect, including handlers for ``IO`` and ``IOExcept``. We omit the

189effect, including handlers for ``IO`` and ``IOExcept``. We omit the

192definition of the top level ``Eff`` functions, as this merely invoke

190definition of the top level ``Eff`` functions, as this merely invoke

193the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.

191the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.

@@ -198,7 +196,6 @@ directly.

198

196

199.. _eff-stdiodef:

197.. _eff-stdiodef:

200.. code-block:: idris

198.. code-block:: idris

201− :caption: Console I/O Effect Definition

202

199

203 data StdIO : Effect where

200 data StdIO : Effect where

204 PutStr : String -> { () } StdIO ()

201 PutStr : String -> { () } StdIO ()

@@ -224,9 +221,14 @@ directly.

224Exceptions

221Exceptions

225----------

222----------

226

223

227−.. _eff-exceptdef:

224+The listing below gives the definition of the ``Exception``

225+effect, including two of its handlers for ``Maybe`` and ``List``. The

226+only operation provided is ``Raise``. The key point to note in the

227+definitions of these handlers is that the continuation ``k`` is not

228+used. Running ``Raise`` therefore means that computation stops with an

229+error.

230+

228.. code-block:: idris

231.. code-block:: idris

229− :caption: Exception Effect Definition

230

232

231 data Exception : Type -> Effect where

233 data Exception : Type -> Effect where

232 Raise : a -> { () } Exception a b

234 Raise : a -> { () } Exception a b

@@ -240,19 +242,17 @@ Exceptions

240 EXCEPTION : Type -> EFFECT

242 EXCEPTION : Type -> EFFECT

241 EXCEPTION t = MkEff () (Exception t)

243 EXCEPTION t = MkEff () (Exception t)

242

244

243−Listing :ref:`eff-exceptdef` gives the definition of the ``Exception``

244−effect, including two of its handlers for ``Maybe`` and ``List``. The

245−only operation provided is ``Raise``. The key point to note in the

246−definitions of these handlers is that the continuation ``k`` is not

247−used. Running ``Raise`` therefore means that computation stops with an

248−error.

249

245

250Non-determinism

246Non-determinism

251---------------

247---------------

252

248

253−.. _eff-selectdef:

249+The following listing gives the definition of the ``Select``

250+effect for writing non-deterministic programs, including a handler for

251+``List`` context which returns all possible successful values, and a

252+handler for ``Maybe`` context which returns the first successful

253+value.

254+

254.. code-block:: idris

255.. code-block:: idris

255− :caption: Non-determinism Effect Definition

256

257 data Selection : Effect where

258 Select : List a -> { () } Selection a

@@ -270,11 +270,6 @@ Non-determinism

270 SELECT : EFFECT

271 SELECT = MkEff () Selection

272

273−Listing :ref:`eff-selectdef` gives the definition of the ``Select``

274−effect for writing non-deterministic programs, including a handler for

275−``List`` context which returns all possible successful values, and a

276−handler for ``Maybe`` context which returns the first successful

277−value.

278

273

279Here, the continuation is called multiple times in each handler, for

274Here, the continuation is called multiple times in each handler, for

280each value in the list of possible values. In the ``List`` handler, we

275each value in the list of possible values. In the ``List`` handler, we

@@ -285,21 +280,13 @@ File Management

285---------------

280---------------

286

281

287Result-dependent effects are no different from non-dependent effects

282Result-dependent effects are no different from non-dependent effects

288−in the way they are implemented. Listing :ref:`eff-filedef`

283+in the way they are implemented. The listing below

289illustrates this for the ``FILE_IO`` effect. The syntax for state

284illustrates this for the ``FILE_IO`` effect. The syntax for state

290transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is

285transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is

291computed from the result of the operation ``res``, follows that for

286computed from the result of the operation ``res``, follows that for

292the equivalent ``Eff`` programs.

287the equivalent ``Eff`` programs.

293

288

294−Note that in the handler for ``Open``, the types passed to the

295−continuation ``k`` are different depending on whether the result is

296−``True`` (opening succeeded) or ``False`` (opening failed). This uses

297−``validFile``, defined in the ``Prelude``, to test whether a file

298−handler refers to an open file or not.

299−

300−.. _eff-filedef:

301.. code-block:: idris

289.. code-block:: idris

302− :caption: File I/O Effect Definition

303

290

304 data FileIO : Effect where

291 data FileIO : Effect where

305 Open : String -> (m : Mode) ->

292 Open : String -> (m : Mode) ->

@@ -327,3 +314,10 @@ handler refers to an open file or not.

327

314

328 FILE_IO : Type -> EFFECT

315 FILE_IO : Type -> EFFECT

329 FILE_IO t = MkEff t FileIO

316 FILE_IO t = MkEff t FileIO

317+

318+Note that in the handler for ``Open``, the types passed to the

319+continuation ``k`` are different depending on whether the result is

320+``True`` (opening succeeded) or ``False`` (opening failed). This uses

321+``validFile``, defined in the ``Prelude``, to test whether a file

322+handler refers to an open file or not.

323+

docs/effects/simpleeff.rst+33−42

@@ -5,12 +5,10 @@ Simple Effects

5==============

7So far we have seen how to write programs with locally mutable state

8−using the ``STATE`` effect. To recap, we have the definitions in

8+using the ``STATE`` effect. To recap, we have the definitions below

9−Listing :ref:`eff-state` in a module ``Effect.State``.

9+in a module ``Effect.State``

11−.. _eff-state:

12.. code-block:: idris

11.. code-block:: idris

13− :caption: State Effect

15 module Effect.State

13 module Effect.State

@@ -45,16 +43,14 @@ section, are summarised in Appendix :ref:`sect-appendix`.

45Console I/O

43Console I/O

46-----------

44-----------

48−Console I/O (Listing :ref:`eff-stdio`) is supported with the ``STDIO``

46+Console I/O is supported with the ``STDIO``

49effect, which allows reading and writing characters and strings to and

47effect, which allows reading and writing characters and strings to and

50from standard input and standard output. Notice that there is a

48from standard input and standard output. Notice that there is a

51constraint here on the computation context ``m``, because it only

49constraint here on the computation context ``m``, because it only

52makes sense to support console I/O operations in a context where we

50makes sense to support console I/O operations in a context where we

53−can perform (or at the very least simulate) console I/O.

51+can perform (or at the very least simulate) console I/O:

55−.. _eff-stdio:

56.. code-block:: idris

53.. code-block:: idris

57− :caption: Console I/0 Effect

59 module Effect.StdIO

55 module Effect.StdIO

@@ -138,14 +134,13 @@ than using a default value with ``run``) we can run the

138Exceptions

134Exceptions

139----------

135----------

140

136

141−Listing :ref:`eff-exception` gives the definition of the ``EXCEPTION``

137+The ``EXCEPTION``

142−effect, declared in module ``Effect.Exception``. This allows programs

138+effect is declared in module ``Effect.Exception``. This allows programs

143to exit immediately with an error, or errors to be handled more

139to exit immediately with an error, or errors to be handled more

144−generally.

140+generally:

145

141

146.. _eff-exception:

142.. _eff-exception:

147.. code-block:: idris

143.. code-block:: idris

148− :caption: Exception Effect

149

144

150 module Effect.Exception

145 module Effect.Exception

151

146

@@ -240,11 +235,9 @@ Random Numbers

240--------------

235--------------

241

236

242Random number generation is also implemented by the library, in module

237Random number generation is also implemented by the library, in module

243−``Effect.Random``. Listing :ref:`eff-random` gives its definition.

238+``Effect.Random``:

244

239

245−.. _eff-random:

246.. code-block:: idris

240.. code-block:: idris

247− :caption: Random Number Effect

248

241

249 module Effect.Random

242 module Effect.Random

250

243

@@ -282,12 +275,30 @@ correct:

282 guess : Int -> { [STDIO] } Eff ()

275 guess : Int -> { [STDIO] } Eff ()

283

276

284For reference, the code for ``guess`` is given in Listing

277For reference, the code for ``guess`` is given in Listing

285−:ref:`eff-game`. Note that we use ``parseNumber`` as defined

278+:ref:`eff-game`.

286−previously to read user input, but we don’t need to list the

287−``EXCEPTION`` effect because we use a nested ``run`` to invoke

288−``parseNumber``, independently of the calling effectful program.

289

279

280+.. _eff-game:

281+.. code-block:: idris

282+

283+ guess : Int -> { [STDIO] } Eff ()

284+ guess target

285+ = do putStr "Guess: "

286+ case run {m=Maybe} (parseNumber 100 (trim !getStr)) of

287+ Nothing => do putStrLn "Invalid input"

288+ guess target

289+ Just (v ** _) =>

290+ case compare v target of

291+ LT => do putStrLn "Too low"

292+ guess target

293+ EQ => putStrLn "You win!"

294+ GT => do putStrLn "Too high"

295+ guess target

296+

297+Note that we use ``parseNumber`` as defined previously to read user input, but

298+we don’t need to list the ``EXCEPTION`` effect because we use a nested ``run``

299+to invoke ``parseNumber``, independently of the calling effectful program.

300+

290−To invoke these, we pick a random number within the range 0–100,

301+To invoke this, we pick a random number within the range 0–100,

291having set up the random number generator with a seed, then run

302having set up the random number generator with a seed, then run

292``guess``:

303``guess``:

293

304

@@ -305,35 +316,16 @@ predictable game, some better source of randomness would be required,

305for example taking an initial seed from the system time. To see how to

316for example taking an initial seed from the system time. To see how to

306do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.

317do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.

307

318

308−.. _eff-game:

309−.. code-block:: idris

310− :caption: Guessing Game

311−

312− guess : Int -> { [STDIO] } Eff ()

313− guess target

314− = do putStr "Guess: "

315− case run {m=Maybe} (parseNumber 100 (trim !getStr)) of

316− Nothing => do putStrLn "Invalid input"

317− guess target

318− Just (v ** _) =>

319− case compare v target of

320− LT => do putStrLn "Too low"

321− guess target

322− EQ => putStrLn "You win!"

323− GT => do putStrLn "Too high"

324− guess target

325

319

326Non-determinism

320Non-determinism

327---------------

321---------------

328

322

329−Listing :ref:`eff-select` gives the definition of the non-determinism

323+The listing below gives the definition of the non-determinism

330effect, which allows a program to choose a value non-deterministically

324effect, which allows a program to choose a value non-deterministically

331from a list of possibilities in such a way that the entire computation

325from a list of possibilities in such a way that the entire computation

332−succeeds.

326+succeeds:

333

327

334−.. _eff-select:

335.. code-block:: idris

328.. code-block:: idris

336− :caption: Non-determinism Effect

337

329

338 import Effects

330 import Effects

339 import Effect.Select

331 import Effect.Select

@@ -444,7 +436,6 @@ does require that the lengths are checked and any discrepancy is dealt

444with gracefully.

436with gracefully.

445

437

446.. code-block:: idris

438.. code-block:: idris

447− :caption: Reading a vector from the console.

448

439

449 read_vec : { [STDIO] } Eff (p ** Vect p Int)

440 read_vec : { [STDIO] } Eff (p ** Vect p Int)

450 read_vec = do putStr "Number (-1 when done): "

441 read_vec = do putStr "Number (-1 when done): "

docs/tutorial/interp.rst+19−21

@@ -42,21 +42,16 @@ argument, so we define everything in a ``using`` block:

43 using (G:Vect n Ty)

45−The full representation of expressions is given in Listing :ref:`exprty`.

46−They are indexed by the types of the local variables, and the type of

45+Expressions are indexed by the types of the local variables, and the type of

47the expression itself:

46the expression itself:

49.. code-block:: idris

48.. code-block:: idris

51 data Expr : Vect n Ty -> Ty -> Type

50 data Expr : Vect n Ty -> Ty -> Type

53−Since expressions are indexed by their type, we can read the typing

52+The full representation of expressions is:

54−rules of the language from the definitions of the constructors. Let us

55−look at each constructor in turn.

57−.. _exprty:

58.. code-block:: idris

54.. code-block:: idris

59− :caption: Expression representation

61 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

56 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

62 Stop : HasType FZ (t :: G) t

57 Stop : HasType FZ (t :: G) t

@@ -73,6 +68,10 @@ look at each constructor in turn.

73 Lazy (Expr G a) ->

68 Lazy (Expr G a) ->

74 Lazy (Expr G a) -> Expr G a

69 Lazy (Expr G a) -> Expr G a

71+Since expressions are indexed by their type, we can read the typing

72+rules of the language from the definitions of the constructors. Let us

73+look at each constructor in turn.

74+

76We use a nameless representation for variables — they are *de Bruijn

75We use a nameless representation for variables — they are *de Bruijn

77indexed*. Variables are represented by a proof of their membership in

76indexed*. Variables are represented by a proof of their membership in

78the context, ``HasType i G T``, which is a proof that variable ``i``

77the context, ``HasType i G T``, which is a proof that variable ``i``

@@ -162,11 +161,19 @@ environment:

162 lookup Stop (x :: xs) = x

161 lookup Stop (x :: xs) = x

163 lookup (Pop k) (x :: xs) = lookup k xs

162 lookup (Pop k) (x :: xs) = lookup k xs

164

163

165−.. _interpdef:

164+Given this, an interpreter is a function which

165+translates an ``Expr`` into a concrete Idris value with respect to a

166+specific environment:

167+

166.. code-block:: idris

168.. code-block:: idris

167− :caption: Intepreter Definition

168

169

169 interp : Env G -> Expr G t -> interpTy t

170 interp : Env G -> Expr G t -> interpTy t

171+

172+The complete interpreter is defined as follows, for reference. For

173+each constructor, we translate it into the corresponding Idris value:

174+

175+.. code-block:: idris

176+

170 interp env (Var i) = lookup i env

177 interp env (Var i) = lookup i env

171 interp env (Val x) = x

178 interp env (Val x) = x

172 interp env (Lam sc) = \x => interp (x :: env) sc

179 interp env (Lam sc) = \x => interp (x :: env) sc

@@ -175,15 +182,8 @@ environment:

175 interp env (If x t e) = if interp env x then interp env t

182 interp env (If x t e) = if interp env x then interp env t

176 else interp env e

183 else interp env e

177

184

178−Given this, an interpreter (Listing :ref:`interpdef`) is a function which

179−translates an ``Expr`` into a concrete Idris value with respect to a

180−specific environment:

181−

182−.. code-block:: idris

183−

184− interp : Env G -> Expr G t -> interpTy t

185−

186−To translate a variable, we simply look it up in the environment:

185+Let us look at each case in turn. To translate a variable, we simply look it

186+up in the environment:

187

188.. code-block:: idris

189

@@ -263,12 +263,10 @@ function on user input:

263Here, ``cast`` is an overloaded function which converts a value from

264one type to another if possible. Here, it converts a string to an

265integer, giving 0 if the input is invalid. An example run of this

266−program at the Idris interactive environment is shown in Listing

266+program at the Idris interactive environment is:

267−:ref:`factrun`.

268

267

269

268

270.. literalinclude:: ../listing/idris-prompt-interp.txt

269.. literalinclude:: ../listing/idris-prompt-interp.txt

271− :caption: Running the well-typed interpreter

272 :name: factrun

270 :name: factrun

273

271

274Aside: ``cast``

272Aside: ``cast``

docs/tutorial/modules.rst+6−11

@@ -8,14 +8,11 @@ An Idris program consists of a collection of modules. Each module

8includes an optional ``module`` declaration giving the name of the

9module, a list of ``import`` statements giving the other modules which

10are to be imported, and a collection of declarations and definitions of

11−types, classes and functions. For example, Listing :ref:`bstmod` gives a

11+types, classes and functions. For example, the listing below gives a

12module which defines a binary tree type ``BTree`` (in a file

13−``btree.idr``) and Listing :ref:`bstmain` gives a main program (in a file

13+``btree.idr``):;

14−``bmain.idr`` which uses the ``bst`` module to sort a list.

16−.. _bstmod:

17.. code-block:: idris

15.. code-block:: idris

18− :caption: Binary Tree Module

20 module btree

17 module btree

@@ -35,9 +32,10 @@ module which defines a binary tree type ``BTree`` (in a file

35 toTree [] = Leaf

32 toTree [] = Leaf

36 toTree (x :: xs) = insert x (toTree xs)

33 toTree (x :: xs) = insert x (toTree xs)

38−.. _bstmain:

35+Then, this gives a main program (in a file

36+``bmain.idr``) which uses the ``bst`` module to sort a list::

37+

39.. code-block:: idris

38.. code-block:: idris

40− :caption: Binary Tree Main Program

42 module Main

40 module Main

@@ -99,12 +97,9 @@ and classes to be marked as: ``public``, ``abstract`` or ``private``:

99 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.

97 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.

100

101For our ``btree`` module, it makes sense for the tree data type and the

99For our ``btree`` module, it makes sense for the tree data type and the

102−functions to be exported as ``abstract``, as we see in

100+functions to be exported as ``abstract``, as we see below:

103−Listing :ref:`bstmodp`.

104

101

105−.. _bstmodp:

106.. code-block:: idris

102.. code-block:: idris

107− :caption: Binary Tree Module, with export modifiers

108

103

109 module btree

104 module btree

110

105

docs/tutorial/starting.rst+1−2

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

72This gives a ``ghci`` style interface which allows evaluation of, as

73well as type checking of, expressions; theorem proving, compilation;

74editing; and various other operations. The command ``:?`` gives a list

75−of supported commands. Listing :ref:`run1` shows an example run in

75+of supported commands. Below, we see an example run in

76which ``hello.idr`` is loaded, the type of ``main`` is checked and

77then the program is compiled to the executable ``hello``. Type

78checking a file, if successful, creates a bytecode version of the file

@@ -80,5 +80,4 @@ checking a file, if successful, creates a bytecode version of the file

80bytecode is regenerated if the source file changes.

82.. literalinclude:: ../listing/idris-prompt-helloworld.txt

83− :caption: Sample Interactive Run

84 :name: run1

83 :name: run1