9c13628 · Idris-dev · git.iko.soy

CHANGELOG+8

compare with master

unifiedsplit

@@ -10,9 +10,17 @@ New in 0.9.18:

10 '%extern' directive, allowing back ends to define their own special

11 purpose primitives

12 + Ptr and ManagedPtr have been removed and replaced with external primitives

13+* Add %hint function annotation, which allows functions to be used as

14+ hints in proof search for 'auto' arguments. Only functions which return

15+ an instance of a data or record type are allowed as hints.

13* Syntax rules no longer perform variable capture. Users of effects will

16* Syntax rules no longer perform variable capture. Users of effects will

14 need to explicitly name results in dependent effect signatures instead

17 need to explicitly name results in dependent effect signatures instead

15 of using the default name "result".

18 of using the default name "result".

19+* Pattern-matching lambdas are allowed to be impossible. For example,

20+ Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of

21+ requiring a separate lemma.

22+* Case alternatives are allowed to be impossible:

23+ case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }

16

24

17New in 0.9.17:

25New in 0.9.17:

18--------------

26--------------

CONTRIBUTING.md+26−17

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

1# Contributing to Idris-Dev

2

3The Idris Community welcomes pull requests, bug reporting, and bug squashing!

4−However, we cannot do it all ourself, and want to make it as easy as possible to contribute changes to get things working.

4+However, we cannot do it all ourselves, and want to make it as easy as possible to contribute changes to get things working.

5Here are a few guidelines that we would like contributors to follow so that we can have a chance of keeping on top of things.

6

7## Getting Started

@@ -22,34 +22,43 @@ We do not want you wasting your time, duplicating somebody's work!

22

23## The Campsite Rule

24

25−A basic rule when contributing to Idris is the **campsite rule**: leave the codebase in better condition than you found it.

25+We try to follow the **campsite rule**: leave the code base in better condition than you found it.

26Please clean up any messes that you find, and don't leave behind new messes for the next contributor.

27

28## Contributing to the default libraries.

29

30Idris ships with a set of packages in `libs/` that is provided as a default library.

31+

32++ `prelude` is a collection of basic definitions, automatically imported by Idris programs.

33++ `base` is tried and tested code that may be useful, and has seen active use in multiple projects.

34++ `contrib` is code that is experimental in design and that we want to test before possible inclusion in `base`.

35++ `effects` is a library which supports effectful programming.

36+

31−These packages should not be seen as the *standard* as when working with dependent types we do not necessarily know how best to work with dependent types.

37+These packages should not be seen as the *standard* as when working with dependent types; we do not necessarily know how best to work with dependent types yet.

32These packages offer functionality that can be built on top of when constructing Idris programs.

38These packages offer functionality that can be built on top of when constructing Idris programs.

33

39

34−One major point to make is that everything in prelude will be imported automatically, unless given

40+Everything in prelude will be imported automatically, unless given the `--noprelude` option.

35−the `--noprelude` option.

36−Likewise, the contents of base are available with no special options.

41+The contents of base are available with no special options, but modules must be imported.

37−The other two packages that ship with Idris, contrib and effects, require a the use of the `-p` command-line argument to bring their contents into the include path.

42+The other two packages that ship with Idris, contrib and effects, require the use of the `-p` command-line argument to bring their contents into the include path.

38−New contributions should probably be sent to contrib first, so that they can get maintained with the Idris distribution.

43+

44+New contributions should be added to the contrib package (never directly to base or prelude!).

39If they turn out to be widely applicable and useful, they may later be moved into base.

45If they turn out to be widely applicable and useful, they may later be moved into base.

40

46

41As Idris is still being developed we are open to suggestions and changes that make improvements to these default packages.

47As Idris is still being developed we are open to suggestions and changes that make improvements to these default packages.

42−Major changes to the library (or Idris itself) should ideally be discussed first through the projects official channels of communication i.e. the mailing list, github wiki, or IRC, or as a [Dragon Egg](https://github.com/idris-lang/Idris-dev/wiki/Feature-proposals).

48+Major changes to the library, or Idris itself, should be discussed first through the project's official channels of communication:

43−Developers then seeking to add content to Idris's prelude and default library, should do so through a PR where more discussion's and refinements can be made.

44

49

45−We do not want you wasting your time nor duplicating somebody's work!

50+1. The mailing List.

51+1. On our IRC Channel `#idris` on freenode, or

52+1. As a [Dragon Egg](https://github.com/idris-lang/Idris-dev/wiki/Feature-proposals).

53+

54+Developers then seeking to add content to Idris's prelude and default library, should do so through a PR where more discussions and refinements can be made.

46

55

47−Of note: developers should be prepared to wait until their PR has been discussed and authorized prior to the PRs inclusion.

56+We do not want you wasting your time nor duplicating somebody's work!

48

57

49## Making Changes

58## Making Changes

50

59

51Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).

60Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).

52−The steps are straightforward.

61+The steps are described below.

53

62

54### New contributors

63### New contributors

55

64

@@ -85,7 +94,7 @@ The remaining steps are the same for both new and existing contributors:

85

94

861. Create, and checkout onto, a topic branch on which to base you work.

951. Create, and checkout onto, a topic branch on which to base you work.

87 * This is typically the master branch.

96 * This is typically the master branch.

88− * For your own sanity, please avoid working on the `master` branch.

97+ * Please avoid working on the `master` branch.

89

98

90```

99```

91$ git branch fix/master/my_contrib master

100$ git branch fix/master/my_contrib master

@@ -118,7 +127,7 @@ $ git diff --check

118 single space, with blank lines in between, but conventions vary here

127 single space, with blank lines in between, but conventions vary here

119

128

1201. Make sure you have added any necessary tests for your changes.

1291. Make sure you have added any necessary tests for your changes.

121−1. Run all the tests to assure nothing else was accidentally broken.

130+1. Run all the tests to ensure nothing else was accidentally broken.

122

131

123```

132```

124$ make test

133$ make test

@@ -136,12 +145,12 @@ From there you will have to wait on one of the `idris-dev` committers to respond

136This response might be an accept or some changes/improvements/alternatives will be suggest.

145This response might be an accept or some changes/improvements/alternatives will be suggest.

137We do not guarantee that all requests will be accepted.

146We do not guarantee that all requests will be accepted.

138

147

139−## Increases chances of acceptance.

148+## Increasing chances of acceptance.

140

149

141To help increase the chance of your pull request being accepted:

150To help increase the chance of your pull request being accepted:

142

151

1431. Run the tests.

1521. Run the tests.

144−1. Update the documentation, the surrounding one, examples elsewhere, guides, whatever is affected by your contribution

153+1. Update the documentation, the surrounding code, examples elsewhere, guides, whatever is affected by your contribution

1451. Use appropriate code formatting for both Idris and Haskell.

1541. Use appropriate code formatting for both Idris and Haskell.

146

155

147## Additional Resources

156## Additional Resources

docs/README.md+6

@@ -18,6 +18,12 @@ Sphinx can be installed either through your hosts package manager or using pip/e

18 of readthedocs and be ignored. In the past we had several code-blocks

19 disappear because of that.

20

21+The ReadTheDocs theme can be installed using pip as follows:

22+

23+```sh

24+pip install sphinx_rtd_theme

25+```

26+

21### LaTeX

27### LaTeX

22

28

23LaTeX can be install either using your systems package manager or direct from TeXLive.

29LaTeX can be install either using your systems package manager or direct from TeXLive.

docs/conf.py+11

@@ -15,6 +15,9 @@

15import sys

16import os

17

18+# True if the readthedocs theme is locally installed

19+on_rtd = os.environ.get('READTHEDOCS', None) == 'True'

20+

18# If extensions (or modules to document with autodoc) are in another directory,

21# If extensions (or modules to document with autodoc) are in another directory,

19# add these directories to sys.path here. If the directory is relative to the

22# add these directories to sys.path here. If the directory is relative to the

20# documentation root, use os.path.abspath to make it absolute, like shown here.

23# documentation root, use os.path.abspath to make it absolute, like shown here.

@@ -111,6 +114,14 @@ todo_include_todos = True

111# a list of builtin themes.

114# a list of builtin themes.

112html_theme = "default"

115html_theme = "default"

113

116

117+if not on_rtd: # only import and set the theme if we're building docs locally

118+ try:

119+ import sphinx_rtd_theme

120+ html_theme = 'sphinx_rtd_theme'

121+ html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]

122+ except ImportError:

123+ html_theme = "default"

124+

114# Theme options are theme-specific and customize the look and feel of a theme

125# Theme options are theme-specific and customize the look and feel of a theme

115# further. For a list of options available for each theme, see the

126# further. For a list of options available for each theme, see the

116# documentation.

127# documentation.

docs/effects/conclusions.rst+2−2

@@ -1,8 +1,8 @@

1.. _sect-further:

2

3−===============

3+***************

4Further Reading

5−===============

5+***************

6

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

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

docs/effects/depeff.rst+6−6

@@ -1,8 +1,8 @@

1.. _sect-depeff:

2

3−=================

3+*****************

4Dependent Effects

5−=================

5+*****************

6

7In the programs we have seen so far, the available effects have remained

8constant. Sometimes, however, an operation can *change* the available

@@ -16,7 +16,7 @@ we will see how this can be used to implement a type-safe and

16resource-safe protocol for file management.

17

18Dependent States

19−----------------

19+================

20

21Suppose we have a function which reads input from the console, converts

22it to an integer, and adds it to a list which is stored in a ``STATE``.

@@ -59,7 +59,7 @@ It has the following type:

59 putM : y -> { [STATE x] ==> [STATE y] } Eff ()

60

61Result-dependent Effects

62−------------------------

62+========================

63

64Often, whether a state is updated could depend on the success or

65otherwise of an operation. In our ``readInt`` example, we might wish to

@@ -134,7 +134,7 @@ check (i.e. whether reading a value succeeded) has indeed been done.

134 being inspected in the type of each branch.

135

136File Management

137−---------------

137+===============

138

139A practical use for dependent effects is in specifying resource usage

140protocols and verifying that they are executed correctly. For example,

@@ -242,7 +242,7 @@ reading, but the effect list contains a ``FILE_IO`` effect carrying a

242file open for writing.

243

244Pattern-matching bind

245−---------------------

245+=====================

246

247It might seem that having to test each potentially failing operation

248with a ``case`` clause could lead to ugly code, with lots of

docs/effects/hangman.rst+10−10

@@ -1,8 +1,8 @@

1.. _sect-hangman:

2

3−=======================================

3+***************************************

4Example: A “Mystery Word” Guessing Game

5−=======================================

5+***************************************

6

7In this section, we will use the techniques and specific effects

8discussed in the tutorial so far to implement a larger example, a simple

@@ -29,7 +29,7 @@ using the newly defined effect (and any others required to implement the

29interface).

30

31Step 1: Game State

32−------------------

32+==================

33

34First, we categorise the game states as running games (where there are a

35number of guesses available, and a number of letters still to guess), or

@@ -53,7 +53,7 @@ this data:

53 data Mystery : GState -> Type

54

55Step 2: Game Rules

56−------------------

56+==================

57

58We describe the game rules as a dependent effect, where each action has

59a *precondition* (i.e. what the game state must be before carrying out

@@ -131,7 +131,7 @@ then allow us to play the game.

131 MYSTERY h = MkEff (Mystery h) MysteryRules

132

133Step 3: Implement Rules

134−-----------------------

134+=======================

135

136To *implement* the rules, we begin by giving a concrete definition of

137game state:

@@ -211,7 +211,7 @@ such a way that the number of missing letters or number of guesses does

211not follow the rules.

212

213Step 4: Implement Interface

214−---------------------------

214+===========================

215

216Having described the rules, and implemented state transitions which

217follow those rules as an effect handler, we can now write an interface

@@ -225,7 +225,7 @@ for the game which uses the ``MYSTERY`` effect:

225The type indicates that the game must start in a running state, with

226some guesses available, and eventually reach a not-running state (i.e.

227won or lost). The only way to achieve this is by correctly following the

228−stated rules.

228+stated rules.

229

230Note that the type of ``game`` makes no assumption that there are

231letters to be guessed in the given word (i.e. it is ``w`` rather than

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

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

268

269A possible complete implementation of ``game`` is

270−presented below:

270+presented below:

271

272.. code-block:: idris

273

@@ -298,7 +298,7 @@ presented below:

298 (S k) => game

299

300Discussion

301−----------

301+==========

302

303Writing the rules separately as an effect, then an implementation

304which uses that effect, ensures that the implementation must follow

@@ -330,4 +330,4 @@ These are, of course, simple errors, but were caught by the type

330checker before any testing of the game.

331

332.. [1]

333− Readers may recognise this game by the name “Hangman.”

333+ Readers may recognise this game by the name “Hangman”.

docs/effects/impleff.rst+9−10

@@ -1,8 +1,8 @@

1.. _sect-impleff:

2

3−====================

3+********************

4Creating New Effects

5−====================

5+********************

6

7We have now seen several side-effecting operations provided by the

8``Effects`` library, and examples of their use in Section

@@ -14,7 +14,7 @@ selection of the available effects are implemented, and show how new

14effectful operations may be provided.

15

16State

17−-----

17+=====

18

19Effects are described by *algebraic data types*, where the

20constructors describe the operations provided when the effect is

@@ -154,7 +154,7 @@ Such details are not important for using the library, or even writing

154new effects, however.

155

156Summary

157−~~~~~~~

157+-------

158

159The following listing summarises what is required to define the

160``STATE`` effect:

@@ -183,7 +183,7 @@ The following listing summarises what is required to define the

183

184

185Console I/O

186−-----------

186+===========

187

188Then listing below gives the definition of the ``STDIO``

189effect, including handlers for ``IO`` and ``IOExcept``. We omit the

@@ -219,7 +219,7 @@ directly.

219 STDIO = MkEff () StdIO

220

221Exceptions

222−----------

222+==========

223

224The listing below gives the definition of the ``Exception``

225effect, including two of its handlers for ``Maybe`` and ``List``. The

@@ -244,7 +244,7 @@ error.

244

245

246Non-determinism

247−---------------

247+===============

248

249The following listing gives the definition of the ``Select``

250effect for writing non-deterministic programs, including a handler for

@@ -277,10 +277,10 @@ accumulate all successful results, and in the ``Maybe`` handler we try

277the first value in the last, and try later values only if that fails.

278

279File Management

280−---------------

280+===============

281

282Result-dependent effects are no different from non-dependent effects

283−in the way they are implemented. The listing below

283+in the way they are implemented. The listing below

284illustrates this for the ``FILE_IO`` effect. The syntax for state

285transitions ``{ x ==> {res} x’ }``, where the result state ``x’`` is

286computed from the result of the operation ``res``, follows that for

@@ -320,4 +320,3 @@ continuation ``k`` are different depending on whether the result is

320``True`` (opening succeeded) or ``False`` (opening failed). This uses

321``validFile``, defined in the ``Prelude``, to test whether a file

322handler refers to an open file or not.

323−

docs/effects/introduction.rst+2−2

@@ -1,6 +1,6 @@

1−============

1+************

2Introduction

3−============

3+************

4

5Pure functional languages with dependent types such as `Idris

6<http://idris-lang.org/>`_ support reasoning about programs directly

docs/effects/simpleeff.rst+13−13

@@ -1,8 +1,8 @@

1.. _sect-simpleff:

2

3−==============

3+**************

4Simple Effects

5−==============

5+**************

6

7So far we have seen how to write programs with locally mutable state

8using the ``STATE`` effect. To recap, we have the definitions below

@@ -41,7 +41,7 @@ All of the effects in the library, including those described in this

41section, are summarised in Appendix :ref:`sect-appendix`.

42

43Console I/O

44−-----------

44+===========

45

46Console I/O is supported with the ``STDIO``

47effect, which allows reading and writing characters and strings to and

@@ -67,7 +67,7 @@ can perform (or at the very least simulate) console I/O:

67 instance Handler StdIO (IOExcept a)

68

69Examples

70−~~~~~~~~

70+--------

71

72A program which reads the user’s name, then says hello, can be written

73as follows:

@@ -117,7 +117,7 @@ read and write from the console. To run this, ``main`` does not need

117to be changed.

118

119Aside: Resource Types

120−~~~~~~~~~~~~~~~~~~~~~

120+---------------------

121

122To find out the resource type of an effect, if necessary (for example

123if we want to initialise a resource explicitiy with ``runInit`` rather

@@ -132,7 +132,7 @@ than using a default value with ``run``) we can run the

132 Int : Type

133

134Exceptions

135−----------

135+==========

136

137The ``EXCEPTION``

138effect is declared in module ``Effect.Exception``. This allows programs

@@ -155,7 +155,7 @@ generally:

155 instance Show a => Handler (Exception a) IO

156

157Example

158−~~~~~~~

158+-------

159

160Suppose we have a ``String`` which is expected to represent an integer

161in the range ``0`` to ``n``. We can write a function ``parseNumber``

@@ -232,7 +232,7 @@ the boundedness proof:

232 else raise NotANumber

233

234Random Numbers

235−--------------

235+==============

236

237Random number generation is also implemented by the library, in module

238``Effect.Random``:

@@ -263,7 +263,7 @@ produce a random number:

263 (essentially a number with an upper bound given in its type).

264

265Example

266−~~~~~~~

266+-------

267

268We can use the ``RND`` effect to implement a simple guessing game. The

269``guess`` function, given a target number, will repeatedly ask the

@@ -317,7 +317,7 @@ do this, see the ``SYSTEM`` effect described in :ref:`sect-appendix`.

317

318

319Non-determinism

320−---------------

320+===============

321

322The listing below gives the definition of the non-determinism

323effect, which allows a program to choose a value non-deterministically

@@ -337,7 +337,7 @@ succeeds:

337 instance Handler Selection List

338

339Example

340−~~~~~~~

340+-------

341

342The ``SELECT`` effect can be used to solve constraint problems, such

343as finding Pythagorean triples. The idea is to use ``select`` to give

@@ -373,7 +373,7 @@ context). We can try this as follows:

373 print $ the (List _) $ run (triple 100)

374

375``vadd`` revisited

376−------------------

376+==================

377

378We now return to the ``vadd`` program from the introduction. Recall the

379definition:

@@ -453,7 +453,7 @@ with gracefully.

453 else raise "Not a number"

454

455Example: An Expression Calculator

456−---------------------------------

456+=================================

457

458To show how these effects can fit together, let us consider an

459evaluator for a simple expression language, with addition and integer

docs/effects/state.rst+8−8

@@ -1,8 +1,8 @@

1.. _sect-state:

2

3−=====

3+*****

4State

5−=====

5+*****

6

7Many programs, even pure programs, can benefit from locally mutable

8state. For example, consider a program which tags binary tree nodes

@@ -34,7 +34,7 @@ specific value ``i``, has the following type:

34 treeTag : (i : Int) -> BTree a -> BTree (Int, a)

35

36First attempt

37−-------------

37+=============

38

39Naïvely, we can implement ``treeTag`` by implementing a helper

40function which propagates a counter, returning the result of the count

@@ -75,7 +75,7 @@ is local mutable state (the counter) which we have had to make

75explicit.

76

77Introducing ``Effects``

78−-----------------------

78+=======================

79

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

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

@@ -217,7 +217,7 @@ shown in Listing [introprog].

217 main = print (treeTag 1 testTree)

218

219Effects and Resources

220−---------------------

220+=====================

221

222Each effect is associated with a *resource*, which is initialised

223before an effectful program can be run. For example, in the case of

@@ -261,7 +261,7 @@ implemented ``treeTag`` by initialising the state as follows:

261 treeTag i x = runPureInit [i] (treeTagAux x)

262

263Labelled Effects

264−----------------

264+================

265

266What if we have more than one state, especially more than one state of

267the same type? How would ``get`` and ``put`` know which state they

@@ -358,7 +358,7 @@ effect. Note that labels are polymorphic in the label type ``lbl``.

358Hence, a label can be anything—a string, an integer, a type, etc.

359

360``!``-notation

361−--------------

361+==============

362

363In many cases, using ``do``-notation can make programs unnecessarily

364verbose, particularly in cases where the value bound is used once,

@@ -412,7 +412,7 @@ is lifted to:

412 f g'

413

414Syntactic Sugar and ``Eff``

415−---------------------------

415+===========================

416

417By now, you may be wondering about the syntax we are using for

418``Eff``, because it doesn’t look like a normal type! (If not, you may

docs/effects/summary.rst+9−9

@@ -1,14 +1,14 @@

1.. _sect-appendix:

2

3−===============

3+***************

4Effects Summary

5−===============

5+***************

6

7This appendix gives interfaces for the core effects provided by the

8library.

9

10EXCEPTION

11−---------

11+=========

12

13.. code-block:: idris

14

@@ -29,7 +29,7 @@ EXCEPTION

29 instance Show a => Handler (Exception a) IO

30

31FILE\_IO

32−--------

32+========

33

34.. code-block:: idris

35

@@ -58,7 +58,7 @@ FILE\_IO

58 instance Handler FileIO IO

59

60RND

61−---

61+===

62

63.. code-block:: idris

64

@@ -77,7 +77,7 @@ RND

77 instance Handler Random m

78

79SELECT

80−------

80+======

81

82.. code-block:: idris

83

@@ -93,7 +93,7 @@ SELECT

93 instance Handler Selection List

94

95STATE

96−-----

96+=====

97

98.. code-block:: idris

99

@@ -111,7 +111,7 @@ STATE

111 instance Handler State m

112

113STDIO

114−-----

114+=====

115

116.. code-block:: idris

117

@@ -133,7 +133,7 @@ STDIO

133 instance Handler StdIO (IOExcept a)

134

135SYSTEM

136−------

136+======

137

138.. code-block:: idris

139

docs/faq/faq.rst+32−16

@@ -1,9 +1,9 @@

1−==========================

1+**************************

2Frequently Asked Questions

3−==========================

3+**************************

4

5What are the differences between Agda and Idris?

6−------------------------------------------------

6+================================================

7

8The main difference is that Idris has been designed from the start to support

9verified systems programming through easy interoperability with C and high

@@ -14,7 +14,7 @@ do notation. Idris also supports tactic based theorem proving, and has a

14lightweight Hugs/GHCI style interface.

15

16Is Idris production ready?

17−--------------------------

17+==========================

18

19Idris is primarily a research tool for exploring the possibilities of software

20development with dependent types, meaning that the primary goal is not (yet) to

@@ -28,8 +28,8 @@ for use in production would be very welcome - this includes (but is not

28limited to) extra library support, polishing the run-time system (and ensuring

29it is robust), providing and maintaining a JVM back end, etc.

30

31−Why does Idris use eager evaluation rather than lazy?

31+Why does Idris use eager evaluation rather than lazy?

32−-----------------------------------------------------

32+=====================================================

33

34Idris uses eager evaluation for more predictable performance, in particular

35because one of the longer term goals is to be able to write efficient and

@@ -57,7 +57,7 @@ concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an

57``Int``.

58

59How can I make lazy control structures?

60−---------------------------------------

60+=======================================

61

62You can make control structures using the special Lazy type. For example,

63``if...then...else`` is defined as follows in the library:

@@ -74,7 +74,7 @@ The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will

74only be evaluated if they are used, that is, they are evaluated lazily.

75

76Evaluation at the REPL doesn't behave as I expect. What's going on?

77−-------------------------------------------------------------------

77+===================================================================

78

79Being a fully dependently typed language, Idris has two phases where it

80evaluates things, compile-time and run-time. At compile-time it will only

@@ -100,31 +100,47 @@ the difference between:

100 \n => \m => plus n (S m) : Nat -> Nat -> Nat

101

102When will Idris be self-hosting?

103−--------------------------------

103+================================

104

105It’s not a priority, though not a bad idea in the long run. It would be a

106worthwhile effort in the short term to implement libraries to support

107self-hosting, such as a good parsing library.

108

109Does Idris have Universe Polymorphism? What is the type of ``Type``?

110−--------------------------------------------------------------------

110+====================================================================

111

112Rather than Universe polymorphism, Idris has a cumulative hierarchy of

113−universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.

113+universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.

114−Cumulativity means that if ``x : Type n`` then also ``x : Type m``,

114+Cumulativity means that if ``x : Type n`` then also ``x : Type m``,

115provided that ``n <= m``.

116

117+Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?

118+===================================================================================

119+

120+Historically the C language and many other languages have used the

121+names ``Float`` and ``Double`` to represent floating point numbers of

122+size 32 and 64 respectivly. Newer languages such as Rust and Julia

123+have begun to follow the naming scheme described in `IEE Standard for

124+Floating-Point Arithmetic (IEEE 754)

125+<http://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes

126+single and double precision numbers as ``Float32`` and ``Float64``;

127+the size is described in the type name.

128+

129+Due to developer familiarity with the older naming convention, and

130+choice by the developers of Idris, Idris uses the C style convention.

131+That is, the names ``Float`` and ``Double`` are used to describe

132+single and double precision numbers.

133+

117What does the name ‘Idris’ mean?

134What does the name ‘Idris’ mean?

118−--------------------------------

135+================================

119

136

120−British people of a certain age may be familiar with this

137+British people of a certain age may be familiar with this

121`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If

138`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If

122that doesn’t help, maybe you can invent a suitable acronym :-) .

139that doesn’t help, maybe you can invent a suitable acronym :-) .

123

140

124Where can I find more answers?

141Where can I find more answers?

125−------------------------------

142+==============================

126

143

127There is an `Unofficial FAQ

144There is an `Unofficial FAQ

128<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on

145<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on

129github which answers more technical questions and may be updated more often.

146github which answers more technical questions and may be updated more often.

130−

docs/guides/type-providers-ffi.rst+12−11

@@ -1,5 +1,6 @@

1+***********************

1Type Providers in Idris

2Type Providers in Idris

2−=======================

3+***********************

3

4

4`Type providers in Idris

5`Type providers in Idris

5<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

6<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__

@@ -9,7 +10,7 @@ foreign functions, because these will often be used with type

9providers.

10providers.

10

11

11The use case

12The use case

12−------------

13+============

13

14

14First, let's talk about *why* we might want type providers. There are

15First, let's talk about *why* we might want type providers. There are

15a number of reasons to use them and there are other examples available

16a number of reasons to use them and there are other examples available

@@ -23,7 +24,7 @@ relied upon. We don't just want to hard-code these types into our

23program... so we'll use a type provider to find them at compile time!

24program... so we'll use a type provider to find them at compile time!

24

25

25A simple example

26A simple example

26−----------------

27+================

27

28

28First, let's go over a basic usage of type providers, because foreign

29First, let's go over a basic usage of type providers, because foreign

29functions can be confusing but it's important to remember that

30functions can be confusing but it's important to remember that

@@ -94,7 +95,7 @@ themselves!

94Don't worry, there's a better way.

95Don't worry, there's a better way.

95

96

96Foreign Functions

97Foreign Functions

97−-----------------

98+=================

98

99

99It's actually pretty easy to write a C function that figures out the

100It's actually pretty easy to write a C function that figures out the

100size of ``size_t``:

101size of ``size_t``:

@@ -114,8 +115,8 @@ So now we can get the size of ``size_t`` as long as we're in C code.

114We'd like to be able to use this from Idris. Can we do this? It turns

115We'd like to be able to use this from Idris. Can we do this? It turns

115out we can.

116out we can.

116

117

117−mkForeign

118+``mkForeign``

118−~~~~~~~~~

119+-------------

119

120

120With mkForeign, we can turn a C function into an IO action. It works

121With mkForeign, we can turn a C function into an IO action. It works

121like this:

122like this:

@@ -138,7 +139,7 @@ compiler "Treat the return value of this C function like it's a C int,

138and when you pass it back into Idris, convert it to an Idris int."

139and when you pass it back into Idris, convert it to an Idris int."

139

140

140Caveats of mkForeign

141Caveats of mkForeign

141−^^^^^^^^^^^^^^^^^^^^

142+--------------------

142

143

143First and foremost: ``mkForeign`` is not actually a function. It is

144First and foremost: ``mkForeign`` is not actually a function. It is

144treated specially by the compiler, and there are certain rules you

145treated specially by the compiler, and there are certain rules you

@@ -185,7 +186,7 @@ applied. This is okay:

185 lengths = mapM strlen listOfStrings

186 lengths = mapM strlen listOfStrings

186

187

187Running foreign functions

188Running foreign functions

188−~~~~~~~~~~~~~~~~~~~~~~~~~

189+-------------------------

189

190

190This is all well and good for writing code that will typecheck. To

191This is all well and good for writing code that will typecheck. To

191actually run the code, we'll need to do just a bit more work. Exactly

192actually run the code, we'll need to do just a bit more work. Exactly

@@ -193,7 +194,7 @@ what we need to do depends on whether we want to interpret or compile

193our code.

194our code.

194

195

195In the interpreter

196In the interpreter

196−^^^^^^^^^^^^^^^^^^

197+------------------

197

198

198If we want to call our foreign functions from interpreted code (such

199If we want to call our foreign functions from interpreted code (such

199as the REPL or a type provider), we need to dynamically link a library

200as the REPL or a type provider), we need to dynamically link a library

@@ -213,7 +214,7 @@ functions from an installed library rather than something you wrote

213yourself, the "./" is not necessary.

214yourself, the "./" is not necessary.

214

215

215In an executable

216In an executable

216−^^^^^^^^^^^^^^^^

217+----------------

217

218

218If we want to run our code from an executable, we can statically link

219If we want to run our code from an executable, we can statically link

219instead. We'll use the ``%include`` and ``%link`` directives:

220instead. We'll use the ``%include`` and ``%link`` directives:

@@ -229,7 +230,7 @@ directives search in the current directory by default. (That is, the

229directory from which we run idris.)

230directory from which we run idris.)

230

231

231Putting it all together

232Putting it all together

232−-----------------------

233+=======================

233

234

234So, at the beginning of this article I said we'd use type providers to

235So, at the beginning of this article I said we'd use type providers to

235port ``struct stat`` to Idris. The relevant part is just translating

236port ``struct stat`` to Idris. The relevant part is just translating

docs/index.rst+3−1

@@ -15,6 +15,7 @@ Documentation for the Idris Language

15

16 More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

17

18+

18* :ref:`tutorial-index`

19* :ref:`tutorial-index`

19* :ref:`eff-tutorial-index`

20* :ref:`eff-tutorial-index`

20* :ref:`faq-index`

21* :ref:`faq-index`

@@ -47,7 +48,7 @@ The Idris Tutorial

47 tutorial/miscellany

48 tutorial/miscellany

48 tutorial/conclusions

49 tutorial/conclusions

49

50

50−.. _effects:

51+.. _faq:

51

52

52##########################

53##########################

53Frequently Asked Questions

54Frequently Asked Questions

@@ -88,6 +89,7 @@ Theorem Proving

88 proofs/pluscomm

89 proofs/pluscomm

89 proofs/inductive

90 proofs/inductive

90 proofs/patterns

91 proofs/patterns

92+ proofs/interactive

91

93

92.. _reference:

94.. _reference:

93

95

docs/proofs/index.rst+1

@@ -21,4 +21,5 @@ A tutorial on theorem proving in Idris.

21 pluscomm

22 inductive

23 patterns

24+ interactive

24

25

docs/proofs/inductive.rst+6−5

@@ -1,5 +1,6 @@

1+****************

1Inductive Proofs

2Inductive Proofs

2−================

3+****************

3

4

4Before embarking on proving ``plus_commutes`` in Idris itself, let us

5Before embarking on proving ``plus_commutes`` in Idris itself, let us

5consider the overall structure of a proof of some property of natural

6consider the overall structure of a proof of some property of natural

@@ -25,7 +26,7 @@ case). Recalling ``plus``:

25

26

26This is total because it covers all possible inputs (the first argument

27This is total because it covers all possible inputs (the first argument

27can only be ``Z`` or ``S k`` for some ``k``, and the second argument

28can only be ``Z`` or ``S k`` for some ``k``, and the second argument

28−``m`` covers all possible ``Nat``\ s) and in the recursive call, ``k``

29+``m`` covers all possible ``Nat``) and in the recursive call, ``k``

29is structurally smaller than ``S k`` so the first argument will always

30is structurally smaller than ``S k`` so the first argument will always

30reach the base case ``Z`` in any sequence of recursive calls.

31reach the base case ``Z`` in any sequence of recursive calls.

31

32

@@ -50,7 +51,7 @@ function capturing all such inductive definitions:

50.. code-block:: idris

51.. code-block:: idris

51

52

52 nat_induction : (P : Nat -> Type) -> -- Property to show

53 nat_induction : (P : Nat -> Type) -> -- Property to show

53− (P Z) -> -- Base case

54+ (P Z) -> -- Base case

54 ((k : Nat) -> P k -> P (S k)) -> -- Inductive step

55 ((k : Nat) -> P k -> P (S k)) -> -- Inductive step

55 (x : Nat) -> -- Show for all x

56 (x : Nat) -> -- Show for all x

56 P x

57 P x

@@ -63,12 +64,12 @@ version of ``plus``:

63.. code-block:: idris

64.. code-block:: idris

64

65

65 plus_ind : Nat -> Nat -> Nat

66 plus_ind : Nat -> Nat -> Nat

66− plus_ind n m

67+ plus_ind n m

67 = nat_induction (\x => Nat)

68 = nat_induction (\x => Nat)

68 m -- Base case, plus_ind Z m

69 m -- Base case, plus_ind Z m

69 (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m

70 (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m

70 -- where k_rec = plus_ind k m

71 -- where k_rec = plus_ind k m

71− n

72+ n

72

73

73To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and

74To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and

74``m``, we can also use induction. Either we can fix ``m`` and perform

75``m``, we can also use induction. Either we can fix ``m`` and perform

docs/proofs/interactive.rstnew file+165

@@ -0,0 +1,165 @@

1+***************************

2+Interactive Theorem Proving

3+***************************

4+

5+Idris also supports interactive theorem proving via tactics. This

6+is generally not recommended to be used directly, but rather used as a

7+mechanism for building proof automation which is beyond the scope of this

8+tutorial. In this section, we briefly discus tactics.

9+

10+One way to write proofs interactively is to write the general *structure* of

11+the proof, and use the interactive mode to complete the details.

12+Consider the following definition, proved in :ref:`sect-theorems`:

13+

14+.. code-block:: idris

15+

16+ plusReduces : (n:Nat) -> plus Z n = n

17+

18+We’ll be constructing the proof by *induction*, so we write the cases for ``Z``

19+and ``S``, with a recursive call in the ``S`` case giving the inductive

20+hypothesis, and insert *metavariables* for the rest of the definition:

21+

22+.. code-block:: idris

23+

24+ plusReducesZ' : (n:Nat) -> n = plus n Z

25+ plusReducesZ' Z = ?plusredZ_Z

26+ plusReducesZ' (S k) = let ih = plusReducesZ' k in

27+ ?plusredZ_S

28+

29+On running , two global names are created, ``plusredZ_Z`` and

30+``plusredZ_S``, with no definition. We can use the ``:m`` command at the

31+prompt to find out which metavariables are still to be solved (or, more

32+precisely, which functions exist but have no definitions), then the

33+``:t`` command to see their types:

34+

35+.. code-block:: idris

36+

37+ *theorems> :m

38+ Global metavariables:

39+ [plusredZ_S,plusredZ_Z]

40+

41+.. code-block:: idris

42+

43+ *theorems> :t plusredZ_Z

44+ plusredZ_Z : Z = plus Z Z

45+

46+ *theorems> :t plusredZ_S

47+ plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z

48+

49+The ``:p`` command enters interactive proof mode, which can be used to

50+complete the missing definitions.

51+

52+.. code-block:: idris

53+

54+ *theorems> :p plusredZ_Z

55+

56+ ---------------------------------- (plusredZ_Z) --------

57+ {hole0} : Z = plus Z Z

58+

59+This gives us a list of premises (above the line; there are none here)

60+and the current goal (below the line; named ``{hole0}`` here). At the

61+prompt we can enter tactics to direct the construction of the proof. In

62+this case, we can normalise the goal with the ``compute`` tactic:

63+

64+.. code-block:: idris

65+

66+ -plusredZ_Z> compute

67+

68+ ---------------------------------- (plusredZ_Z) --------

69+ {hole0} : Z = Z

70+

71+Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by

72+``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which

73+introduces subgoals for each of the function’s explicit arguments

74+(``Refl`` has none):

75+

76+.. code-block:: idris

77+

78+ -plusredZ_Z> refine Refl

79+ plusredZ_Z: no more goals

80+

81+Here, we could also have used the ``trivial`` tactic, which tries to

82+refine by ``Refl``, and if that fails, tries to refine by each name in

83+the local context. When a proof is complete, we use the ``qed`` tactic

84+to add the proof to the global context, and remove the metavariable from

85+the unsolved metavariables list. This also outputs a trace of the proof:

86+

87+.. code-block:: idris

88+

89+ -plusredZ_Z> qed

90+ plusredZ_Z = proof

91+ compute

92+ refine Refl

93+

94+.. code-block:: idris

95+

96+ *theorems> :m

97+ Global metavariables:

98+ [plusredZ_S]

99+

100+The ``:addproof`` command, at the interactive prompt, will add the proof

101+to the source file (effectively in an appendix). Let us now prove the

102+other required lemma, ``plusredZ_S``:

103+

104+.. code-block:: idris

105+

106+ *theorems> :p plusredZ_S

107+

108+ ---------------------------------- (plusredZ_S) --------

109+ {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z

110+

111+In this case, the goal is a function type, using ``k`` (the argument

112+accessible by pattern matching) and ``ih`` — the local variable

113+containing the result of the recursive call. We can introduce these as

114+premisses using the ``intro`` tactic twice (or ``intros``, which

115+introduces all arguments as premisses). This gives:

116+

117+.. code-block:: idris

118+

119+ k : Nat

120+ ih : k = plus k Z

121+ ---------------------------------- (plusredZ_S) --------

122+ {hole2} : S k = plus (S k) Z

123+

124+Since plus is defined by recursion on its first argument, the term

125+``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.

126+

127+.. code-block:: idris

128+

129+ k : Nat

130+ ih : k = plus k Z

131+ ---------------------------------- (plusredZ_S) --------

132+ {hole2} : S k = S (plus k Z)

133+

134+We know, from the type of ``ih``, that ``k = plus k Z``, so we would

135+like to use this knowledge to replace ``plus k Z`` in the goal with

136+``k``. We can achieve this with the ``rewrite`` tactic:

137+

138+.. code-block:: idris

139+

140+ -plusredZ_S> rewrite ih

141+

142+ k : Nat

143+ ih : k = plus k Z

144+ ---------------------------------- (plusredZ_S) --------

145+ {hole3} : S k = S k

146+

147+ -plusredZ_S>

148+

149+The ``rewrite`` tactic takes an equality proof as an argument, and tries

150+to rewrite the goal using that proof. Here, it results in an equality

151+which is trivially provable:

152+

153+.. code-block:: idris

154+

155+ -plusredZ_S> trivial

156+ plusredZ_S: no more goals

157+ -plusredZ_S> qed

158+ plusredZ_S = proof {

159+ intros;

160+ rewrite ih;

161+ trivial;

162+ }

163+

164+Again, we can add this proof to the end of our source file using the

165+``:addproof`` command at the interactive prompt.

docs/proofs/patterns.rst+7−6

@@ -1,5 +1,6 @@

1+***********************

1Pattern Matching Proofs

2Pattern Matching Proofs

2−=======================

3+***********************

3

4

4In this section, we will provide a proof of ``plus_commutes`` directly,

5In this section, we will provide a proof of ``plus_commutes`` directly,

5by writing a pattern matching definition. We will use interactive

6by writing a pattern matching definition. We will use interactive

@@ -26,7 +27,7 @@ mapping to Emacs commands.

26

27

28

28Creating a Definition

29Creating a Definition

29−---------------------

30+=====================

30

31

31To begin, create a file ``pluscomm.idr`` containing the following type

32To begin, create a file ``pluscomm.idr`` containing the following type

32declaration:

33declaration:

@@ -87,7 +88,7 @@ It is a good idea to give these slightly more meaningful names:

87 plus_commutes (S k) m = ?plus_commutes_S

88 plus_commutes (S k) m = ?plus_commutes_S

88

89

89Base Case

90Base Case

90−---------

91+=========

91

92

92We can create a separate lemma for the base case interactively, by

93We can create a separate lemma for the base case interactively, by

93pressing ``\l`` with the cursor over ``plus_commutes_Z``. This

94pressing ``\l`` with the cursor over ``plus_commutes_Z``. This

@@ -263,7 +264,7 @@ proof, giving:

263The base case is now complete.

264The base case is now complete.

264

265

265Inductive Step

266Inductive Step

266−--------------

267+==============

267

268

268Our main theorem, ``plus_commutes`` should currently be in the following

269Our main theorem, ``plus_commutes`` should currently be in the following

269state:

270state:

@@ -333,9 +334,9 @@ defined by matching on its first argument. The complete definition is:

333 plus_commutes_S k Z = Refl

334 plus_commutes_S k Z = Refl

334 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

335

336

336−All metavariables have now been solved,

337+All metavariables have now been solved,

337

338

338−The ``total`` annotation means that we require the final function to

339+The ``total`` annotation means that we require the final function to

339pass the totality checker; i.e. it will terminate on all possible

340pass the totality checker; i.e. it will terminate on all possible

340well-typed inputs. This is important for proofs, since it provides a

341well-typed inputs. This is important for proofs, since it provides a

341guarantee that the proof is valid in *all* cases, not just those for

342guarantee that the proof is valid in *all* cases, not just those for

docs/proofs/pluscomm.rst+7−6

@@ -1,5 +1,6 @@

1+********************************************

1Running example: Addition of Natural Numbers

2Running example: Addition of Natural Numbers

2−============================================

3+********************************************

3

4

4Throughout this tutorial, we will be working with the following

5Throughout this tutorial, we will be working with the following

5function, defined in the Idris prelude, which defines addition on

6function, defined in the Idris prelude, which defines addition on

@@ -44,7 +45,7 @@ We can use these properties in an Idris program, but in order to do so

44we must *prove* them.

45we must *prove* them.

45

46

46Equality Proofs

47Equality Proofs

47−---------------

48+===============

48

49

49Idris has a built-in propositional equality type, conceptually defined

50Idris has a built-in propositional equality type, conceptually defined

50as follows:

51as follows:

@@ -93,7 +94,7 @@ error:

93 4 = 5 (Expected type)

94 4 = 5 (Expected type)

94

95

95Type checking equality proofs

96Type checking equality proofs

96−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

97+-----------------------------

97

98

98An important step in type checking Idris programs is *unification*,

99An important step in type checking Idris programs is *unification*,

99which attempts to resolve implicit arguments such as the implicit

100which attempts to resolve implicit arguments such as the implicit

@@ -123,7 +124,7 @@ following equalities directly:

123 plus_reduces_Sk k m = Refl

124 plus_reduces_Sk k m = Refl

124

125

125Heterogeneous Equality

126Heterogeneous Equality

126−----------------------

127+======================

127

128

128Equality in Idris is *heterogeneous*, meaning that we can even propose

129Equality in Idris is *heterogeneous*, meaning that we can even propose

129equalities between values in different types:

130equalities between values in different types:

@@ -164,7 +165,7 @@ there is only one value which will type check:

164 vect_eq_length xs _ Refl = Refl

165 vect_eq_length xs _ Refl = Refl

165

166

166Properties of ``plus``

167Properties of ``plus``

167−----------------------

168+======================

168

169

169Using the ``(=)`` type, we can now state the properties of ``plus``

170Using the ``(=)`` type, we can now state the properties of ``plus``

170given above as Idris type declarations:

171given above as Idris type declarations:

@@ -185,4 +186,4 @@ the function.) We will also discuss how to use such equality proofs, and

185see where the need for them arises in practice.

186see where the need for them arises in practice.

186

187

187.. [1]

188.. [1]

188− This is known as the Curry-Howard correspondence

189+ This is known as the Curry-Howard correspondence.

docs/reference/documenting.rst+4−4

@@ -1,8 +1,8 @@

1.. _sect-documenting:

2

3−======================

3+**********************

4Documenting Idris Code

5−======================

5+**********************

6

7Idris documentation comes in two major forms: comments, which exist

8for a reader’s edification and are ignored by the compiler, and inline

@@ -12,7 +12,7 @@ reference. To consult the documentation for a declaration ``f``, write

12(``C-c C-d`` in Emacs, in Vim).

13

14Comments

15−--------

15+========

16

17Use comments to explain why code is written the way that it

18is. Idris’s comment syntax is the same as that of Haskell: lines

@@ -22,7 +22,7 @@ lines. These can be used to comment out lines of code or provide

22simple documentation for the readers of Idris code.

23

24Inline Documentation

25−--------------------

25+====================

26

27Idris also supports a comprehensive and rich inline syntax for Idris

28code to be generated. This syntax also allows for named parameters and

docs/reference/erasure.rst+21−20

@@ -1,5 +1,6 @@

1+*************************

1Erasure By Usage Analysis

2Erasure By Usage Analysis

2−=========================

3+*************************

3

4

4This work stems from this `feature proposal

5This work stems from this `feature proposal

5<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__

6<https://github.com/idris-lang/Idris-dev/wiki/Egg-%232%3A-Erasure-annotations>`__

@@ -8,7 +9,7 @@ is out of date — and sometimes even in direct contradiction with the

8eventual implementation.

9eventual implementation.

9

10

10Motivation

11Motivation

11−----------

12+==========

12

13

13Traditional dependently typed languages (Agda, Coq) are good at

14Traditional dependently typed languages (Agda, Coq) are good at

14erasing *proofs* (either via irrelevance or an extra universe).

15erasing *proofs* (either via irrelevance or an extra universe).

@@ -52,7 +53,7 @@ The following two sections describe two cases where doing so improves

52the runtime performance asymptotically.

53the runtime performance asymptotically.

53

54

54Binary numbers

55Binary numbers

55−~~~~~~~~~~~~~~

56+--------------

56

57

57- O(n) instead of O(log n)

58- O(n) instead of O(log n)

58

59

@@ -106,7 +107,7 @@ should get rid of them and get runtime code similar to what a idris

106programmer would write.

107programmer would write.

107

108

108U-views of lists

109U-views of lists

109−~~~~~~~~~~~~~~~~

110+----------------

110

111

111- O(n^2) instead of O(n)

112- O(n^2) instead of O(n)

112

113

@@ -141,7 +142,7 @@ linear time — so we need to erase the index ``xs`` if we want to

141achieve this goal.

142achieve this goal.

142

143

143Changes to Idris

144Changes to Idris

144−----------------

145+================

145

146

146Usage analysis is run at every compilation and its outputs are used

147Usage analysis is run at every compilation and its outputs are used

147for various purposes. This is actually invisible to the user but it's

148for various purposes. This is actually invisible to the user but it's

@@ -185,7 +186,7 @@ Postulates are no longer required to be collapsible. They are now

185required to be *unused* instead.

186required to be *unused* instead.

186

187

187Changes to the language

188Changes to the language

188−-----------------------

189+=======================

189

190

190You can use dots to mark fields that are not intended to be used at

191You can use dots to mark fields that are not intended to be used at

191runtime.

192runtime.

@@ -221,7 +222,7 @@ You can also put dots in types of functions to get more guarantees.

221and free implicits are automatically dotted here, too.

222and free implicits are automatically dotted here, too.

222

223

223What it means

224What it means

224−-------------

225+=============

225

226

226Dot annotations serve two purposes:

227Dot annotations serve two purposes:

227

228

@@ -235,7 +236,7 @@ are there mainly to help the programmer (and the compiler) refrain

235from using the values they want to erase.

236from using the values they want to erase.

236

237

237How to use it

238How to use it

238−-------------

239+=============

239

240

240Ideally, few or no extra annotations are needed -- in practice, it

241Ideally, few or no extra annotations are needed -- in practice, it

241turns out that having free implicits automatically dotted is enough to

242turns out that having free implicits automatically dotted is enough to

@@ -250,7 +251,7 @@ compiles to a reasonable binary. Generally, it's sufficient to follow

250erasure warnings (which may be sometimes unhelpful at the moment).

251erasure warnings (which may be sometimes unhelpful at the moment).

251

252

252Benchmarks

253Benchmarks

253−----------

254+==========

254

255

255- source: https://github.com/ziman/idris-benchmarks

256- source: https://github.com/ziman/idris-benchmarks

256- results: http://ziman.functor.sk/erasure-bm/

257- results: http://ziman.functor.sk/erasure-bm/

@@ -258,7 +259,7 @@ Benchmarks

258It can be clearly seen that asymptotics are improved by erasure.

259It can be clearly seen that asymptotics are improved by erasure.

259

260

260Shortcomings

261Shortcomings

261−------------

262+============

262

263

263You can't get warnings in libraries because usage analysis starts from

264You can't get warnings in libraries because usage analysis starts from

264``Main.main``. This will be solved by the planned ``%default_usage``

265``Main.main``. This will be solved by the planned ``%default_usage``

@@ -300,7 +301,7 @@ only if it is unused in every implementation of the method that occurs

300in the program.

301in the program.

301

302

302Planned features

303Planned features

303−----------------

304+================

304

305

305- Fixes to the above shortcomings in general.

306- Fixes to the above shortcomings in general.

306

307

@@ -316,10 +317,10 @@ Planned features

316 in compiled programs.

317 in compiled programs.

317

318

318Troubleshooting

319Troubleshooting

319−---------------

320+===============

320

321

321My program is slower

322My program is slower

322−~~~~~~~~~~~~~~~~~~~~

323+--------------------

323

324

324The patch introducing erasure by usage analysis also disabled some

325The patch introducing erasure by usage analysis also disabled some

325optimisations that were in place before; these are subsumed by the new

326optimisations that were in place before; these are subsumed by the new

@@ -336,14 +337,14 @@ getting compiled into the binary.

336The solution is to change the code so that there are no warnings.

337The solution is to change the code so that there are no warnings.

337

338

338Usage warnings are unhelpful

339Usage warnings are unhelpful

339−~~~~~~~~~~~~~~~~~~~~~~~~~~~~

340+----------------------------

340

341

341This is a known issue and we are working on it. For now, see the section

342This is a known issue and we are working on it. For now, see the section

342`How to read and resolve erasure

343`How to read and resolve erasure

343warnings <#how-to-read-and-resolve-erasure-warnings>`__.

344warnings <#how-to-read-and-resolve-erasure-warnings>`__.

344

345

345There should be no warnings in this function

346There should be no warnings in this function

346−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

347+--------------------------------------------

347

348

348A possible cause is non-totality of the function (more precisely,

349A possible cause is non-totality of the function (more precisely,

349non-coverage). If a function is non-covering, the program needs to

350non-coverage). If a function is non-covering, the program needs to

@@ -361,7 +362,7 @@ https://gist.github.com/ziman/10458331). You can either rephrase the

361function or wait until this is fixed, hopefully soon. Fixed.

362function or wait until this is fixed, hopefully soon. Fixed.

362

363

363The compiler refuses to recognise this thing as erased

364The compiler refuses to recognise this thing as erased

364−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

365+------------------------------------------------------

365

366

366You can force anything to be erased by wrapping it in the ``Erased``

367You can force anything to be erased by wrapping it in the ``Erased``

367monad. While this program triggers usage warnings,

368monad. While this program triggers usage warnings,

@@ -379,10 +380,10 @@ the following program does not:

379 f g x = g (Erase x) -- OK

380 f g x = g (Erase x) -- OK

380

381

381How to read and resolve erasure warnings

382How to read and resolve erasure warnings

382−----------------------------------------

383+========================================

383

384

384Example 1

385Example 1

385−~~~~~~~~~

386+---------

386

387

387Consider the following program:

388Consider the following program:

388

389

@@ -439,7 +440,7 @@ or fixing ``vlen`` to not use the index:

439Which solution is appropriate depends on the usecase.

440Which solution is appropriate depends on the usecase.

440

441

441Example 2

442Example 2

442−~~~~~~~~~

443+---------

443

444

444Consider the following program manipulating value-indexed binary

445Consider the following program manipulating value-indexed binary

445numbers.

446numbers.

@@ -494,7 +495,7 @@ with every constructor of ``Bin`` and make it a bound implicit:

494 I : {n : Nat} -> bin n -> Bin (1 + n + n)

495 I : {n : Nat} -> bin n -> Bin (1 + n + n)

495

496

496References

497References

497−----------

498+==========

498

499

499.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

500.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

500 families need not store their indices

501 families need not store their indices

docs/reference/ffi.rst+8−7

@@ -1,5 +1,6 @@

1+******************************

1New Foreign Function Interface

2New Foreign Function Interface

2−==============================

3+******************************

3

4

4.. sectionauthor:: Edwin Brady

5.. sectionauthor:: Edwin Brady

5

6

@@ -19,7 +20,7 @@ are some things you will need to be aware of, which this page

19describes.

20describes.

20

21

21The ``IO'`` monad, and ``main``

22The ``IO'`` monad, and ``main``

22−-------------------------------

23+===============================

23

24

24The ``IO`` monad exists as before, but is now specific to the C

25The ``IO`` monad exists as before, but is now specific to the C

25backend (or, more precisely, any backend whose foreign function calls

26backend (or, more precisely, any backend whose foreign function calls

@@ -61,7 +62,7 @@ function's name, but potentially something more complicated such as an

61external library file or even a URL).

62external library file or even a URL).

62

63

63FFI descriptors

64FFI descriptors

64−---------------

65+===============

65

66

66An FFI descriptor is a record containing a predicate which holds when

67An FFI descriptor is a record containing a predicate which holds when

67a type can be marshalled, and the type of the target of a foreign

68a type can be marshalled, and the type of the target of a foreign

@@ -98,7 +99,7 @@ For C, this is:

98 String -- the name of the C function

99 String -- the name of the C function

99

100

100Foreign calls

101Foreign calls

101−-------------

102+=============

102

103

103To call a foreign function, the ``foreign`` function is used. For

104To call a foreign function, the ``foreign`` function is used. For

104example:

105example:

@@ -134,7 +135,7 @@ example a shorthand for calling external JavaScript functions:

134 jscall fname ty = foreign FFI_JS fname ty

135 jscall fname ty = foreign FFI_JS fname ty

135

136

136FFI implementation

137FFI implementation

137−~~~~~~~~~~~~~~~~~~

138+------------------

138

139

139In order to write bindings to external libraries, the details of how

140In order to write bindings to external libraries, the details of how

140``foreign`` works are unnecessary --- you simply need to know that

141``foreign`` works are unnecessary --- you simply need to know that

@@ -172,7 +173,7 @@ builds the following implicit proof as the ``fty`` argument to

172 FFun C_Str (FFun C_Str (FRet C_Ptr))

173 FFun C_Str (FFun C_Str (FRet C_Ptr))

173

174

174Compiling foreign calls

175Compiling foreign calls

175−-----------------------

176+=======================

176

177

177(This section assumes some knowledge of the Idris internals.)

178(This section assumes some knowledge of the Idris internals.)

178

179

@@ -232,7 +233,7 @@ to marshal the arguments and return value appropriately.

232 the function ``toFType``, to see how this works in practice.

233 the function ``toFType``, to see how this works in practice.

233

234

234JavaScript FFI descriptor

235JavaScript FFI descriptor

235−~~~~~~~~~~~~~~~~~~~~~~~~~

236+=========================

236

237

237The JavaScript FFI descriptor is a little more complex, because the

238The JavaScript FFI descriptor is a little more complex, because the

238JavaScript FFI supports marshalling functions. It is defined as

239JavaScript FFI supports marshalling functions. It is defined as

docs/reference/uniqueness-types.rst+5−4

@@ -1,5 +1,6 @@

1+****************

1Uniqueness Types

2Uniqueness Types

2−================

3+****************

3

4

4Uniqueness Types are an experimental feature available from Idris

5Uniqueness Types are an experimental feature available from Idris

50.9.15. A value with a unique type is guaranteed to have *at most one*

60.9.15. A value with a unique type is guaranteed to have *at most one*

@@ -25,7 +26,7 @@ include:

25 allocate

26 allocate

26

27

27Using Uniqueness

28Using Uniqueness

28−~~~~~~~~~~~~~~~~

29+================

29

30

30If ``x : T`` and ``T : UniqueType``, then there is at most one reference

31If ``x : T`` and ``T : UniqueType``, then there is at most one reference

31to ``x`` at any time during run-time execution. For example, we can

32to ``x`` at any time during run-time execution. For example, we can

@@ -129,7 +130,7 @@ such a function may be passed a ``UniqueType``, any value of type

129once on the right hand side.

130once on the right hand side.

130

131

131Borrowed Types

132Borrowed Types

132−~~~~~~~~~~~~~~

133+--------------

133

134

134It quickly becomes obvious when working with uniqueness types that

135It quickly becomes obvious when working with uniqueness types that

135having only one reference at a time can be painful. For example, what

136having only one reference at a time can be painful. For example, what

@@ -227,7 +228,7 @@ therefore write ``showU`` as follows:

227 showU' (x :: xs) = show x ++ ", " ++ showU' xs

228 showU' (x :: xs) = show x ++ ", " ++ showU' xs

228

229

229Problems/Disadvantages/Still to do...

230Problems/Disadvantages/Still to do...

230−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

231+-------------------------------------

231

232

232This is a work in progress, there is lots to do. The most obvious

233This is a work in progress, there is lots to do. The most obvious

233problem is the loss of abstraction. On the one hand, we have more

234problem is the loss of abstraction. On the one hand, we have more

docs/tutorial/classes.rst+12−12

@@ -1,8 +1,8 @@

1.. _sect-classes:

2

3−============

3+************

4Type Classes

5−============

5+************

6

7We often want to define functions which work across several different

8data types. For example, we would like arithmetic operators to work on

@@ -65,7 +65,7 @@ going to use it to convert each element to a ``String``:

65 show' (x :: xs) = show x ++ ", " ++ show' xs

66

67Default Definitions

68−-------------------

68+===================

69

70The library defines an ``Eq`` class which provides an interface for

71comparing values for equality or inequality, with instances for all of

@@ -110,7 +110,7 @@ definition is missing, and there is a default definition for it, then

110the default is used instead.

111

112Extending Classes

113−-----------------

113+=================

114

115Classes can also be extended. A logical next step from an equality

116relation ``Eq`` is to define an ordering relation ``Ord``. We can

@@ -155,7 +155,7 @@ separated list, for example:

155 sortAndShow xs = show (sort xs)

156

157Functors and Applicatives

158−-------------------------

158+=========================

159

160So far, we have seen single parameter type classes, where the parameter

161is of type ``Type``. In general, there can be any number (greater than

@@ -195,7 +195,7 @@ abstracts the notion of function application:

195 (<*>) : f (a -> b) -> f a -> f b

196

197Monads and ``do``-notation

198−--------------------------

198+==========================

199

200The ``Monad`` class allows us to encapsulate binding and computation,

201and is the basis of ``do``-notation introduced in Section

@@ -248,7 +248,7 @@ are available, or return ``Nothing`` if they are not. Managing the

248 Nothing : Maybe Int

249

250``!``-notation

251−~~~~~~~~~~~~~~

251+--------------

252

253In many cases, using ``do``-notation can make programs unnecessarily

254verbose, particularly in cases such as ``m_add`` above where the value

@@ -292,7 +292,7 @@ is lifted to:

292 f g'

293

294Monad comprehensions

295−~~~~~~~~~~~~~~~~~~~~

295+--------------------

296

297The list comprehension notation we saw in Section

298:ref:`sect-more-expr` is more general, and applies to anything which

@@ -336,7 +336,7 @@ would be:

336 m_add x y = [ x' + y' | x' <- x, y' <- y ]

337

338Idiom brackets

339−--------------

339+==============

340

341While ``do`` notation gives an alternative meaning to sequencing,

342idioms give an alternative meaning to *application*. The notation and

@@ -386,7 +386,7 @@ application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>

386 m_add' x y = [| x + y |]

387

388An error-handling interpreter

389−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

389+-----------------------------

390

391Idiom notation is commonly useful when defining evaluators. McBride

392and Paterson describe such an evaluator [1]_, for a language similar

@@ -455,7 +455,7 @@ to handle errors:

455 MkEval envFn => envFn env

456

457Named Instances

458−---------------

458+===============

459

460It can be desirable to have multiple instances of a type class, for

461example to provide alternative methods for sorting or printing values.

@@ -492,7 +492,7 @@ instance ``myord`` as follows, at the Idris prompt:

492

493

494Determining Parameters

495−----------------------

495+======================

496

497When a class has more than one parameter, it can help resolution if

498the parameters used to resolve the type class are restricted. For

docs/tutorial/conclusions.rst+2−2

@@ -1,8 +1,8 @@

1.. _sect-concs:

2

3−===============

3+***************

4Further Reading

5−===============

5+***************

6

7Further information about Idris programming, and programming with

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

docs/tutorial/index.rst+3−3

@@ -1,8 +1,8 @@

1.. _tutorial-index:

2

3−####################

3+##################

4− The Idris Tutorial

4+The Idris Tutorial

5−####################

5+##################

6

7The is the Idris Tutorial. It will teach you about programming in the Idris Language.

8

docs/tutorial/interactive.rst+10−10

@@ -1,8 +1,8 @@

1.. _sect-interactive:

2

3−===================

3+*******************

4Interactive Editing

5−===================

5+*******************

6

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

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

@@ -25,7 +25,7 @@ available.

25

26

27Editing at the REPL

28−-------------------

28+===================

29

30The REPL provides a number of commands, which we will describe

31shortly, which generate new program fragments based on the currently

@@ -59,10 +59,10 @@ A text editor can take advantage of this, along with the editing

59commands, in order to provide interactive editing support.

60

61Editing Commands

62−----------------

62+================

63

64:addclause

65−~~~~~~~~~~

65+----------

66

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

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

@@ -91,7 +91,7 @@ This declares that any names generated for types in the ``Vect`` family

91should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.

92

93:casesplit

94−~~~~~~~~~~

94+----------

95

96The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the

97pattern variable ``x`` on line ``n`` into the various pattern forms it

@@ -125,7 +125,7 @@ That is, the pattern variable ``ys`` has been split into one case

125ys`` would lead to a unification error.

126

127:addmissing

128−~~~~~~~~~~~

128+-----------

129

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

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

@@ -148,7 +148,7 @@ generates the required clauses, and eliminates the clauses which would

148lead to unification errors.

149

150:proofsearch

151−~~~~~~~~~~~~

151+------------

152

153The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to

154find a value for the metavariable ``f`` on line ``n`` by proof search,

@@ -186,7 +186,7 @@ must have type ``c`` and the only way to get this is to apply ``f`` to

186recursively.

187

188:makewith

189−~~~~~~~~~

189+---------

190

191The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a

192``with`` to a pattern clause. For example, recall ``parity``. If line

@@ -219,7 +219,7 @@ dependent pattern matching by showing a programmer exactly what the

219valid patterns are.

220

221Interactive Editing in Vim

222−--------------------------

222+==========================

223

224The editor mode for Vim provides syntax highlighting, indentation and

225interactive editing support using the commands described above.

docs/tutorial/interp.rst+7−7

@@ -1,8 +1,8 @@

1.. _sect-interp:

2

3−===================================

3+***********************************

4Example: The Well-Typed Interpreter

5−===================================

5+***********************************

6

7In this section, we’ll use the features we’ve seen so far to write a

8larger example, an interpreter for a simple functional programming

@@ -12,7 +12,7 @@ system to ensure that any programs which can be represented are

12well-typed.

13

14Representing Languages

15−----------------------

15+======================

16

17First, let us define the types in the language. We have integers,

18booleans, and functions, represented by ``Ty``:

@@ -140,7 +140,7 @@ that only the branch which is taken need be evaluated:

140 Expr G a

141

142Writing the Interpreter

143−-----------------------

143+=======================

144

145When we evaluate an ``Expr``, we’ll need to know the values in scope,

146as well as their types. ``Env`` is an environment, indexed over the

@@ -225,7 +225,7 @@ its operands directly, and for ``If``, we apply the Idris

225 else interp env e

226

227Testing

228−-------

228+=======

229

230We can make some simple test functions. Firstly, adding two inputs

231``\x. \y. y + x`` is written as follows:

@@ -248,7 +248,7 @@ can be written as:

248 (Var Stop)))

249

250Running

251−-------

251+=======

252

253To finish, we write a ``main`` program which interprets the factorial

254function on user input:

@@ -271,7 +271,7 @@ program at the Idris interactive environment is:

271

272

273Aside: ``cast``

274−~~~~~~~~~~~~~~~

274+---------------

275

276The prelude defines a type class ``Cast`` which allows conversion

277between types:

docs/tutorial/introduction.rst+4−4

@@ -1,8 +1,8 @@

1.. _sect-intro:

2

3−============

3+************

4Introduction

5−============

5+************

6

7In conventional programming languages, there is a clear distinction

8between *types* and *values*. For example, in `Haskell

@@ -44,7 +44,7 @@ a lightweight foreign function interface which allows easy interaction

44with external ``C`` libraries.

45

46Intended Audience

47−-----------------

47+=================

48

49This tutorial is intended as a brief introduction to the language, and

50is aimed at readers already familiar with a functional language such

@@ -55,7 +55,7 @@ briefly. The reader is also assumed to have some interest in using

55dependent types for writing and verifying systems software.

56

57Example Code

58−------------

58+============

59

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

61Idris version . The files are available in the Idris

docs/tutorial/miscellany.rst+17−17

@@ -1,8 +1,8 @@

1.. _sect-misc:

2

3−==========

3+**********

4Miscellany

5−==========

5+**********

6

7In this section we discuss a variety of additional features:

8

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

15+ the universe hierarchy.

16

17Auto implicit arguments

18−-----------------------

18+=======================

19

20We have already seen implicit arguments, which allows arguments to be

21omitted when they can be inferred by the type checker, e.g.

@@ -70,7 +70,7 @@ to:

70 head (x :: xs) = x

71

72Implicit conversions

73−--------------------

73+====================

74

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

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

@@ -99,7 +99,7 @@ specific language, or to hide details of a proof. Such examples are

99beyond the scope of this tutorial.

100

101Literate programming

102−--------------------

102+====================

103

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

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

@@ -120,7 +120,7 @@ program line (beginning with ``>``) and a comment line (beginning with

120any other character).

121

122Foreign function calls

123−----------------------

123+======================

124

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

126external libraries, particularly for interfacing with the operating

@@ -191,7 +191,7 @@ function is implemented as follows, as a call to an external function

191 putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

192

193Include and linker directives

194−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

194+-----------------------------

195

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

197with appropriate conversion between the Idris representation of a

@@ -215,7 +215,7 @@ through the following directives:

215 object ``x.so``.

216

217Testing foreign function calls

218−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

218+------------------------------

219

220Normally, the Idris interpreter (used for typechecking and at the REPL)

221will not perform IO actions. Additionally, as it neither generates C

@@ -232,7 +232,7 @@ command or the ``%dynamic`` directive. For example:

232 0.9995736030415051 : Float

233

234Type Providers

235−--------------

235+==============

236

237Idris type providers, inspired by F#’s type providers, are a means of

238making our types be “about” something in the world outside of Idris. For

@@ -301,7 +301,7 @@ provider implementations, including a statically-checked SQLite binding,

301are available in an external collection [1]_.

302

303C Target

304−--------

304+========

305

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

307

@@ -341,14 +341,14 @@ is shown below :

341 putStrLn $ show $ factorial 3

342

343JavaScript Target

344−-----------------

344+=================

345

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

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

348FFI to communicate with the *JavaScript* ecosystem.

349

350Code Generation

351−~~~~~~~~~~~~~~~

351+---------------

352

353Code generation is split into two separate targets. To generate code

354that is tailored for running in the browser issue the following command:

@@ -375,7 +375,7 @@ automatically add a newline to the end of each string. This behaviour

375does not show up in the *NodeJS* code generator.

376

377Using the FFI

378−~~~~~~~~~~~~~

378+-------------

379

380To write a useful application we need to communicate with the outside

381world. Maybe we want to manipulate the DOM or send an Ajax request. For

@@ -441,7 +441,7 @@ program:

441The program outputs ``3``, just like we expected.

442

443Including external *JavaScript* files

444−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

444+-------------------------------------

445

446Whenever one is working with *JavaScript* one might want to include

447external libraries or just some functions that she or he wants to call

@@ -470,7 +470,7 @@ And for use in the browser:

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

471

472Including *NodeJS* modules

473−~~~~~~~~~~~~~~~~~~~~~~~~~~

473+--------------------------

474

475The *NodeJS* code generator can also include modules with the ``%lib``

476directive.

@@ -486,7 +486,7 @@ This directive compiles into the following *JavaScript*

486 var fs = require("fs");

487

488Shrinking down generated *JavaScript*

489−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

489+-------------------------------------

490

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

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

@@ -497,7 +497,7 @@ and it’s highly recommended to use it when shipping a *JavaScript*

497application written in Idris.

498

499Cumulativity

500−------------

500+============

501

502Since values can appear in types and *vice versa*, it is natural that

503types themselves have types. For example:

docs/tutorial/modules.rst+5−5

@@ -1,8 +1,8 @@

1.. _sect-namespaces:

2

3−=======================

3+**********************

4Modules and Namespaces

5−=======================

5+**********************

6

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

8includes an optional ``module`` declaration giving the name of the

@@ -72,7 +72,7 @@ main module, with the ``main`` function, must be called

72``Main``—although its filename need not be ``Main.idr``.

73

74Export Modifiers

75−----------------

75+================

76

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

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

@@ -146,7 +146,7 @@ abstract names in module ``C``, but will not re-export anything from

146module ``B``.

147

148Explicit Namespaces

149−-------------------

149+===================

150

151Defining a module also defines a namespace implicitly. However,

152namespaces can also be given *explicitly*. This is most useful if you

@@ -176,7 +176,7 @@ disambiguated by their types:

176 "foofoo" : String

177

178Parameterised blocks

179−--------------------

179+====================

180

181Groups of functions can be parameterised over a number of arguments

182using a ``parameters`` declaration, for example:

docs/tutorial/packages.rst+4−4

@@ -1,8 +1,8 @@

1.. _sect-packages:

2

3−========

3+********

4Packages

5−========

5+********

6

7Idris includes a simple system for building packages from a

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

@@ -10,7 +10,7 @@ compiler to manage the development process of your Idris

10programmes and packages.

11

12Package Descriptions

13−--------------------

13+====================

14

15A package description includes the following:

16

@@ -58,7 +58,7 @@ external ``C`` libraries, the following options are available:

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

59

60Using Package files

61−-------------------

61+===================

62

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

64

docs/tutorial/provisional.rst+5−5

@@ -1,8 +1,8 @@

1.. _sect-provisional:

2

3−=======================

3+***********************

4Provisional Definitions

5−=======================

5+***********************

6

7Sometimes when programming with dependent types, the type required by

8the type checker and the type of the program we have written will be

@@ -54,7 +54,7 @@ reduction. These values are obviously equal — how can we rewrite the

54program to fix this problem?

55

56Provisional definitions

57−-----------------------

57+=======================

58

59*Provisional definitions* help with this problem by allowing us to defer

60the proof details until a later point. There are two main reasons why

@@ -159,7 +159,7 @@ reversed:

159 "[False, True, False, True, False, True]" : String

160

161Suspension of Disbelief

162−-----------------------

162+=======================

163

164Idris requires that proofs be complete before compiling programs

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

@@ -192,7 +192,7 @@ The ``exact`` tactic allows us to provide an exact value for the proof.

192In this case, we assert that the value we gave was correct.

193

194Example: Binary numbers

195−-----------------------

195+=======================

196

197Previously, we implemented conversion to binary numbers using the

198``Parity`` view. Here, we show how to use the same view to implement a

docs/tutorial/starting.rst+5−5

@@ -1,11 +1,11 @@

1.. _sect-starting:

2

3−===============

3+***************

4Getting Started

5−===============

5+***************

6

7Prerequisites

8−-------------

8+=============

9

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

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

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

18 from MacPorts/Homebrew and all major Linux distributions.

19

20Downloading and Installing

21−--------------------------

21+==========================

22

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

24prerequisites, is to type:

@@ -69,7 +69,7 @@ instead. Some useful options to the Idris command are:

69- ``--help`` display usage summary and command line options

70

71The Interactive Environment

72−---------------------------

72+===========================

73

74Entering ``idris`` at the shell prompt starts up the interactive

75environment. You should see something like the following:

docs/tutorial/syntax.rst+11−8

@@ -1,14 +1,17 @@

1+.. _sect-syntax:

2+

3+*****************

1Syntax Extensions

4Syntax Extensions

2−=================

5+*****************

3

6

4−supports the implementation of *Embedded Domain Specific Languages*

7+Idris supports the implementation of *Embedded Domain Specific

5−(EDSLs) in several ways [1]_. One way, as we have already seen, is

8+Languages* (EDSLs) in several ways [1]_. One way, as we have already

6−through extending ``do`` notation. Another important way is to allow

9+seen, is through extending ``do`` notation. Another important way is

7−extension of the core syntax. In this section we describe two ways of

10+to allow extension of the core syntax. In this section we describe two

8−extending the syntax: ``syntax`` rules and ``dsl`` notation.

11+ways of extending the syntax: ``syntax`` rules and ``dsl`` notation.

9

12

10``syntax`` rules

13``syntax`` rules

11−----------------

14+================

12

15

13We have seen ``if...then...else`` expressions, but these are not built

16We have seen ``if...then...else`` expressions, but these are not built

14in. Instead, we can define a function in the prelude as follows (we

17in. Instead, we can define a function in the prelude as follows (we

@@ -101,7 +104,7 @@ a bound variable, substituted on the right hand side. We have also put

101``in`` in quotation marks since it is already a reserved word.

104``in`` in quotation marks since it is already a reserved word.

102

105

103``dsl`` notation

106``dsl`` notation

104−----------------

107+================

105

108

106The well-typed interpreter in Section :ref:`sect-interp` is a simple

109The well-typed interpreter in Section :ref:`sect-interp` is a simple

107example of a common programming pattern with dependent types. Namely:

110example of a common programming pattern with dependent types. Namely:

docs/tutorial/theorems.rst+12−168

@@ -1,11 +1,11 @@

1.. _sect-theorems:

2

3−===============

3+***************

4Theorem Proving

5−===============

5+***************

6

7Equality

8−--------

8+========

9

10Idris allows propositional equalities to be declared, allowing theorems about

11programs to be stated and proved. Equality is built in, but conceptually

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

31.. _sect-empty:

32

33The Empty Type

34−--------------

34+==============

35

36There is an empty type, :math:`\bot`, which has no constructors. It is

37therefore impossible to construct an element of the empty type, at least

@@ -64,7 +64,7 @@ contradiction.

64 void : Void -> a

65

66Simple Theorems

67−---------------

67+===============

68

69When type checking dependent types, the type itself gets *normalised*.

70So imagine we want to prove the following theorem about the reduction

@@ -116,172 +116,16 @@ We can do the same for the reduction behaviour of plus on successors:

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

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

118becomes 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

123−an editor, see :ref:`proofs-index`. In the rest of this section, we discuss

123+an editor, see :ref:`proofs-index`.

124−Idris's interactive proof mode.

125−

126−Interactive theorem proving

127−---------------------------

128−

129−Instead of writing the proof in one go, we can use Idris’s interactive proof

130−mode. To do this, we write the general *structure* of the proof, and use

131−the interactive mode to complete the details. We’ll be constructing the

132−proof by *induction*, so we write the cases for ``Z`` and ``S``, with a

133−recursive call in the ``S`` case giving the inductive hypothesis, and

134−insert *metavariables* for the rest of the definition:

135−

136−.. code-block:: idris

137−

138− plusReducesZ' : (n:Nat) -> n = plus n Z

139− plusReducesZ' Z = ?plusredZ_Z

140− plusReducesZ' (S k) = let ih = plusReducesZ' k in

141− ?plusredZ_S

142−

143−On running , two global names are created, ``plusredZ_Z`` and

144−``plusredZ_S``, with no definition. We can use the ``:m`` command at the

145−prompt to find out which metavariables are still to be solved (or, more

146−precisely, which functions exist but have no definitions), then the

147−``:t`` command to see their types:

148−

149−.. code-block:: idris

150−

151− *theorems> :m

152− Global metavariables:

153− [plusredZ_S,plusredZ_Z]

154−

155−.. code-block:: idris

156−

157− *theorems> :t plusredZ_Z

158− plusredZ_Z : Z = plus Z Z

159−

160− *theorems> :t plusredZ_S

161− plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z

162−

163−The ``:p`` command enters interactive proof mode, which can be used to

164−complete the missing definitions.

165−

166−.. code-block:: idris

167−

168− *theorems> :p plusredZ_Z

169−

170− ---------------------------------- (plusredZ_Z) --------

171− {hole0} : Z = plus Z Z

172−

173−This gives us a list of premises (above the line; there are none here)

174−and the current goal (below the line; named ``{hole0}`` here). At the

175−prompt we can enter tactics to direct the construction of the proof. In

176−this case, we can normalise the goal with the ``compute`` tactic:

177−

178−.. code-block:: idris

179−

180− -plusredZ_Z> compute

181−

182− ---------------------------------- (plusredZ_Z) --------

183− {hole0} : Z = Z

184−

185−Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by

186−``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which

187−introduces subgoals for each of the function’s explicit arguments

188−(``Refl`` has none):

189−

190−.. code-block:: idris

191−

192− -plusredZ_Z> refine Refl

193− plusredZ_Z: no more goals

194−

195−Here, we could also have used the ``trivial`` tactic, which tries to

196−refine by ``Refl``, and if that fails, tries to refine by each name in

197−the local context. When a proof is complete, we use the ``qed`` tactic

198−to add the proof to the global context, and remove the metavariable from

199−the unsolved metavariables list. This also outputs a trace of the proof:

200−

201−.. code-block:: idris

202−

203− -plusredZ_Z> qed

204− plusredZ_Z = proof

205− compute

206− refine Refl

207−

208−.. code-block:: idris

209−

210− *theorems> :m

211− Global metavariables:

212− [plusredZ_S]

213−

214−The ``:addproof`` command, at the interactive prompt, will add the proof

215−to the source file (effectively in an appendix). Let us now prove the

216−other required lemma, ``plusredZ_S``:

217−

218−.. code-block:: idris

219−

220− *theorems> :p plusredZ_S

221−

222− ---------------------------------- (plusredZ_S) --------

223− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z

224−

225−In this case, the goal is a function type, using ``k`` (the argument

226−accessible by pattern matching) and ``ih`` — the local variable

227−containing the result of the recursive call. We can introduce these as

228−premisses using the ``intro`` tactic twice (or ``intros``, which

229−introduces all arguments as premisses). This gives:

230−

231−.. code-block:: idris

232−

233− k : Nat

234− ih : k = plus k Z

235− ---------------------------------- (plusredZ_S) --------

236− {hole2} : S k = plus (S k) Z

237−

238−Since plus is defined by recursion on its first argument, the term

239−``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.

240−

241−.. code-block:: idris

242−

243− k : Nat

244− ih : k = plus k Z

245− ---------------------------------- (plusredZ_S) --------

246− {hole2} : S k = S (plus k Z)

247−

248−We know, from the type of ``ih``, that ``k = plus k Z``, so we would

249−like to use this knowledge to replace ``plus k Z`` in the goal with

250−``k``. We can achieve this with the ``rewrite`` tactic:

251−

252−.. code-block:: idris

253−

254− -plusredZ_S> rewrite ih

255−

256− k : Nat

257− ih : k = plus k Z

258− ---------------------------------- (plusredZ_S) --------

259− {hole3} : S k = S k

260−

261− -plusredZ_S>

262−

263−The ``rewrite`` tactic takes an equality proof as an argument, and tries

264−to rewrite the goal using that proof. Here, it results in an equality

265−which is trivially provable:

266−

267−.. code-block:: idris

268−

269− -plusredZ_S> trivial

270− plusredZ_S: no more goals

271− -plusredZ_S> qed

272− plusredZ_S = proof {

273− intros;

274− rewrite ih;

275− trivial;

276− }

277−

278−Again, we can add this proof to the end of our source file using the

279−``:addproof`` command at the interactive prompt.

280

124

281.. _sect-totality:

125.. _sect-totality:

282

126

283Totality Checking

127Totality Checking

284−-----------------

128+=================

285

129

286If we really want to trust our proofs, it is important that they are

130If we really want to trust our proofs, it is important that they are

287defined by *total* functions — that is, a function which is defined for

131defined by *total* functions — that is, a function which is defined for

@@ -351,7 +195,7 @@ total, a function ``f`` must:

351- Not call any non-total functions

195- Not call any non-total functions

352

196

353Directives and Compiler Flags for Totality

197Directives and Compiler Flags for Totality

354−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

198+------------------------------------------

355

199

356By default, Idris allows all well-typed definitions, whether total or not.

200By default, Idris allows all well-typed definitions, whether total or not.

357However, it is desirable for functions to be total as far as possible, as this

201However, it is desirable for functions to be total as far as possible, as this

@@ -372,7 +216,7 @@ Finally, the compiler flag ``--warnpartial`` causes to print a warning

372for any undeclared partial function.

216for any undeclared partial function.

373

217

374Totality checking issues

218Totality checking issues

375−~~~~~~~~~~~~~~~~~~~~~~~~

219+------------------------

376

220

377Please note that the totality checker is not perfect! Firstly, it is

221Please note that the totality checker is not perfect! Firstly, it is

378necessarily conservative due to the undecidability of the halting

222necessarily conservative due to the undecidability of the halting

@@ -382,14 +226,14 @@ into it so far, so there may still be cases where it believes a function

382is total which is not. Do not rely on it for your proofs yet!

226is total which is not. Do not rely on it for your proofs yet!

383

227

384Hints for totality

228Hints for totality

385−~~~~~~~~~~~~~~~~~~

229+------------------

386

230

387In cases where you believe a program is total, but Idris does not agree, it is

231In cases where you believe a program is total, but Idris does not agree, it is

388possible to give hints to the checker to give more detail for a termination

232possible to give hints to the checker to give more detail for a termination

389argument. The checker works by ensuring that all chains of recursive calls

233argument. The checker works by ensuring that all chains of recursive calls

390eventually lead to one of the arguments decreasing towards a base case, but

234eventually lead to one of the arguments decreasing towards a base case, but

391sometimes this is hard to spot. For example, the following definition cannot be

235sometimes this is hard to spot. For example, the following definition cannot be

392−checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``

236+checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``

393will always be smaller than ``(x :: xs)``:

237will always be smaller than ``(x :: xs)``:

394

238

395.. code-block:: idris

239.. code-block:: idris

docs/tutorial/typesfuns.rst+42−33

@@ -1,11 +1,11 @@

1.. _sect-typefuns:

2

3−===================

3+*******************

4Types and Functions

5−===================

5+*******************

6

7Primitive Types

8−---------------

8+===============

9

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

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

@@ -71,7 +71,7 @@ work on user defined types. Boolean expressions can be tested with the

71 "The answer!" : String

72

73Data Types

74−----------

74+==========

75

76Data types are declared in a similar way to Haskell data types, with a

77similar syntax. Natural numbers and lists, for example, can be

@@ -105,7 +105,7 @@ symbols:

105 :+-*/=_.?|&><!@$%^~.

106

107Functions

108−---------

108+=========

109

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

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

@@ -175,7 +175,7 @@ numbers. This means it can optimise the representation, and functions

175such as ``plus`` and ``mult``.

176

177``where`` clauses

178−~~~~~~~~~~~~~~~~~

178+-----------------

179

180Functions can also be defined *locally* using ``where`` clauses. For

181example, to define a function which reverses a list, we can use an

@@ -241,10 +241,10 @@ So, for example, the following definitions are legal:

241 where z w = y + w

242

243Dependent Types

244−---------------

244+===============

245

246Vectors

247−~~~~~~~

247+-------

248

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

250length”, conventionally called vectors in the dependent type

@@ -322,7 +322,7 @@ two vectors — we needed a vector of length ``k + m``, but provided a

322vector of length ``k + k``.

323

324The Finite Sets

325−~~~~~~~~~~~~~~~

325+---------------

326

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

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

@@ -334,16 +334,25 @@ importing ``Data.Fin``, or can be declared as follows:

334 FZ : Fin (S k)

335 FS : Fin k -> Fin (S k)

336

337+From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.

338+So this is not a set in the sense of a collection that is a container of objects,

339+rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.

340+Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where

341+``n`` is the argument used to instantiate the ``Fin`` type.

342+For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.

343+

344+Let us look at the constructors in greater detail.

345+

337``FZ`` is the zeroth element of a finite set with ``S k`` elements;

346``FZ`` is the zeroth element of a finite set with ``S k`` elements;

338``FS n`` is the ``n+1``\ th element of a finite set with ``S k``

347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``

339elements. ``Fin`` is indexed by a ``Nat``, which represents the number

348elements. ``Fin`` is indexed by a ``Nat``, which represents the number

340−of elements in the set. Obviously we can’t construct an element of an

349+of elements in the set. Since we can’t construct an element of an

341−empty set, so neither constructor targets ``Fin Z``.

350+empty set, neither constructor targets ``Fin Z``.

342

351

343−A useful application of the ``Fin`` family is to represent bounded

352+As mentioned above, a useful application of the ``Fin`` family is to represent bounded

344natural numbers. Since the first ``n`` natural numbers form a finite

353natural numbers. Since the first ``n`` natural numbers form a finite

345−set of ``n`` elements, we can treat ``Fin n`` as the set of natural

354+set of ``n`` elements, we can treat ``Fin n`` as the set of integers

346−numbers bounded by ``n``.

355+greater than or equal to zero and less than ``n``.

347

356

348For example, the following function which looks up an element in a

357For example, the following function which looks up an element in a

349``Vect``, by a bounded index given as a ``Fin n``, is defined in the

358``Vect``, by a bounded index given as a ``Fin n``, is defined in the

@@ -359,7 +368,7 @@ This function looks up a value at a given location in a vector. The

359location is bounded by the length of the vector (``n`` in each case),

368location is bounded by the length of the vector (``n`` in each case),

360so there is no need for a run-time bounds check. The type checker

369so there is no need for a run-time bounds check. The type checker

361guarantees that the location is no larger than the length of the

370guarantees that the location is no larger than the length of the

362−vector.

371+vector, and of course no less than zero.

363

372

364Note also that there is no case for ``Nil`` here. This is because it

373Note also that there is no case for ``Nil`` here. This is because it

365is impossible. Since there is no element of ``Fin Z``, and the

374is impossible. Since there is no element of ``Fin Z``, and the

@@ -368,7 +377,7 @@ attempting to look up an element in an empty vector would give a

368compile time type error, since it would force ``n`` to be ``Z``.

377compile time type error, since it would force ``n`` to be ``Z``.

369

378

370Implicit Arguments

379Implicit Arguments

371−~~~~~~~~~~~~~~~~~~

380+------------------

372

381

373Let us take a closer look at the type of ``index``:

382Let us take a closer look at the type of ``index``:

374

383

@@ -411,7 +420,7 @@ help document a function by making the purpose of an argument more

411clear.

420clear.

412

421

413“``using``” notation

422“``using``” notation

414−~~~~~~~~~~~~~~~~~~~~

423+--------------------

415

424

416Sometimes it is useful to provide types of implicit arguments,

425Sometimes it is useful to provide types of implicit arguments,

417particularly where there is a dependency ordering, or where the

426particularly where there is a dependency ordering, or where the

@@ -451,7 +460,7 @@ appear within the block:

451 There : Elem x xs -> Elem x (y :: xs)

460 There : Elem x xs -> Elem x (y :: xs)

452

461

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

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

454−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

463+---------------------------------------------

455

464

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

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

457dependent types allow functions to appear as part of types, and their

466dependent types allow functions to appear as part of types, and their

@@ -476,7 +485,7 @@ depend on the reduction behaviour of any of the functions in the

476block.

485block.

477

486

478I/O

487I/O

479−---

488+===

480

489

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

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

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

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

@@ -533,7 +542,7 @@ example for reading and writing files, including:

533.. _sect-do:

542.. _sect-do:

534

543

535“``do``” notation

544“``do``” notation

536−-----------------

545+=================

537

546

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

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

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

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

@@ -564,7 +573,7 @@ can be overloaded.

564.. _sect-lazy:

573.. _sect-lazy:

565

574

566Laziness

575Laziness

567−--------

576+========

568

577

569Normally, arguments to functions are evaluated before the function

578Normally, arguments to functions are evaluated before the function

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

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

@@ -602,7 +611,7 @@ without any explicit use of ``Force`` or ``Delay``:

602 boolCase False t e = e;

611 boolCase False t e = e;

603

612

604Useful Data Types

613Useful Data Types

605−-----------------

614+=================

606

615

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

616Idris includes a number of useful data types and library functions

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

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

@@ -610,7 +619,7 @@ describes a few of these. The functions described here are imported

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

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

611

620

612``List`` and ``Vect``

621``List`` and ``Vect``

613−~~~~~~~~~~~~~~~~~~~~~

622+---------------------

614

623

615We have already seen the ``List`` and ``Vect`` data types:

624We have already seen the ``List`` and ``Vect`` data types:

616

625

@@ -683,7 +692,7 @@ remember that Idris is still in development, so if you don’t see

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

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

684

693

685Aside: Anonymous functions and operator sections

694Aside: Anonymous functions and operator sections

686−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

695+------------------------------------------------

687

696

688There are actually neater ways to write the above expression. One way

697There are actually neater ways to write the above expression. One way

689would be to use an anonymous function:

698would be to use an anonymous function:

@@ -710,7 +719,7 @@ by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand

710to ``\x => 2 * x``.

719to ``\x => 2 * x``.

711

720

712Maybe

721Maybe

713−~~~~~

722+-----

714

723

715``Maybe`` describes an optional value. Either there is a value of the

724``Maybe`` describes an optional value. Either there is a value of the

716given type, or there isn’t:

725given type, or there isn’t:

@@ -744,7 +753,7 @@ simply ``b``. Since the default value might not be used, we mark it as

744discarding it would be wasteful.

753discarding it would be wasteful.

745

754

746Tuples and Dependent Pairs

755Tuples and Dependent Pairs

747−~~~~~~~~~~~~~~~~~~~~~~~~~~

756+--------------------------

748

757

749Values can be paired with the following built-in data type:

758Values can be paired with the following built-in data type:

750

759

@@ -765,7 +774,7 @@ contain an arbitrary number of values, represented as nested pairs:

765 jim = ("Jim", 25, "Cambridge")

774 jim = ("Jim", 25, "Cambridge")

766

775

767Dependent Pairs

776Dependent Pairs

768−~~~~~~~~~~~~~~~

777+---------------

769

778

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

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

771on the value of the first element. Traditionally, these are referred to

780on the value of the first element. Traditionally, these are referred to

@@ -843,10 +852,10 @@ We will see more on ``with`` notation later.

843.. _sect-more-expr:

852.. _sect-more-expr:

844

853

845More Expressions

854More Expressions

846−----------------

855+================

847

856

848``let`` bindings

857``let`` bindings

849−~~~~~~~~~~~~~~~~

858+----------------

850

859

851Intermediate values can be calculated using ``let`` bindings:

860Intermediate values can be calculated using ``let`` bindings:

852

861

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

875 name ++ " is " ++ show age ++ " years old"

884 name ++ " is " ++ show age ++ " years old"

876

885

877List comprehensions

886List comprehensions

878−~~~~~~~~~~~~~~~~~~~

887+-------------------

879

888

880Idris provides *comprehension* notation as a convenient shorthand

889Idris provides *comprehension* notation as a convenient shorthand

881for building lists. The general form is:

890for building lists. The general form is:

@@ -902,7 +911,7 @@ by the difference between ``a`` and ``b``. This works for any numeric

902type, using the ``count`` function from the prelude.

911type, using the ``count`` function from the prelude.

903

912

904``case`` expressions

913``case`` expressions

905−~~~~~~~~~~~~~~~~~~~~

914+--------------------

906

915

907Another way of inspecting intermediate values of *simple* types is to

916Another way of inspecting intermediate values of *simple* types is to

908use a ``case`` expression. The following function, for example, splits

917use a ``case`` expression. The following function, for example, splits

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

956 itself.

965 itself.

957

966

958Dependent Records

967Dependent Records

959−-----------------

968+=================

960

969

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

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

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

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

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

1027 : Class

1036 : Class

1028

1037

1029Nested record update

1038Nested record update

1030−~~~~~~~~~~~~~~~~~~~~

1039+--------------------

1031

1040

1032Idris also provides a convenient syntax for accessing and updating

1041Idris also provides a convenient syntax for accessing and updating

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

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

docs/tutorial/views.rst+4−4

@@ -1,11 +1,11 @@

1.. _sec-views:

2

3−=============================

3+*****************************

4Views and the “``with``” rule

5−=============================

5+*****************************

6

7Dependent pattern matching

8−--------------------------

8+==========================

9

10Since types can depend on values, the form of some arguments can be

11determined by the value of others. For example, if we were to write

@@ -25,7 +25,7 @@ case, the definition would not be well typed.

25.. _sect-nattobin:

26

27The ``with`` rule — matching intermediate values

28−------------------------------------------------

28+================================================

29

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

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

idris.cabal+8−2

@@ -531,6 +531,9 @@ Extra-source-files:

531 test/proof009/*.idr

532 test/proof009/expected

533 test/proof009/input

534+ test/proof010/run

535+ test/proof010/*.idr

536+ test/proof010/expected

534

537

535 test/quasiquote001/run

538 test/quasiquote001/run

536 test/quasiquote001/*.idr

539 test/quasiquote001/*.idr

@@ -608,6 +611,9 @@ Extra-source-files:

608 test/totality008/run

611 test/totality008/run

609 test/totality008/*.idr

612 test/totality008/*.idr

610 test/totality008/expected

613 test/totality008/expected

614+ test/totality009/run

615+ test/totality009/*.idr

616+ test/totality009/expected

611

617

612 test/tutorial001/run

618 test/tutorial001/run

613 test/tutorial001/*.idr

619 test/tutorial001/*.idr

@@ -814,10 +820,10 @@ Library

814 , containers >= 0.5 && < 0.6

820 , containers >= 0.5 && < 0.6

815 , deepseq < 1.5

821 , deepseq < 1.5

816 , directory >= 1.2 && < 1.3

822 , directory >= 1.2 && < 1.3

817− , filepath < 1.4

823+ , filepath < 1.5

818 , fingertree >= 0.1 && < 0.2

824 , fingertree >= 0.1 && < 0.2

819 , haskeline >= 0.7 && < 0.8

825 , haskeline >= 0.7 && < 0.8

820− , lens >= 4.1.1 && < 4.8

826+ , lens >= 4.1.1 && < 4.9

821 , mtl >= 2.1 && < 2.3

827 , mtl >= 2.1 && < 2.3

822 , network < 2.7

828 , network < 2.7

823 , optparse-applicative >= 0.11 && < 0.12

829 , optparse-applicative >= 0.11 && < 0.12

libs/base/Control/Monad/RWS.idr+1−1

@@ -23,7 +23,7 @@ instance (Monoid w, Monad m) => Applicative (RWST r w s m) where

23 pure a = MkRWST $ \_,s => return (a, s, neutral)

24 (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

25 (fn, ss, w') <- f r s

26− return (fn a, ss, w <+> w)

26+ return (fn a, ss, w <+> w')

27

28instance (Monoid w, Monad m) => Monad (RWST r w s m) where

29 (MkRWST m) >>= k = MkRWST $ \r,s => do (a, s', w) <- m r s

libs/contrib/Control/WellFounded.idrnew file+83

@@ -0,0 +1,83 @@

1+||| Well-founded recursion.

2+|||

3+||| This is to let us implement some functions that don't have trivial

4+||| recursion patterns over datatypes, but instead are using some

5+||| other metric of size.

6+module Control.WellFounded

7+

8+%default total

9+

10+

11+||| Accessibility: some element `x` is accessible if all `y` such that

12+||| `rel y x` are themselves accessible.

13+|||

14+||| @ a the type of elements

15+||| @ rel a relation on a

16+||| @ x the acessible element

17+data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where

18+ ||| Accessibility

19+ |||

20+ ||| @ x the accessible element

21+ ||| @ acc' a demonstration that all smaller elements are also accessible

22+ Access : (acc' : (y : a) -> rel y x -> Accessible rel y) ->

23+ Accessible rel x

24+

25+||| A relation `rel` on `a` is well-founded if all elements of `a` are

26+||| acessible.

27+|||

28+||| @ rel the well-founded relation

29+class WellFounded (rel : a -> a -> Type) where

30+ wellFounded : (x : _) -> Accessible rel x

31+

32+

33+||| A recursor over accessibility.

34+|||

35+||| This allows us to recurse over the subset of some type that is

36+||| accessible according to some relation.

37+|||

38+||| @ rel the well-founded relation

39+||| @ step how to take steps on reducing arguments

40+||| @ z the starting point

41+accRec : {rel : a -> a -> Type} ->

42+ (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->

43+ (z : a) -> Accessible rel z -> b

44+accRec step z (Access f) =

45+ step z $ \y, lt => accRec step y (f y lt)

46+

47+||| An induction principle for accessibility.

48+|||

49+||| This allows us to recurse over the subset of some type that is

50+||| accessible according to some relation, producing a dependent type

51+||| as a result.

52+|||

53+||| @ rel the well-founded relation

54+||| @ step how to take steps on reducing arguments

55+||| @ z the starting point

56+accInd : {rel : a -> a -> Type} -> {P : a -> Type} ->

57+ (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->

58+ (z : a) -> Accessible rel z -> P z

59+accInd step z (Access f) =

60+ step z $ \y, lt => accInd step y (f y lt)

61+

62+

63+||| Use well-foundedness of a relation to write terminating operations.

64+|||

65+||| @ rel a well-founded relation

66+wfRec : WellFounded rel =>

67+ (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->

68+ a -> b

69+wfRec {rel} step x = accRec step x (wellFounded {rel} x)

70+

71+

72+||| Use well-foundedness of a relation to write proofs

73+|||

74+||| @ rel a well-founded relation

75+||| @ P the motive for the induction

76+||| @ step the induction step: take an element and its accessibility,

77+||| and give back a demonstration of P for that element,

78+||| potentially using accessibility

79+wfInd : WellFounded rel => {P : a -> Type} ->

80+ (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->

81+ (x : a) -> P x

82+wfInd {rel} step x = accInd step x (wellFounded {rel} x)

83+

libs/contrib/Data/Nat.idrnew file+165

@@ -0,0 +1,165 @@

1+||| Extra utilities for working with Nats

2+module Data.Nat

3+

4+import Data.Fin

5+import Data.So

6+

7+import Control.WellFounded

8+

9+%default total

10+

11+||| A strict less-than relation on `Nat`.

12+|||

13+||| @ n the smaller number

14+||| @ m the larger number

15+data LT' : (n,m : Nat) -> Type where

16+ ||| n < 1 + n

17+ LTSucc : LT' n (S n)

18+ ||| n < m implies that n < m + 1

19+ LTStep : LT' n m -> LT' n (S m)

20+

21+%name LT' lt, lt'

22+

23+||| Nothing is strictly less than zero

24+instance Uninhabited (LT' n 0) where

25+ uninhabited LTSucc impossible

26+

27+||| Zero is less than any non-zero number.

28+LTZeroLeast : LT' Z (S n)

29+LTZeroLeast {n = Z} = LTSucc

30+LTZeroLeast {n = S n} = LTStep LTZeroLeast

31+

32+||| If n < m, then 1 + n < 1 + m

33+ltSuccSucc : LT' n m -> LT' (S n) (S m)

34+ltSuccSucc LTSucc = LTSucc

35+ltSuccSucc (LTStep lt) = LTStep $ ltSuccSucc lt

36+

37+||| If n + 1 < m, then n < m

38+lteToLt' : LTE (S n) m -> LT' n m

39+lteToLt' {n = Z} (LTESucc x) = LTZeroLeast

40+lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x

41+

42+||| Convert from LT' to LTE

43+ltToLTE : LT' n m -> LTE (S n) m

44+ltToLTE LTSucc = lteRefl

45+ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt

46+

47+||| Subtraction gives a result that is actually smaller.

48+minusLT' : (x,y : Nat) -> x - y `LT'` S x

49+minusLT' Z y = LTSucc

50+minusLT' (S k) Z = LTSucc

51+minusLT' (S k) (S j) = LTStep (minusLT' k j)

52+

53+||| Strict less-than is well-founded, with the cascade stopping at

54+||| zero (because there's nothing less than zero). This can't be done

55+||| for LTE, because that one doesn't stop at zero (because `LTE 0 0`

56+||| is inhabited).

57+instance WellFounded LT' where

58+ wellFounded x = Access (acc x)

59+ where

60+ ||| Show accessibility by induction on the structure of the LT' witness

61+ acc : (x, y : Nat) -> LT' y x -> Accessible LT' y

62+ -- Zero is vacuously accessible: there's nothing smaller to check

63+ acc Z y lt = absurd lt

64+ -- If the element being accessed is one smaller, we're done

65+ acc (S y) y LTSucc = Access (acc y)

66+ -- If the element is more than one smaller, we need to go further

67+ acc (S k) y (LTStep smaller) = acc k y smaller

68+

69+||| The result of division on natural numbers.

70+|||

71+||| @ dividend the dividend

72+||| @ divisor the divisor

73+data DivMod : (dividend, divisor : Nat) -> Type where

74+ ||| The result of division, with a quotient and a remainder.

75+ |||

76+ ||| @ dividend the dividend

77+ ||| @ divisor the divisor

78+ ||| @ quotient the quotient

79+ ||| @ remainder the remainder (bounded by the divisor)

80+ ||| @ ok the fact that this is, in fact, a result of division

81+ DivModRes : {dividend, divisor : Nat} ->

82+ (quotient : Nat) -> (remainder : Fin divisor) ->

83+ (ok : dividend = finToNat remainder + quotient * divisor) ->

84+ DivMod dividend divisor

85+

86+

87+||| Any natural number can be a `Fin` where the bound is itself plus some difference.

88+private

89+toFin : (x : Nat) -> (diff : Nat) -> Fin (plus x (S diff))

90+toFin Z diff = FZ

91+toFin (S k) diff = FS $ toFin k diff

92+

93+||| Converting to a `Fin` and back to `Nat` preserves the input. This is a correctness proof for `toFin`.

94+private

95+toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x

96+toFinAndBack Z diff = Refl

97+toFinAndBack (S k) diff = cong (toFinAndBack k diff)

98+

99+

100+||| The accessibilty predicate used for division.

101+private

102+accPlusLT' : LT' (S j) (S (plus k (S j)))

103+accPlusLT' {j = Z} {k = Z} = LTSucc

104+accPlusLT' {j = Z} {k = S k} = LTStep (accPlusLT' {j = Z} {k = k})

105+accPlusLT' {j = S j} {k = k} = rewrite sym $ plusSuccRightSucc k (S j) in

106+ ltSuccSucc accPlusLT'

107+

108+

109+||| Division and modulus on `Nat`, inspired by the definition in the

110+||| Agda standard library.

111+|||

112+||| This uses well-founded recursion on `LT'`.

113+|||

114+||| @ dividend the dividend

115+||| @ divisor the divisor

116+||| @ nonzero division by zero is nonsense

117+total -- yay!

118+divMod : (dividend, divisor : Nat) ->

119+ {auto nonzero : So (not (decAsBool (decEq divisor Z)))} ->

120+ DivMod dividend divisor

121+divMod _ Z {nonzero} = absurd nonzero

122+divMod Z (S k) = DivModRes 0 FZ Refl

123+divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero

124+ where

125+ ||| The goal passed to the accessibility eliminator.

126+ |||

127+ ||| This is responsible for generating the goal in the

128+ ||| well-founded fixed point.

129+ |||

130+ ||| @ dividend the dividend to recurse over

131+ P : (dividend : Nat) -> Type

132+ P dividend = (divisor : Nat) -> (nonzero : So (not (decAsBool (decEq divisor Z)))) -> DivMod dividend divisor

133+

134+

135+ ||| Well-founded recursion needs a recursion operator.

136+ |||

137+ ||| @ dividend the dividend we are recursing over

138+ ||| @ rec the recursive call provided by the well-founded induction operator

139+ stepDiv : (dividend : Nat) -> (rec : (d' : Nat) -> LT' d' dividend -> P d') -> P dividend

140+ -- We need not consider division by zero

141+ stepDiv dividend rec Z nonzero = absurd nonzero

142+ -- Dividing zero by anyting else gives 0, with 0 remainder

143+ stepDiv Z rec (S k) nonzero = DivModRes 0 0 Refl

144+ -- To divide two non-zero values, we must know which is larger

145+ stepDiv (S j) rec (S k) nonzero with (cmp j k)

146+ -- n / n = 1 remainder 0

147+ stepDiv (S j) rec (S j) nonzero | CmpEQ =

148+ DivModRes 1 0 (sym $ cong (plusZeroRightNeutral j))

149+ -- if n < m, then m = n + r, and the quotient is 0 with remainder r

150+ stepDiv (S j) rec (S (plus j (S diff))) nonzero | CmpLT diff =

151+ DivModRes 0 (toFin (S j) diff) $

152+ rewrite toFinAndBack j diff

153+ in sym $ cong (plusZeroRightNeutral j)

154+ -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder

155+ stepDiv (S (plus k (S diff))) rec (S k) nonzero | CmpGT diff =

156+ let res = rec (S diff) accPlusLT' (S k) Oh

157+ in case res of

158+ DivModRes quotient remainder ok =>

159+ DivModRes (S quotient) remainder $

160+ rewrite plusAssociative (finToNat remainder) (S k) (mult quotient (S k)) in

161+ rewrite plusCommutative (finToNat remainder) (S k) in

162+ rewrite sym $ plusAssociative (S k) (finToNat remainder) (mult quotient (S k)) in

163+ rewrite ok in Refl

164+

165+

libs/contrib/contrib.ipkg+2

@@ -3,9 +3,11 @@ package contrib

3opts = "--nobasepkgs --total -i ../prelude -i ../base"

4modules = Control.Algebra,

5 Control.Isomorphism.Primitives,

6+ Control.WellFounded,

6 Classes.Verified,

7 Classes.Verified,

7 Data.Fun, Data.Rel,

8 Data.Fun, Data.Rel,

8 Data.Hash, Data.Matrix,

9 Data.Hash, Data.Matrix,

10+ Data.Nat,

9 Data.ZZ, Data.Sign,

11 Data.ZZ, Data.Sign,

10 Data.BoundedList,

12 Data.BoundedList,

11 Data.Heap,

13 Data.Heap,

libs/prelude/Builtins.idr−2

@@ -162,8 +162,6 @@ abstract data ManagedPtr : Type

162

163%extern prim__readFile : prim__WorldType -> Ptr -> String

164%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int

165−%extern prim__readString : prim__WorldType -> String

166−%extern prim__writeString : prim__WorldType -> String -> Int

167

165

168%extern prim__vm : Ptr

166%extern prim__vm : Ptr

169%extern prim__stdin : Ptr

167%extern prim__stdin : Ptr

libs/prelude/Prelude.idr+6

@@ -31,6 +31,12 @@ import public Language.Reflection.Errors

31%access public

32%default total

33

34+-- Things that can't be elsewhere for import cycle reasons

35+decAsBool : Dec p -> Bool

36+decAsBool (Yes _) = True

37+decAsBool (No _) = False

38+

39+

34-- Show and instances

40-- Show and instances

35

41

36class Show a where

42class Show a where

libs/prelude/Prelude/Nat.idr+14

@@ -99,6 +99,9 @@ data LTE : (n, m : Nat) -> Type where

99 ||| If n <= m, then n + 1 <= m + 1

100 LTESucc : LTE left right -> LTE (S left) (S right)

101

102+instance Uninhabited (LTE (S n) Z) where

103+ uninhabited LTEZero impossible

104+

102||| Greater than or equal to

105||| Greater than or equal to

103total GTE : Nat -> Nat -> Type

106total GTE : Nat -> Nat -> Type

104GTE left right = LTE right left

107GTE left right = LTE right left

@@ -127,6 +130,17 @@ isLTE (S k) (S j) with (isLTE k j)

127 isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)

130 isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)

128 isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

131 isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

129

132

133+||| `LTE` is reflexive.

134+lteRefl : LTE n n

135+lteRefl {n = Z} = LTEZero

136+lteRefl {n = S k} = LTESucc lteRefl

137+

138+||| n < m implies n < m + 1

139+lteSuccRight : LTE n m -> LTE n (S m)

140+lteSuccRight LTEZero = LTEZero

141+lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)

142+

143+

130||| Boolean test than one Nat is less than or equal to another

144||| Boolean test than one Nat is less than or equal to another

131total lte : Nat -> Nat -> Bool

145total lte : Nat -> Nat -> Bool

132lte Z right = True

146lte Z right = True

rts/Makefile+2−2

@@ -1,10 +1,10 @@

1include ../config.mk

2

3OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \

4− idris_opts.o idris_stats.o idris_utf8.o mini-gmp.o

4+ idris_opts.o idris_stats.o idris_utf8.o mini-gmp.o getline.o

5HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

6 idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \

7− idris_utf8.h

7+ idris_utf8.h getline.h

8CFLAGS:=-fPIC $(CFLAGS)

9CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\""

10CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\""

rts/getline.cnew file+81

@@ -0,0 +1,81 @@

1+/* $NetBSD: fgetln.c,v 1.9 2008/04/29 06:53:03 martin Exp $ */

2+

3+/*-

6+ *

7+ * This code is derived from software contributed to The NetBSD Foundation

8+ * by Christos Zoulas.

9+ *

10+ * Redistribution and use in source and binary forms, with or without

11+ * modification, are permitted provided that the following conditions

12+ * are met:

13+ * 1. Redistributions of source code must retain the above copyright

14+ * notice, this list of conditions and the following disclaimer.

15+ * 2. Redistributions in binary form must reproduce the above copyright

16+ * notice, this list of conditions and the following disclaimer in the

17+ * documentation and/or other materials provided with the distribution.

18+ *

19+ * THIS SOFTWARE IS PROVIDED BY THE NETBSD FOUNDATION, INC. AND CONTRIBUTORS

20+ * ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED

21+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR

22+ * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE FOUNDATION OR CONTRIBUTORS

23+ * BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR

24+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF

25+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS

26+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN

27+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)

28+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE

29+ * POSSIBILITY OF SUCH DAMAGE.

30+ */

31+

32+#include <stdlib.h>

33+#include <stdio.h>

34+#include <unistd.h>

35+#include <errno.h>

36+#include <string.h>

37+

38+ssize_t

39+getdelim(char **buf, size_t *bufsiz, int delimiter, FILE *fp)

40+{

41+ char *ptr, *eptr;

42+

43+

44+ if (*buf == NULL || *bufsiz == 0) {

45+ *bufsiz = BUFSIZ;

46+ if ((*buf = malloc(*bufsiz)) == NULL)

47+ return -1;

48+ }

49+

50+ for (ptr = *buf, eptr = *buf + *bufsiz;;) {

51+ int c = fgetc(fp);

52+ if (c == -1) {

53+ if (feof(fp))

54+ return ptr == *buf ? -1 : ptr - *buf;

55+ else

56+ return -1;

57+ }

58+ *ptr++ = c;

59+ if (c == delimiter) {

60+ *ptr = '\0';

61+ return ptr - *buf;

62+ }

63+ if (ptr + 2 >= eptr) {

64+ char *nbuf;

65+ size_t nbufsiz = *bufsiz * 2;

66+ ssize_t d = ptr - *buf;

67+ if ((nbuf = realloc(*buf, nbufsiz)) == NULL)

68+ return -1;

69+ *buf = nbuf;

70+ *bufsiz = nbufsiz;

71+ eptr = nbuf + nbufsiz;

72+ ptr = nbuf + d;

73+ }

74+ }

75+}

76+

77+ssize_t

78+getline(char **buf, size_t *bufsiz, FILE *fp)

79+{

80+ return getdelim(buf, bufsiz, '\n', fp);

81+}

rts/getline.hnew file+7

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

1+#ifndef GETLINE_H

2+#define GETLINE_H

3+#include <stdlib.h>

4+#include <stdio.h>

5+ssize_t getdelim(char **buf, size_t *bufsiz, int delimiter, FILE *fp);

6+ssize_t getline(char **buf, size_t *bufsiz, FILE *fp);

7+#endif // GETLINE_H

rts/idris_rts.c+10−42

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

4#include "idris_gc.h"

5#include "idris_utf8.h"

6#include "idris_bitstring.h"

7+#include "getline.h"

7

8

8#ifdef HAS_PTHREAD

9#ifdef HAS_PTHREAD

9static pthread_key_t vm_key;

10static pthread_key_t vm_key;

@@ -499,51 +500,18 @@ VAL idris_strlen(VM* vm, VAL l) {

499 return MKINT((i_int)(idris_utf8_strlen(GETSTR(l))));

500 return MKINT((i_int)(idris_utf8_strlen(GETSTR(l))));

500}

501}

501

502

502−#define BUFSIZE 256

503−

504VAL idris_readStr(VM* vm, FILE* h) {

503VAL idris_readStr(VM* vm, FILE* h) {

505−// Modified from 'safe-fgets.c' in the gdb distribution.

504+ char *buffer = NULL;

506−// (see http://www.gnu.org/software/gdb/current/)

505+ size_t n = 0;

507− char *line_ptr;

506+ ssize_t len;

508− char* line_buf = (char *) malloc (BUFSIZE);

507+ len = getline(&buffer, &n, h);

509− int line_buf_size = BUFSIZE;

510−

511− /* points to last byte */

512− line_ptr = line_buf + line_buf_size - 1;

513−

514− /* so we can see if fgets put a 0 there */

515− *line_ptr = 1;

516− if (fgets (line_buf, line_buf_size, h) == 0)

517− return MKSTR(vm, "");

518−

519− /* we filled the buffer? */

520− while (line_ptr[0] == 0 && line_ptr[-1] != '\n')

521− {

522− /* Make the buffer bigger and read more of the line */

523− line_buf_size += BUFSIZE;

524− { /* limit the scope of new_line_buf to where it's needed for errors*/

525− char *new_line_buf = realloc (line_buf, line_buf_size);

526− if (new_line_buf == NULL)

527− {

528− fprintf(stderr, "Fatal Error: couldn't allocate a larger line buffer.");

529− exit(EXIT_FAILURE);

530− } else {

531− line_buf = new_line_buf;

532− }

533− }

534− /* points to last byte again */

535− line_ptr = line_buf + line_buf_size - 1;

536− /* so we can see if fgets put a 0 there */

537− *line_ptr = 1;

538

508

539− if (fgets (line_buf + line_buf_size - BUFSIZE - 1, BUFSIZE + 1, h) == 0)

509+ if (len <= 0) {

540− return MKSTR(vm, "");

510+ return MKSTR(vm, "");

511+ } else {

512+ return MKSTR(vm, buffer);

541 }

513 }

542−

514+ free(buffer);

543− VAL str = MKSTR(vm, line_buf);

544−// printf("DBG: %s\n", line_buf);

545− free(line_buf);

546− return str;

547}

515}

548

516

549VAL idris_strHead(VM* vm, VAL str) {

517VAL idris_strHead(VM* vm, VAL str) {

src/IRTS/CodegenC.hs+7−8

@@ -529,6 +529,13 @@ doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r +

529doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

530doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

531

532+doOp v LReadStr [_] = v ++ "idris_readStr(vm, stdin)"

533+doOp v LWriteStr [_,s]

534+ = v ++ "MKINT((i_int)(idris_writeStr(stdout"

535+ ++ ",GETSTR("

536+ ++ creg s ++ "))))"

537+

538+

532-- String functions which need to know we're UTF8

539-- String functions which need to know we're UTF8

533doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

540doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

534doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

541doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

@@ -548,14 +555,6 @@ doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

548doOp v LNoOp args = v ++ creg (last args)

555doOp v LNoOp args = v ++ creg (last args)

549

556

550-- Pointer primitives (declared as %extern in Builtins.idr)

557-- Pointer primitives (declared as %extern in Builtins.idr)

551−doOp v (LExternal rs) [_]

552− | rs == sUN "prim__readString" = v ++ "idris_readStr(vm, stdin)"

553−doOp v (LExternal ws) [_,s]

554− | ws == sUN "prim__writeString"

555− = v ++ "MKINT((i_int)(idris_writeStr(stdout"

556− ++ ",GETSTR("

557− ++ creg s ++ "))))"

558−

559doOp v (LExternal rf) [_,x]

558doOp v (LExternal rf) [_,x]

560 | rf == sUN "prim__readFile"

559 | rf == sUN "prim__readFile"

561 = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

560 = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

src/IRTS/CodegenJavaScript.hs+1−2

@@ -679,8 +679,7 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

679 jsOP'

680 | LNoOp <- op = translateReg (last args)

681

682− | (LExternal ws) <- op,

682+ | LWriteStr <- op,

683− ws == sUN "prim__writeString",

684 (_:str:_) <- args = JSAssign (translateReg reg)

683 (_:str:_) <- args = JSAssign (translateReg reg)

685 (JSApp (JSIdent "i$putStr") [translateReg str])

684 (JSApp (JSIdent "i$putStr") [translateReg str])

686

685

src/IRTS/Lang.hs+1

@@ -75,6 +75,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

75 | LFSqrt | LFFloor | LFCeil | LFNegate

76

78+ | LReadStr | LWriteStr

78

79

79 -- system info

80 -- system info

80 | LSystemInfo

81 | LSystemInfo

src/Idris/AbsSyntax.hs+17

@@ -385,6 +385,23 @@ addClass n i

385 _ -> i

386 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

387

388+addAutoHint :: Name -> Name -> Idris ()

389+addAutoHint n hint =

390+ do ist <- getIState

391+ case lookupCtxtExact n (idris_autohints ist) of

392+ Nothing ->

393+ do let hs = addDef n [hint] (idris_autohints ist)

394+ putIState $ ist { idris_autohints = hs }

395+ Just nhints ->

396+ do let hs = addDef n (hint : nhints) (idris_autohints ist)

397+ putIState $ ist { idris_autohints = hs }

398+

399+getAutoHints :: Name -> Idris [Name]

400+getAutoHints n = do ist <- getIState

401+ case lookupCtxtExact n (idris_autohints ist) of

402+ Nothing -> return []

403+ Just ns -> return ns

404+

388addIBC :: IBCWrite -> Idris ()

405addIBC :: IBCWrite -> Idris ()

389addIBC ibc@(IBCDef n)

406addIBC ibc@(IBCDef n)

390 = do i <- getIState

407 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+6

@@ -18,6 +18,8 @@ import Idris.Colours

18import System.Console.Haskeline

19import System.IO

20

21+import Prelude hiding ((<$>))

22+

21import Control.Applicative ((<|>))

23import Control.Applicative ((<|>))

22

24

23import Control.Monad.Trans.State.Strict

25import Control.Monad.Trans.State.Strict

@@ -179,6 +181,7 @@ data IState = IState {

179 idris_tyinfodata :: Ctxt TIData,

181 idris_tyinfodata :: Ctxt TIData,

180 idris_fninfo :: Ctxt FnInfo,

182 idris_fninfo :: Ctxt FnInfo,

181 idris_transforms :: Ctxt [(Term, Term)],

183 idris_transforms :: Ctxt [(Term, Term)],

184+ idris_autohints :: Ctxt [Name],

182 idris_totcheck :: [(FC, Name)], -- names to check totality on

185 idris_totcheck :: [(FC, Name)], -- names to check totality on

183 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

186 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

184 idris_totcheckfail :: [(FC, String)],

187 idris_totcheckfail :: [(FC, String)],

@@ -307,6 +310,7 @@ data IBCWrite = IBCFix FixDecl

307 | IBCModDocs Name -- ^ The name is the special name used to track module docs

310 | IBCModDocs Name -- ^ The name is the special name used to track module docs

308 | IBCUsage (Name, Int)

311 | IBCUsage (Name, Int)

309 | IBCExport Name

312 | IBCExport Name

313+ | IBCAutoHint Name Name

310 deriving Show

314 deriving Show

311

315

312-- | The initial state for the compiler

316-- | The initial state for the compiler

@@ -316,6 +320,7 @@ idrisInit = IState initContext S.empty []

316 emptyContext emptyContext emptyContext emptyContext

320 emptyContext emptyContext emptyContext emptyContext

317 emptyContext emptyContext emptyContext emptyContext

321 emptyContext emptyContext emptyContext emptyContext

318 emptyContext emptyContext emptyContext emptyContext

322 emptyContext emptyContext emptyContext emptyContext

323+ emptyContext

319 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

324 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

320 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

325 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

321 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

326 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

@@ -560,6 +565,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

560 | Reflection -- a reflecting function, compile-time only

565 | Reflection -- a reflecting function, compile-time only

561 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

566 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

562 | Constructor -- Data constructor type

567 | Constructor -- Data constructor type

568+ | AutoHint -- use in auto implicit search

563 deriving (Show, Eq)

569 deriving (Show, Eq)

564{-!

570{-!

565deriving instance Binary FnOpt

571deriving instance Binary FnOpt

src/Idris/Core/Evaluate.hs+5−3

@@ -286,7 +286,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

286 -- block reduction immediately under codata (and not forced)

287 ev ntimes stk top env

288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

289− | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

289+ | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)

290 = do let (f, _) = unApply arg

291 let ntimes' = case f of

292 P _ fn _ -> (fn, 0) : ntimes

@@ -576,8 +576,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where

576 | x `elem` holes || y `elem` holes = return True

577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

579+ ceq ps x (Bind n (Lam t) (App y (V 0)))

580+ = ceq ps x (substV (P Bound n t) y)

580− ceq ps (Bind n (Lam t) (App x (V 0))) y = ceq ps x y

581+ ceq ps (Bind n (Lam t) (App x (V 0))) y

582+ = ceq ps (substV (P Bound n t) x) y

581 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

583 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

582 | n == n' = ceq ps x y

584 | n == n' = ceq ps x y

583 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

585 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

src/Idris/Core/Unify.hs+2

@@ -707,9 +707,11 @@ recoverable (App f a) (App f' a')

707recoverable f (Bind _ (Pi _ _ _) sc)

708 | (P (DCon _ _ _) _ _, _) <- unApply f = False

709 | (P (TCon _ _) _ _, _) <- unApply f = False

710+ | (Constant _) <- f = False

710recoverable (Bind _ (Pi _ _ _) sc) f

711recoverable (Bind _ (Pi _ _ _) sc) f

711 | (P (DCon _ _ _) _ _, _) <- unApply f = False

712 | (P (DCon _ _ _) _ _, _) <- unApply f = False

712 | (P (TCon _ _) _ _, _) <- unApply f = False

713 | (P (TCon _ _) _ _, _) <- unApply f = False

714+ | (Constant _) <- f = False

713recoverable (Bind _ (Lam _) sc) f = recoverable sc f

715recoverable (Bind _ (Lam _) sc) f = recoverable sc f

714recoverable f (Bind _ (Lam _) sc) = recoverable f sc

716recoverable f (Bind _ (Lam _) sc) = recoverable f sc

715recoverable x y = True

717recoverable x y = True

src/Idris/DeepSeq.hs+1

@@ -119,6 +119,7 @@ instance NFData FnOpt where

119 rnf Reflection = ()

120 rnf (Specialise x1) = rnf x1 `seq` ()

121 rnf Constructor = ()

122+ rnf AutoHint = ()

122

123

123instance NFData DataOpt where

124instance NFData DataOpt where

124 rnf Codata = ()

125 rnf Codata = ()

src/Idris/Delaborate.hs+2

@@ -13,6 +13,8 @@ import Idris.Core.Evaluate

13import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

14import Idris.ErrReverse

15

16+import Prelude hiding ((<$>))

17+

16import Data.List (intersperse, nub)

18import Data.List (intersperse, nub)

17import qualified Data.Text as T

19import qualified Data.Text as T

18import Control.Monad.State

20import Control.Monad.State

src/Idris/Docs.hs+2

@@ -11,6 +11,8 @@ import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, rende

11

12import Util.Pretty

13

14+import Prelude hiding ((<$>))

15+

14import Control.Arrow (first)

16import Control.Arrow (first)

15

17

16import Data.Maybe

18import Data.Maybe

src/Idris/Docstrings.hs+2

@@ -15,6 +15,8 @@ import Util.Pretty

15

16import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term, Err)

17

18+import Prelude hiding ((<$>))

19+

18import qualified Data.Text as T

20import qualified Data.Text as T

19import qualified Data.Foldable as F

21import qualified Data.Foldable as F

20import Data.Foldable (Foldable)

22import Data.Foldable (Foldable)

src/Idris/Elab/Clause.hs+1−1

@@ -702,7 +702,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

702 (crhs, crhsty) <- if not inf

703 then recheckC_borrowing True borrowed fc id [] rhs'

704 else return (rhs', clhsty)

705− logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

705+ logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

706 ctxt <- getContext

707 let constv = next_tvar ctxt

708 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

src/Idris/Elab/Instance.hs+3−2

@@ -90,7 +90,9 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

90 PApp _ _ args -> getWParams (map getTm args)

91 a@(PRef fc f) -> getWParams [a]

92 _ -> return []) ps

93+ ist <- getIState

93− let pnames = map pname (concat (nub wparams))

94+ let pnames = nub $ map pname (concat (nub wparams)) ++

95+ concatMap (namesIn [] ist) ps

94 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

96 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

95 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances

97 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances

96 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

98 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

@@ -119,7 +121,6 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

119 show (concat (nub wparams))

121 show (concat (nub wparams))

120

122

121 -- Bring variables in instance head into scope

123 -- Bring variables in instance head into scope

122− ist <- getIState

123 let headVars = nub $ mapMaybe (\p -> case p of

124 let headVars = nub $ mapMaybe (\p -> case p of

124 PRef _ n ->

125 PRef _ n ->

125 case lookupTy n (tt_ctxt ist) of

126 case lookupTy n (tt_ctxt ist) of

src/Idris/Elab/Type.hs+8−3

@@ -146,8 +146,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

146 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

147 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

148

149− let (t, _) = unApply (getRetTy nty')

149+ let (fam, _) = unApply (getRetTy nty')

150− let corec = case t of

150+ let corec = case fam of

151 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

152 [TI _ True _ _ _] -> True

153 _ -> False

@@ -157,7 +157,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

157 let usety = if norm then nty' else nty

158 ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

159 addIBC (IBCDef n)

160− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

160+ let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds

161 addDeferred ds'

162 setFlags n opts'

163 checkDocs fc argDocs ty

@@ -171,6 +171,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

171 addIBC (IBCOpt n)

172 when (Implicit `elem` opts') $ do addCoercion n

173 addIBC (IBCCoercion n)

174+ when (AutoHint `elem` opts') $

175+ case fam of

176+ P _ tyn _ -> do addAutoHint tyn n

177+ addIBC (IBCAutoHint tyn n)

178+ t -> ifail $ "Hints must return a data or record type"

174

179

175 -- If the function is declared as an error handler and the language

180 -- If the function is declared as an error handler and the language

176 -- extension is enabled, then add it to the list of error handlers.

181 -- extension is enabled, then add it to the list of error handlers.

src/Idris/ElabTerm.hs+15−11

@@ -289,26 +289,29 @@ elab ist info emode opts fn tm

289 --trace ("ELAB " ++ show t') $

290 let fc = fileFC "Force"

291 env <- get_env

292− handleError (forceErr env)

292+ handleError (forceErr t' env)

293 (elab' ina fc' t')

294 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

295 [pimp (sUN "t") Placeholder True,

296 pimp (sUN "a") Placeholder True,

297 pexp ct])) True

298

299− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

299+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

300 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

301− ht == txt "Lazy'" = True

301+ ht == txt "Lazy'" = notDelay orig

302− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

302+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

303 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

304− ht == txt "Lazy'" = True

304+ ht == txt "Lazy'" = notDelay orig

305− forceErr env (InfiniteUnify _ t _)

305+ forceErr orig env (InfiniteUnify _ t _)

306 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

307− ht == txt "Lazy'" = True

307+ ht == txt "Lazy'" = notDelay orig

308− forceErr env (Elaborating _ _ t) = forceErr env t

308+ forceErr orig env (Elaborating _ _ t) = forceErr orig env t

309− forceErr env (ElaboratingArg _ _ _ t) = forceErr env t

309+ forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

310− forceErr env (At _ t) = forceErr env t

310+ forceErr orig env (At _ t) = forceErr orig env t

311− forceErr env t = False

311+ forceErr orig env t = False

312+

313+ notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

314+ notDelay _ = True

312

315

313 local f = do e <- get_env

316 local f = do e <- get_env

314 return (f `elem` map fst e)

317 return (f `elem` map fst e)

@@ -498,6 +501,7 @@ elab ist info emode opts fn tm

498 if null a'

501 if null a'

499 then erun fc $ do apply (Var n) []; solve

502 then erun fc $ do apply (Var n) []; solve

500 else elab' ina fc' (PApp fc tm [])

503 else elab' ina fc' (PApp fc tm [])

504+ elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

501 elab' ina _ (PLam fc n Placeholder sc)

505 elab' ina _ (PLam fc n Placeholder sc)

502 = do -- if n is a type constructor name, this makes no sense...

506 = do -- if n is a type constructor name, this makes no sense...

503 ctxt <- get_context

507 ctxt <- get_context

src/Idris/IBC.hs+15−5

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 103

40+ibcVersion = 104

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

@@ -82,7 +82,8 @@ data IBCFile = IBCFile { ver :: Word8,

82 ibc_externs :: ![(Name, Int)],

83 ibc_parsedSpan :: !(Maybe FC),

84 ibc_usage :: ![(Name, Int)],

85− ibc_exports :: ![Name]

85+ ibc_exports :: ![Name],

86+ ibc_autohints :: ![(Name, Name)]

86 }

87 }

87 deriving Show

88 deriving Show

88{-!

89{-!

@@ -90,7 +91,7 @@ deriving instance Binary IBCFile

90!-}

91!-}

91

92

92initIBC :: IBCFile

93initIBC :: IBCFile

93−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

94+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

94

95

95loadIBC :: Bool -- ^ True = reexport, False = make everything private

96loadIBC :: Bool -- ^ True = reexport, False = make everything private

96 -> FilePath -> Idris ()

97 -> FilePath -> Idris ()

@@ -237,6 +238,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

237 _ -> ifail "IBC write failed"

238 _ -> ifail "IBC write failed"

238ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

239ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

239ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

240ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

241+ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

240

242

241process :: Bool -- ^ Reexporting

243process :: Bool -- ^ Reexporting

242 -> IBCFile -> FilePath -> Idris ()

244 -> IBCFile -> FilePath -> Idris ()

@@ -296,6 +298,7 @@ process reexp i fn

296 pParsedSpan $ force (ibc_parsedSpan i)

298 pParsedSpan $ force (ibc_parsedSpan i)

297 pUsage $ force (ibc_usage i)

299 pUsage $ force (ibc_usage i)

298 pExports $ force (ibc_exports i)

300 pExports $ force (ibc_exports i)

301+ pAutoHints $ force (ibc_autohints i)

299

302

300timestampOlder :: FilePath -> FilePath -> Idris ()

303timestampOlder :: FilePath -> FilePath -> Idris ()

301timestampOlder src ibc = do srct <- runIO $ getModificationTime src

304timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -326,6 +329,9 @@ pExports :: [Name] -> Idris ()

326pExports ns = do ist <- getIState

329pExports ns = do ist <- getIState

327 putIState ist { idris_exports = ns ++ idris_exports ist }

330 putIState ist { idris_exports = ns ++ idris_exports ist }

328

331

332+pAutoHints :: [(Name, Name)] -> Idris ()

333+pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns

334+

329pImportDirs :: [FilePath] -> Idris ()

335pImportDirs :: [FilePath] -> Idris ()

330pImportDirs fs = mapM_ addImportDir fs

336pImportDirs fs = mapM_ addImportDir fs

331

337

@@ -942,7 +948,7 @@ instance Binary MetaInformation where

942 _ -> error "Corrupted binary data for MetaInformation"

948 _ -> error "Corrupted binary data for MetaInformation"

943

949

944instance Binary IBCFile where

950instance Binary IBCFile where

945− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44)

951+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45)

946 = {-# SCC "putIBCFile" #-}

952 = {-# SCC "putIBCFile" #-}

947 do put x1

953 do put x1

948 put x2

954 put x2

@@ -988,6 +994,7 @@ instance Binary IBCFile where

988 put x42

994 put x42

989 put x43

995 put x43

990 put x44

996 put x44

997+ put x45

991

998

992 get

999 get

993 = do x1 <- get

1000 = do x1 <- get

@@ -1035,7 +1042,8 @@ instance Binary IBCFile where

1035 x42 <- get

1042 x42 <- get

1036 x43 <- get

1043 x43 <- get

1037 x44 <- get

1044 x44 <- get

1045+ x45 <- get

1038− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44)

1046+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45)

1039 else return (initIBC { ver = x1 })

1047 else return (initIBC { ver = x1 })

1040

1048

1041instance Binary DataOpt where

1049instance Binary DataOpt where

@@ -1072,6 +1080,7 @@ instance Binary FnOpt where

1072 Constructor -> putWord8 13

1080 Constructor -> putWord8 13

1073 CExport x1 -> do putWord8 14

1081 CExport x1 -> do putWord8 14

1074 put x1

1082 put x1

1083+ AutoHint -> putWord8 15

1075 get

1084 get

1076 = do i <- getWord8

1085 = do i <- getWord8

1077 case i of

1086 case i of

@@ -1092,6 +1101,7 @@ instance Binary FnOpt where

1092 13 -> return Constructor

1101 13 -> return Constructor

1093 14 -> do x1 <- get

1102 14 -> do x1 <- get

1094 return $ CExport x1

1103 return $ CExport x1

1104+ 15 -> return AutoHint

1095 _ -> error "Corrupted binary data for FnOpt"

1105 _ -> error "Corrupted binary data for FnOpt"

1096

1106

1097instance Binary Fixity where

1107instance Binary Fixity where

src/Idris/Output.hs+3−1

@@ -15,10 +15,12 @@ import Util.ScreenSize (getScreenWidth)

15

16import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

17

18−import System.Console.Haskeline.MonadException

18+import System.Console.Haskeline.MonadException

19 (MonadException (controlIO), RunIO (RunIO))

20import System.IO (stdout, Handle, hPutStrLn)

21

22+import Prelude hiding ((<$>))

23+

22import Data.Char (isAlpha)

24import Data.Char (isAlpha)

23import Data.List (nub, intersperse)

25import Data.List (nub, intersperse)

24import Data.Maybe (fromMaybe)

26import Data.Maybe (fromMaybe)

src/Idris/ParseExpr.hs+31−16

@@ -234,6 +234,14 @@ internalExpr syn =

234 <|> app syn

235 <?> "expression"

236

237+{- | Parses the "impossible" keyword

238+@

239+Impossible ::= 'impossible'

240+@

241+-}

242+impossible :: IdrisParser PTerm

243+impossible = PImpossible <$ reserved "impossible"

244+

237{- | Parses a case expression

245{- | Parses a case expression

238@

246@

239CaseExpr ::=

247CaseExpr ::=

@@ -250,13 +258,13 @@ caseExpr syn = do reserved "case"; fc <- getFC

250{- | Parses a case in a case expression

258{- | Parses a case in a case expression

251@

259@

252CaseOption ::=

260CaseOption ::=

253− Expr '=>' Expr Terminator

261+ Expr (Impossible | '=>' Expr) Terminator

254 ;

262 ;

255@

263@

256-}

264-}

257caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

265caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

258caseOption syn = do lhs <- expr (syn { inPattern = True })

266caseOption syn = do lhs <- expr (syn { inPattern = True })

259− symbol "=>"; r <- expr syn

267+ r <- impossible <|> symbol "=>" *> expr syn

260 return (lhs, r)

268 return (lhs, r)

261 <?> "case option"

269 <?> "case option"

262

270

@@ -732,8 +740,8 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu

732{- | Parses a lambda expression

740{- | Parses a lambda expression

733@

741@

734Lambda ::=

742Lambda ::=

735− '\\' TypeOptDeclList '=>' Expr

743+ '\\' TypeOptDeclList LambdaTail

736− | '\\' SimpleExprList '=>' Expr

744+ | '\\' SimpleExprList LambdaTail

737 ;

745 ;

738@

746@

739@

747@

@@ -742,27 +750,34 @@ SimpleExprList ::=

742 | SimpleExpr ',' SimpleExprList

750 | SimpleExpr ',' SimpleExprList

743 ;

751 ;

744@

752@

753+@

754+LambdaTail ::=

755+ Impossible

756+ | '=>' Expr

757+@

745-}

758-}

746lambda :: SyntaxInfo -> IdrisParser PTerm

759lambda :: SyntaxInfo -> IdrisParser PTerm

747lambda syn = do lchar '\\' <?> "lambda expression"

760lambda syn = do lchar '\\' <?> "lambda expression"

748− (do xt <- try $ tyOptDeclList syn

761+ ((do xt <- try $ tyOptDeclList syn

749− fc <- getFC

762+ fc <- getFC

750− symbol "=>"

763+ sc <- lambdaTail

751− sc <- expr syn

752− return (bindList (PLam fc) xt sc)) <|> do

764+ return (bindList (PLam fc) xt sc))

765+ <|>

753− ps <- sepBy (do fc <- getFC

766+ (do ps <- sepBy (do fc <- getFC

754− e <- simpleExpr (syn { inPattern = True })

767+ e <- simpleExpr (syn { inPattern = True })

755− return (fc, e)) (lchar ',')

768+ return (fc, e))

756− symbol "=>"

769+ (lchar ',')

757− sc <- expr syn

770+ sc <- lambdaTail

758− return (pmList (zip [0..] ps) sc)

771+ return (pmList (zip [0..] ps) sc)))

759− <?> "lambda expression"

772+ <?> "lambda expression"

760 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

773 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

761 pmList [] sc = sc

774 pmList [] sc = sc

762 pmList ((i, (fc, x)) : xs) sc

775 pmList ((i, (fc, x)) : xs) sc

763 = PLam fc (sMN i "lamp") Placeholder

776 = PLam fc (sMN i "lamp") Placeholder

764 (PCase fc (PRef fc (sMN i "lamp"))

777 (PCase fc (PRef fc (sMN i "lamp"))

765 [(x, pmList xs sc)])

778 [(x, pmList xs sc)])

779+ lambdaTail :: IdrisParser PTerm

780+ lambdaTail = impossible <|> symbol "=>" *> expr syn

766

781

767{- | Parses a term rewrite expression

782{- | Parses a term rewrite expression

768@

783@

src/Idris/Parser.hs+4−2

@@ -479,6 +479,8 @@ fnOpts opts

479 fnOpts (ErrorReverse : opts)

480 <|> do try (lchar '%' *> reserved "reflection");

481 fnOpts (Reflection : opts)

482+ <|> do try (lchar '%' *> reserved "hint");

483+ fnOpts (AutoHint : opts)

482 <|> do lchar '%'; reserved "specialise";

484 <|> do lchar '%'; reserved "specialise";

483 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

485 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

484 fnOpts (Specialise ns : opts)

486 fnOpts (Specialise ns : opts)

@@ -813,7 +815,7 @@ argExpr syn = let syn' = syn { inPattern = True } in

813@

815@

814RHS ::= '=' Expr

816RHS ::= '=' Expr

815 | '?=' RHSName? Expr

817 | '?=' RHSName? Expr

816− | 'impossible'

818+ | Impossible

817 ;

819 ;

818@

820@

819

821

@@ -829,7 +831,7 @@ rhs syn n = do lchar '='; expr syn

829 return n)

831 return n)

830 r <- expr syn

832 r <- expr syn

831 return (addLet fc name r)

833 return (addLet fc name r)

832− <|> do reserved "impossible"; return PImpossible

834+ <|> impossible

833 <?> "function right hand side"

835 <?> "function right hand side"

834 where mkN :: Name -> Name

836 where mkN :: Name -> Name

835 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))

837 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))

src/Idris/Primitives.hs+4−23

@@ -166,29 +166,10 @@ primitives =

166 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

167 (1, LStrRev) total,

168

169−-- Prim (sUN "prim__readFile") (ty [WorldType,PtrType] StrType) 2 (p_cantreduce)

170−-- (2, LReadFile) total, -- total is okay, because we have 'WorldType'

171−-- Prim (sUN "prim__writeFile") (ty [WorldType,PtrType,StrType] (AType (ATInt ITNative))) 3 (p_cantreduce)

172−-- (3, LWriteFile) total,

173−-- Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

169+ Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

174−-- (1, LReadStr) total, -- total is okay, because we have 'WorldType'

170+ (1, LReadStr) total, -- total is okay, because we have 'WorldType'

175−-- Prim (sUN "prim__writeString") (ty [WorldType,StrType] (AType (ATInt ITNative))) 2 (p_cantreduce)

171+ Prim (sUN "prim__writeString") (ty [WorldType,StrType] (AType (ATInt ITNative))) 2 (p_cantreduce)

176−-- (2, LWriteStr) total,

172+ (2, LWriteStr) total,

177−--

178−-- Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

179−-- (0, LVMPtr) total,

180−-- -- Streams

181−-- Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

182−-- (0, LStdIn) total,

183−-- Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

184−-- (0, LStdOut) total,

185−-- Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

186−-- (0, LStdErr) total,

187−-- Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

188−-- (0, LNullPtr) total,

189−-- -- Managed pointer registration

190−-- Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)

191−-- (2, LRegisterPtr) total,

192 Prim (sUN "prim__systemInfo") (ty [AType (ATInt ITNative)] StrType) 1 (p_cantreduce)

173 Prim (sUN "prim__systemInfo") (ty [AType (ATInt ITNative)] StrType) 1 (p_cantreduce)

193 (1, LSystemInfo) total

174 (1, LSystemInfo) total

194 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

175 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

src/Idris/ProofSearch.hs+46−32

@@ -91,7 +91,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

91 if ambigok || argsok then

92 case lookupCtxt nroot (idris_tyinfodata ist) of

93 [TISolution ts] -> findInferredTy ts

94− _ -> psRec rec maxDepth

94+ _ -> psRec rec maxDepth []

95 else autoArg (sUN "auto") -- not enough info in the type yet

96 where

97 findInferredTy (t : _) = elab (delab ist (toUN t))

@@ -99,10 +99,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

99 conArgsOK ty

100 = let (f, as) = unApply ty in

101 case f of

102− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

102+ P _ n _ -> case lookupCtxtExact n (idris_datatypes ist) of

103− [t] -> do rs <- mapM (conReady as) (con_names t)

103+ Just t -> do rs <- mapM (conReady as) (con_names t)

104− return (and rs)

104+ return (and rs)

105− _ -> fail "Ambiguous name"

105+ Nothing -> -- local variable, go for it

106+ return True

106 TType _ -> return True

107 TType _ -> return True

107 _ -> fail "Not a data type"

108 _ -> fail "Not a data type"

108

109

@@ -129,12 +130,17 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

129 toUN (App f a) = App (toUN f) (toUN a)

130 toUN (App f a) = App (toUN f) (toUN a)

130 toUN t = t

131 toUN t = t

131

132

133+ -- psRec counts depth and the local variable applications we're under

134+ -- (so we don't try a pointless application of something to itself,

135+ -- which obviously won't work anyway but might lead us on a wild

136+ -- goose chase...)

132− psRec _ 0 | fromProver = cantSolveGoal

137+ psRec _ 0 locs | fromProver = cantSolveGoal

133− psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"

138+ psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"

134− psRec False d = tryCons d hints

139+ psRec False d locs = tryCons d locs hints

140+ psRec True d locs

135− psRec True d = do compute

141+ = do compute

136 try' (trivial elab ist)

142 try' (trivial elab ist)

137− (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

143+ (try' (try' (resolveByCon (d - 1) locs) (resolveByLocals (d - 1) locs)

138 True)

144 True)

139 -- if all else fails, make a new metavariable

145 -- if all else fails, make a new metavariable

140 (if fromProver

146 (if fromProver

@@ -145,42 +151,50 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

145 getFn d (Just f) | d < maxDepth-1 = [f]

151 getFn d (Just f) | d < maxDepth-1 = [f]

146 | otherwise = []

152 | otherwise = []

147

153

148− resolveByCon d

154+ resolveByCon d locs

149 = do t <- goal

155 = do t <- goal

150 let (f, _) = unApply t

156 let (f, _) = unApply t

151 case f of

157 case f of

152− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

158+ P _ n _ ->

159+ do let autohints = case lookupCtxtExact n (idris_autohints ist) of

160+ Nothing -> []

161+ Just hs -> hs

162+ case lookupCtxtExact n (idris_datatypes ist) of

163+ Just t -> tryCons d locs (hints ++

153− [t] -> tryCons d (hints ++ con_names t ++

164+ con_names t ++

165+ autohints ++

154− getFn d fn)

166+ getFn d fn)

155− _ -> fail "Not a data type"

167+ Nothing -> fail "Not a data type"

156 _ -> fail "Not a data type"

168 _ -> fail "Not a data type"

157

169

158 -- if there are local variables which have a function type, try

170 -- if there are local variables which have a function type, try

159 -- applying them too

171 -- applying them too

160− resolveByLocals d

172+ resolveByLocals d locs

161 = do env <- get_env

173 = do env <- get_env

162− tryLocals d env

174+ tryLocals d locs env

163

175

164− tryLocals d [] = fail "Locals failed"

176+ tryLocals d locs [] = fail "Locals failed"

177+ tryLocals d locs ((x, t) : xs)

178+ | x `elem` locs = tryLocals d locs xs

165− tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True

179+ | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True

166

180

167− tryCons d [] = fail "Constructors failed"

181+ tryCons d locs [] = fail "Constructors failed"

168− tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True

182+ tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True

169

183

184+ tryLocal d locs n t

170− tryLocal d n t = do let a = getPArity (delab ist (binderTy t))

185+ = do let a = getPArity (delab ist (binderTy t))

171− tryLocalArg d n a

186+ tryLocalArg d locs n a

172

187

173− tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)

188+ tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)

174− tryLocalArg d n i = simple_app False (tryLocalArg d n (i - 1))

189+ tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))

175− (psRec True d) "proof search local apply"

190+ (psRec True d locs) "proof search local apply"

176

191

177 -- Like type class resolution, but searching with constructors

192 -- Like type class resolution, but searching with constructors

178− tryCon d n =

193+ tryCon d locs n =

179 do ty <- goal

194 do ty <- goal

180− let imps = case lookupCtxtName n (idris_implicits ist) of

195+ let imps = case lookupCtxtExact n (idris_implicits ist) of

181− [] -> []

196+ Nothing -> []

182− [args] -> map isImp (snd args)

197+ Just args -> map isImp args

183− _ -> fail "Ambiguous name"

184 ps <- get_probs

198 ps <- get_probs

185 hs <- get_holes

199 hs <- get_holes

186 args <- map snd <$> try' (apply (Var n) imps)

200 args <- map snd <$> try' (apply (Var n) imps)

@@ -190,7 +204,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

190 when (length ps < length ps') $ fail "Can't apply constructor"

204 when (length ps < length ps') $ fail "Can't apply constructor"

191 mapM_ (\ (_, h) -> do focus h

205 mapM_ (\ (_, h) -> do focus h

192 aty <- goal

206 aty <- goal

193− psRec True d)

207+ psRec True d locs)

194 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

208 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

195 solve

209 solve

196

210

src/Idris/REPL.hs+1−1

@@ -59,7 +59,7 @@ import IRTS.System

59

60import Control.Category

61import qualified Control.Exception as X

62−import Prelude hiding ((.), id)

62+import Prelude hiding ((<$>), (.), id)

63import Data.List.Split (splitOn)

64import Data.List (groupBy)

65import qualified Data.Text as T

test/proof009/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris $@ --quiet proof009.idr < input

2+idris $@ --consolewidth 70 --quiet proof009.idr < input

3rm -f *.ibc

test/proof010/expectednew file+6

@@ -0,0 +1,6 @@

1+2, << function >>

2+3, << function >>

3+

4+some bools

5+some bools

6+

test/proof010/proof010.idrnew file+39

@@ -0,0 +1,39 @@

1+data MyShow : Type -> Type where

2+ ShowInstance : (show : a -> String) -> MyShow a

3+

4+myshow : {auto inst : MyShow a} -> a -> String

5+myshow {inst = ShowInstance show} x1 = show x1

6+

7+%hint

8+showNat : MyShow Nat

9+showNat = ShowInstance show

10+

11+%hint

12+showFn : MyShow (a -> b)

13+showFn = ShowInstance (\x => "<< function >>")

14+

15+%hint

16+showBools : MyShow (Bool, Bool)

17+showBools = ShowInstance (\x => "some bools")

18+

19+%hint

20+showStuff : MyShow a -> MyShow b -> MyShow (a, b)

21+showStuff sa sb = ShowInstance showPair

22+ where

23+ showPair : (a, b) -> String

24+ showPair (x, y) = myshow x ++ ", " ++ myshow y

25+

26+testShow : List (Bool, Bool) -> String

27+testShow [] = ""

28+testShow (x :: xs) = myshow x ++ "\n" ++ testShow xs

29+

30+testShow2 : List (Nat, Int -> Int) -> String

31+testShow2 [] = ""

32+testShow2 (x :: xs) = myshow x ++ "\n" ++ testShow2 xs

33+

34+main : IO ()

35+main = do putStrLn $ testShow2 [(2, (+1)), (3, abs)]

36+ putStrLn $ testShow [(True, False), (False, True)]

37+

38+

39+

test/proof010/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ proof010.idr -o proof010

3+./proof010

4+rm -f proof010 *.ibc

test/totality009/TestLambdaImpossible.idrnew file+29

@@ -0,0 +1,29 @@

1+module TestLambdaImpossible

2+

3+%default total

4+

5+eqBool : (x, y : Bool) -> Dec (x = y)

6+eqBool False False = Yes Refl

7+eqBool False True = No (\(Refl) impossible)

8+eqBool True False = No (\(Refl) impossible)

9+eqBool True True = Yes Refl

10+

11+data Elem : {a : Type} -> a -> Prelude.List.List a -> Type where

12+ Here : {a : Type} -> {x : a} -> {xs : List a} -> Elem x (x :: xs)

13+ There : {a : Type} -> {x, y : a} -> {xs : List a} -> Elem x xs -> Elem x (y :: xs)

14+

15+notHereNotThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

16+notHereNotThere notEq notElem Here = notEq Refl

17+notHereNotThere notEq notElem (There elem) = notElem elem

18+

19+decElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

20+decElem x [] = No (\Here impossible)

21+decElem x (y :: xs) with (decEq x y)

22+ decElem x (x :: xs) | (Yes Refl) = Yes Here

23+ decElem x (y :: xs) | (No notHere) with (decElem x xs)

24+ decElem x (y :: xs) | (No notHere) | (Yes prf) = Yes (There prf)

25+ decElem x (y :: xs) | (No notHere) | (No notThere) = No $ notHereNotThere notHere notThere

26+

27+notEta : ((a : Type) -> (b : Type) -> (f : a -> b) -> f = (\x => f x)) -> Void

28+notEta eta = case eta Nat Nat id of

29+ Refl impossible

test/totality009/TestLambdaPossible.idrnew file+13

@@ -0,0 +1,13 @@

1+||| Some functions that should be non-total, as detected with --warnpartial

2+module TestLambdaPossible

3+

4+data Nool : Bool -> Type where

5+ Flase : Nool False

6+ Ture : Nool True

7+

8+wrongPossible : Nool True -> Bool

9+wrongPossible = (\Flase impossible)

10+

11+wrongPossible' : Nool True -> Bool

12+wrongPossible' x = case x of

13+ Flase impossible

test/totality009/expectednew file+8

@@ -0,0 +1,8 @@

1+TestLambdaPossible.idr:9:25:Warning - TestLambdaPossible.case block in wrongPossible is not total as there are missing cases

2+TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible

3+TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' is not total as there are missing cases

4+TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible'

5+TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPossible is not total as there are missing cases

6+TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible

7+TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' is not total as there are missing cases

8+TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible'

test/totality009/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+OPTS="--consolewidth infinite --nocolour"

3+idris "$@" $OPTS --check TestLambdaImpossible

4+idris "$@" $OPTS --check --warnpartial TestLambdaPossible

5+rm -f *.ibc