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

git.iko.soy/Idris-dev

Remove captions from docs

(and reword a bit) since readthedocs doesn't support it in the version of sphinx it uses

commit628ddcb4b4772776b550c5ab35a772da9cd6e001 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 24 Mar 2015, 08:43 (12 years ago) parenta87a66b

7 files changed+88−115

compare with master

unifiedsplit

docs/effects/depeff.rst+2−5 docs/effects/hangman.rst+3−4 docs/effects/impleff.rst+24−30 docs/effects/simpleeff.rst+33−42 docs/tutorial/interp.rst+19−21 docs/tutorial/modules.rst+6−11 docs/tutorial/starting.rst+1−2

docs/effects/depeff.rst+2−5

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

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

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

158158either 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

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

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

162162

163−.. _eff-fileio:

164163.. code-block:: idris

165− :caption: File I/O Effect

166164

167165 module Effect.File

168166

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

200198

201199.. _eff-readfile:

202200.. code-block:: idris

203− :caption: Reading a File

204201

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

206203 readFile = readAcc [] where

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

210207 then readAcc (!readLine :: acc)

211208 else pure (reverse acc)

212209

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

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

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

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

216213correctly following the protocol:

docs/effects/hangman.rst+3−4

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

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

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

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

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

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

228+stated rules.

230229

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

232231letters 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

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

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

269268

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

270+presented below:

270271

271−.. _mword:

272272.. code-block:: idris

273− :caption: Mystery Word Game Implementation

274273

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

276275 [MYSTERY NotRunning, STDIO] } Eff ()

docs/effects/impleff.rst+24−30

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

156156Summary

157157~~~~~~~

158158

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

160−``STATE`` effect.

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

160+``STATE`` effect:

161161

162−.. _eff-statedef:

163162.. code-block:: idris

164− :caption: Complete State Effect Definition

165163

166164 data State : Effect where

167165 Get : { a } State a

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

187185Console I/O

188186-----------

189187

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

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

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

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

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

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

198196

199197.. _eff-stdiodef:

200198.. code-block:: idris

201− :caption: Console I/O Effect Definition

202199

203200 data StdIO : Effect where

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

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

224221Exceptions

225222----------

226223

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+

228231.. code-block:: idris

229− :caption: Exception Effect Definition

230232

231233 data Exception : Type -> Effect where

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

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

240242 EXCEPTION : Type -> EFFECT

241243 EXCEPTION t = MkEff () (Exception t)

242244

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.

249245

250246Non-determinism

251247---------------

252248

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+

254255.. code-block:: idris

255− :caption: Non-determinism Effect Definition

256256

257257 data Selection : Effect where

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

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

270270 SELECT : EFFECT

271271 SELECT = MkEff () Selection

272272

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.

278273

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

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

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

285280---------------

286281

287282Result-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

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

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

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

292287the equivalent ``Eff`` programs.

293288

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:

301289.. code-block:: idris

302− :caption: File I/O Effect Definition

303290

304291 data FileIO : Effect where

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

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

327314

328315 FILE_IO : Type -> EFFECT

329316 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

55==============

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

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

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

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

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

1010

11−.. _eff-state:

1211.. code-block:: idris

13− :caption: State Effect

1412

1513 module Effect.State

1614

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

4543Console I/O

4644-----------

4745

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

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

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

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

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

5250makes 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:

5452

55−.. _eff-stdio:

5653.. code-block:: idris

57− :caption: Console I/0 Effect

5854

5955 module Effect.StdIO

6056

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

138134Exceptions

139135----------

140136

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

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

137+The ``EXCEPTION``

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

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

144−generally.

140+generally:

145141

146142.. _eff-exception:

147143.. code-block:: idris

148− :caption: Exception Effect

149144

150145 module Effect.Exception

151146

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

240235--------------

241236

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

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

238+``Effect.Random``:

244239

245−.. _eff-random:

246240.. code-block:: idris

247− :caption: Random Number Effect

248241

249242 module Effect.Random

250243

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

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

283276

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

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

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.

278+:ref:`eff-game`.

289279

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

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+

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

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

292303``guess``:

293304

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

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

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

307318

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

325319

326320Non-determinism

327321---------------

328322

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

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

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

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

332−succeeds.

326+succeeds:

333327

334−.. _eff-select:

335328.. code-block:: idris

336− :caption: Non-determinism Effect

337329

338330 import Effects

339331 import Effect.Select

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

444436with gracefully.

445437

446438.. code-block:: idris

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

448439

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

450441 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:

4242

4343 using (G:Vect n Ty)

4444

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

4746the expression itself:

4847

4948.. code-block:: idris

5049

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

5251

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

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

55−look at each constructor in turn.

52+The full representation of expressions is:

5653

57−.. _exprty:

5854.. code-block:: idris

59− :caption: Expression representation

6055

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

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

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

7368 Lazy (Expr G a) ->

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

7570

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+

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

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

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

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

162161 lookup Stop (x :: xs) = x

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

164163

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+

166168.. code-block:: idris

167− :caption: Intepreter Definition

168169

169170 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+

170177 interp env (Var i) = lookup i env

171178 interp env (Val x) = x

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

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

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

176183 else interp env e

177184

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:

187187

188188.. code-block:: idris

189189

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

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

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

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

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

267−:ref:`factrun`.

266+program at the Idris interactive environment is:

268267

269268

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

271− :caption: Running the well-typed interpreter

272270 :name: factrun

273271

274272Aside: ``cast``

docs/tutorial/modules.rst+6−11

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

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

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

1010are 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

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

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

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

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

1514

16−.. _bstmod:

1715.. code-block:: idris

18− :caption: Binary Tree Module

1916

2017 module btree

2118

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

3532 toTree [] = Leaf

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

3734

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+

3938.. code-block:: idris

40− :caption: Binary Tree Main Program

4139

4240 module Main

4341

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

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

10098

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

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

103−Listing :ref:`bstmodp`.

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

104101

105−.. _bstmodp:

106102.. code-block:: idris

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

108103

109104 module btree

110105

docs/tutorial/starting.rst+1−2

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

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

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

7474editing; 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

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

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

7878checking 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

8080bytecode is regenerated if the source file changes.

8181

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

83− :caption: Sample Interactive Run

8483 :name: run1