64c5f70 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3831 from clayrat/patch-2

fix a few typos in Control.ST tutorial

commit64c5f70267f70011ff4f2bf34ea2872358f44e24 authorNiklas Larsson <metaniklas@gmail.com> dateFri 2 Jun 2017, 22:31 (9 years ago) parent4d8350c b60dc36

4 files changed+14−14

compare with master

unifiedsplit

docs/st/composing.rst+5−5 docs/st/examples.rst+3−3 docs/st/machines.rst+4−4 libs/contrib/Control/ST.idr+2−2

docs/st/composing.rst+5−5

@@ -348,7 +348,7 @@ We'll need to be able to create a new ``Surface`` by opening a window:

348348 initWindow : Int -> Int -> ST m Var [add Surface]

349349

350350However, this isn't quite right. It's possible that opening a window

351−will fail, for example if our program is running in a termina without

351+will fail, for example if our program is running in a terminal without

352352a windowing system available. So, somehow, ``initWindow`` needs to cope

353353with the possibility of failure. We can do this by returning a

354354``Maybe Var``, rather than a ``Var``, and only adding the ``Surface``

@@ -657,14 +657,14 @@ resources and merge them into one composite resource. Before we run

657657``combine``, the target resource must exist (``comp`` here) and must be

658658of type ``State ()``.

659659

660−It is instructive to look at the types of ``split`` and combine to see

660+It is instructive to look at the types of ``split`` and ``combine`` to see

661661the requirements on resource lists they work with. The type of ``split``

662662is the following:

663663

664664.. code-block:: idris

665665

666666 split : (lbl : Var) -> {auto prf : InState lbl (Composite vars) res} ->

667− STrans m (VarList vars) res (\ vs => mkRes vs ++ updateRes res prf (State ()))

667+ STrans m (VarList vars) res (\vs => mkRes vs ++ updateRes res prf (State ()))

668668

669669The implicit ``prf`` argument says that the ``lbl`` being split must be

670670a composite resource. It returns a variable list, built from the composite

@@ -713,8 +713,8 @@ A ``Line`` is defined as a start location, and end location, and a colour:

713713 Line : Type

714714 Line = ((Int, Int), (Int, Int), Col)

715715

716−To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``)

717−if this is impossible, we begin by initialising the drawing surface then

716+To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``

717+if this is impossible), we begin by initialising the drawing surface then

718718all of the components of the state. Finally, we combine all of these

719719into a composite resource for the turtle:

720720

docs/st/examples.rst+3−3

@@ -225,7 +225,7 @@ and uses the ``ConsoleIO`` and ``Sockets`` interfaces:

225225The first thing we need to do is create a socket for binding to a port

226226and listening for incoming connections, using ``socket``. This might fail,

227227so we'll need to deal with the case where it returns ``Right sock``, where

228−``sock`` is the new socket variable, or wher it returns ``Left err``:

228+``sock`` is the new socket variable, or where it returns ``Left err``:

229229

230230.. code-block:: idris

231231

@@ -340,7 +340,7 @@ connection:

340340 ST m () [remove sock (Sock {m} Listening)]

341341 echoServer sock =

342342 do Right new <- accept sock | Left err => do close sock; remove sock

343− Right msg <- recv new | Left err => do close sock; remove sock; remove ne

343+ Right msg <- recv new | Left err => do close sock; remove sock; remove new

344344 Right ok <- send new ("You said " ++ msg)

345345 | Left err => do remove new; close sock; remove sock

346346 close new; remove new; echoServer sock

@@ -429,7 +429,7 @@ find the complete echo server there, ``EchoServer.idr``. There is also

429429a higher level network protocol, ``RandServer.idr``, using a hierarchy of

430430state machines to implement a high level network communication protocol

431431in terms of the lower level sockets API. This also uses threading, to

432−handle incoming requests asyncronously. You can find some more detail

432+handle incoming requests asynchronously. You can find some more detail

433433on threading and the random number server in the draft paper

434434`State Machines All The Way Down <https://www.idris-lang.org/drafts/sms.pdf>`_

435435by Edwin Brady.

docs/st/machines.rst+4−4

@@ -352,7 +352,7 @@ than directly with ``delete``.

352352

353353We can complete ``getData`` as follows, using a pattern matching bind

354354alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a

355−``case`` statement to catch the possibilty of an error with ``login``:

355+``case`` statement to catch the possibility of an error with ``login``:

356356

357357.. code-block:: idris

358358

@@ -367,7 +367,7 @@ alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a

367367 disconnect st

368368

369369We can't yet try this out, however, because we don't have any implementations

370−of ``getData``! If we try to execute it in an ``IO`` context, for example,

370+of ``DataStore``! If we try to execute it in an ``IO`` context, for example,

371371we'll get an error saying that there's no implementation of ``DataStore IO``:

372372

373373.. code::

@@ -383,7 +383,7 @@ of ``DataStore``.

383383Implementing the interface

384384==========================

385385

386−To execute ``getData`` in ``IO``, we'll need to provided an implementation

386+To execute ``getData`` in ``IO``, we'll need to provide an implementation

387387of ``DataStore`` which works in the ``IO`` context. We can begin as

388388follows:

389389

@@ -526,7 +526,7 @@ like ``getData``, and constrain by only the interfaces we need, rather than

526526using a concrete context ``IO``.

527527

528528We've now seen how to manipulate states, and how to encapsulate state

529−transitions for a specific system like the data store inn an interface.

529+transitions for a specific system like the data store in an interface.

530530However, realistic systems will need to *compose* state machines. We'll

531531either need to use more than one state machine at a time, or implement one

532532state machine in terms of one or more others. We'll see how to achieve this

libs/contrib/Control/ST.idr+2−2

@@ -306,7 +306,7 @@ data STrans : (m : Type -> Type) ->

306306 Split : (lbl : Var) ->

307307 (prf : InState lbl (Composite vars) res) ->

308308 STrans m (VarList vars) res

309− (\ vs => mkRes vs ++

309+ (\vs => mkRes vs ++

310310 updateRes res prf (State ()))

311311 Combine : (comp : Var) -> (vs : List Var) ->

312312 (prf : VarsIn (comp :: vs) res) ->

@@ -456,7 +456,7 @@ export

456456split : (lbl : Var) ->

457457 {auto prf : InState lbl (Composite vars) res} ->

458458 STrans m (VarList vars) res

459− (\ vs => mkRes vs ++

459+ (\vs => mkRes vs ++

460460 updateRes res prf (State ()))

461461split lbl {prf} = Split lbl prf

462462