16ee8cf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

fix some more typos

16ee8cfAlex Gryzlov9 years ago

docs/st/composing.rst+5−5

compare with master

unifiedsplit

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

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

349

350However, 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

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

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

354``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

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

658of type ``State ()``.

659

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

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

662is the following:

663

664.. code-block:: idris

665

666 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 ()))

668

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

670a 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:

713 Line : Type

714 Line = ((Int, Int), (Int, Int), Col)

715

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

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

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

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

719into a composite resource for the turtle:

720

docs/st/examples.rst+3−3

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

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

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

227so 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``:

229

230.. code-block:: idris

231

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

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

341 echoServer sock =

342 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

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

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

346 close new; remove new; echoServer sock

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

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

430state machines to implement a high level network communication protocol

431in 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

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

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

435by Edwin Brady.

docs/st/machines.rst+4−4

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

352

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

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

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

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

356

357.. code-block:: idris

358

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

367 disconnect st

368

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

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

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

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

372

373.. code::

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

383Implementing the interface

384==========================

385

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

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

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

388follows:

389

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

526using a concrete context ``IO``.

527

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

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

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

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

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

532state 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) ->

306 Split : (lbl : Var) ->

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

308 STrans m (VarList vars) res

309− (\ vs => mkRes vs ++

309+ (\vs => mkRes vs ++

310 updateRes res prf (State ()))

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

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

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

456split : (lbl : Var) ->

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

458 STrans m (VarList vars) res

459− (\ vs => mkRes vs ++

459+ (\vs => mkRes vs ++

460 updateRes res prf (State ()))

461split lbl {prf} = Split lbl prf

462