83ff2b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2047 from jfdm/userdocs/package-creation

Add section on package creation, and typo fixes.

commit83ff2b65162cb06debfa12364b8115f2270e9843 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateSun 22 Mar 2015, 21:36 (12 years ago) parentc4f31c4 c093a9a

21 files changed+169−90

compare with master

unifiedsplit

docs/effects/conclusions.rst+1−1

@@ -5,7 +5,7 @@ Further Reading

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

77This tutorial has given an introduction to writing and reasoning about

8−side-effecting programs in ``Idris``, using the ``Effects`` library.

8+side-effecting programs in Idris, using the ``Effects`` library.

99More details about the *implementation* of the library, such as how

1010``run`` works, how handlers are invoked, etc, are given in a separate

1111paper [1]_.

docs/effects/hangman.rst+1−1

@@ -264,7 +264,7 @@ generator, then pick a random ``Fin`` to index into a list of

264264.. note::

265265 Rather than have to explicitly declare a type with the vector’s

266266 length, it is convenient to give a metavariable ``?wtype`` and let

267− ``Idris``’s proof search mechanism find the type. This is a

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

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

269269

270270

docs/effects/introduction.rst+5−5

@@ -14,10 +14,10 @@ and supports programming and reasoning with side-effecting programs,

1414supporting mutable state, interaction with the outside world,

1515exceptions, and verified resource management.

1616

17−This tutorial assumes familiarity with pure programming in ``Idris``,

17+This tutorial assumes familiarity with pure programming in Idris,

1818as described in Sections 1–6 of the main tutorial [1]_. The examples

19−are presented are tested with ``Idris`` and can be found in the

20−examples directory of the ``Idris`` repository.

19+are presented are tested with Idris and can be found in the

20+examples directory of the Idris repository.

2121

2222Consider, for example, the following introductory function which

2323illustrates the kind of properties which can be expressed in the type

@@ -47,7 +47,7 @@ able to apply the ``vadd`` function? Before doing so, we will have to:

4747

4848The complete program will include side-effects for I/O and error

4949handling, before we can get to the pure core functionality. In this

50−tutorial, we will see how ``Idris`` supports side-effects.

50+tutorial, we will see how Idris supports side-effects.

5151Furthermore, we will see how we can use the dependent type system to

5252*reason* about stateful and side-effecting programs. We will return to

5353this specific example later.

@@ -78,7 +78,7 @@ returns the unit value. All programs using the ``Effects`` library must

7878``import Effects``. The details of the ``Eff`` type will be presented in the

7979remainder of this tutorial.

8080

81−To compile and run this program, ``Idris`` needs to be told to include

81+To compile and run this program, Idris needs to be told to include

8282the ``Effects`` package, using the ``-p effects`` flag (this flag is

8383required for all examples in this tutorial):

8484

docs/effects/simpleeff.rst+1−1

@@ -592,7 +592,7 @@ which ``eval`` can be ``run`` to those which support ``STDIO``, such

592592as ``IO``. Once effect lists get longer, it can be a good idea instead

593593to encapsulate sets of effects in a type synonym. This is achieved as

594594follows, simply by defining a function which computes a type, since

595−types are first class in ``Idris``:

595+types are first class in Idris:

596596

597597.. code-block:: idris

598598

docs/effects/state.rst+1−1

@@ -77,7 +77,7 @@ explicit.

7777Introducing ``Effects``

7878-----------------------

7979

80−``Idris`` provides a library, ``Effects`` [3]_, which captures this

80+Idris provides a library, ``Effects`` [3]_, which captures this

8181pattern and many others involving effectful computation [1]_. An

8282effectful program ``f`` has a type of the following form:

8383

docs/index.rst+1

@@ -35,6 +35,7 @@ The Idris Tutorial

3535 tutorial/typesfuns

3636 tutorial/classes

3737 tutorial/modules

38+ tutorial/packages

3839 tutorial/interp

3940 tutorial/views

4041 tutorial/theorems

docs/reference/erasure.rst+4−4

@@ -94,11 +94,11 @@ cannot get below O(n) with time complexities.

9494One could argue that Idris in fact compiles ``Nat`` via GMP but

9595that's a moot point for two reasons:

9696

97−* First, whenever we try to index our datastructures with anything

98−else than ``Nat``, the compiler is not going to come to the rescue.

97++ First, whenever we try to index our datastructures with anything

98+ else than ``Nat``, the compiler is not going to come to the rescue.

9999

100−* Second, even with ``Nat``, the GMP integers are *still* there and

101−they slow the runtime down.

100++ Second, even with ``Nat``, the GMP integers are *still* there and

101+ they slow the runtime down.

102102

103103This ought not to be the case since the ``Nat`` are never used at

104104runtime and they are only there for typechecking purposes. Hence we

docs/tutorial/classes.rst+2−2

@@ -366,7 +366,7 @@ Rather than having to insert ``m_app`` everywhere there is an

366366application, we can use to do the job for us. To do this, we can make

367367``Maybe`` an instance of ``Applicative`` as follows, where ``<>`` is

368368defined in the same way as ``m_app`` above (this is defined in the

369−``Idris`` library):

369+Idris library):

370370

371371.. code-block:: idris

372372

@@ -481,7 +481,7 @@ Given the following list:

481481 testList = [3,4,1]

482482

483483We can sort it using the default ``Ord`` instance, then the named

484−instance ``myord`` as follows, at the ``Idris`` prompt:

484+instance ``myord`` as follows, at the Idris prompt:

485485

486486::

487487

docs/tutorial/conclusions.rst+4−4

@@ -4,10 +4,10 @@

44Further Reading

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

7−Further information about ``Idris`` programming, and programming with

7+Further information about Idris programming, and programming with

88dependent types in general, can be obtained from various sources:

10−- The ``Idris`` web site (http://idris-lang.org/) and by asking

10+- The Idris web site (http://idris-lang.org/) and by asking

1111 questions on the mailing list.

1212

1313- The IRC channel ``#idris``, on

@@ -21,14 +21,14 @@ dependent types in general, can be obtained from various sources:

2121 - https://github.com/idris-lang/Idris-dev/wiki/Language-Features

2222

2323- Examining the prelude and exploring the ``samples`` in the

24− distribution. The ``Idris`` source can be found online at:

24+ distribution. The Idris source can be found online at:

2525 https://github.com/idris-lang/Idris-dev.

2626

2727- Existing projects on the ``Idris Hackers`` web space:

2828 http://idris-hackers.github.io.

2929

3030- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly

31− describe older versions of ``Idris``.

31+ describe older versions of Idris.

3232

3333.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems

3434 programming with embedded domain specific languages. In

docs/tutorial/index.rst+1

@@ -23,6 +23,7 @@ The is the Idris Tutorial. It will teach you about programming in the Idris Lang

2323 typesfuns

2424 classes

2525 modules

26+ packages

2627 interp

2728 views

2829 theorems

docs/tutorial/interactive.rst+3−3

@@ -4,7 +4,7 @@

44Interactive Editing

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

7−By now, we have seen several examples of how ``Idris``’ dependent type

7+By now, we have seen several examples of how Idris’ dependent type

88system can give extra confidence in a function’s correctness by giving

99a more precise description of its intended behaviour in its *type*. We

1010have also seen an example of how the type system can help with EDSL

@@ -13,7 +13,7 @@ object language. However, precise types give us more than verification

1313of programs — we can also exploit types to help write programs which

1414are *correct by construction*.

1515

16−The ``Idris`` REPL provides several commands for inspecting and

16+The Idris REPL provides several commands for inspecting and

1717modifying parts of programs, based on their types, such as case

1818splitting on a pattern variable, inspecting the type of a

1919metavariable, and even a basic proof search mechanism. In this

@@ -121,7 +121,7 @@ according to the same heuristic. If we update the file (using

121121 vzipWith f [] [] = ?vzipWith_rhs_3

122122

123123That is, the pattern variable ``ys`` has been split into one case

124−``[]``, ``Idris`` having noticed that the other possible case ``y ::

124+``[]``, Idris having noticed that the other possible case ``y ::

125125ys`` would lead to a unification error.

126126

127127:addmissing

docs/tutorial/interp.rst+6−6

@@ -22,7 +22,7 @@ booleans, and functions, represented by ``Ty``:

2222 data Ty = TyInt | TyBool | TyFun Ty Ty

2323

2424We can write a function to translate these representations to a concrete

25−``Idris`` type — remember that types are first class, so can be

25+Idris type — remember that types are first class, so can be

2626calculated just like any other value:

2727

2828.. code-block:: idris

@@ -176,7 +176,7 @@ environment:

176176 else interp env e

177177

178178Given this, an interpreter (Listing :ref:`interpdef`) is a function which

179−translates an ``Expr`` into a concrete ``Idris`` value with respect to a

179+translates an ``Expr`` into a concrete Idris value with respect to a

180180specific environment:

181181

182182.. code-block:: idris

@@ -199,7 +199,7 @@ value:

199199Lambdas are more interesting. In this case, we construct a function

200200which interprets the scope of the lambda with a new value in the

201201environment. So, a function in the object language is translated to an

202−``Idris`` function:

202+Idris function:

203203

204204.. code-block:: idris

205205

@@ -214,8 +214,8 @@ because of its type:

214214 interp env (App f s) = interp env f (interp env s)

215215

216216Operators and interpreters are, again, direct translations into the

217−equivalent ``Idris`` constructs. For operators, we apply the function to

218−its operands directly, and for ``If``, we apply the ``Idris``

217+equivalent Idris constructs. For operators, we apply the function to

218+its operands directly, and for ``If``, we apply the Idris

219219``if...then...else`` construct directly.

220220

221221.. code-block:: idris

@@ -263,7 +263,7 @@ 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

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

267267:ref:`factrun`.

268268

269269

docs/tutorial/introduction.rst+4−4

@@ -35,10 +35,10 @@ following type to the ``app`` function, which concatenates vectors:

3535

3636 app : Vect n a -> Vect m a -> Vect (n + m) a

3737

38−This tutorial introduces ``Idris``, a general purpose functional

39−programming language with dependent types. The goal of the ``Idris``

38+This tutorial introduces Idris, a general purpose functional

39+programming language with dependent types. The goal of the Idris

4040project is to build a dependently typed language suitable for

41−verifiable *systems* programming. To this end, ``Idris`` is a compiled

41+verifiable *systems* programming. To this end, Idris is a compiled

4242language which aims to generate efficient executable code. It also has

4343a lightweight foreign function interface which allows easy interaction

4444with external ``C`` libraries.

@@ -58,7 +58,7 @@ Example Code

5858------------

5959

6060This tutorial includes some example code, which has been tested with

61−``Idris`` version . The files are available in the ``Idris``

61+Idris version . The files are available in the Idris

6262distribution, and provided along side the tutorial source, so that you

6363can try them out easily, under ``tutorial/examples``. However, it is

6464strongly recommended that you can type them in yourself, rather than

docs/tutorial/miscellany.rst+17−17

@@ -48,7 +48,7 @@ this to happen silently. We define ``head`` as follows:

4848 head : (xs : List a) -> {auto p : isCons xs = True} -> a

4949 head (x :: xs) = x

5050

51−The ``auto`` annotation on the implicit argument means that ``Idris``

51+The ``auto`` annotation on the implicit argument means that Idris

5252will attempt to fill in the implicit argument using the ``trivial``

5353tactic, which searches through the context for a proof, and tries to

5454solve with ``refl`` if a proof is not found. Now when ``head`` is

@@ -72,7 +72,7 @@ to:

7272Implicit conversions

7373--------------------

7474

75−``Idris`` supports the creation of *implicit conversions*, which allow

75+Idris supports the creation of *implicit conversions*, which allow

7676automatic conversion of values from one type to another when required to

7777make a term type correct. This is intended to increase convenience and

7878reduce verbosity. A contrived but simple example is the following:

@@ -101,7 +101,7 @@ beyond the scope of this tutorial.

101101Literate programming

102102--------------------

103103

104−Like Haskell, ``Idris`` supports *literate* programming. If a file has

104+Like Haskell, Idris supports *literate* programming. If a file has

105105an extension of ``.lidr`` then it is assumed to be a literate file. In

106106literate programs, everything is assumed to be a comment unless the line

107107begins with a greater than sign ``>``, for example:

@@ -124,7 +124,7 @@ Foreign function calls

124124

125125For practical programming, it is often necessary to be able to use

126126external libraries, particularly for interfacing with the operating

127−system, file system, networking, *et cetera*. ``Idris`` provides a

127+system, file system, networking, *et cetera*. Idris provides a

128128lightweight foreign function interface for achieving this, as part of

129129the prelude. For this, we assume a certain amount of knowledge of C and

130130the ``gcc`` compiler. First, we define a datatype which describes the

@@ -136,7 +136,7 @@ external types we can handle:

136136

137137Each of these corresponds directly to a C type. Respectively: ``int``,

138138``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a

139−translation to a concrete ``Idris`` type, described by the following

139+translation to a concrete Idris type, described by the following

140140function:

141141

142142.. code-block:: idris

@@ -150,7 +150,7 @@ function:

150150 interpFTy FUnit = ()

151151

152152A foreign function is described by a list of input types and a return

153−type, which can then be converted to an ``Idris`` type:

153+type, which can then be converted to an Idris type:

154154

155155.. code-block:: idris

156156

@@ -170,7 +170,7 @@ A foreign function is assumed to be impure, so ``ForeignTy`` builds an

170170We build a call to a foreign function by giving the name of the

171171function, a list of argument types and the return type. The built in

172172construct ``mkForeign`` converts this description to a function callable

173−by ``Idris``:

173+by Idris:

174174

175175.. code-block:: idris

176176

@@ -194,7 +194,7 @@ Include and linker directives

194194~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

195195

196196Foreign function calls are translated directly to calls to C functions,

197−with appropriate conversion between the ``Idris`` representation of a

197+with appropriate conversion between the Idris representation of a

198198value and the C representation. Often this will require extra libraries

199199to be linked in, or extra header and object files. This is made possible

200200through the following directives:

@@ -303,7 +303,7 @@ are available in an external collection [1]_.

303303C Target

304304--------

305305

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

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

307307

308308::

309309

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

343343JavaScript Target

344344-----------------

345345

346−``Idris`` is capable of producing *JavaScript* code that can be run in a

346+Idris is capable of producing *JavaScript* code that can be run in a

347347browser as well as in the *NodeJS* environment or alike. One can use the

348348FFI to communicate with the *JavaScript* ecosystem.

349349

@@ -360,7 +360,7 @@ that is tailored for running in the browser issue the following command:

360360The resulting file can be embedded into your HTML just like any other

361361*JavaScript* code.

362362

363−Generating code for *NodeJS* is slightly different. ``Idris`` outputs a

363+Generating code for *NodeJS* is slightly different. Idris outputs a

364364*JavaScript* file that can be directly executed via ``node``.

365365

366366::

@@ -421,7 +421,7 @@ the way we use ``f`` in ``twice``, it would be more obvious if

421421

422422The *JavaScript* FFI is able to understand functions as arguments when

423423you give it something of type ``FFunction``. The following example code

424−calls ``twice`` in *JavaScript* and returns the result to our ``Idris``

424+calls ``twice`` in *JavaScript* and returns the result to our Idris

425425program:

426426

427427.. code-block:: idris

@@ -450,7 +450,7 @@ via FFI which are stored in external files. The *JavaScript* and

450450mind that *JavaScript* and *NodeJS* are handled as different code

451451generators, therefore you will have to state which one you want to

452452target. This means that you can include different files for *JavaScript*

453−and *NodeJS* in the same ``Idris`` source file.

453+and *NodeJS* in the same Idris source file.

454454

455455So whenever you want to add an external *JavaScript* file you can do

456456this like so:

@@ -488,13 +488,13 @@ This directive compiles into the following *JavaScript*

488488Shrinking down generated *JavaScript*

489489~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

490490

491−``Idris`` can produce very big chunks of *JavaScript* code. However, the

491+Idris can produce very big chunks of *JavaScript* code. However, the

492492generated code can be minified using the ``closure-compiler`` from

493493Google. Any other minifier is also suitable but ``closure-compiler``

494494offers advanced compilation that does some aggressive inlining and code

495−elimination. ``Idris`` can take full advantage of this compilation mode

495+elimination. Idris can take full advantage of this compilation mode

496496and it’s highly recommended to use it when shipping a *JavaScript*

497−application written in ``Idris``.

497+application written in Idris.

498498

499499Cumulativity

500500------------

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

509509 *universe> :t Vect

510510 Vect : Nat -> Type -> Type

511511

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

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

513513

514514::

515515

docs/tutorial/modules.rst+2−2

@@ -4,7 +4,7 @@

44Modules and Namespaces

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

7−An ``Idris`` program consists of a collection of modules. Each module

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

@@ -76,7 +76,7 @@ Export Modifiers

7676

7777By default, all names defined in a module are exported for use by other

7878modules. However, it is good practice only to export a minimal interface

79−and keep internal details abstract. ``Idris`` allows functions, types,

79+and keep internal details abstract. Idris allows functions, types,

8080and classes to be marked as: ``public``, ``abstract`` or ``private``:

8181

8282- ``public`` means that both the name and definition are exported. For

docs/tutorial/packages.rstnew file+77

@@ -0,0 +1,77 @@

1+.. _sect-packages:

3+========

4+Packages

5+========

7+Idris includes a simple system for building packages from a

8+package description file. These files can be used with the Idris

9+compiler to manage the development process of your Idris

10+programmes and packages.

11+

12+Package Descriptions

13+--------------------

14+

15+A package description includes the following:

16+

17++ A header, consisting of the keyword package followed by the package name.

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

19+

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

21+comma separated list of modules. For example, a library test which

22+has two modules ``foo.idr`` and ``bar.idr`` as source files would be

23+written as follows::

24+

25+ package foo

26+

27+ modules = foo, bar

28+

29+Other examples of package files can be found in the ``libs`` directory

30+of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.

31+

32+Other common fields which may be present in an ``ipkg`` file are:

33+

34++ ``sourcedir = <dir>``, which gives the directory (relative to the

35+ current directory) which contains the source. Default is the current

36+ directory.

37+

38++ ``executable = <output>``, which gives the name of the executable

39+ file to generate.

40+

41++ ``main = <module>``, which gives the name of the main module, and

42+ must be present if the executable field is present.

43+

44++ ``opts = "<idris options>"``, which allows options (such as other

45+ packages) to be passed to Idris.

46+

47+In more advanced cases, particularly to support creating bindings to

48+external ``C`` libraries, the following options are available:

49+

50++ ``makefile = <file>``, which specifies a ``Makefile``, to be built

51+ before the Idris modules, for example to support linking with a

52+ ``C`` library.

53+

54++ ``libs = <libs>``, which gives a comma separated list of libraries

55+ which must be present for the package to be usable.

56+

57++ ``objs = <objs>``, which gives a comma separated list of additional

58+ object files to be installed, perhaps generated by the ``Makefile``.

59+

60+Using Package files

61+-------------------

62+

63+Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler as follows:

64+

65++ ``idris --build test.ipkg`` will build all modules in the package

66+

67++ ``idris --install test.ipkg`` will install the package, making it

68+ accessible by other Idris libraries and programs.

69+

70++ ``idris --clean test.ipkg`` will delete all intermediate code and

71+ executable files generated when building.

72+

73+Once the test package has been installed, the command line option

74+``--package test`` makes it accessible (abbreviated to ``-p test``).

75+For example::

76+

77+ idris -p test Main.idr

docs/tutorial/provisional.rst+4−4

@@ -71,9 +71,9 @@ Provisional definitions are written in the same way as ordinary

7171definitions, except that they introduce the right hand side with a

7272``?=`` rather than ``=``. We define ``parity`` as follows:

7373

74−When written in this form, instead of reporting a type error, ``Idris``

74+When written in this form, instead of reporting a type error, Idris

7575will insert a metavariable standing for a theorem which will correct the

76−type error. ``Idris`` tells us we have two proof obligations, with names

76+type error. Idris tells us we have two proof obligations, with names

7777generated from the module and function names:

7878

7979.. code-block:: idris

@@ -161,14 +161,14 @@ reversed:

161161Suspension of Disbelief

162162-----------------------

163163

164−``Idris`` requires that proofs be complete before compiling programs

164+Idris requires that proofs be complete before compiling programs

165165(although evaluation at the prompt is possible without proof details).

166166Sometimes, especially when prototyping, it is easier not to have to do

167167this. It might even be beneficial to test programs before attempting to

168168prove things about them — if testing finds an error, you know you had

169169better not waste your time proving something!

170170

171−Therefore, ``Idris`` provides a built-in coercion function, which allows

171+Therefore, Idris provides a built-in coercion function, which allows

172172you to use a value of the incorrect types:

173173

174174.. code-block:: idris

docs/tutorial/starting.rst+5−5

@@ -7,7 +7,7 @@ Getting Started

77Prerequisites

88-------------

10−Before installing ``Idris``, you will need to make sure you have all

10+Before installing Idris, you will need to make sure you have all

1111of the necessary libraries and tools. You will need:

1212

1313- A fairly recent Haskell platform. Version 2013.2.0.0 should be

@@ -20,7 +20,7 @@ of the necessary libraries and tools. You will need:

2020Downloading and Installing

2121--------------------------

2222

23−The easiest way to install ``Idris``, if you have all of the

23+The easiest way to install Idris, if you have all of the

2424prerequisites, is to type:

2525

2626::

@@ -33,7 +33,7 @@ development version you can find it, as well as build intructions, on

3333GitHub at: https://github.com/idris-lang/Idris-dev.

3434

3535To check that installation has succeeded, and to write your first

36−``Idris`` program, create a file called “``hello.idr``” containing the

36+Idris program, create a file called “``hello.idr``” containing the

3737following text:

3838

3939If you are familiar with Haskell, it should be fairly clear what the

@@ -48,11 +48,11 @@ create an executable called ``hello``, which you can run:

4848 $ ./hello

4949 Hello world

5050

51−Note that the ``$`` indicates the shell prompt! Should the ``Idris``

51+Note that the ``$`` indicates the shell prompt! Should the Idris

5252executable not be found please ensure that you have added

5353``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X

5454users may find they need to use ``~/Library/Haskell/bin``

55−instead. Some useful options to the ``Idris`` command are:

55+instead. Some useful options to the Idris command are:

5656

5757- ``-o prog`` to compile to an executable called ``prog``.

5858

docs/tutorial/syntax.rst+1−1

@@ -122,7 +122,7 @@ hard to program this way in practice. Recall the factorial program in

122122 (Val 1) (Op (*) (app fact (Op (-) (Var Stop) (Val 1)))

123123 (Var Stop)))

124124

125−Since this is a particularly useful pattern, ``Idris`` provides syntax

125+Since this is a particularly useful pattern, Idris provides syntax

126126overloading [1]_ to make it easier to program in such object

127127languages:

128128

docs/tutorial/typesfuns.rst+28−28

@@ -7,13 +7,13 @@ Types and Functions

77Primitive Types

88---------------

10−``Idris`` defines several primitive types: ``Int``, ``Integer`` and

10+Idris defines several primitive types: ``Int``, ``Integer`` and

1111``Float`` for numeric operations, ``Char`` and ``String`` for text

1212manipulation, and ``Ptr`` which represents foreign pointers. There are

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

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

1515these 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

1717prims.idr``:

1818

1919.. code-block:: idris

@@ -32,9 +32,9 @@ prims.idr``:

3232 quux : Bool

3333 quux = False

3434

35−An ``Idris`` file consists of an optional module declaration (here

35+An Idris file consists of an optional module declaration (here

3636``module prims``) followed by an optional list of imports (none here,

37−however ``Idris`` programs can consist of several modules, and the

37+however Idris programs can consist of several modules, and the

3838definitions in each module each have their own namespace, as we will

3939discuss in Section :ref:`sect-namespaces`) and a collection of

4040declarations and definitions. The order of definitions is significant

@@ -46,7 +46,7 @@ declaration. Alternatively, declarations may be terminated with a

4646semicolon.

4747

4848A library module ``prelude`` is automatically imported by every

49−``Idris`` program, including facilities for IO, arithmetic, data

49+Idris program, including facilities for IO, arithmetic, data

5050structures and various common functions. The prelude defines several

5151arithmetic and comparison operators, which we can use at the prompt.

5252Evaluating things at the prompt gives an answer, and the type of the

@@ -108,7 +108,7 @@ Functions

108108---------

109109

110110Functions are implemented by pattern matching, again using a similar

111−syntax to Haskell. The main difference is that ``Idris`` requires type

111+syntax to Haskell. The main difference is that Idris requires type

112112declarations for all functions, using a single colon ``:`` (rather

113113than Haskell’s double colon ``::``). Some natural number arithmetic

114114functions can be defined as follows, again taken from the standard

@@ -133,7 +133,7 @@ names must begin with a capital letter or not. Function names

133133(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,

134134``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are

135135all part of the same namespace. We can test these functions at the

136−``Idris`` prompt:

136+Idris prompt:

137137

138138::

139139

@@ -144,10 +144,10 @@ all part of the same namespace. We can test these functions at the

144144

145145.. note::

146146

147− ``Idris`` automatically desugars the ``Nat`` representation into a

147+ Idris automatically desugars the ``Nat`` representation into a

148148 more human readable format. The result of ``plus (S (S Z)) (S (S Z))``

149149 is actually ``(S (S (S (S Z))))`` which is the Integer 4. This can be

150− checked at the ``Idris`` prompt:

150+ checked at the Idris prompt:

151151

152152::

153153

@@ -169,7 +169,7 @@ computers have perfectly good integer arithmetic built in. The reason

169169is primarily that unary numbers have a very convenient structure which

170170is easy to reason about, and easy to relate to other data structures

171171as we will see later. Nevertheless, we do not want this convenience to

172−be at the expense of efficiency. Fortunately, ``Idris`` knows about

172+be at the expense of efficiency. Fortunately, Idris knows about

173173the relationship between ``Nat`` (and similarly structured types) and

174174numbers. This means it can optimise the representation, and functions

175175such as ``plus`` and ``mult``.

@@ -248,7 +248,7 @@ Vectors

248248

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

250250length”, conventionally called vectors in the dependent type

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

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

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

253253

254254.. code-block:: idris

@@ -258,7 +258,7 @@ importing ``Data.Vect``, or we can declare them as follows:

258258 (::) : a -> Vect k a -> Vect (S k) a

259259

260260Note that we have used the same constructor names as for ``List``.

261−Ad-hoc name overloading such as this is accepted by ``Idris``,

261+Ad-hoc name overloading such as this is accepted by Idris,

262262provided that the names are declared in different namespaces (in

263263practice, normally in different modules). Ambiguous constructor names

264264can normally be resolved from context.

@@ -289,7 +289,7 @@ defined as follows, appends two ``Vect``:

289289

290290The type of ``(++)`` states that the resulting vector’s length will be

291291the sum of the input lengths. If we get the definition wrong in such a

292−way that this does not hold, ``Idris`` will not accept the definition.

292+way that this does not hold, Idris will not accept the definition.

293293For example:

294294

295295.. code-block:: idris

@@ -298,7 +298,7 @@ For example:

298298 (++) Nil ys = ys

299299 (++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

300300

301−When run through the ``Idris`` type checker, this results in the

301+When run through the Idris type checker, this results in the

302302following:

303303

304304::

@@ -325,7 +325,7 @@ The Finite Sets

325325~~~~~~~~~~~~~~~

326326

327327Finite sets, as the name suggests, are sets with a finite number of

328−elements. They are available as part of the ``Idris`` library, by

328+elements. They are available as part of the Idris library, by

329329importing ``Data.Fin``, or can be declared as follows:

330330

331331.. code-block:: idris

@@ -480,9 +480,9 @@ I/O

480480

481481Computer programs are of little use if they do not interact with the

482482user or the system in some way. The difficulty in a pure language such

483−as ``Idris`` — that is, a language where expressions do not have

483+as Idris — that is, a language where expressions do not have

484484side-effects — is that I/O is inherently side-effecting. Therefore in

485−``Idris``, such interactions are encapsulated in the type ``IO``:

485+Idris, such interactions are encapsulated in the type ``IO``:

486486

487487.. code-block:: idris

488488

@@ -567,7 +567,7 @@ Laziness

567567--------

568568

569569Normally, arguments to functions are evaluated before the function

570−itself (that is, ``Idris`` uses *eager* evaluation). However, this is

570+itself (that is, Idris uses *eager* evaluation). However, this is

571571not always the best approach. Consider the following function:

572572

573573.. code-block:: idris

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

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

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

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

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

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

583583data type, which allows evaluation to be suspended:

584584

585585.. code-block:: idris

@@ -590,7 +590,7 @@ data type, which allows evaluation to be suspended:

590590 Force : Lazy a -> a

591591

592592A value of type ``Lazy a`` is unevaluated until it is forced by

593−``Force``. The ``Idris`` type checker knows about the ``Lazy`` type,

593+``Force``. The Idris type checker knows about the ``Lazy`` type,

594594and inserts conversions where necessary between ``Lazy a`` and ``a``,

595595and vice versa. We can therefore write ``boolCase`` as follows,

596596without any explicit use of ``Force`` or ``Delay``:

@@ -604,10 +604,10 @@ without any explicit use of ``Force`` or ``Delay``:

604604Useful Data Types

605605-----------------

606606

607−``Idris`` includes a number of useful data types and library functions

607+Idris includes a number of useful data types and library functions

608608(see the ``libs/`` directory in the distribution). This chapter

609609describes a few of these. The functions described here are imported

610−automatically by every ``Idris`` program, as part of ``Prelude.idr``.

610+automatically by every Idris program, as part of ``Prelude.idr``.

611611

612612``List`` and ``Vect``

613613~~~~~~~~~~~~~~~~~~~~~

@@ -679,7 +679,7 @@ directory. For more details of the functions available on ``List`` and

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

680680

681681Functions include filtering, appending, reversing, and so on. Also

682−remember that ``Idris`` is still in development, so if you don’t see

682+remember that Idris is still in development, so if you don’t see

683683the function you need, please feel free to add it and submit a patch!

684684

685685Aside: Anonymous functions and operator sections

@@ -877,7 +877,7 @@ pattern matching at the top level:

877877List comprehensions

878878~~~~~~~~~~~~~~~~~~~

879879

880−``Idris`` provides *comprehension* notation as a convenient shorthand

880+Idris provides *comprehension* notation as a convenient shorthand

881881for building lists. The general form is:

882882

883883::

@@ -958,10 +958,10 @@ matching ``let`` and lambda bindings. It will *only* work if:

958958Dependent Records

959959-----------------

960960

961−*Records* are data types which collect several values (the record’s

962−*fields*) together. ``Idris`` provides syntax for defining records and

961+*Records* are data types which collect several values (the record's

962+*fields*) together. Idris provides syntax for defining records and

963963*automatically generating field access and update functions. For

964−*example, we can represent a person’s name and age in a record:

964+*example, we can represent a person's name and age in a record:

965965

966966.. code-block:: idris

967967

@@ -1029,7 +1029,7 @@ length because it will not affect the type of the record:

10291029Nested record update

10301030~~~~~~~~~~~~~~~~~~~~

10311031

1032−``Idris`` also provides a convenient syntax for accessing and updating

1032+Idris also provides a convenient syntax for accessing and updating

10331033nested records. For example, if a field is accessible with the

10341034expression ``c (b (a x))``, it can be updated using the following

10351035syntax:

docs/tutorial/views.rst+1−1

@@ -28,7 +28,7 @@ The ``with`` rule — matching intermediate values

2828------------------------------------------------

2929

3030Very often, we need to match on the result of an intermediate

31−computation. ``Idris`` provides a construct for this, the ``with``

31+computation. Idris provides a construct for this, the ``with``

3232rule, inspired by views in ``Epigram`` [1]_, which takes account of

3333the fact that matching on a value in a dependently typed language can

3434affect what we know about the forms of other values. In its simplest