Remove captions from docs

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

docs/effects/depeff.rst

@@ -156,13 +156,11 @@ file management follows a resource usage protocol with the following
 These requirements can be expressed formally in , by creating a
 ``FILE_IO`` effect parameterised over a file handle state, which is
 either empty, open for reading, or open for writing. The ``FILE_IO``
-effect’s definition is given in Listing :ref:`eff-fileio`. Note that this
+effect’s definition is given below. Note that this
 effect is mainly for illustrative purposes—typically we would also like
 to support random access files and better reporting of error conditions.
 
-.. _eff-fileio:
 .. code-block:: idris
-    :caption: File I/O Effect
 
     module Effect.File
 
@@ -200,7 +198,6 @@ we continue the protocol accordingly.
 
 .. _eff-readfile:
 .. code-block:: idris
-    :caption: Reading a File
 
     readFile : { [FILE_IO (OpenFile Read)] } Eff (List String)
     readFile = readAcc [] where
@@ -210,7 +207,7 @@ we continue the protocol accordingly.
                          then readAcc (!readLine :: acc)
                          else pure (reverse acc)
 
-Given a function ``readFile`` (Listing :ref:`eff-readfile`) which reads from
+Given a function ``readFile``, above, which reads from
 an open file until reaching the end, we can write a program which opens
 a file, reads it, then displays the contents and closes it, as follows,
 correctly following the protocol:

docs/effects/hangman.rst

@@ -225,8 +225,7 @@ for the game which uses the ``MYSTERY`` effect:
 The type indicates that the game must start in a running state, with
 some guesses available, and eventually reach a not-running state (i.e.
 won or lost). The only way to achieve this is by correctly following the
-stated rules. A possible complete implementation of ``game`` is
-presented in Listing :ref:`mword`.
+stated rules. 
 
 Note that the type of ``game`` makes no assumption that there are
 letters 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
     Idris’s proof search mechanism find the type. This is a
     limited form of type inference, but very useful in practice.
 
+A possible complete implementation of ``game`` is
+presented below: 
 
-.. _mword:
 .. code-block:: idris
-    :caption: Mystery Word Game Implementation
 
     game : { [MYSTERY (Running (S g) w), STDIO] ==>
              [MYSTERY NotRunning, STDIO] } Eff ()

docs/effects/impleff.rst

@@ -156,12 +156,10 @@ new effects, however.
 Summary
 ~~~~~~~
 
-Listing :ref:`eff-statedef` summarises what is required to define the
-``STATE`` effect.
+The following listing summarises what is required to define the
+``STATE`` effect:
 
-.. _eff-statedef:
 .. code-block:: idris
-    :caption: Complete State Effect Definition
 
     data State : Effect where
          Get :      { a }       State a
@@ -187,7 +185,7 @@ Listing :ref:`eff-statedef` summarises what is required to define the
 Console I/O
 -----------
 
-Listing :ref:`eff-stdiodef` gives the definition of the ``STDIO``
+Then listing below gives the definition of the ``STDIO``
 effect, including handlers for ``IO`` and ``IOExcept``. We omit the
 definition of the top level ``Eff`` functions, as this merely invoke
 the effects ``PutStr``, ``GetStr``, ``PutCh`` and ``GetCh`` directly.
@@ -198,7 +196,6 @@ directly.
 
 .. _eff-stdiodef:
 .. code-block:: idris
-    :caption: Console I/O Effect Definition
 
     data StdIO : Effect where
          PutStr : String -> { () } StdIO ()
@@ -224,9 +221,14 @@ directly.
 Exceptions
 ----------
 
-.. _eff-exceptdef:
+The listing below gives the definition of the ``Exception``
+effect, including two of its handlers for ``Maybe`` and ``List``. The
+only operation provided is ``Raise``. The key point to note in the
+definitions of these handlers is that the continuation ``k`` is not
+used. Running ``Raise`` therefore means that computation stops with an
+error.
+
 .. code-block:: idris
-    :caption: Exception Effect Definition
 
     data Exception : Type -> Effect where
          Raise : a -> { () } Exception a b
@@ -240,19 +242,17 @@ Exceptions
     EXCEPTION : Type -> EFFECT
     EXCEPTION t = MkEff () (Exception t)
 
-Listing :ref:`eff-exceptdef` gives the definition of the ``Exception``
-effect, including two of its handlers for ``Maybe`` and ``List``. The
-only operation provided is ``Raise``. The key point to note in the
-definitions of these handlers is that the continuation ``k`` is not
-used. Running ``Raise`` therefore means that computation stops with an
-error.
 
 Non-determinism
 ---------------
 
-.. _eff-selectdef:
+The following listing gives the definition of the ``Select``
+effect for writing non-deterministic programs, including a handler for
+``List`` context which returns all possible successful values, and a
+handler for ``Maybe`` context which returns the first successful
+value.
+
 .. code-block:: idris
-    :caption: Non-determinism Effect Definition
 
     data Selection : Effect where
          Select : List a -> { () } Selection a
@@ -270,11 +270,6 @@ Non-determinism
     SELECT : EFFECT
     SELECT = MkEff () Selection
 
-Listing :ref:`eff-selectdef` gives the definition of the ``Select``
-effect for writing non-deterministic programs, including a handler for
-``List`` context which returns all possible successful values, and a
-handler for ``Maybe`` context which returns the first successful
-value.
 
 Here, the continuation is called multiple times in each handler, for
 each value in the list of possible values. In the ``List`` handler, we
@@ -285,21 +280,13 @@ File Management
 ---------------
 
 Result-dependent effects are no different from non-dependent effects
-in the way they are implemented. Listing :ref:`eff-filedef`
+in the way they are implemented. The listing below 
 illustrates this for the ``FILE_IO`` effect. The syntax for state
 transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is
 computed from the result of the operation ``res``, follows that for
 the equivalent ``Eff`` programs.
 
-Note that in the handler for ``Open``, the types passed to the
-continuation ``k`` are different depending on whether the result is
-``True`` (opening succeeded) or ``False`` (opening failed). This uses
-``validFile``, defined in the ``Prelude``, to test whether a file
-handler refers to an open file or not.
-
-.. _eff-filedef:
 .. code-block:: idris
-    :caption: File I/O Effect Definition
 
     data FileIO : Effect where
          Open  : String -> (m : Mode) ->
@@ -327,3 +314,10 @@ handler refers to an open file or not.
 
     FILE_IO : Type -> EFFECT
     FILE_IO t = MkEff t FileIO
+
+Note that in the handler for ``Open``, the types passed to the
+continuation ``k`` are different depending on whether the result is
+``True`` (opening succeeded) or ``False`` (opening failed). This uses
+``validFile``, defined in the ``Prelude``, to test whether a file
+handler refers to an open file or not.
+

docs/effects/simpleeff.rst

@@ -5,12 +5,10 @@ Simple Effects
 ==============
 
 So far we have seen how to write programs with locally mutable state
-using the ``STATE`` effect. To recap, we have the definitions in
-Listing :ref:`eff-state` in a module ``Effect.State``.
+using the ``STATE`` effect. To recap, we have the definitions below
+in a module ``Effect.State``
 
-.. _eff-state:
 .. code-block:: idris
-    :caption: State Effect
 
     module Effect.State
 
@@ -45,16 +43,14 @@ section, are summarised in Appendix :ref:`sect-appendix`.
 Console I/O
 -----------
 
-Console I/O (Listing :ref:`eff-stdio`) is supported with the ``STDIO``
+Console I/O is supported with the ``STDIO``
 effect, which allows reading and writing characters and strings to and
 from standard input and standard output. Notice that there is a
 constraint here on the computation context ``m``, because it only
 makes sense to support console I/O operations in a context where we
-can perform (or at the very least simulate) console I/O.
+can perform (or at the very least simulate) console I/O:
 
-.. _eff-stdio:
 .. code-block:: idris
-    :caption: Console I/0 Effect
 
     module Effect.StdIO
 
@@ -138,14 +134,13 @@ than using a default value with ``run``) we can run the
 Exceptions
 ----------
 
-Listing :ref:`eff-exception` gives the definition of the ``EXCEPTION``
-effect, declared in module ``Effect.Exception``. This allows programs
+The ``EXCEPTION``
+effect is declared in module ``Effect.Exception``. This allows programs
 to exit immediately with an error, or errors to be handled more
-generally.
+generally:
 
 .. _eff-exception:
 .. code-block:: idris
-    :caption: Exception Effect
 
     module Effect.Exception
 
@@ -240,11 +235,9 @@ Random Numbers
 --------------
 
 Random number generation is also implemented by the library, in module
-``Effect.Random``. Listing :ref:`eff-random` gives its definition.
+``Effect.Random``:
 
-.. _eff-random:
 .. code-block:: idris
-   :caption: Random Number Effect
 
     module Effect.Random
 
@@ -282,12 +275,30 @@ correct:
     guess : Int -> { [STDIO] } Eff ()
 
 For reference, the code for ``guess`` is given in Listing
-:ref:`eff-game`.  Note that we use ``parseNumber`` as defined
-previously to read user input, but we don’t need to list the
-``EXCEPTION`` effect because we use a nested ``run`` to invoke
-``parseNumber``, independently of the calling effectful program.
+:ref:`eff-game`.  
 
-To invoke these, we pick a random number within the range 0–100,
+.. _eff-game:
+.. code-block:: idris
+
+    guess : Int -> { [STDIO] } Eff ()
+    guess target
+        = do putStr "Guess: "
+             case run {m=Maybe} (parseNumber 100 (trim !getStr)) of
+                  Nothing => do putStrLn "Invalid input"
+                                guess target
+                  Just (v ** _) =>
+                             case compare v target of
+                                 LT => do putStrLn "Too low"
+                                          guess target
+                                 EQ => putStrLn "You win!"
+                                 GT => do putStrLn "Too high"
+                                          guess target
+
+Note that we use ``parseNumber`` as defined previously to read user input, but
+we don’t need to list the ``EXCEPTION`` effect because we use a nested ``run``
+to invoke ``parseNumber``, independently of the calling effectful program.
+
+To invoke this, we pick a random number within the range 0–100,
 having set up the random number generator with a seed, then run
 ``guess``:
 
@@ -305,35 +316,16 @@ predictable game, some better source of randomness would be required,
 for example taking an initial seed from the system time. To see how to
 do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.
 
-.. _eff-game:
-.. code-block:: idris
-    :caption: Guessing Game
-
-    guess : Int -> { [STDIO] } Eff ()
-    guess target
-        = do putStr "Guess: "
-             case run {m=Maybe} (parseNumber 100 (trim !getStr)) of
-                  Nothing => do putStrLn "Invalid input"
-                                guess target
-                  Just (v ** _) =>
-                             case compare v target of
-                                 LT => do putStrLn "Too low"
-                                          guess target
-                                 EQ => putStrLn "You win!"
-                                 GT => do putStrLn "Too high"
-                                          guess target
 
 Non-determinism
 ---------------
 
-Listing :ref:`eff-select` gives the definition of the non-determinism
+The listing below gives the definition of the non-determinism
 effect, which allows a program to choose a value non-deterministically
 from a list of possibilities in such a way that the entire computation
-succeeds.
+succeeds:
 
-.. _eff-select:
 .. code-block:: idris
-   :caption: Non-determinism Effect
 
     import Effects
     import Effect.Select
@@ -444,7 +436,6 @@ does require that the lengths are checked and any discrepancy is dealt
 with gracefully.
 
 .. code-block:: idris
-    :caption: Reading a vector from the console.
 
     read_vec : { [STDIO] } Eff (p ** Vect p Int)
     read_vec = do putStr "Number (-1 when done): "