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

git.iko.soy/Idris-dev

Merge branch 'master' into agda-style-records

commit9c13628838371c2733076617ece14636f5006634 authorsualitu <sual@itu.dk> dateWed 1 Apr 2015, 15:35 (12 years ago) parent26dba59 53c0fd7

81 files changed+1185−604

compare with master

unifiedsplit

CHANGELOG+8 CONTRIBUTING.md+26−17 docs/README.md+6 docs/conf.py+11 docs/effects/conclusions.rst+2−2 docs/effects/depeff.rst+6−6 docs/effects/hangman.rst+10−10 docs/effects/impleff.rst+9−10 docs/effects/introduction.rst+2−2 docs/effects/simpleeff.rst+13−13 docs/effects/state.rst+8−8 docs/effects/summary.rst+9−9 docs/faq/faq.rst+32−16 docs/guides/type-providers-ffi.rst+12−11 docs/index.rst+3−1 docs/proofs/index.rst+1 docs/proofs/inductive.rst+6−5 docs/proofs/interactive.rst+165 docs/proofs/patterns.rst+7−6 docs/proofs/pluscomm.rst+7−6 docs/reference/documenting.rst+4−4 docs/reference/erasure.rst+21−20 docs/reference/ffi.rst+8−7 docs/reference/uniqueness-types.rst+5−4 docs/tutorial/classes.rst+12−12 docs/tutorial/conclusions.rst+2−2 docs/tutorial/index.rst+3−3 docs/tutorial/interactive.rst+10−10 docs/tutorial/interp.rst+7−7 docs/tutorial/introduction.rst+4−4 docs/tutorial/miscellany.rst+17−17 docs/tutorial/modules.rst+5−5 docs/tutorial/packages.rst+4−4 docs/tutorial/provisional.rst+5−5 docs/tutorial/starting.rst+5−5 docs/tutorial/syntax.rst+11−8 docs/tutorial/theorems.rst+12−168 docs/tutorial/typesfuns.rst+42−33 docs/tutorial/views.rst+4−4 idris.cabal+8−2 libs/base/Control/Monad/RWS.idr+1−1 libs/contrib/Control/WellFounded.idr+83 libs/contrib/Data/Nat.idr+165 libs/contrib/contrib.ipkg+2 libs/prelude/Builtins.idr−2 libs/prelude/Prelude.idr+6 libs/prelude/Prelude/Nat.idr+14 rts/Makefile+2−2 rts/getline.c+81 rts/getline.h+7 rts/idris_rts.c+10−42 src/IRTS/CodegenC.hs+7−8 src/IRTS/CodegenJavaScript.hs+1−2 src/IRTS/Lang.hs+1 src/Idris/AbsSyntax.hs+17 src/Idris/AbsSyntaxTree.hs+6 src/Idris/Core/Evaluate.hs+5−3 src/Idris/Core/Unify.hs+2 src/Idris/DeepSeq.hs+1 src/Idris/Delaborate.hs+2 src/Idris/Docs.hs+2 src/Idris/Docstrings.hs+2 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Instance.hs+3−2 src/Idris/Elab/Type.hs+8−3 src/Idris/ElabTerm.hs+15−11 src/Idris/IBC.hs+15−5 src/Idris/Output.hs+3−1 src/Idris/ParseExpr.hs+31−16 src/Idris/Parser.hs+4−2 src/Idris/Primitives.hs+4−23 src/Idris/ProofSearch.hs+46−32 src/Idris/REPL.hs+1−1 test/proof009/run+1−1 test/proof010/expected+6 test/proof010/proof010.idr+39 test/proof010/run+4 test/totality009/TestLambdaImpossible.idr+29 test/totality009/TestLambdaPossible.idr+13 test/totality009/expected+8 test/totality009/run+5

CHANGELOG+8

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

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

1111 purpose primitives

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

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

1417 need to explicitly name results in dependent effect signatures instead

1518 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 }

1624

1725New in 0.9.17:

1826--------------

CONTRIBUTING.md+26−17

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

11# Contributing to Idris-Dev

33The 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.

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

77## Getting Started

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

2222

2323## The Campsite Rule

2424

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.

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

2727

2828## Contributing to the default libraries.

2929

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

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.

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+

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.

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

3339

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

35−the `--noprelude` option.

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

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.

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

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

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

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.

43+

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

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

4046

4147As 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).

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.

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

4449

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.

4655

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!

4857

4958## Making Changes

5059

5160Idris 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.

5362

5463### New contributors

5564

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

8594

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

8796 * 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.

8998

9099```

91100$ git branch fix/master/my_contrib master

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

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

119128

1201291. 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.

122131

123132```

124133$ make test

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

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

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

138147

139−## Increases chances of acceptance.

148+## Increasing chances of acceptance.

140149

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

142151

1431521. 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

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

146155

147156## Additional Resources

docs/README.md+6

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

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

1919 disappear because of that.

2020

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

22+

23+```sh

24+pip install sphinx_rtd_theme

25+```

26+

2127### LaTeX

2228

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

docs/conf.py+11

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

1515import sys

1616import os

1717

18+# True if the readthedocs theme is locally installed

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

20+

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

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

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

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

111114# a list of builtin themes.

112115html_theme = "default"

113116

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+

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

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

116127# documentation.

docs/effects/conclusions.rst+2−2

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

11.. _sect-further:

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

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

44Further Reading

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

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

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

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

docs/effects/depeff.rst+6−6

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

11.. _sect-depeff:

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

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

44Dependent Effects

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

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

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

88constant. 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

1616resource-safe protocol for file management.

1717

1818Dependent States

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

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

2020

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

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

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

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

6060

6161Result-dependent Effects

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

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

6363

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

6565otherwise 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.

134134 being inspected in the type of each branch.

135135

136136File Management

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

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

138138

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

140140protocols 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

242242file open for writing.

243243

244244Pattern-matching bind

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

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

246246

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

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

docs/effects/hangman.rst+10−10

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

11.. _sect-hangman:

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

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

44Example: A “Mystery Word” Guessing Game

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

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

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

88discussed 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

2929interface).

3030

3131Step 1: Game State

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

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

3333

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

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

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

5353 data Mystery : GState -> Type

5454

5555Step 2: Game Rules

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

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

5757

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

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

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

131131 MYSTERY h = MkEff (Mystery h) MysteryRules

132132

133133Step 3: Implement Rules

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

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

135135

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

137137game state:

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

211211not follow the rules.

212212

213213Step 4: Implement Interface

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

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

215215

216216Having described the rules, and implemented state transitions which

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

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

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

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

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

228−stated rules.

228+stated rules.

229229

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

231231letters 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

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

268268

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

270−presented below:

270+presented below:

271271

272272.. code-block:: idris

273273

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

298298 (S k) => game

299299

300300Discussion

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

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

302302

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

304304which 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

330330checker before any testing of the game.

331331

332332.. [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 @@

11.. _sect-impleff:

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

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

44Creating New Effects

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

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

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

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

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

1414effectful operations may be provided.

1515

1616State

17−-----

17+=====

1818

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

2020constructors describe the operations provided when the effect is

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

154154new effects, however.

155155

156156Summary

157−~~~~~~~

157+-------

158158

159159The following listing summarises what is required to define the

160160``STATE`` effect:

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

183183

184184

185185Console I/O

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

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

187187

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

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

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

219219 STDIO = MkEff () StdIO

220220

221221Exceptions

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

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

223223

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

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

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

244244

245245

246246Non-determinism

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

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

248248

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

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

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

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

278278

279279File Management

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

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

281281

282282Result-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

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

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

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

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

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

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

322322handler refers to an open file or not.

323−

docs/effects/introduction.rst+2−2

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

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

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

22Introduction

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

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

55Pure functional languages with dependent types such as `Idris

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

docs/effects/simpleeff.rst+13−13

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

11.. _sect-simpleff:

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

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

44Simple Effects

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

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

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

88using 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

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

4242

4343Console I/O

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

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

4545

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

4747effect, 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:

6767 instance Handler StdIO (IOExcept a)

6868

6969Examples

70−~~~~~~~~

70+--------

7171

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

7373as follows:

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

117117to be changed.

118118

119119Aside: Resource Types

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

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

121121

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

123123if 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

132132 Int : Type

133133

134134Exceptions

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

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

136136

137137The ``EXCEPTION``

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

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

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

156156

157157Example

158−~~~~~~~

158+-------

159159

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

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

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

232232 else raise NotANumber

233233

234234Random Numbers

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

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

236236

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

238238``Effect.Random``:

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

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

264264

265265Example

266−~~~~~~~

266+-------

267267

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

269269``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`.

317317

318318

319319Non-determinism

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

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

321321

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

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

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

337337 instance Handler Selection List

338338

339339Example

340−~~~~~~~

340+-------

341341

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

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

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

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

374374

375375``vadd`` revisited

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

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

377377

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

379379definition:

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

453453 else raise "Not a number"

454454

455455Example: An Expression Calculator

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

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

457457

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

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

docs/effects/state.rst+8−8

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

11.. _sect-state:

3−=====

3+*****

44State

5−=====

5+*****

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

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

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

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

3535

3636First attempt

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

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

3838

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

4040function 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

7575explicit.

7676

7777Introducing ``Effects``

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

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

7979

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

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

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

217217 main = print (treeTag 1 testTree)

218218

219219Effects and Resources

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

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

221221

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

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

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

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

262262

263263Labelled Effects

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

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

265265

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

267267the 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``.

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

359359

360360``!``-notation

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

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

362362

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

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

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

412412 f g'

413413

414414Syntactic Sugar and ``Eff``

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

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

416416

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

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

docs/effects/summary.rst+9−9

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

11.. _sect-appendix:

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

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

44Effects Summary

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

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

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

88library.

1010EXCEPTION

11−---------

11+=========

1212

1313.. code-block:: idris

1414

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

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

3030

3131FILE\_IO

32−--------

32+========

3333

3434.. code-block:: idris

3535

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

5858 instance Handler FileIO IO

5959

6060RND

61−---

61+===

6262

6363.. code-block:: idris

6464

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

7777 instance Handler Random m

7878

7979SELECT

80−------

80+======

8181

8282.. code-block:: idris

8383

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

9393 instance Handler Selection List

9494

9595STATE

96−-----

96+=====

9797

9898.. code-block:: idris

9999

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

111111 instance Handler State m

112112

113113STDIO

114−-----

114+=====

115115

116116.. code-block:: idris

117117

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

133133 instance Handler StdIO (IOExcept a)

134134

135135SYSTEM

136−------

136+======

137137

138138.. code-block:: idris

139139

docs/faq/faq.rst+32−16

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

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

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

22Frequently Asked Questions

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

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

55What are the differences between Agda and Idris?

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

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

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

99verified 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

1414lightweight Hugs/GHCI style interface.

1515

1616Is Idris production ready?

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

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

1818

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

2020development 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

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

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

3030

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

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

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

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

3333

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

3535because 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

5757``Int``.

5858

5959How can I make lazy control structures?

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

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

6161

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

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

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

7575

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

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

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

7878

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

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

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

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

101101

102102When will Idris be self-hosting?

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

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

104104

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

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

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

108108

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

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

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

111111

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

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

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

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

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

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

116116

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+

117134What does the name ‘Idris’ mean?

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

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

119136

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

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

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

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

123140

124141Where can I find more answers?

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

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

126143

127144There is an `Unofficial FAQ

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

129146github 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+***********************

12Type Providers in Idris

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

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

45`Type providers in Idris

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

910providers.

1011

1112The use case

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

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

1314

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

1516a 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

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

2425

2526A simple example

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

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

2728

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

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

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

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

9596

9697Foreign Functions

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

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

9899

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

100101size 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.

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

115116out we can.

116117

117−mkForeign

118−~~~~~~~~~

118+``mkForeign``

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

119120

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

121122like this:

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

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

139140

140141Caveats of mkForeign

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

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

142143

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

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

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

185186 lengths = mapM strlen listOfStrings

186187

187188Running foreign functions

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

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

189190

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

191192actually 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

193194our code.

194195

195196In the interpreter

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

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

197198

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

199200as 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

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

214215

215216In an executable

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

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

217218

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

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

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

229230directory from which we run idris.)

230231

231232Putting it all together

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

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

233234

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

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

docs/index.rst+3−1

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

1515

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

1717

18+

1819* :ref:`tutorial-index`

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

2021* :ref:`faq-index`

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

4748 tutorial/miscellany

4849 tutorial/conclusions

4950

50−.. _effects:

51+.. _faq:

5152

5253##########################

5354Frequently Asked Questions

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

8889 proofs/pluscomm

8990 proofs/inductive

9091 proofs/patterns

92+ proofs/interactive

9193

9294.. _reference:

9395

docs/proofs/index.rst+1

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

2121 pluscomm

2222 inductive

2323 patterns

24+ interactive

2425

docs/proofs/inductive.rst+6−5

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

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

12Inductive Proofs

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

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

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

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

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

2526

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

2728can 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``

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

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

3132

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

5051.. code-block:: idris

5152

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

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

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

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

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

5657 P x

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

6364.. code-block:: idris

6465

6566 plus_ind : Nat -> Nat -> Nat

66− plus_ind n m

67+ plus_ind n m

6768 = nat_induction (\x => Nat)

6869 m -- Base case, plus_ind Z m

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

7071 -- where k_rec = plus_ind k m

71− n

72+ n

7273

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

7475``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+***************************

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.

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

12Pattern Matching Proofs

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

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

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

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

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

2627

2728

2829Creating a Definition

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

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

3031

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

3233declaration:

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

8788 plus_commutes (S k) m = ?plus_commutes_S

8889

8990Base Case

90−---------

91+=========

9192

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

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

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

263264The base case is now complete.

264265

265266Inductive Step

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

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

267268

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

269270state:

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

333334 plus_commutes_S k Z = Refl

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

335336

336−All metavariables have now been solved,

337+All metavariables have now been solved,

337338

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

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

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

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

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

docs/proofs/pluscomm.rst+7−6

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

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

12Running example: Addition of Natural Numbers

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

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

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

56function, 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

4445we must *prove* them.

4546

4647Equality Proofs

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

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

4849

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

5051as follows:

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

9394 4 = 5 (Expected type)

9495

9596Type checking equality proofs

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

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

9798

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

99100which attempts to resolve implicit arguments such as the implicit

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

123124 plus_reduces_Sk k m = Refl

124125

125126Heterogeneous Equality

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

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

127128

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

129130equalities between values in different types:

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

164165 vect_eq_length xs _ Refl = Refl

165166

166167Properties of ``plus``

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

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

168169

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

170171given above as Idris type declarations:

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

185186see where the need for them arises in practice.

186187

187188.. [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 @@

11.. _sect-documenting:

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

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

44Documenting Idris Code

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

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

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

88for 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

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

1313

1414Comments

15−--------

15+========

1616

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

1818is. 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

2222simple documentation for the readers of Idris code.

2323

2424Inline Documentation

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

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

2626

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

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

docs/reference/erasure.rst+21−20

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

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

12Erasure By Usage Analysis

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

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

45This work stems from this `feature proposal

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

89eventual implementation.

910

1011Motivation

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

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

1213

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

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

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

5253the runtime performance asymptotically.

5354

5455Binary numbers

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

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

5657

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

5859

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

106107programmer would write.

107108

108109U-views of lists

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

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

110111

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

112113

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

141142achieve this goal.

142143

143144Changes to Idris

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

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

145146

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

147148for 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

185186required to be *unused* instead.

186187

187188Changes to the language

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

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

189190

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

191192runtime.

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

221222and free implicits are automatically dotted here, too.

222223

223224What it means

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

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

225226

226227Dot annotations serve two purposes:

227228

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

235236from using the values they want to erase.

236237

237238How to use it

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

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

239240

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

241242turns 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

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

251252

252253Benchmarks

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

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

254255

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

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

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

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

259260

260261Shortcomings

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

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

262263

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

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

300301in the program.

301302

302303Planned features

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

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

304305

305306- Fixes to the above shortcomings in general.

306307

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

316317 in compiled programs.

317318

318319Troubleshooting

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

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

320321

321322My program is slower

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

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

323324

324325The patch introducing erasure by usage analysis also disabled some

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

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

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

337338

338339Usage warnings are unhelpful

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

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

340341

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

342343`How to read and resolve erasure

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

344345

345346There should be no warnings in this function

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

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

347348

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

349350non-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

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

362363

363364The compiler refuses to recognise this thing as erased

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

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

365366

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

367368monad. While this program triggers usage warnings,

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

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

380381

381382How to read and resolve erasure warnings

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

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

383384

384385Example 1

385−~~~~~~~~~

386+---------

386387

387388Consider the following program:

388389

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

439440Which solution is appropriate depends on the usecase.

440441

441442Example 2

442−~~~~~~~~~

443+---------

443444

444445Consider the following program manipulating value-indexed binary

445446numbers.

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

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

495496

496497References

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

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

498499

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

500501 families need not store their indices

docs/reference/ffi.rst+8−7

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

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

12New Foreign Function Interface

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

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

45.. sectionauthor:: Edwin Brady

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

1920describes.

2021

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

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

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

2324

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

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

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

6162external library file or even a URL).

6263

6364FFI descriptors

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

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

6566

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

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

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

9899 String -- the name of the C function

99100

100101Foreign calls

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

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

102103

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

104105example:

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

134135 jscall fname ty = foreign FFI_JS fname ty

135136

136137FFI implementation

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

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

138139

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

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

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

172173 FFun C_Str (FFun C_Str (FRet C_Ptr))

173174

174175Compiling foreign calls

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

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

176177

177178(This section assumes some knowledge of the Idris internals.)

178179

@@ -232,7 +233,7 @@ to marshal the arguments and return value appropriately.

232233 the function ``toFType``, to see how this works in practice.

233234

234235JavaScript FFI descriptor

235−~~~~~~~~~~~~~~~~~~~~~~~~~

236+=========================

236237

237238The JavaScript FFI descriptor is a little more complex, because the

238239JavaScript FFI supports marshalling functions. It is defined as

docs/reference/uniqueness-types.rst+5−4

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

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

12Uniqueness Types

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

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

45Uniqueness Types are an experimental feature available from Idris

560.9.15. A value with a unique type is guaranteed to have *at most one*

@@ -25,7 +26,7 @@ include:

2526 allocate

2627

2728Using Uniqueness

28−~~~~~~~~~~~~~~~~

29+================

2930

3031If ``x : T`` and ``T : UniqueType``, then there is at most one reference

3132to ``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

129130once on the right hand side.

130131

131132Borrowed Types

132−~~~~~~~~~~~~~~

133+--------------

133134

134135It quickly becomes obvious when working with uniqueness types that

135136having only one reference at a time can be painful. For example, what

@@ -227,7 +228,7 @@ therefore write ``showU`` as follows:

227228 showU' (x :: xs) = show x ++ ", " ++ showU' xs

228229

229230Problems/Disadvantages/Still to do...

230−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

231+-------------------------------------

231232

232233This is a work in progress, there is lots to do. The most obvious

233234problem is the loss of abstraction. On the one hand, we have more

docs/tutorial/classes.rst+12−12

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

11.. _sect-classes:

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

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

44Type Classes

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

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

77We often want to define functions which work across several different

88data 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``:

6565 show' (x :: xs) = show x ++ ", " ++ show' xs

6666

6767Default Definitions

68−-------------------

68+===================

6969

7070The library defines an ``Eq`` class which provides an interface for

7171comparing 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

110110the default is used instead.

111111

112112Extending Classes

113−-----------------

113+=================

114114

115115Classes can also be extended. A logical next step from an equality

116116relation ``Eq`` is to define an ordering relation ``Ord``. We can

@@ -155,7 +155,7 @@ separated list, for example:

155155 sortAndShow xs = show (sort xs)

156156

157157Functors and Applicatives

158−-------------------------

158+=========================

159159

160160So far, we have seen single parameter type classes, where the parameter

161161is of type ``Type``. In general, there can be any number (greater than

@@ -195,7 +195,7 @@ abstracts the notion of function application:

195195 (<*>) : f (a -> b) -> f a -> f b

196196

197197Monads and ``do``-notation

198−--------------------------

198+==========================

199199

200200The ``Monad`` class allows us to encapsulate binding and computation,

201201and is the basis of ``do``-notation introduced in Section

@@ -248,7 +248,7 @@ are available, or return ``Nothing`` if they are not. Managing the

248248 Nothing : Maybe Int

249249

250250``!``-notation

251−~~~~~~~~~~~~~~

251+--------------

252252

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

254254verbose, particularly in cases such as ``m_add`` above where the value

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

292292 f g'

293293

294294Monad comprehensions

295−~~~~~~~~~~~~~~~~~~~~

295+--------------------

296296

297297The list comprehension notation we saw in Section

298298:ref:`sect-more-expr` is more general, and applies to anything which

@@ -336,7 +336,7 @@ would be:

336336 m_add x y = [ x' + y' | x' <- x, y' <- y ]

337337

338338Idiom brackets

339−--------------

339+==============

340340

341341While ``do`` notation gives an alternative meaning to sequencing,

342342idioms give an alternative meaning to *application*. The notation and

@@ -386,7 +386,7 @@ application ``[| f a1 …an |]`` is translated into ``pure f <> a1 <>

386386 m_add' x y = [| x + y |]

387387

388388An error-handling interpreter

389−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

389+-----------------------------

390390

391391Idiom notation is commonly useful when defining evaluators. McBride

392392and Paterson describe such an evaluator [1]_, for a language similar

@@ -455,7 +455,7 @@ to handle errors:

455455 MkEval envFn => envFn env

456456

457457Named Instances

458−---------------

458+===============

459459

460460It can be desirable to have multiple instances of a type class, for

461461example to provide alternative methods for sorting or printing values.

@@ -492,7 +492,7 @@ instance ``myord`` as follows, at the Idris prompt:

492492

493493

494494Determining Parameters

495−----------------------

495+======================

496496

497497When a class has more than one parameter, it can help resolution if

498498the parameters used to resolve the type class are restricted. For

docs/tutorial/conclusions.rst+2−2

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

11.. _sect-concs:

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

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

44Further Reading

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

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

77Further information about Idris programming, and programming with

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

docs/tutorial/index.rst+3−3

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

11.. _tutorial-index:

3−####################

4− The Idris Tutorial

5−####################

3+##################

4+The Idris Tutorial

5+##################

77The is the Idris Tutorial. It will teach you about programming in the Idris Language.

docs/tutorial/interactive.rst+10−10

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

11.. _sect-interactive:

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

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

44Interactive Editing

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

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

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

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

@@ -25,7 +25,7 @@ available.

2525

2626

2727Editing at the REPL

28−-------------------

28+===================

2929

3030The REPL provides a number of commands, which we will describe

3131shortly, 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

5959commands, in order to provide interactive editing support.

6060

6161Editing Commands

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

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

6363

6464:addclause

65−~~~~~~~~~~

65+----------

6666

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

6868template 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

9191should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.

9292

9393:casesplit

94−~~~~~~~~~~

94+----------

9595

9696The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the

9797pattern 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

125125ys`` would lead to a unification error.

126126

127127:addmissing

128−~~~~~~~~~~~

128+-----------

129129

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

131131clauses 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

148148lead to unification errors.

149149

150150:proofsearch

151−~~~~~~~~~~~~

151+------------

152152

153153The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to

154154find 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

186186recursively.

187187

188188:makewith

189−~~~~~~~~~

189+---------

190190

191191The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a

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

219219valid patterns are.

220220

221221Interactive Editing in Vim

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

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

223223

224224The editor mode for Vim provides syntax highlighting, indentation and

225225interactive editing support using the commands described above.

docs/tutorial/interp.rst+7−7

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

11.. _sect-interp:

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

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

44Example: The Well-Typed Interpreter

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

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

77In this section, we’ll use the features we’ve seen so far to write a

88larger example, an interpreter for a simple functional programming

@@ -12,7 +12,7 @@ system to ensure that any programs which can be represented are

1212well-typed.

1313

1414Representing Languages

15−----------------------

15+======================

1616

1717First, let us define the types in the language. We have integers,

1818booleans, and functions, represented by ``Ty``:

@@ -140,7 +140,7 @@ that only the branch which is taken need be evaluated:

140140 Expr G a

141141

142142Writing the Interpreter

143−-----------------------

143+=======================

144144

145145When we evaluate an ``Expr``, we’ll need to know the values in scope,

146146as 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

225225 else interp env e

226226

227227Testing

228−-------

228+=======

229229

230230We can make some simple test functions. Firstly, adding two inputs

231231``\x. \y. y + x`` is written as follows:

@@ -248,7 +248,7 @@ can be written as:

248248 (Var Stop)))

249249

250250Running

251−-------

251+=======

252252

253253To finish, we write a ``main`` program which interprets the factorial

254254function on user input:

@@ -271,7 +271,7 @@ program at the Idris interactive environment is:

271271

272272

273273Aside: ``cast``

274−~~~~~~~~~~~~~~~

274+---------------

275275

276276The prelude defines a type class ``Cast`` which allows conversion

277277between types:

docs/tutorial/introduction.rst+4−4

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

11.. _sect-intro:

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

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

44Introduction

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

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

77In conventional programming languages, there is a clear distinction

88between *types* and *values*. For example, in `Haskell

@@ -44,7 +44,7 @@ a lightweight foreign function interface which allows easy interaction

4444with external ``C`` libraries.

4545

4646Intended Audience

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

47+=================

4848

4949This tutorial is intended as a brief introduction to the language, and

5050is 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

5555dependent types for writing and verifying systems software.

5656

5757Example Code

58−------------

58+============

5959

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

6161Idris version . The files are available in the Idris

docs/tutorial/miscellany.rst+17−17

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

11.. _sect-misc:

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

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

44Miscellany

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

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

77In this section we discuss a variety of additional features:

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

1515+ the universe hierarchy.

1616

1717Auto implicit arguments

18−-----------------------

18+=======================

1919

2020We have already seen implicit arguments, which allows arguments to be

2121omitted when they can be inferred by the type checker, e.g.

@@ -70,7 +70,7 @@ to:

7070 head (x :: xs) = x

7171

7272Implicit conversions

73−--------------------

73+====================

7474

7575Idris supports the creation of *implicit conversions*, which allow

7676automatic 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

9999beyond the scope of this tutorial.

100100

101101Literate programming

102−--------------------

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

103103

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

105105an 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

120120any other character).

121121

122122Foreign function calls

123−----------------------

123+======================

124124

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

126126external libraries, particularly for interfacing with the operating

@@ -191,7 +191,7 @@ function is implemented as follows, as a call to an external function

191191 putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

192192

193193Include and linker directives

194−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

194+-----------------------------

195195

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

197197with appropriate conversion between the Idris representation of a

@@ -215,7 +215,7 @@ through the following directives:

215215 object ``x.so``.

216216

217217Testing foreign function calls

218−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

218+------------------------------

219219

220220Normally, the Idris interpreter (used for typechecking and at the REPL)

221221will not perform IO actions. Additionally, as it neither generates C

@@ -232,7 +232,7 @@ command or the ``%dynamic`` directive. For example:

232232 0.9995736030415051 : Float

233233

234234Type Providers

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

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

236236

237237Idris type providers, inspired by F#’s type providers, are a means of

238238making our types be “about” something in the world outside of Idris. For

@@ -301,7 +301,7 @@ provider implementations, including a statically-checked SQLite binding,

301301are available in an external collection [1]_.

302302

303303C Target

304−--------

304+========

305305

306306The default target of Idris is C. Compiling via :

307307

@@ -341,14 +341,14 @@ is shown below :

341341 putStrLn $ show $ factorial 3

342342

343343JavaScript Target

344−-----------------

344+=================

345345

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

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

348348FFI to communicate with the *JavaScript* ecosystem.

349349

350350Code Generation

351−~~~~~~~~~~~~~~~

351+---------------

352352

353353Code generation is split into two separate targets. To generate code

354354that 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

375375does not show up in the *NodeJS* code generator.

376376

377377Using the FFI

378−~~~~~~~~~~~~~

378+-------------

379379

380380To write a useful application we need to communicate with the outside

381381world. Maybe we want to manipulate the DOM or send an Ajax request. For

@@ -441,7 +441,7 @@ program:

441441The program outputs ``3``, just like we expected.

442442

443443Including external *JavaScript* files

444−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

444+-------------------------------------

445445

446446Whenever one is working with *JavaScript* one might want to include

447447external libraries or just some functions that she or he wants to call

@@ -470,7 +470,7 @@ And for use in the browser:

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

471471

472472Including *NodeJS* modules

473−~~~~~~~~~~~~~~~~~~~~~~~~~~

473+--------------------------

474474

475475The *NodeJS* code generator can also include modules with the ``%lib``

476476directive.

@@ -486,7 +486,7 @@ This directive compiles into the following *JavaScript*

486486 var fs = require("fs");

487487

488488Shrinking down generated *JavaScript*

489−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

489+-------------------------------------

490490

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

492492generated 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*

497497application written in Idris.

498498

499499Cumulativity

500−------------

500+============

501501

502502Since values can appear in types and *vice versa*, it is natural that

503503types themselves have types. For example:

docs/tutorial/modules.rst+5−5

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

11.. _sect-namespaces:

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

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

44Modules and Namespaces

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

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

77An Idris program consists of a collection of modules. Each module

88includes an optional ``module`` declaration giving the name of the

@@ -72,7 +72,7 @@ main module, with the ``main`` function, must be called

7272``Main``—although its filename need not be ``Main.idr``.

7373

7474Export Modifiers

75−----------------

75+================

7676

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

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

@@ -146,7 +146,7 @@ abstract names in module ``C``, but will not re-export anything from

146146module ``B``.

147147

148148Explicit Namespaces

149−-------------------

149+===================

150150

151151Defining a module also defines a namespace implicitly. However,

152152namespaces can also be given *explicitly*. This is most useful if you

@@ -176,7 +176,7 @@ disambiguated by their types:

176176 "foofoo" : String

177177

178178Parameterised blocks

179−--------------------

179+====================

180180

181181Groups of functions can be parameterised over a number of arguments

182182using a ``parameters`` declaration, for example:

docs/tutorial/packages.rst+4−4

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

11.. _sect-packages:

3−========

3+********

44Packages

5−========

5+********

77Idris includes a simple system for building packages from a

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

@@ -10,7 +10,7 @@ compiler to manage the development process of your Idris

1010programmes and packages.

1111

1212Package Descriptions

13−--------------------

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

1414

1515A package description includes the following:

1616

@@ -58,7 +58,7 @@ external ``C`` libraries, the following options are available:

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

5959

6060Using Package files

61−-------------------

61+===================

6262

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

6464

docs/tutorial/provisional.rst+5−5

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

11.. _sect-provisional:

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

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

44Provisional Definitions

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

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

77Sometimes when programming with dependent types, the type required by

88the 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

5454program to fix this problem?

5555

5656Provisional definitions

57−-----------------------

57+=======================

5858

5959*Provisional definitions* help with this problem by allowing us to defer

6060the proof details until a later point. There are two main reasons why

@@ -159,7 +159,7 @@ reversed:

159159 "[False, True, False, True, False, True]" : String

160160

161161Suspension of Disbelief

162−-----------------------

162+=======================

163163

164164Idris requires that proofs be complete before compiling programs

165165(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.

192192In this case, we assert that the value we gave was correct.

193193

194194Example: Binary numbers

195−-----------------------

195+=======================

196196

197197Previously, we implemented conversion to binary numbers using the

198198``Parity`` view. Here, we show how to use the same view to implement a

docs/tutorial/starting.rst+5−5

@@ -1,11 +1,11 @@

11.. _sect-starting:

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

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

44Getting Started

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

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

77Prerequisites

8−-------------

8+=============

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

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

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

1818 from MacPorts/Homebrew and all major Linux distributions.

1919

2020Downloading and Installing

21−--------------------------

21+==========================

2222

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

2424prerequisites, is to type:

@@ -69,7 +69,7 @@ instead. Some useful options to the Idris command are:

6969- ``--help`` display usage summary and command line options

7070

7171The Interactive Environment

72−---------------------------

72+===========================

7373

7474Entering ``idris`` at the shell prompt starts up the interactive

7575environment. You should see something like the following:

docs/tutorial/syntax.rst+11−8

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

1+.. _sect-syntax:

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

14Syntax Extensions

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

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

4−supports the implementation of *Embedded Domain Specific Languages*

5−(EDSLs) in several ways [1]_. One way, as we have already seen, is

6−through extending ``do`` notation. Another important way is to allow

7−extension of the core syntax. In this section we describe two ways of

8−extending the syntax: ``syntax`` rules and ``dsl`` notation.

7+Idris supports the implementation of *Embedded Domain Specific

8+Languages* (EDSLs) in several ways [1]_. One way, as we have already

9+seen, is through extending ``do`` notation. Another important way is

10+to allow extension of the core syntax. In this section we describe two

11+ways of extending the syntax: ``syntax`` rules and ``dsl`` notation.

912

1013``syntax`` rules

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

14+================

1215

1316We have seen ``if...then...else`` expressions, but these are not built

1417in. 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

101104``in`` in quotation marks since it is already a reserved word.

102105

103106``dsl`` notation

104−----------------

107+================

105108

106109The well-typed interpreter in Section :ref:`sect-interp` is a simple

107110example of a common programming pattern with dependent types. Namely:

docs/tutorial/theorems.rst+12−168

@@ -1,11 +1,11 @@

11.. _sect-theorems:

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

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

44Theorem Proving

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

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

77Equality

8−--------

8+========

1010Idris allows propositional equalities to be declared, allowing theorems about

1111programs to be stated and proved. Equality is built in, but conceptually

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

3131.. _sect-empty:

3232

3333The Empty Type

34−--------------

34+==============

3535

3636There is an empty type, :math:`\bot`, which has no constructors. It is

3737therefore impossible to construct an element of the empty type, at least

@@ -64,7 +64,7 @@ contradiction.

6464 void : Void -> a

6565

6666Simple Theorems

67−---------------

67+===============

6868

6969When type checking dependent types, the type itself gets *normalised*.

7070So 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:

116116Even for trival theorems like these, the proofs are a little tricky to

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

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

119−mode’.

119+mode’.

120120

121121Idris provides interactive editing capabilities, which can help with

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

123−an editor, see :ref:`proofs-index`. In the rest of this section, we discuss

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.

123+an editor, see :ref:`proofs-index`.

280124

281125.. _sect-totality:

282126

283127Totality Checking

284−-----------------

128+=================

285129

286130If we really want to trust our proofs, it is important that they are

287131defined by *total* functions — that is, a function which is defined for

@@ -351,7 +195,7 @@ total, a function ``f`` must:

351195- Not call any non-total functions

352196

353197Directives and Compiler Flags for Totality

354−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

198+------------------------------------------

355199

356200By default, Idris allows all well-typed definitions, whether total or not.

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

372216for any undeclared partial function.

373217

374218Totality checking issues

375−~~~~~~~~~~~~~~~~~~~~~~~~

219+------------------------

376220

377221Please note that the totality checker is not perfect! Firstly, it is

378222necessarily 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

382226is total which is not. Do not rely on it for your proofs yet!

383227

384228Hints for totality

385−~~~~~~~~~~~~~~~~~~

229+------------------

386230

387231In cases where you believe a program is total, but Idris does not agree, it is

388232possible to give hints to the checker to give more detail for a termination

389233argument. The checker works by ensuring that all chains of recursive calls

390234eventually lead to one of the arguments decreasing towards a base case, but

391235sometimes 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``

393237will always be smaller than ``(x :: xs)``:

394238

395239.. code-block:: idris

docs/tutorial/typesfuns.rst+42−33

@@ -1,11 +1,11 @@

11.. _sect-typefuns:

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

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

44Types and Functions

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

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

77Primitive Types

8−---------------

8+===============

1010Idris defines several primitive types: ``Int``, ``Integer`` and

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

7171 "The answer!" : String

7272

7373Data Types

74−----------

74+==========

7575

7676Data types are declared in a similar way to Haskell data types, with a

7777similar syntax. Natural numbers and lists, for example, can be

@@ -105,7 +105,7 @@ symbols:

105105 :+-*/=_.?|&><!@$%^~.

106106

107107Functions

108−---------

108+=========

109109

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

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

@@ -175,7 +175,7 @@ numbers. This means it can optimise the representation, and functions

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

176176

177177``where`` clauses

178−~~~~~~~~~~~~~~~~~

178+-----------------

179179

180180Functions can also be defined *locally* using ``where`` clauses. For

181181example, to define a function which reverses a list, we can use an

@@ -241,10 +241,10 @@ So, for example, the following definitions are legal:

241241 where z w = y + w

242242

243243Dependent Types

244−---------------

244+===============

245245

246246Vectors

247−~~~~~~~

247+-------

248248

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

250250length”, conventionally called vectors in the dependent type

@@ -322,7 +322,7 @@ two vectors — we needed a vector of length ``k + m``, but provided a

322322vector of length ``k + k``.

323323

324324The Finite Sets

325−~~~~~~~~~~~~~~~

325+---------------

326326

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

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

@@ -334,16 +334,25 @@ importing ``Data.Fin``, or can be declared as follows:

334334 FZ : Fin (S k)

335335 FS : Fin k -> Fin (S k)

336336

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+

337346``FZ`` is the zeroth element of a finite set with ``S k`` elements;

338347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``

339348elements. ``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

341−empty set, so neither constructor targets ``Fin Z``.

349+of elements in the set. Since we can’t construct an element of an

350+empty set, neither constructor targets ``Fin Z``.

342351

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

344353natural 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

346−numbers bounded by ``n``.

354+set of ``n`` elements, we can treat ``Fin n`` as the set of integers

355+greater than or equal to zero and less than ``n``.

347356

348357For example, the following function which looks up an element in a

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

359368location is bounded by the length of the vector (``n`` in each case),

360369so there is no need for a run-time bounds check. The type checker

361370guarantees that the location is no larger than the length of the

362−vector.

371+vector, and of course no less than zero.

363372

364373Note also that there is no case for ``Nil`` here. This is because it

365374is 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

368377compile time type error, since it would force ``n`` to be ``Z``.

369378

370379Implicit Arguments

371−~~~~~~~~~~~~~~~~~~

380+------------------

372381

373382Let us take a closer look at the type of ``index``:

374383

@@ -411,7 +420,7 @@ help document a function by making the purpose of an argument more

411420clear.

412421

413422“``using``” notation

414−~~~~~~~~~~~~~~~~~~~~

423+--------------------

415424

416425Sometimes it is useful to provide types of implicit arguments,

417426particularly where there is a dependency ordering, or where the

@@ -451,7 +460,7 @@ appear within the block:

451460 There : Elem x xs -> Elem x (y :: xs)

452461

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

454−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

463+---------------------------------------------

455464

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

457466dependent 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

476485block.

477486

478487I/O

479−---

488+===

480489

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

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

@@ -533,7 +542,7 @@ example for reading and writing files, including:

533542.. _sect-do:

534543

535544“``do``” notation

536−-----------------

545+=================

537546

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

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

@@ -564,7 +573,7 @@ can be overloaded.

564573.. _sect-lazy:

565574

566575Laziness

567−--------

576+========

568577

569578Normally, arguments to functions are evaluated before the function

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

@@ -602,7 +611,7 @@ without any explicit use of ``Force`` or ``Delay``:

602611 boolCase False t e = e;

603612

604613Useful Data Types

605−-----------------

614+=================

606615

607616Idris includes a number of useful data types and library functions

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

@@ -610,7 +619,7 @@ describes a few of these. The functions described here are imported

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

611620

612621``List`` and ``Vect``

613−~~~~~~~~~~~~~~~~~~~~~

622+---------------------

614623

615624We have already seen the ``List`` and ``Vect`` data types:

616625

@@ -683,7 +692,7 @@ remember that Idris is still in development, so if you don’t see

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

684693

685694Aside: Anonymous functions and operator sections

686−~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

695+------------------------------------------------

687696

688697There are actually neater ways to write the above expression. One way

689698would be to use an anonymous function:

@@ -710,7 +719,7 @@ by 2. It expands to ``\x => x * 2``. Similarly, ``(2*)`` would expand

710719to ``\x => 2 * x``.

711720

712721Maybe

713−~~~~~

722+-----

714723

715724``Maybe`` describes an optional value. Either there is a value of the

716725given type, or there isn’t:

@@ -744,7 +753,7 @@ simply ``b``. Since the default value might not be used, we mark it as

744753discarding it would be wasteful.

745754

746755Tuples and Dependent Pairs

747−~~~~~~~~~~~~~~~~~~~~~~~~~~

756+--------------------------

748757

749758Values can be paired with the following built-in data type:

750759

@@ -765,7 +774,7 @@ contain an arbitrary number of values, represented as nested pairs:

765774 jim = ("Jim", 25, "Cambridge")

766775

767776Dependent Pairs

768−~~~~~~~~~~~~~~~

777+---------------

769778

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

771780on the value of the first element. Traditionally, these are referred to

@@ -843,10 +852,10 @@ We will see more on ``with`` notation later.

843852.. _sect-more-expr:

844853

845854More Expressions

846−----------------

855+================

847856

848857``let`` bindings

849−~~~~~~~~~~~~~~~~

858+----------------

850859

851860Intermediate values can be calculated using ``let`` bindings:

852861

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

875884 name ++ " is " ++ show age ++ " years old"

876885

877886List comprehensions

878−~~~~~~~~~~~~~~~~~~~

887+-------------------

879888

880889Idris provides *comprehension* notation as a convenient shorthand

881890for building lists. The general form is:

@@ -902,7 +911,7 @@ by the difference between ``a`` and ``b``. This works for any numeric

902911type, using the ``count`` function from the prelude.

903912

904913``case`` expressions

905−~~~~~~~~~~~~~~~~~~~~

914+--------------------

906915

907916Another way of inspecting intermediate values of *simple* types is to

908917use a ``case`` expression. The following function, for example, splits

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

956965 itself.

957966

958967Dependent Records

959−-----------------

968+=================

960969

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

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

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

10271036 : Class

10281037

10291038Nested record update

1030−~~~~~~~~~~~~~~~~~~~~

1039+--------------------

10311040

10321041Idris also provides a convenient syntax for accessing and updating

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

docs/tutorial/views.rst+4−4

@@ -1,11 +1,11 @@

11.. _sec-views:

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

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

44Views and the “``with``” rule

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

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

77Dependent pattern matching

8−--------------------------

8+==========================

1010Since types can depend on values, the form of some arguments can be

1111determined by the value of others. For example, if we were to write

@@ -25,7 +25,7 @@ case, the definition would not be well typed.

2525.. _sect-nattobin:

2626

2727The ``with`` rule — matching intermediate values

28−------------------------------------------------

28+================================================

2929

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

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

idris.cabal+8−2

@@ -531,6 +531,9 @@ Extra-source-files:

531531 test/proof009/*.idr

532532 test/proof009/expected

533533 test/proof009/input

534+ test/proof010/run

535+ test/proof010/*.idr

536+ test/proof010/expected

534537

535538 test/quasiquote001/run

536539 test/quasiquote001/*.idr

@@ -608,6 +611,9 @@ Extra-source-files:

608611 test/totality008/run

609612 test/totality008/*.idr

610613 test/totality008/expected

614+ test/totality009/run

615+ test/totality009/*.idr

616+ test/totality009/expected

611617

612618 test/tutorial001/run

613619 test/tutorial001/*.idr

@@ -814,10 +820,10 @@ Library

814820 , containers >= 0.5 && < 0.6

815821 , deepseq < 1.5

816822 , directory >= 1.2 && < 1.3

817− , filepath < 1.4

823+ , filepath < 1.5

818824 , fingertree >= 0.1 && < 0.2

819825 , haskeline >= 0.7 && < 0.8

820− , lens >= 4.1.1 && < 4.8

826+ , lens >= 4.1.1 && < 4.9

821827 , mtl >= 2.1 && < 2.3

822828 , network < 2.7

823829 , 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

2323 pure a = MkRWST $ \_,s => return (a, s, neutral)

2424 (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

2525 (fn, ss, w') <- f r s

26− return (fn a, ss, w <+> w)

26+ return (fn a, ss, w <+> w')

2727

2828instance (Monoid w, Monad m) => Monad (RWST r w s m) where

2929 (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

8+%default total

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

4+import Data.Fin

5+import Data.So

7+import Control.WellFounded

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

33opts = "--nobasepkgs --total -i ../prelude -i ../base"

44modules = Control.Algebra,

55 Control.Isomorphism.Primitives,

6+ Control.WellFounded,

67 Classes.Verified,

78 Data.Fun, Data.Rel,

89 Data.Hash, Data.Matrix,

10+ Data.Nat,

911 Data.ZZ, Data.Sign,

1012 Data.BoundedList,

1113 Data.Heap,

libs/prelude/Builtins.idr−2

@@ -162,8 +162,6 @@ abstract data ManagedPtr : Type

162162

163163%extern prim__readFile : prim__WorldType -> Ptr -> String

164164%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int

165−%extern prim__readString : prim__WorldType -> String

166−%extern prim__writeString : prim__WorldType -> String -> Int

167165

168166%extern prim__vm : Ptr

169167%extern prim__stdin : Ptr

libs/prelude/Prelude.idr+6

@@ -31,6 +31,12 @@ import public Language.Reflection.Errors

3131%access public

3232%default total

3333

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+

3440-- Show and instances

3541

3642class Show a where

libs/prelude/Prelude/Nat.idr+14

@@ -99,6 +99,9 @@ data LTE : (n, m : Nat) -> Type where

9999 ||| If n <= m, then n + 1 <= m + 1

100100 LTESucc : LTE left right -> LTE (S left) (S right)

101101

102+instance Uninhabited (LTE (S n) Z) where

103+ uninhabited LTEZero impossible

104+

102105||| Greater than or equal to

103106total GTE : Nat -> Nat -> Type

104107GTE left right = LTE right left

@@ -127,6 +130,17 @@ isLTE (S k) (S j) with (isLTE k j)

127130 isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)

128131 isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

129132

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+

130144||| Boolean test than one Nat is less than or equal to another

131145total lte : Nat -> Nat -> Bool

132146lte Z right = True

rts/Makefile+2−2

@@ -1,10 +1,10 @@

11include ../config.mk

33OBJS = 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

55HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

66 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

88CFLAGS:=-fPIC $(CFLAGS)

99CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\""

1010CFLAGS += -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 $ */

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

44#include "idris_gc.h"

55#include "idris_utf8.h"

66#include "idris_bitstring.h"

7+#include "getline.h"

89#ifdef HAS_PTHREAD

910static pthread_key_t vm_key;

@@ -499,51 +500,18 @@ VAL idris_strlen(VM* vm, VAL l) {

499500 return MKINT((i_int)(idris_utf8_strlen(GETSTR(l))));

500501}

501502

502−#define BUFSIZE 256

503−

504503VAL idris_readStr(VM* vm, FILE* h) {

505−// Modified from 'safe-fgets.c' in the gdb distribution.

506−// (see http://www.gnu.org/software/gdb/current/)

507− char *line_ptr;

508− char* line_buf = (char *) malloc (BUFSIZE);

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;

504+ char *buffer = NULL;

505+ size_t n = 0;

506+ ssize_t len;

507+ len = getline(&buffer, &n, h);

538508

539− if (fgets (line_buf + line_buf_size - BUFSIZE - 1, BUFSIZE + 1, h) == 0)

540− return MKSTR(vm, "");

509+ if (len <= 0) {

510+ return MKSTR(vm, "");

511+ } else {

512+ return MKSTR(vm, buffer);

541513 }

542−

543− VAL str = MKSTR(vm, line_buf);

544−// printf("DBG: %s\n", line_buf);

545− free(line_buf);

546− return str;

514+ free(buffer);

547515}

548516

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

529529doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

530530doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

531531

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+

532539-- String functions which need to know we're UTF8

533540doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

534541doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

@@ -548,14 +555,6 @@ doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

548555doOp v LNoOp args = v ++ creg (last args)

549556

550557-- 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−

559558doOp v (LExternal rf) [_,x]

560559 | rf == sUN "prim__readFile"

561560 = 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'

679679 jsOP'

680680 | LNoOp <- op = translateReg (last args)

681681

682− | (LExternal ws) <- op,

683− ws == sUN "prim__writeString",

682+ | LWriteStr <- op,

684683 (_:str:_) <- args = JSAssign (translateReg reg)

685684 (JSApp (JSIdent "i$putStr") [translateReg str])

686685

src/IRTS/Lang.hs+1

@@ -75,6 +75,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

7575 | LFSqrt | LFFloor | LFCeil | LFNegate

7676

78+ | LReadStr | LWriteStr

7879

7980 -- system info

8081 | LSystemInfo

src/Idris/AbsSyntax.hs+17

@@ -385,6 +385,23 @@ addClass n i

385385 _ -> i

386386 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

387387

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+

388405addIBC :: IBCWrite -> Idris ()

389406addIBC ibc@(IBCDef n)

390407 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+6

@@ -18,6 +18,8 @@ import Idris.Colours

1818import System.Console.Haskeline

1919import System.IO

2020

21+import Prelude hiding ((<$>))

22+

2123import Control.Applicative ((<|>))

2224

2325import Control.Monad.Trans.State.Strict

@@ -179,6 +181,7 @@ data IState = IState {

179181 idris_tyinfodata :: Ctxt TIData,

180182 idris_fninfo :: Ctxt FnInfo,

181183 idris_transforms :: Ctxt [(Term, Term)],

184+ idris_autohints :: Ctxt [Name],

182185 idris_totcheck :: [(FC, Name)], -- names to check totality on

183186 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

184187 idris_totcheckfail :: [(FC, String)],

@@ -307,6 +310,7 @@ data IBCWrite = IBCFix FixDecl

307310 | IBCModDocs Name -- ^ The name is the special name used to track module docs

308311 | IBCUsage (Name, Int)

309312 | IBCExport Name

313+ | IBCAutoHint Name Name

310314 deriving Show

311315

312316-- | The initial state for the compiler

@@ -316,6 +320,7 @@ idrisInit = IState initContext S.empty []

316320 emptyContext emptyContext emptyContext emptyContext

317321 emptyContext emptyContext emptyContext emptyContext

318322 emptyContext emptyContext emptyContext emptyContext

323+ emptyContext

319324 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

320325 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

321326 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

@@ -560,6 +565,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

560565 | Reflection -- a reflecting function, compile-time only

561566 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

562567 | Constructor -- Data constructor type

568+ | AutoHint -- use in auto implicit search

563569 deriving (Show, Eq)

564570{-!

565571deriving 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

286286 -- block reduction immediately under codata (and not forced)

287287 ev ntimes stk top env

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

290290 = do let (f, _) = unApply arg

291291 let ntimes' = case f of

292292 P _ fn _ -> (fn, 0) : ntimes

@@ -576,8 +576,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where

576576 | x `elem` holes || y `elem` holes = return True

577577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

578578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

580− ceq ps (Bind n (Lam t) (App x (V 0))) y = 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)

581+ ceq ps (Bind n (Lam t) (App x (V 0))) y

582+ = ceq ps (substV (P Bound n t) x) y

581583 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

582584 | n == n' = ceq ps x y

583585 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')

707707recoverable f (Bind _ (Pi _ _ _) sc)

708708 | (P (DCon _ _ _) _ _, _) <- unApply f = False

709709 | (P (TCon _ _) _ _, _) <- unApply f = False

710+ | (Constant _) <- f = False

710711recoverable (Bind _ (Pi _ _ _) sc) f

711712 | (P (DCon _ _ _) _ _, _) <- unApply f = False

712713 | (P (TCon _ _) _ _, _) <- unApply f = False

714+ | (Constant _) <- f = False

713715recoverable (Bind _ (Lam _) sc) f = recoverable sc f

714716recoverable f (Bind _ (Lam _) sc) = recoverable f sc

715717recoverable x y = True

src/Idris/DeepSeq.hs+1

@@ -119,6 +119,7 @@ instance NFData FnOpt where

119119 rnf Reflection = ()

120120 rnf (Specialise x1) = rnf x1 `seq` ()

121121 rnf Constructor = ()

122+ rnf AutoHint = ()

122123

123124instance NFData DataOpt where

124125 rnf Codata = ()

src/Idris/Delaborate.hs+2

@@ -13,6 +13,8 @@ import Idris.Core.Evaluate

1313import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

1414import Idris.ErrReverse

1515

16+import Prelude hiding ((<$>))

17+

1618import Data.List (intersperse, nub)

1719import qualified Data.Text as T

1820import Control.Monad.State

src/Idris/Docs.hs+2

@@ -11,6 +11,8 @@ import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, rende

1111

1212import Util.Pretty

1313

14+import Prelude hiding ((<$>))

15+

1416import Control.Arrow (first)

1517

1618import Data.Maybe

src/Idris/Docstrings.hs+2

@@ -15,6 +15,8 @@ import Util.Pretty

1515

1616import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term, Err)

1717

18+import Prelude hiding ((<$>))

19+

1820import qualified Data.Text as T

1921import qualified Data.Foldable as F

2022import 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

702702 (crhs, crhsty) <- if not inf

703703 then recheckC_borrowing True borrowed fc id [] rhs'

704704 else return (rhs', clhsty)

705− logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

705+ logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

706706 ctxt <- getContext

707707 let constv = next_tvar ctxt

708708 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

9090 PApp _ _ args -> getWParams (map getTm args)

9191 a@(PRef fc f) -> getWParams [a]

9292 _ -> return []) ps

93− let pnames = map pname (concat (nub wparams))

93+ ist <- getIState

94+ let pnames = nub $ map pname (concat (nub wparams)) ++

95+ concatMap (namesIn [] ist) ps

9496 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

9597 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances

9698 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

119121 show (concat (nub wparams))

120122

121123 -- Bring variables in instance head into scope

122− ist <- getIState

123124 let headVars = nub $ mapMaybe (\p -> case p of

124125 PRef _ n ->

125126 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

146146 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

147147 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

148148

149− let (t, _) = unApply (getRetTy nty')

150− let corec = case t of

149+ let (fam, _) = unApply (getRetTy nty')

150+ let corec = case fam of

151151 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

152152 [TI _ True _ _ _] -> True

153153 _ -> False

@@ -157,7 +157,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

157157 let usety = if norm then nty' else nty

158158 ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

159159 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

161161 addDeferred ds'

162162 setFlags n opts'

163163 checkDocs fc argDocs ty

@@ -171,6 +171,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

171171 addIBC (IBCOpt n)

172172 when (Implicit `elem` opts') $ do addCoercion n

173173 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"

174179

175180 -- If the function is declared as an error handler and the language

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

289289 --trace ("ELAB " ++ show t') $

290290 let fc = fileFC "Force"

291291 env <- get_env

292− handleError (forceErr env)

292+ handleError (forceErr t' env)

293293 (elab' ina fc' t')

294294 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

295295 [pimp (sUN "t") Placeholder True,

296296 pimp (sUN "a") Placeholder True,

297297 pexp ct])) True

298298

299− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

299+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

300300 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

301− ht == txt "Lazy'" = True

302− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

301+ ht == txt "Lazy'" = notDelay orig

302+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

303303 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

304− ht == txt "Lazy'" = True

305− forceErr env (InfiniteUnify _ t _)

304+ ht == txt "Lazy'" = notDelay orig

305+ forceErr orig env (InfiniteUnify _ t _)

306306 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

307− ht == txt "Lazy'" = True

308− forceErr env (Elaborating _ _ t) = forceErr env t

309− forceErr env (ElaboratingArg _ _ _ t) = forceErr env t

310− forceErr env (At _ t) = forceErr env t

311− forceErr env t = False

307+ ht == txt "Lazy'" = notDelay orig

308+ forceErr orig env (Elaborating _ _ t) = forceErr orig env t

309+ forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

310+ forceErr orig env (At _ t) = forceErr orig env t

311+ forceErr orig env t = False

312+

313+ notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

314+ notDelay _ = True

312315

313316 local f = do e <- get_env

314317 return (f `elem` map fst e)

@@ -498,6 +501,7 @@ elab ist info emode opts fn tm

498501 if null a'

499502 then erun fc $ do apply (Var n) []; solve

500503 else elab' ina fc' (PApp fc tm [])

504+ elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

501505 elab' ina _ (PLam fc n Placeholder sc)

502506 = do -- if n is a type constructor name, this makes no sense...

503507 ctxt <- get_context

src/Idris/IBC.hs+15−5

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 103

40+ibcVersion = 104

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

@@ -82,7 +82,8 @@ data IBCFile = IBCFile { ver :: Word8,

8282 ibc_externs :: ![(Name, Int)],

8383 ibc_parsedSpan :: !(Maybe FC),

8484 ibc_usage :: ![(Name, Int)],

85− ibc_exports :: ![Name]

85+ ibc_exports :: ![Name],

86+ ibc_autohints :: ![(Name, Name)]

8687 }

8788 deriving Show

8889{-!

@@ -90,7 +91,7 @@ deriving instance Binary IBCFile

9091!-}

9192

9293initIBC :: IBCFile

93−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

94+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

9495

9596loadIBC :: Bool -- ^ True = reexport, False = make everything private

9697 -> FilePath -> Idris ()

@@ -237,6 +238,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

237238 _ -> ifail "IBC write failed"

238239ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

239240ibc 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 }

240242

241243process :: Bool -- ^ Reexporting

242244 -> IBCFile -> FilePath -> Idris ()

@@ -296,6 +298,7 @@ process reexp i fn

296298 pParsedSpan $ force (ibc_parsedSpan i)

297299 pUsage $ force (ibc_usage i)

298300 pExports $ force (ibc_exports i)

301+ pAutoHints $ force (ibc_autohints i)

299302

300303timestampOlder :: FilePath -> FilePath -> Idris ()

301304timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -326,6 +329,9 @@ pExports :: [Name] -> Idris ()

326329pExports ns = do ist <- getIState

327330 putIState ist { idris_exports = ns ++ idris_exports ist }

328331

332+pAutoHints :: [(Name, Name)] -> Idris ()

333+pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns

334+

329335pImportDirs :: [FilePath] -> Idris ()

330336pImportDirs fs = mapM_ addImportDir fs

331337

@@ -942,7 +948,7 @@ instance Binary MetaInformation where

942948 _ -> error "Corrupted binary data for MetaInformation"

943949

944950instance 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)

946952 = {-# SCC "putIBCFile" #-}

947953 do put x1

948954 put x2

@@ -988,6 +994,7 @@ instance Binary IBCFile where

988994 put x42

989995 put x43

990996 put x44

997+ put x45

991998

992999 get

9931000 = do x1 <- get

@@ -1035,7 +1042,8 @@ instance Binary IBCFile where

10351042 x42 <- get

10361043 x43 <- get

10371044 x44 <- 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)

1045+ x45 <- get

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)

10391047 else return (initIBC { ver = x1 })

10401048

10411049instance Binary DataOpt where

@@ -1072,6 +1080,7 @@ instance Binary FnOpt where

10721080 Constructor -> putWord8 13

10731081 CExport x1 -> do putWord8 14

10741082 put x1

1083+ AutoHint -> putWord8 15

10751084 get

10761085 = do i <- getWord8

10771086 case i of

@@ -1092,6 +1101,7 @@ instance Binary FnOpt where

10921101 13 -> return Constructor

10931102 14 -> do x1 <- get

10941103 return $ CExport x1

1104+ 15 -> return AutoHint

10951105 _ -> error "Corrupted binary data for FnOpt"

10961106

10971107instance Binary Fixity where

src/Idris/Output.hs+3−1

@@ -15,10 +15,12 @@ import Util.ScreenSize (getScreenWidth)

1515

1616import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

1717

18−import System.Console.Haskeline.MonadException

18+import System.Console.Haskeline.MonadException

1919 (MonadException (controlIO), RunIO (RunIO))

2020import System.IO (stdout, Handle, hPutStrLn)

2121

22+import Prelude hiding ((<$>))

23+

2224import Data.Char (isAlpha)

2325import Data.List (nub, intersperse)

2426import Data.Maybe (fromMaybe)

src/Idris/ParseExpr.hs+31−16

@@ -234,6 +234,14 @@ internalExpr syn =

234234 <|> app syn

235235 <?> "expression"

236236

237+{- | Parses the "impossible" keyword

238+@

239+Impossible ::= 'impossible'

240+@

241+-}

242+impossible :: IdrisParser PTerm

243+impossible = PImpossible <$ reserved "impossible"

244+

237245{- | Parses a case expression

238246@

239247CaseExpr ::=

@@ -250,13 +258,13 @@ caseExpr syn = do reserved "case"; fc <- getFC

250258{- | Parses a case in a case expression

251259@

252260CaseOption ::=

253− Expr '=>' Expr Terminator

261+ Expr (Impossible | '=>' Expr) Terminator

254262 ;

255263@

256264-}

257265caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

258266caseOption syn = do lhs <- expr (syn { inPattern = True })

259− symbol "=>"; r <- expr syn

267+ r <- impossible <|> symbol "=>" *> expr syn

260268 return (lhs, r)

261269 <?> "case option"

262270

@@ -732,8 +740,8 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu

732740{- | Parses a lambda expression

733741@

734742Lambda ::=

735− '\\' TypeOptDeclList '=>' Expr

736− | '\\' SimpleExprList '=>' Expr

743+ '\\' TypeOptDeclList LambdaTail

744+ | '\\' SimpleExprList LambdaTail

737745 ;

738746@

739747@

@@ -742,27 +750,34 @@ SimpleExprList ::=

742750 | SimpleExpr ',' SimpleExprList

743751 ;

744752@

753+@

754+LambdaTail ::=

755+ Impossible

756+ | '=>' Expr

757+@

745758-}

746759lambda :: SyntaxInfo -> IdrisParser PTerm

747760lambda syn = do lchar '\\' <?> "lambda expression"

748− (do xt <- try $ tyOptDeclList syn

749− fc <- getFC

750− symbol "=>"

751− sc <- expr syn

752− return (bindList (PLam fc) xt sc)) <|> do

753− ps <- sepBy (do fc <- getFC

754− e <- simpleExpr (syn { inPattern = True })

755− return (fc, e)) (lchar ',')

756− symbol "=>"

757− sc <- expr syn

758− return (pmList (zip [0..] ps) sc)

759− <?> "lambda expression"

761+ ((do xt <- try $ tyOptDeclList syn

762+ fc <- getFC

763+ sc <- lambdaTail

764+ return (bindList (PLam fc) xt sc))

765+ <|>

766+ (do ps <- sepBy (do fc <- getFC

767+ e <- simpleExpr (syn { inPattern = True })

768+ return (fc, e))

769+ (lchar ',')

770+ sc <- lambdaTail

771+ return (pmList (zip [0..] ps) sc)))

772+ <?> "lambda expression"

760773 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

761774 pmList [] sc = sc

762775 pmList ((i, (fc, x)) : xs) sc

763776 = PLam fc (sMN i "lamp") Placeholder

764777 (PCase fc (PRef fc (sMN i "lamp"))

765778 [(x, pmList xs sc)])

779+ lambdaTail :: IdrisParser PTerm

780+ lambdaTail = impossible <|> symbol "=>" *> expr syn

766781

767782{- | Parses a term rewrite expression

768783@

src/Idris/Parser.hs+4−2

@@ -479,6 +479,8 @@ fnOpts opts

479479 fnOpts (ErrorReverse : opts)

480480 <|> do try (lchar '%' *> reserved "reflection");

481481 fnOpts (Reflection : opts)

482+ <|> do try (lchar '%' *> reserved "hint");

483+ fnOpts (AutoHint : opts)

482484 <|> do lchar '%'; reserved "specialise";

483485 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

484486 fnOpts (Specialise ns : opts)

@@ -813,7 +815,7 @@ argExpr syn = let syn' = syn { inPattern = True } in

813815@

814816RHS ::= '=' Expr

815817 | '?=' RHSName? Expr

816− | 'impossible'

818+ | Impossible

817819 ;

818820@

819821

@@ -829,7 +831,7 @@ rhs syn n = do lchar '='; expr syn

829831 return n)

830832 r <- expr syn

831833 return (addLet fc name r)

832− <|> do reserved "impossible"; return PImpossible

834+ <|> impossible

833835 <?> "function right hand side"

834836 where mkN :: Name -> Name

835837 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))

src/Idris/Primitives.hs+4−23

@@ -166,29 +166,10 @@ primitives =

166166 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

167167 (1, LStrRev) total,

168168

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)

174−-- (1, LReadStr) total, -- total is okay, because we have 'WorldType'

175−-- Prim (sUN "prim__writeString") (ty [WorldType,StrType] (AType (ATInt ITNative))) 2 (p_cantreduce)

176−-- (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,

169+ Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

170+ (1, LReadStr) total, -- total is okay, because we have 'WorldType'

171+ Prim (sUN "prim__writeString") (ty [WorldType,StrType] (AType (ATInt ITNative))) 2 (p_cantreduce)

172+ (2, LWriteStr) total,

192173 Prim (sUN "prim__systemInfo") (ty [AType (ATInt ITNative)] StrType) 1 (p_cantreduce)

193174 (1, LSystemInfo) total

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

9191 if ambigok || argsok then

9292 case lookupCtxt nroot (idris_tyinfodata ist) of

9393 [TISolution ts] -> findInferredTy ts

94− _ -> psRec rec maxDepth

94+ _ -> psRec rec maxDepth []

9595 else autoArg (sUN "auto") -- not enough info in the type yet

9696 where

9797 findInferredTy (t : _) = elab (delab ist (toUN t))

@@ -99,10 +99,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

9999 conArgsOK ty

100100 = let (f, as) = unApply ty in

101101 case f of

102− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

103− [t] -> do rs <- mapM (conReady as) (con_names t)

104− return (and rs)

105− _ -> fail "Ambiguous name"

102+ P _ n _ -> case lookupCtxtExact n (idris_datatypes ist) of

103+ Just t -> do rs <- mapM (conReady as) (con_names t)

104+ return (and rs)

105+ Nothing -> -- local variable, go for it

106+ return True

106107 TType _ -> return True

107108 _ -> fail "Not a data type"

108109

@@ -129,12 +130,17 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

129130 toUN (App f a) = App (toUN f) (toUN a)

130131 toUN t = t

131132

132− psRec _ 0 | fromProver = cantSolveGoal

133− psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"

134− psRec False d = tryCons d hints

135− psRec True d = do compute

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...)

137+ psRec _ 0 locs | fromProver = cantSolveGoal

138+ psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"

139+ psRec False d locs = tryCons d locs hints

140+ psRec True d locs

141+ = do compute

136142 try' (trivial elab ist)

137− (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

143+ (try' (try' (resolveByCon (d - 1) locs) (resolveByLocals (d - 1) locs)

138144 True)

139145 -- if all else fails, make a new metavariable

140146 (if fromProver

@@ -145,42 +151,50 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

145151 getFn d (Just f) | d < maxDepth-1 = [f]

146152 | otherwise = []

147153

148− resolveByCon d

154+ resolveByCon d locs

149155 = do t <- goal

150156 let (f, _) = unApply t

151157 case f of

152− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

153− [t] -> tryCons d (hints ++ con_names t ++

154− getFn d fn)

155− _ -> fail "Not a data type"

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

164+ con_names t ++

165+ autohints ++

166+ getFn d fn)

167+ Nothing -> fail "Not a data type"

156168 _ -> fail "Not a data type"

157169

158170 -- if there are local variables which have a function type, try

159171 -- applying them too

160− resolveByLocals d

172+ resolveByLocals d locs

161173 = do env <- get_env

162− tryLocals d env

174+ tryLocals d locs env

163175

164− tryLocals d [] = fail "Locals failed"

165− tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True

176+ tryLocals d locs [] = fail "Locals failed"

177+ tryLocals d locs ((x, t) : xs)

178+ | x `elem` locs = tryLocals d locs xs

179+ | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True

166180

167− tryCons d [] = fail "Constructors failed"

168− tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True

181+ tryCons d locs [] = fail "Constructors failed"

182+ tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True

169183

170− tryLocal d n t = do let a = getPArity (delab ist (binderTy t))

171− tryLocalArg d n a

184+ tryLocal d locs n t

185+ = do let a = getPArity (delab ist (binderTy t))

186+ tryLocalArg d locs n a

172187

173− tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)

174− tryLocalArg d n i = simple_app False (tryLocalArg d n (i - 1))

175− (psRec True d) "proof search local apply"

188+ tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)

189+ tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))

190+ (psRec True d locs) "proof search local apply"

176191

177192 -- Like type class resolution, but searching with constructors

178− tryCon d n =

193+ tryCon d locs n =

179194 do ty <- goal

180− let imps = case lookupCtxtName n (idris_implicits ist) of

181− [] -> []

182− [args] -> map isImp (snd args)

183− _ -> fail "Ambiguous name"

195+ let imps = case lookupCtxtExact n (idris_implicits ist) of

196+ Nothing -> []

197+ Just args -> map isImp args

184198 ps <- get_probs

185199 hs <- get_holes

186200 args <- map snd <$> try' (apply (Var n) imps)

@@ -190,7 +204,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

190204 when (length ps < length ps') $ fail "Can't apply constructor"

191205 mapM_ (\ (_, h) -> do focus h

192206 aty <- goal

193− psRec True d)

207+ psRec True d locs)

194208 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

195209 solve

196210

src/Idris/REPL.hs+1−1

@@ -59,7 +59,7 @@ import IRTS.System

5959

6060import Control.Category

6161import qualified Control.Exception as X

62−import Prelude hiding ((.), id)

62+import Prelude hiding ((<$>), (.), id)

6363import Data.List.Split (splitOn)

6464import Data.List (groupBy)

6565import qualified Data.Text as T

test/proof009/run+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−idris $@ --quiet proof009.idr < input

2+idris $@ --consolewidth 70 --quiet proof009.idr < input

33rm -f *.ibc

test/proof010/expectednew file+6

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

1+2, << function >>

2+3, << function >>

4+some bools

5+some bools

test/proof010/proof010.idrnew file+39

@@ -0,0 +1,39 @@

1+data MyShow : Type -> Type where

2+ ShowInstance : (show : a -> String) -> MyShow a

4+myshow : {auto inst : MyShow a} -> a -> String

5+myshow {inst = ShowInstance show} x1 = show x1

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

3+%default total

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

4+data Nool : Bool -> Type where

5+ Flase : Nool False

6+ Ture : Nool True

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