ed93603 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix some typos and normalize the use of punctuations.

ed93603Oling Cat9 years ago

docs/st/composing.rst+16−16

compare with master

unifiedsplit

@@ -1,7 +1,7 @@

1.. _composing:

3************************

4−Composing State Machines

4+Composing State Machines

5************************

7In the previous section, we defined a ``DataStore`` interface and used it

@@ -28,7 +28,7 @@ there was a login failure in a state.

29Furthermore, we may have *hierarchies* of state machines, in that one

30state machine could be implemented by composing several others. For

31−example, we can have a state machine representing the state of a

31+example, we can have a state machine representing the state of a

32graphics system, and use this to implement a *higher level* graphics API

33such as turtle graphics, which uses the graphics system plus some additional

34state for the turtle.

@@ -50,7 +50,7 @@ count to zero, a session might run as follows:

50 *LoginCount> :exec main

51 Enter password: Mornington Crescent

52 Secret is: "Secret Data"

53− Enter password: Dollis Hill

53+ Enter password: Dollis Hill

54 Failure

55 Number of failures: 1

56 Enter password: Mornington Crescent

@@ -63,7 +63,7 @@ count to zero, a session might run as follows:

63We'll start by adding a state resource to ``getData`` to keep track of the

64number of failures:

66−.. code-block:: idrs

66+.. code-block:: idris

68 getData : (ConsoleIO m, DataStore m) =>

69 (failcount : Var) -> ST m () [failcount ::: State Integer]

@@ -116,7 +116,7 @@ match:

116 Required result states here are: st2_fn

117

118In other words, ``connect`` requires that there are *no* resources on

119−entry, but we have *one*, the failure count!

119+entry, but we have *one*, the failure count!

120This shouldn't be a problem, though: the required resources are a *subset* of

121the resources we have, after all, and the additional resources (here, the

122failure count) are not relevant to ``connect``. What we need, therefore,

@@ -214,7 +214,7 @@ ordering of resources is allowed to change, although resources which

214appear in ``old`` can't appear in the ``sub`` list more than once (you will

215get a type error if you try this).

216

217−The function ``updateWith`` takes the *output* resources of the

217+The function ``updateWith`` takes the *output* resources of the

218called function, and updates them in the current resource list. It makes

219an effort to preserve ordering as far as possible, although this isn't

220always possible if the called function does some complicated resource

@@ -338,7 +338,7 @@ representing a surface on which we'll draw lines and rectangles:

338

339.. code-block:: idris

340

341− interface Draw (m : Type -> Type) where

341+ interface Draw (m : Type -> Type) where

342 Surface : Type

343

344We'll need to be able to create a new ``Surface`` by opening a window:

@@ -369,7 +369,7 @@ succeeds (that is, returns a result of the form ``Just val``.

369 an operation returns ``Just ty``, there's also ``addIfRight``:

370

371 .. code-block:: idris

372−

372+

373 addIfJust : Type -> Action (Maybe Var)

374 addIfRight : Type -> Action (Either a Var)

375

@@ -378,10 +378,10 @@ succeeds (that is, returns a result of the form ``Just val``.

378 of an operation:

379

380 .. code-block:: idris

381−

381+

382 Add : (ty -> Resources) -> Action ty

383−

383+

384− Using this, you can create your own actions to add resources

384+ Using this, you can create your own actions to add resources

385 based on the result of an operation, if required. For example,

386 ``addIfJust`` is implemented as follows:

387

@@ -479,7 +479,7 @@ For example, assuming we have a surface ``win`` to draw onto, we can write a

479

480The ``flip win`` at the end is necessary because the drawing primitives

481are double buffered, to prevent flicker. We draw onto one buffer, off-screen,

482−and display the other. When we call ``flip``, it displays the off-screen

482+and display the other. When we call ``flip``, it displays the off-screen

483buffer, and creates a new off-screen buffer for drawing the next frame.

484

485To include this in a program, we'll write a main loop which renders our

@@ -496,7 +496,7 @@ application:

496

497Finally, we can create a main program which initialises a window, if

498possible, then runs the main loop:

499−

499+

500.. code-block:: idris

501

502 drawMain : (ConsoleIO m, Draw m) => ST m () []

@@ -593,7 +593,7 @@ is implemented using the following type, defined by ``Control.ST``:

593

594.. code-block:: idris

595

596− data Composite : List Type -> Type

596+ data Composite : List Type -> Type

597

598If we have a composite resource, we can split it into its constituent

599resources, and create new variables for each of those resources, using

@@ -604,7 +604,7 @@ the *split* function. For example:

604 splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]

605 splitComp comp = do [int, str] <- split comp

606 ?whatNow

607−

607+

608The call ``split comp`` extracts the ``State Int`` and ``State String`` from

609the composite resource ``comp``, and stores them in the variables ``int``

610and ``str`` respectively. If we check the type of ``whatNow``, we'll see

@@ -713,7 +713,7 @@ 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``

717if 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:

docs/tutorial/interactive.rst+4−5

@@ -23,7 +23,6 @@ editor, and specifically how to do so in `Vim

23for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also

24available.

26−

27Editing at the REPL

26Editing at the REPL

28===================

27===================

@@ -64,9 +63,9 @@ Editing Commands

64:addclause

63:addclause

65----------

64----------

67−The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a

66+The ``:addclause n f`` command, abbreviated ``:ac n f``, creates a

68template definition for the function named ``f`` declared on line

67template definition for the function named ``f`` declared on line

69−``n``. For example, if the code beginning on line 94 contains:

68+``n``. For example, if the code beginning on line 94 contains:

71.. code-block:: idris

70.. code-block:: idris

@@ -129,7 +128,7 @@ ys`` would lead to a unification error.

129

128

130The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

129The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

131clauses which are required to make the function ``f`` on line ``n``

130clauses which are required to make the function ``f`` on line ``n``

132−cover all inputs. For example, if the code beginning on line 94 is

131+cover all inputs. For example, if the code beginning on line 94 is:

133

132

134.. code-block:: idris

133.. code-block:: idris

135

134

@@ -143,7 +142,7 @@ then ``:am 96 vzipWith`` gives:

143

142

144 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

143 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

145

144

146−That is, it notices that there are no cases for non-empty vectors,

145+That is, it notices that there are no cases for empty vectors,

147generates the required clauses, and eliminates the clauses which would

146generates the required clauses, and eliminates the clauses which would

148lead to unification errors.

147lead to unification errors.

149

148

docs/tutorial/interfaces.rst+6−7

@@ -11,8 +11,8 @@ data types. For example, we would like arithmetic operators to work on

11to display different types in a uniform way.

13To achieve this, we use *interfaces*, which are similar to type classes in

14−Haskell or traits in Rust. To define an interface, we provide a collection of

14+Haskell or traits in Rust. To define an interface, we provide a collection of

15−overloadable functions. A simple example is the ``Show``

15+overloadable functions. A simple example is the ``Show``

16interface, which is defined in the prelude and provides an interface for

17converting values to ``String``:

@@ -31,8 +31,7 @@ This generates a function of the following type (which we call a

31We can read this as: “under the constraint that ``a`` has an implementation

32of ``Show``, take an input ``a`` and return a ``String``.” An implementation

33of an interface is defined by giving definitions of the methods of the interface.

34−For example, the

35−``Show`` implementation for ``Nat`` could be defined as:

34+For example, the ``Show`` implementation for ``Nat`` could be defined as:

37.. code-block:: idris

36.. code-block:: idris

@@ -49,7 +48,7 @@ Only one implementation of an interface can be given for a type — implementati

49not overlap. Implementation declarations can themselves have constraints.

48not overlap. Implementation declarations can themselves have constraints.

50To help with resolution, the arguments of an implementation must be

49To help with resolution, the arguments of an implementation must be

51constructors (either data or type constructors) or variables

50constructors (either data or type constructors) or variables

52−(i.e. you cannot give an implementation for a function). For

51+(i.e. you cannot give an implementation for a function). For

53example, to define a ``Show`` implementation for vectors, we need to know

52example, to define a ``Show`` implementation for vectors, we need to know

54that there is a ``Show`` implementation for the element type, because we are

53that there is a ``Show`` implementation for the element type, because we are

55going to use it to convert each element to a ``String``:

54going to use it to convert each element to a ``String``:

@@ -534,7 +533,7 @@ Named Implementations

534

533

535It can be desirable to have multiple implementations of an interface for the

534It can be desirable to have multiple implementations of an interface for the

536same type, for example to provide alternative methods for sorting or printing

535same type, for example to provide alternative methods for sorting or printing

537−values. To achieve this, implementations can be *named* as follows:

536+values. To achieve this, implementations can be *named* as follows:

538

537

539.. code-block:: idris

538.. code-block:: idris

540

539

@@ -574,7 +573,7 @@ the prelude defines the following ``Semigroup`` interface:

574 interface Semigroup ty where

573 interface Semigroup ty where

575 (<+>) : ty -> ty -> ty

574 (<+>) : ty -> ty -> ty

576

575

577−Then it defines ``Monoid``, which extends ``Semigroup`` with a "neutral"

576+Then it defines ``Monoid``, which extends ``Semigroup`` with a “neutral”

578value:

577value:

579

578

580.. code-block:: idris

579.. code-block:: idris

docs/tutorial/interp.rst+2−2

@@ -106,7 +106,7 @@ the ``Var`` constructor:

106

107 Var : HasType i G t -> Expr G t

108

109−So, in an expression ``\x,\y. x y``, the variable ``x`` would have a

109+So, in an expression ``\x. \y. x y``, the variable ``x`` would have a

110de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,

111represented as ``Stop``. We find these by counting the number of

112lambdas between the definition and the use.

@@ -194,7 +194,7 @@ each constructor, we translate it into the corresponding Idris value:

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

195 else interp env e

196

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

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

198up in the environment:

199

200.. code-block:: idris

docs/tutorial/miscellany.rst+19−19

@@ -8,7 +8,7 @@ In this section we discuss a variety of additional features:

9+ auto, implicit, and default arguments;

10+ literate programming;

11−+ interfacing with external libraries through the foreign function

11++ interfacing with external libraries through the foreign function;

12+ interface;

13+ type providers;

14+ code generation; and

@@ -23,7 +23,7 @@ omitted when they can be inferred by the type checker, e.g.

23.. code-block:: idris

25 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

26−

26+

27Auto implicit arguments

28------------------------

@@ -69,17 +69,17 @@ In the case that a proof is not found, it can be provided explicitly as normal:

69.. code-block:: idris

71 head xs {p = ?headProof}

72−

72+

73Default implicit arguments

74---------------------------

76−Besides having Idris automatically find a value of a given type, sometimes we

76+Besides having Idris automatically find a value of a given type, sometimes we

77want to have an implicit argument with a specific default value. In Idris, we can

78do this using the ``default`` annotation. While this is primarily intended to assist

79−in automatically constructing a proof where auto fails, or finds an unhelpful value,

79+in automatically constructing a proof where auto fails, or finds an unhelpful value,

80−it might be easier to first consider a simpler case, not involving proofs.

80+it might be easier to first consider a simpler case, not involving proofs.

82−If we want to compute the n'th fibonacci number (and defining the 0th fibonacci

82+If we want to compute the n'th fibonacci number (and defining the 0th fibonacci

83number as 0), we could write:

85.. code-block:: idris

@@ -89,8 +89,8 @@ number as 0), we could write:

89 fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n

91After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,

92−and will return the 5th fibonacci number. Note that while this works, this is not the

92+and will return the 5th fibonacci number. Note that while this works, this is not the

93−intended use of the ``default`` annotation. It is included here for illustrative purposes

93+intended use of the ``default`` annotation. It is included here for illustrative purposes

94only. Usually, ``default`` is used to provide things like a custom proof search script.

@@ -329,13 +329,13 @@ are available in an external collection [1]_.

329C Target

330========

331

332−The default target of Idris is C. Compiling via :

332+The default target of Idris is C. Compiling via:

333

334::

335

336 $ idris hello.idr -o hello

337

338−is equivalent to :

338+is equivalent to:

339

340::

341

@@ -344,14 +344,14 @@ is equivalent to :

344When the command above is used, a temporary C source is generated, which

345is then compiled into an executable named ``hello``.

346

347−In order to view the generated C code, compile via :

347+In order to view the generated C code, compile via:

348

349::

350

351 $ idris hello.idr -S -o hello.c

352

353To turn optimisations on, use the ``%flag C`` pragma within the code, as

354−is shown below :

354+is shown below:

355

356.. code-block:: idris

357

@@ -368,7 +368,7 @@ is shown below :

368

369To compile the generated C with debugging information e.g. to use

370``gdb`` to debug segmentation faults in Idris programs, use the

371−``%flag C`` pragma to include debugging symbols, as is shown below :

371+``%flag C`` pragma to include debugging symbols, as is shown below:

372

373.. code-block:: idris

374

@@ -503,13 +503,13 @@ And for use in the browser:

503

504The given files will be added to the top of the generated code.

505For library packages you can also use the ipkg objs option to include the

506−js file in the installation, and use

506+js file in the installation, and use:

507

508.. code-block:: idris

509

510 %include Node "package/external.js"

511

512−This javascript and node backends idris will also lookup for the file on

512+The *JavaScript* and *NodeJS* backends of Idris will also lookup for the file

513on that location.

514

515Including *NodeJS* modules

@@ -552,7 +552,7 @@ types themselves have types. For example:

552 *universe> :t Vect

553 Vect : Nat -> Type -> Type

554

555−But what about the type of ``Type``? If we ask Idris it reports

555+But what about the type of ``Type``? If we ask Idris it reports:

556

557::

558

@@ -560,8 +560,8 @@ But what about the type of ``Type``? If we ask Idris it reports

560 Type : Type 1

561

562If ``Type`` were its own type, it would lead to an inconsistency due to

563−`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_ , so internally there is a

563+`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,

564−*hierarchy* of types (or *universes*):

564+so internally there is a *hierarchy* of types (or *universes*):

565

566.. code-block:: idris

567

docs/tutorial/modules.rst+8−11

@@ -53,8 +53,7 @@ Then, this gives a main program (in a file

53 print (Btree.toList t)

55The same names can be defined in multiple modules: names are *qualified* with

56−the name of the module. The names defined in the ``Btree`` module are, in

56+the name of the module. The names defined in the ``Btree`` module are, in full:

57−full:

59+ ``Btree.BTree``

58+ ``Btree.BTree``

60+ ``Btree.Leaf``

59+ ``Btree.Leaf``

@@ -74,7 +73,7 @@ directories. For example, ``import foo.bar`` would import the file

74``foo/bar.idr``, which would conventionally have the module declaration

73``foo/bar.idr``, which would conventionally have the module declaration

75``module foo.bar``. The only requirement for module names is that the

74``module foo.bar``. The only requirement for module names is that the

76main module, with the ``main`` function, must be called

75main module, with the ``main`` function, must be called

77−``Main``—although its filename need not be ``Main.idr``.

76+``Main`` — although its filename need not be ``Main.idr``.

79Export Modifiers

78Export Modifiers

80================

79================

@@ -82,18 +81,16 @@ Export Modifiers

82Idris allows for fine-grained control over the visibility of a

81Idris allows for fine-grained control over the visibility of a

83module's contents. By default, all names defined in a module are kept

82module's contents. By default, all names defined in a module are kept

84private. This aides in specification of a minimal interface and for

83private. This aides in specification of a minimal interface and for

85−internal details to be left hidden. Idris allows for functions,

84+internal details to be left hidden. Idris allows for functions,

86types, and interfaces to be marked as: ``private``, ``export``, or

85types, and interfaces to be marked as: ``private``, ``export``, or

87−``public export``. Their general meaning is as follows:

86+``public export``. Their general meaning is as follows:

89−- ``private`` meaning that it's not exported at all. This is the

88+- ``private`` meaning that it's not exported at all. This is the default.

90− default.

92- ``export`` meaning that its top level type is exported.

90- ``export`` meaning that its top level type is exported.

94- ``public export`` meaning that the entire definition is exported.

92- ``public export`` meaning that the entire definition is exported.

96−

97A further restriction in modifying the visibility is that definitions

94A further restriction in modifying the visibility is that definitions

98must not refer to anything within a lower level of visibility. For

95must not refer to anything within a lower level of visibility. For

99example, ``public export`` definitions cannot use private names, and

96example, ``public export`` definitions cannot use private names, and

@@ -129,10 +126,9 @@ Meaning for Data Types

129

126

130For data types, the meanings are:

127For data types, the meanings are:

131

128

132−- ``export`` the type constructor is exported

129+- ``export`` the type constructor is exported

133

130

134−- ``public export`` the type constructor and data constructors are

131+- ``public export`` the type constructor and data constructors are exported

135− exported

136

132

137

133

138Meaning for Interfaces

134Meaning for Interfaces

@@ -141,6 +137,7 @@ Meaning for Interfaces

141For interfaces, the meanings are:

137For interfaces, the meanings are:

142

138

143- ``export`` the interface name is exported

139- ``export`` the interface name is exported

140+

144- ``public export`` the interface name, method names and default

141- ``public export`` the interface name, method names and default

145 definitions are exported

142 definitions are exported

146

143

docs/tutorial/packages.rst+39−29

@@ -1,26 +1,31 @@

1+.. _sect-packages:

1********

3********

2Packages

4Packages

3********

5********

5−

6−Idris includes a simple build system for building packages and executables from a named package description file.

7+Idris includes a simple build system for building packages and executables

8+from a named package description file. These files can be used with the

7−These files can be used with the Idris compiler to manage the development process .

9+Idris compiler to manage the development process .

9Package Descriptions

11Package Descriptions

10====================

12====================

12A package description includes the following:

14A package description includes the following:

14−+ A header, consisting of the keyword package followed by the package

16++ A header, consisting of the keyword ``package`` followed by a package

15 name. Package names can be any valid Idris identifier. The iPKG

17 name. Package names can be any valid Idris identifier. The iPKG

16 format also takes a quoted version that accepts any valid filename.

18 format also takes a quoted version that accepts any valid filename.

19+

17−+ Fields describing package contents, ``<field> = <value>``

20++ Fields describing package contents, ``<field> = <value>``.

19At least one field must be the modules field, where the value is a

22At least one field must be the modules field, where the value is a

20−comma separated list of modules. For example, given an idris package

23+comma separated list of modules. For example, given an idris package

21``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,

24``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,

22``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding

25``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding

23−package file would be::

26+package file would be:

27+

28+::

25 package maths

30 package maths

@@ -38,7 +43,6 @@ of the main Idris repository, and in `third-party libraries

38Using Package files

43Using Package files

39===================

44===================

41−

42Idris itself is aware about packages, and special commands are

46Idris itself is aware about packages, and special commands are

43available to help with, for example, building packages, installing

47available to help with, for example, building packages, installing

44packages, and cleaning packages. For instance, given the ``maths``

48packages, and cleaning packages. For instance, given the ``maths``

@@ -54,7 +58,9 @@ package from earlier we can use Idris as follows:

55Once the maths package has been installed, the command line option

59Once the maths package has been installed, the command line option

56``--package maths`` makes it accessible (abbreviated to ``-p maths``).

60``--package maths`` makes it accessible (abbreviated to ``-p maths``).

57−For example::

61+For example:

62+

63+::

59 idris -p maths Main.idr

65 idris -p maths Main.idr

@@ -66,20 +72,18 @@ The integrated build system includes a simple testing framework.

66This framework collects functions listed in the ``ipkg`` file under ``tests``.

72This framework collects functions listed in the ``ipkg`` file under ``tests``.

67All test functions must return ``IO ()``.

73All test functions must return ``IO ()``.

69−

70When you enter ``idris --testpkg yourmodule.ipkg``,

75When you enter ``idris --testpkg yourmodule.ipkg``,

71the build system creates a temporary file in a fresh environment on your machine

76the build system creates a temporary file in a fresh environment on your machine

72by listing the ``tests`` functions under a single ``main`` function.

77by listing the ``tests`` functions under a single ``main`` function.

73It compiles this temporary file to an executable and then executes it.

78It compiles this temporary file to an executable and then executes it.

75−

76The tests themselves are responsible for reporting their success or failure.

80The tests themselves are responsible for reporting their success or failure.

77Test functions commonly use ``putStrLn`` to report test results.

81Test functions commonly use ``putStrLn`` to report test results.

78The test framework does not impose any standards for reporting and consequently

82The test framework does not impose any standards for reporting and consequently

79does not aggregate test results.

83does not aggregate test results.

81−

82−For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

85+For example, lets take the following list of functions that are defined in a

86+module called ``NumOps`` for a sample package ``maths``:

84.. name: Math/NumOps.idr

88.. name: Math/NumOps.idr

85.. code-block:: idris

89.. code-block:: idris

@@ -94,7 +98,8 @@ For example, lets take the following list of functions that are defined in a mod

94 triple : Num a => a -> a

98 triple : Num a => a -> a

95 triple a = a + double a

99 triple a = a + double a

100

101+

97−A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

102+A simple test module, with a qualified name of ``Test.NumOps`` can be declared as:

103

99.. name: Math/TestOps.idr

104.. name: Math/TestOps.idr

100.. code-block:: idris

105.. code-block:: idris

@@ -122,8 +127,11 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a

122 testTriple = assertNotEq (triple 2) 5

127 testTriple = assertNotEq (triple 2) 5

123

128

124

129

125−The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.

130+The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing,

131+and failing, equality tests. The actual tests are ``testDouble`` and ``testTriple``,

126−The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::

132+and are declared in the ``maths.ipkg`` file as follows:

133+

134+::

127

135

128 package maths

136 package maths

129

137

@@ -134,7 +142,9 @@ The actual tests are ``testDouble`` and ``testTriple``, and are declared in the

134 , Test.NumOps.testTriple

142 , Test.NumOps.testTriple

135

143

136

144

137−The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

145+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``:

146+

147+::

138

148

139 > idris --testpkg maths.ipkg

149 > idris --testpkg maths.ipkg

140 Type checking ./Maths/NumOps.idr

150 Type checking ./Maths/NumOps.idr

@@ -146,25 +156,25 @@ The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

146Note how both tests have reported success by printing ``Test Passed``

156Note how both tests have reported success by printing ``Test Passed``

147as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

157as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

148

158

149−Package Dependencies Using Atom

159+Package Dependencies Using Atom

150===============================

160===============================

151

161

152−If you are using the Atom editor and have a dependency on another package,

162+If you are using the Atom editor and have a dependency on another package,

153−corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,

163+corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,

154−you need to let Atom know that it should be loaded. The easiest way to

164+you need to let Atom know that it should be loaded. The easiest way to

155−accomplish that is with a .ipkg file. The general contents of an ipkg file

165+accomplish that is with a .ipkg file. The general contents of an ipkg file

156−will be described in the next section of the tutorial, but for now here is

166+will be described in the next section of the tutorial, but for now here is

157−a simple recipe for this trivial case.

167+a simple recipe for this trivial case:

158

168

159−- Create a folder myProject.

169+- Create a folder myProject.

160

170

161−- Add a file myProject.ipkg containing just a couple of lines:

171+- Add a file myProject.ipkg containing just a couple of lines:

162

172

163−``package myProject``

173+``package myProject``

164

174

165−``pkgs = pruviloj, lightyear``

175+``pkgs = pruviloj, lightyear``

166

176

167−- In Atom, use the File menu to Open Folder myProject.

177+- In Atom, use the File menu to Open Folder myProject.

168

178

169More information

179More information

170================

180================

docs/tutorial/syntax.rst+4−4

@@ -34,7 +34,7 @@ rule, and the right hand side describes its expansion. The syntax rule

34itself consists of:

36- **Keywords** — here, ``if``, ``then`` and ``else``, which must be

37− valid identifiers

37+ valid identifiers.

39- **Non-terminals** — included in square brackets, ``[test]``, ``[t]``

40 and ``[e]`` here, which stand for arbitrary expressions. To avoid

@@ -44,9 +44,9 @@ itself consists of:

44- **Names** — included in braces, which stand for names which may be

45 bound on the right hand side.

47−- **Symbols** — included in quotations marks, e.g. ``:=``. This can

47+- **Symbols** — included in quotations marks, e.g. ``":="``. This can

48 also be used to include reserved words in syntax rules, such as

49− ``let`` or ``in``.

49+ ``"let"`` or ``"in"``.

51The limitations on the form of a syntax rule are that it must include

52at least one symbol or keyword, and there must be no repeated

@@ -63,7 +63,7 @@ recursive. The following syntax extensions would therefore be valid:

63 syntax select [x] from [t] "where" [w] = SelectWhere x t w;

64 syntax select [x] from [t] = Select x t;

66−Syntax macros can be further restricted to apply only in patterns (i.e.,

66+Syntax macros can be further restricted to apply only in patterns (i.e.

67only on the left hand side of a pattern match clause) or only in terms

68(i.e. everywhere but the left hand side of a pattern match clause) by

69being marked as ``pattern`` or ``term`` syntax rules. For example, we

docs/tutorial/theorems.rst+3−3

@@ -115,8 +115,8 @@ We can do the same for the reduction behaviour of plus on successors:

115

116Even for trivial theorems like these, the proofs are a little tricky to

117construct in one go. When things get even slightly more complicated, it

118−becomes too much to think about to construct proofs in this ‘batch

118+becomes too much to think about to construct proofs in this “batch

119−mode’.

119+mode”.

120

121Idris provides interactive editing capabilities, which can help with

122building proofs. For more details on building proofs interactively in

@@ -383,7 +383,7 @@ will always be smaller than ``(x :: xs)``:

383 = qsort (filter (< x) xs) ++

384 (x :: qsort (filter (>= x) xs))

385

386−The function ``assert_smaller``, defined in the Prelude, is intended to

386+The function ``assert_smaller``, defined in the prelude, is intended to

387address this problem:

388

389.. code-block:: idris

docs/tutorial/typesfuns.rst+22−30

@@ -13,8 +13,7 @@ manipulation, and ``Ptr`` which represents foreign pointers. There are

13also several data types declared in the library, including ``Bool``,

14with values ``True`` and ``False``. We can declare some constants with

15these types. Enter the following into a file ``Prims.idr`` and load it

16−into the Idris interactive environment by typing ``idris

16+into the Idris interactive environment by typing ``idris Prims.idr``:

17−Prims.idr``:

19.. code-block:: idris

18.. code-block:: idris

@@ -38,7 +37,7 @@ collection of declarations and definitions. In this example no imports

38have been specified. However Idris programs can consist of several

37have been specified. However Idris programs can consist of several

39modules and the definitions in each module each have their own

38modules and the definitions in each module each have their own

40namespace. This is discussed further in Section

39namespace. This is discussed further in Section

41−:ref:`sect-namespaces`). When writing Idris programs both the order in which

40+:ref:`sect-namespaces`. When writing Idris programs both the order in which

42definitions are given and indentation are significant. Functions and

41definitions are given and indentation are significant. Functions and

43data types must be defined before use, incidentally each definition must

42data types must be defined before use, incidentally each definition must

44have a type declaration, for example see ``x : Int``, ``foo :

43have a type declaration, for example see ``x : Int``, ``foo :

@@ -343,7 +342,7 @@ Vectors

343

342

344A standard example of a dependent data type is the type of “lists with

343A standard example of a dependent data type is the type of “lists with

345length”, conventionally called vectors in the dependent type

344length”, conventionally called vectors in the dependent type

346−literature. They are available as part of the Idris library, by

345+literature. They are available as part of the Idris library, by

347importing ``Data.Vect``, or we can declare them as follows:

346importing ``Data.Vect``, or we can declare them as follows:

348

347

349.. code-block:: idris

348.. code-block:: idris

@@ -521,8 +520,8 @@ help document a function by making the purpose of an argument more

521clear.

520clear.

522

521

523Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.

522Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.

524−``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";

523+``{var = pat}`` gets an implicit variable and attempts to pattern match on “pat”;

525−For example :

524+For example:

526

525

527.. code-block:: idris

526.. code-block:: idris

528

527

@@ -559,7 +558,6 @@ vector. For example:

559 inVect : IsElem 5 Main.testVec

558 inVect : IsElem 5 Main.testVec

560 inVect = There (There Here)

559 inVect = There (There Here)

561

560

562−

563.. important:: Implicit Arguments and Scope

561.. important:: Implicit Arguments and Scope

564

562

565 Within the type signature the typechecker will treat all variables

563 Within the type signature the typechecker will treat all variables

@@ -569,7 +567,6 @@ vector. For example:

569 ``testVec``. In the example above, we have assumed that the code

567 ``testVec``. In the example above, we have assumed that the code

570 lives within the ``Main`` module.

568 lives within the ``Main`` module.

571

569

572−

573If the same implicit arguments are being used a lot, it can make a

570If the same implicit arguments are being used a lot, it can make a

574definition difficult to read. To avoid this problem, a ``using`` block

571definition difficult to read. To avoid this problem, a ``using`` block

575gives the types and ordering of any implicit arguments which can

572gives the types and ordering of any implicit arguments which can

@@ -582,15 +579,13 @@ appear within the block:

582 Here : IsElem x (x :: xs)

579 Here : IsElem x (x :: xs)

583 There : IsElem x xs -> IsElem x (y :: xs)

580 There : IsElem x xs -> IsElem x (y :: xs)

584

581

585−

586−

587Note: Declaration Order and ``mutual`` blocks

582Note: Declaration Order and ``mutual`` blocks

588~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

583~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

589

584

590In general, functions and data types must be defined before use, since

585In general, functions and data types must be defined before use, since

591dependent types allow functions to appear as part of types, and type

586dependent types allow functions to appear as part of types, and type

592checking can rely on how particular functions are defined (though this

587checking can rely on how particular functions are defined (though this

593−is only true of total functions; see Section :ref:`sect-totality`)).

588+is only true of total functions; see Section :ref:`sect-totality`).

594However, this restriction can be relaxed by using a ``mutual`` block,

589However, this restriction can be relaxed by using a ``mutual`` block,

595which allows data types and functions to be defined simultaneously:

590which allows data types and functions to be defined simultaneously:

596

591

@@ -673,7 +668,7 @@ Note that several of these return ``Either``, since they may fail.

673I/O programs will typically need to sequence actions, feeding the

668I/O programs will typically need to sequence actions, feeding the

674output of one computation into the input of the next. ``IO`` is an

669output of one computation into the input of the next. ``IO`` is an

675abstract type, however, so we can’t access the result of a computation

670abstract type, however, so we can’t access the result of a computation

676−directly. Instead, we sequence operations with ``do`` notation:

671+directly. Instead, we sequence operations with ``do`` notation:

677

672

678.. code-block:: idris

673.. code-block:: idris

679

674

@@ -713,7 +708,7 @@ not always the best approach. Consider the following function:

713

708

714This function uses one of the ``t`` or ``e`` arguments, but not both

709This function uses one of the ``t`` or ``e`` arguments, but not both

715(in fact, this is used to implement the ``if...then...else`` construct

710(in fact, this is used to implement the ``if...then...else`` construct

716−as we will see later. We would prefer if *only* the argument which was

711+as we will see later). We would prefer if *only* the argument which was

717used was evaluated. To achieve this, Idris provides a ``Lazy``

712used was evaluated. To achieve this, Idris provides a ``Lazy``

718data type, which allows evaluation to be suspended:

713data type, which allows evaluation to be suspended:

719

714

@@ -797,7 +792,7 @@ infinite loop and cause a stack overflow.

797To fix this we must add explicit ``Inf`` declarations to the constructor

792To fix this we must add explicit ``Inf`` declarations to the constructor

798parameter types, since codata will not add it to constructor parameters of a

793parameter types, since codata will not add it to constructor parameters of a

799**different** type from the one being defined. For example, the following

794**different** type from the one being defined. For example, the following

800−outputs "1".

795+outputs ``1``.

801

796

802.. code-block:: idris

797.. code-block:: idris

803

798

@@ -902,7 +897,7 @@ For more details of the functions available on ``List`` and

902

897

903- ``libs/base/Data/VectType.idr``

898- ``libs/base/Data/VectType.idr``

904

899

905−Functions include filtering, appending, reversing, and so on.

900+Functions include filtering, appending, reversing, and so on.

906

901

907Aside: Anonymous functions and operator sections

902Aside: Anonymous functions and operator sections

908~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

903~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -999,7 +994,7 @@ Dependent Pairs

999---------------

994---------------

1000

995

1001Dependent pairs allow the type of the second element of a pair to depend

996Dependent pairs allow the type of the second element of a pair to depend

1002−on the value of the first element.

997+on the value of the first element:

1003

998

1004.. code-block:: idris

999.. code-block:: idris

1005

1000

@@ -1009,7 +1004,7 @@ on the value of the first element.

1009Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

1004Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

1010of a pair of A and P, where the name ``a`` can occur inside ``P``.

1005of a pair of A and P, where the name ``a`` can occur inside ``P``.

1011``( a ** p )`` constructs a value of this type. For example, we can

1006``( a ** p )`` constructs a value of this type. For example, we can

1012−pair a number with a ``Vect`` of a particular length.

1007+pair a number with a ``Vect`` of a particular length:

1013

1008

1014.. code-block:: idris

1009.. code-block:: idris

1015

1010

@@ -1017,7 +1012,7 @@ pair a number with a ``Vect`` of a particular length.

1017 vec = (2 ** [3, 4])

1012 vec = (2 ** [3, 4])

1018

1013

1019If you like, you can write it out the long way, the two are precisely

1014If you like, you can write it out the long way, the two are precisely

1020−equivalent.

1015+equivalent:

1021

1016

1022.. code-block:: idris

1017.. code-block:: idris

1023

1018

@@ -1070,7 +1065,7 @@ intermediate values:

1070

1065

1071We will see more on ``with`` notation later.

1066We will see more on ``with`` notation later.

1072

1067

1073−Dependent pairs are sometimes referred to as “sigma types”.

1068+Dependent pairs are sometimes referred to as “Sigma types”.

1074

1069

1075Records

1070Records

1076-------

1071-------

@@ -1080,7 +1075,7 @@ Records

1080automatically generating field access and update functions. Unlike

1075automatically generating field access and update functions. Unlike

1081the syntax used for data structures, records in Idris follow a

1076the syntax used for data structures, records in Idris follow a

1082different syntax to that seen with Haskell. For example, we can

1077different syntax to that seen with Haskell. For example, we can

1083−represent a person's name and age in a record:

1078+represent a person’s name and age in a record:

1084

1079

1085.. code-block:: idris

1080.. code-block:: idris

1086

1081

@@ -1092,12 +1087,11 @@ represent a person's name and age in a record:

1092 fred : Person

1087 fred : Person

1093 fred = MkPerson "Fred" "Joe" "Bloggs" 30

1088 fred = MkPerson "Fred" "Joe" "Bloggs" 30

1094

1089

1095−

1096The constructor name is provided using the ``constructor`` keyword,

1090The constructor name is provided using the ``constructor`` keyword,

1097and the *fields* are then given which are in an indented block

1091and the *fields* are then given which are in an indented block

1098following the `where` keyword (here, ``firstName``, ``middleName``,

1092following the `where` keyword (here, ``firstName``, ``middleName``,

1099``lastName``, and ``age``). You can declare multiple fields on a

1093``lastName``, and ``age``). You can declare multiple fields on a

1100−single line, provided that they have the same type. The field names

1094+single line, provided that they have the same type. The field names

1101can be used to access the field values:

1095can be used to access the field values:

1102

1096

1103::

1097::

@@ -1171,7 +1165,7 @@ syntax:

1171 record { a->b->c = val } x

1165 record { a->b->c = val } x

1172

1166

1173This returns a new record, with the field accessed by the path

1167This returns a new record, with the field accessed by the path

1174−``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {

1168+``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {

1175a->b->c = val }`` itself has a function type. Symmetrically, the field

1169a->b->c = val }`` itself has a function type. Symmetrically, the field

1176can also be accessed with the following syntax:

1170can also be accessed with the following syntax:

1177

1171

@@ -1196,12 +1190,10 @@ name. For example, a pair type could be defined as follows:

1196 fst : a

1190 fst : a

1197 snd : b

1191 snd : b

1198

1192

1199−

1200Using the ``class`` record from earlier, the size of the class can be

1193Using the ``class`` record from earlier, the size of the class can be

1201restricted using a ``Vect`` and the size included in the type by parameterising

1194restricted using a ``Vect`` and the size included in the type by parameterising

1202the record with the size. For example:

1195the record with the size. For example:

1203

1196

1204−

1205.. code-block:: idris

1197.. code-block:: idris

1206

1198

1207 record SizedClass (size : Nat) where

1199 record SizedClass (size : Nat) where

@@ -1214,7 +1206,7 @@ function from earlier, since that would change the size of the class. A

1214function to add a student must now specify in the type that the

1206function to add a student must now specify in the type that the

1215size of the class has been increased by one. As the size is specified

1207size of the class has been increased by one. As the size is specified

1216using natural numbers, the new value can be incremented using the

1208using natural numbers, the new value can be incremented using the

1217−``S`` constructor.

1209+``S`` constructor:

1218

1210

1219.. code-block:: idris

1211.. code-block:: idris

1220

1212

@@ -1327,7 +1319,7 @@ matching ``let`` and lambda bindings. It will *only* work if:

1327- Each branch *matches* a value of the same type, and *returns* a

1319- Each branch *matches* a value of the same type, and *returns* a

1328 value of the same type.

1320 value of the same type.

1329

1321

1330−- The type of the result is "known". i.e. the type of the expression

1322+- The type of the result is “known”. i.e. the type of the expression

1331 can be determined *without* type checking the ``case``-expression

1323 can be determined *without* type checking the ``case``-expression

1332 itself.

1324 itself.

1333

1325

@@ -1337,7 +1329,7 @@ Totality

1337Idris distinguishes between *total* and *partial* functions.

1329Idris distinguishes between *total* and *partial* functions.

1338A total function is a function that either:

1330A total function is a function that either:

1339

1331

1340−+ Terminates for all possible inputs, or

1332++ Terminates for all possible inputs, or

1341+ Produces a non-empty, finite, prefix of a possibly infinite result

1333+ Produces a non-empty, finite, prefix of a possibly infinite result

1342

1334

1343If a function is total, we can consider its type a precise description of what

1335If a function is total, we can consider its type a precise description of what

@@ -1345,12 +1337,12 @@ that function will do. For example, if we have a function with a return

1345type of ``String`` we know something different, depending on whether or not

1337type of ``String`` we know something different, depending on whether or not

1346it's total:

1338it's total:

1347

1339

1348−+ If it's total, it will return a value of type ``String`` in finite time

1340++ If it's total, it will return a value of type ``String`` in finite time;

1349+ If it's partial, then as long as it doesn't crash or enter an infinite loop,

1341+ If it's partial, then as long as it doesn't crash or enter an infinite loop,

1350 it will return a ``String``.

1342 it will return a ``String``.

1351

1343

1352Idris makes this distinction so that it knows which functions are safe to

1344Idris makes this distinction so that it knows which functions are safe to

1353−evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,

1345+evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,

1354if it tries to evaluate a function during type checking which doesn't

1346if it tries to evaluate a function during type checking which doesn't

1355terminate, then type checking won't terminate!

1347terminate, then type checking won't terminate!

1356Therefore, only total functions will be evaluated during type checking.

1348Therefore, only total functions will be evaluated during type checking.