packages feed

idris 0.99.2 → 1.0

raw patch · 72 files changed

+854/−738 lines, 72 filesdep ~aesondep ~vectorPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: aeson, vector

API changes (from Hackage documentation)

Files

CHANGELOG.md view
@@ -1,3 +1,7 @@+# New in 1.0+++ It's about time+ # New in 0.99.2  ## Library Updates
CONTRIBUTORS view
@@ -171,7 +171,7 @@ Philip Rasmussen PoroCYon raichoo-Reynir Reynisson+Reynir Björnsson Ricky Elrod Robert Clipsham Robert Edström
INSTALL.md view
@@ -92,6 +92,17 @@  * `stack build --nix` +### before rebuilding new pulls+the default build will currently just reuse `.ibc` files which can result+in build-failures in the `Building libraries...` phase.++A safer way to do this is therefore to recursively delete all the `*.ibc`+files from the `libs/` folder.++On Linux(or similar) you can do this with++    find . -name "*.ibc" -exec rm -rf {} \;+ ### System GHC  The flag `--system-ghc` can be added to enforce use of your system's@@ -111,4 +122,4 @@  ``` PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig stack build-```+```
docs/conf.py view
@@ -59,9 +59,9 @@ # built documents. # # The short X.Y version.-version = '0.99.2'+version = '1.0' # The full version, including alpha/beta/rc tags.-release = '0.99.2'+release = '1.0'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.
docs/listing/idris-prompt-helloworld.txt view
@@ -1,7 +1,7 @@ $ idris hello.idr      ____    __     _     /  _/___/ /____(_)____-    / // __  / ___/ / ___/     Version 0.99.2+    / // __  / ___/ / ___/     Version 1.0   _/ // /_/ / /  / (__  )      http://www.idris-lang.org/  /___/\__,_/_/  /_/____/       Type :? for help
docs/listing/idris-prompt-interp.txt view
@@ -1,7 +1,7 @@ $ idris interp.idr      ____    __     _     /  _/___/ /____(_)____-    / // __  / ___/ / ___/     Version 0.99.2+    / // __  / ___/ / ___/     Version 1.0   _/ // /_/ / /  / (__  )      http://www.idris-lang.org/  /___/\__,_/_/  /_/____/       Type :? for help
docs/listing/idris-prompt-start.txt view
@@ -1,7 +1,7 @@ $ idris     ____    __     _    /  _/___/ /____(_)____-   / // __  / ___/ / ___/     Version 0.99.2+   / // __  / ___/ / ___/     Version 1.0  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/ /___/\__,_/_/  /_/____/       Type :? for help
docs/tutorial/index.rst view
@@ -4,7 +4,10 @@ The Idris Tutorial ################## -This is the Idris Tutorial. It will teach you about programming in the Idris Language.+This is the Idris Tutorial. +It provides a brief introduction to programming in the Idris Language.+It covers the core language features, and assumes some familiarity with an+existing functional programming language such as Haskell or OCaml.  .. note::    The documentation for Idris has been published under the Creative@@ -27,7 +30,6 @@    interp    views    theorems-   provisional    interactive    syntax    miscellany
docs/tutorial/interfaces.rst view
@@ -253,9 +253,9 @@  :: -    *ifaces> m_add (Just 20) (Just 22)+    *Interfaces> m_add (Just 20) (Just 22)     Just 42 : Maybe Int-    *ifaces> m_add (Just 20) Nothing+    *Interfaces> m_add (Just 20) Nothing     Nothing : Maybe Int  Pattern Matching Bind@@ -565,6 +565,49 @@     *named_impl> show (sort @{myord} testList)     "[ssssO, sssO, sO]" : String ++Sometimes, we also need access to a named parent implementation. For example,+the prelude defines the following ``Semigroup`` interface:++.. code-block:: idris++    interface Semigroup ty where+      (<+>) : ty -> ty -> ty++Then it defines ``Monoid``, which extends ``Semigroup`` with a "neutral"+value:++.. code-block:: idris++    interface Semigroup ty => Monoid ty where+      neutral : ty++We can define two different implementations of ``Semigroup`` and+``Monoid`` for ``Nat``, one based on addition and one on multiplication:++.. code-block:: idris++    [PlusNatSemi] Semigroup Nat where+      (<+>) x y = x + y++    [MultNatSemi] Semigroup Nat where+      (<+>) x y = x * y++The neutral value for addition is ``0``, but the neutral value for multiplication+is ``1``. It's important, therefore, that when we define implementations+of ``Monoid`` they extend the correct ``Semigroup`` implementation. We can+do this with a ``using`` clause in the implementation as follows:++.. code-block:: idris++    [PlusNatMonoid] Monoid Nat using PlusNatSemi where+      neutral = 0++    [MultNatMonoid] Monoid Nat using MultNatSemi where+      neutral = 1++The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should+extend ``PlusNatSemi`` specifically.  Determining Parameters ======================
docs/tutorial/introduction.rst view
@@ -55,6 +55,11 @@ briefly. The reader is also assumed to have some interest in using dependent types for writing and verifying systems software. +For a more in-depth introduction to Idris, which proceeds at a much slower+pace, covering interactive program development, with many more examples, see+`Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_+by Edwin Brady, available from `Manning <https://www.manning.com>`_.+ Example Code ============
docs/tutorial/miscellany.rst view
@@ -67,16 +67,6 @@      head xs {p = ?headProof} -More generally, we can fill in implicit arguments with a default value-by annotating them with ``default``. The definition above is equivalent-to:--.. code-block:: idris--    head : (xs : List a) ->-           {default proof { trivial; } p : isCons xs = True} -> a-    head (x :: xs) = x- Implicit conversions ====================
docs/tutorial/modules.rst view
@@ -16,22 +16,28 @@      module Btree +    public export     data BTree a = Leaf                  | Node (BTree a) a (BTree a) +    export     insert : Ord a => a -> BTree a -> BTree a     insert x Leaf = Node Leaf x Leaf     insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)                                        else (Node l v (insert x r)) +    export     toList : BTree a -> List a     toList Leaf = []     toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r) +    export     toTree : Ord a => List a -> BTree a     toTree [] = Leaf     toTree (x :: xs) = insert x (toTree xs) +The modifiers ``export`` and ``public export`` say which names are visible+from other modules. These are explained further below.  Then, this gives a main program (in a file ``bmain.idr``) which uses the ``Btree`` module to sort a list:@@ -46,11 +52,9 @@     main = do let t = toTree [1,8,2,7,9,3]               print (Btree.toList t) ---The same names can be defined in multiple modules. This is possible-because in practice names are *qualified* with the name of the module.-The names defined in the ``Btree`` module are, in full:+The same names can be defined in multiple modules: names are *qualified* with+the name of the module.  The names defined in the ``Btree`` module are, in+full:  + ``Btree.BTree`` + ``Btree.Leaf``@@ -115,6 +119,10 @@    the module. Otherwise, Idris won't know what the synonym is a    synonym for. +Since ``public export`` means that a function's definition is exported,+this effectively makes the function definition part of the module's API.+Therefore, it's generally a good idea to avoid using ``public export`` for+functions unless you really mean to export the full definition.  Meaning for Data Types ----------------------@@ -136,41 +144,10 @@ - ``public export`` the interface name, method names and default   definitions are exported ---``BTree`` Revisited-+++++++++++++++++++--For our ``BTree`` module, it makes sense for the tree data type and the-functions to be exported as ``export``, as we see below:--.. code-block:: idris--    module BTree--    export data BTree a = Leaf-                        | Node (BTree a) a (BTree a)--    export-    insert : Ord a => a -> BTree a -> BTree a-    insert x Leaf = Node Leaf x Leaf-    insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)-                                       else (Node l v (insert x r))--    export-    toList : BTree a -> List a-    toList Leaf = []-    toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)--    export-    toTree : Ord a => List a -> BTree a-    toTree [] = Leaf-    toTree (x :: xs) = insert x (toTree xs)- ``%access`` Directive ---------------------- -Finally, the default export mode can be changed with the ``%access``+The default export mode can be changed with the ``%access`` directive, for example:  .. code-block:: idris@@ -179,8 +156,9 @@      %access export +    public export     data BTree a = Leaf-                          | Node (BTree a) a (BTree a)+                 | Node (BTree a) a (BTree a)      insert : Ord a => a -> BTree a -> BTree a     insert x Leaf = Node Leaf x Leaf@@ -237,14 +215,14 @@       test x = x ++ x  This (admittedly contrived) module defines two functions with fully-qualified names ``foo.x.test`` and ``foo.y.test``, which can be+qualified names ``Foo.x.test`` and ``Foo.y.test``, which can be disambiguated by their types:  :: -    *foo> test 3+    *Foo> test 3     6 : Int-    *foo> test "foo"+    *Foo> test "foo"     "foofoo" : String  Parameterised blocks@@ -301,22 +279,3 @@     "[1, 2, 3, 4, 5, 6]" : String  -Modules Dependencies Using Atom -===============================--If you are using the Atom editor and have a dependency on another package, -corresponding to for instance ``import Lightyear`` or ``import Pruviloj``, -you need to let Atom know that it should be loaded. The easiest way to -accomplish that is with a .ipkg file. The general contents of an ipkg file -will be described in the next section of the tutorial, but for now here is -a simple recipe for this trivial case. --- Create a folder myProject. --- Add a file myProject.ipkg containing just a couple of lines: --``package myProject`` --``pkgs = pruviloj, lightyear`` --- In Atom, use the File menu to Open Folder myProject.
docs/tutorial/packages.rst view
@@ -146,6 +146,26 @@ Note how both tests have reported success by printing ``Test Passed`` as we arranged for with the ``assertEq`` and ``assertNoEq`` functions. +Package Dependencies Using Atom +===============================++If you are using the Atom editor and have a dependency on another package, +corresponding to for instance ``import Lightyear`` or ``import Pruviloj``, +you need to let Atom know that it should be loaded. The easiest way to +accomplish that is with a .ipkg file. The general contents of an ipkg file +will be described in the next section of the tutorial, but for now here is +a simple recipe for this trivial case. ++- Create a folder myProject. ++- Add a file myProject.ipkg containing just a couple of lines: ++``package myProject`` ++``pkgs = pruviloj, lightyear`` ++- In Atom, use the File menu to Open Folder myProject. + More information ================
docs/tutorial/starting.rst view
@@ -10,7 +10,8 @@ Before installing Idris, you will need to make sure you have all of the necessary libraries and tools. You will need: -- A fairly recent Haskell platform. Version ``2013.2.0.0`` should be sufficiently recent, though it is better to be completely up to date.+- A fairly recent version of `GHC <https://www.haskell.org/ghc/>`_. The+  earliest version we currently test with is 7.6.3.  - The *GNU Multiple Precision Arithmetic Library* (GMP) is available  from MacPorts/Homebrew and all major Linux distributions.
docs/tutorial/theorems.rst view
@@ -122,6 +122,145 @@ building proofs. For more details on building proofs interactively in an editor, see :ref:`proofs-index`. +.. _sect-parity:++Theorems in Practice+====================++The need to prove theorems can arise naturally in practice. For example,+previously (:ref:`sec-views`) we implemented ``natToBin`` using a function+``parity``:++.. code-block:: idris++    parity : (n:Nat) -> Parity n++However, we didn't provide a definition for ``parity``. We might expect it+to look something like the following:++.. code-block:: idris++    parity : (n:Nat) -> Parity n+    parity Z     = Even {n=Z}+    parity (S Z) = Odd {n=Z}+    parity (S (S k)) with (parity k)+      parity (S (S (j + j)))     | Even = Even {n=S j}+      parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}++Unfortunately, this fails with a type error:++::++    When checking right hand side of with block in views.parity with expected type+            Parity (S (S (j + j)))++    Type mismatch between+            Parity (S j + S j) (Type of Even)+    and+            Parity (S (S (plus j j))) (Expected type)++The problem is that normalising ``S j + S j``, in the type of ``Even``+doesn't result in what we need for the type of the right hand side of+``Parity``. We know that ``S (S (plus j j))`` is going to be equal to+``S j + S j``, but we need to explain it to Idris with a proof. We can+begin by adding some *holes* (see :ref:`sect-holes`) to the definition:++.. code-block:: idris++    parity : (n:Nat) -> Parity n+    parity Z     = Even {n=Z}+    parity (S Z) = Odd {n=Z}+    parity (S (S k)) with (parity k)+      parity (S (S (j + j)))     | Even = let result = Even {n=S j} in+                                              ?helpEven+      parity (S (S (S (j + j)))) | Odd  = let result = Odd {n=S j} in+                                              ?helpOdd++Checking the type of ``helpEven`` shows us what we need to prove for the+``Even`` case:++::++      j : Nat+      result : Parity (S (plus j (S j)))+    --------------------------------------+    helpEven : Parity (S (S (plus j j)))++We can therefore write a helper function to *rewrite* the type to the form+we need:++.. code-block:: idris++    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))+    helpEven j p = rewrite plusSuccRightSucc j j in p++The ``rewrite ... in`` syntax allows you to change the required type of an+expression by rewriting it according to an equality proof. Here, we have+used ``plusSuccRightSucc``, which has the following type:++.. code-block:: idris++    plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right++We can see the effect of ``rewrite`` by replacing the right hand side of+``helpEven`` with a hole, and working step by step. Beginning with the following:++.. code-block:: idris++    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))+    helpEven j p = ?helpEven_rhs++We can look at the type of ``helpEven_rhs``:++.. code-block:: idris++      j : Nat+      p : Parity (S (plus j (S j)))+    --------------------------------------+    helpEven_rhs : Parity (S (S (plus j j)))++Then we can ``rewrite`` by applying ``plusSuccRightSucc j j``, which gives+an equation ``S (j + j) = j + S j``, thus replacing ``S (j + j)`` (or,+in this case, ``S (plus j j)`` since ``S (j + j)`` reduces to that) in the+type with ``j + S j``:++.. code-block:: idris++    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))+    helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs++Checking the type of ``helpEven_rhs`` now shows what has happened, including+the type of the equation we just used (as the type of ``_rewrite_rule``):++.. code-block:: idris++      j : Nat+      p : Parity (S (plus j (S j)))+      _rewrite_rule : S (plus j j) = plus j (S j)+    --------------------------------------+    helpEven_rhs : Parity (S (plus j (S j)))++Using ``rewrite`` and another helper for the ``Odd`` case, we can complete+``parity`` as follows:++.. code-block:: idris++    helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))+    helpEven j p = rewrite plusSuccRightSucc j j in p++    helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))+    helpOdd j p = rewrite plusSuccRightSucc j j in p++    parity : (n:Nat) -> Parity n+    parity Z     = Even {n=Z}+    parity (S Z) = Odd {n=Z}+    parity (S (S k)) with (parity k)+      parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})+      parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})++Full details of ``rewrite`` are beyond the scope of this introductory tutorial,+but it is covered in the theorem proving tutorial (see :ref:`proofs-index`).+ .. _sect-totality:  Totality Checking@@ -151,10 +290,10 @@  :: -    *theorems> :total empty1+    *Theorems> :total empty1     possibly not total due to: empty1#hd         not total as there are missing cases-    *theorems> :total empty2+    *Theorems> :total empty2     possibly not total due to recursive path empty2  Note the use of the word “possibly” — a totality check can, of course,
docs/tutorial/typesfuns.rst view
@@ -250,17 +250,65 @@             d y = c (y + 1 + z y)                   where z w = y + w +.. _sect-holes: +Holes+-----++Idris programs can contain *holes* which stand for incomplete parts of+programs. For example, we could leave a hole for the greeting in our+"Hello world" program:++.. code-block:: idris++    main : IO ()+    main = putStrLn ?greeting++The syntax ``?greeting`` introduces a hole, which stands for a part of+a program which is not yet written. This is a valid Idris program, and you+can check the type of ``greeting``:++::++    *Hello> :t greeting+    --------------------------------------+    greeting : String++Checking the type of a hole also shows the types of any variables in scope.+For example, given an incomplete definition of ``even``:++.. code-block:: idris++    even : Nat -> Bool+    even Z = True+    even (S k) = ?even_rhs++We can check the type of ``even_rhs`` and see the expected return type,+and the type of the variable ``k``:++::++    *Even> :t even_rhs+      k : Nat+    --------------------------------------+    even_rhs : Bool++Holes are useful because they help us write functions *incrementally*.+Rather than writing an entire function in one go, we can leave some parts+unwritten and use Idris to tell us what is necessary to complete the+definition.+ Dependent Types =============== +.. _sect-fctypes:+ First Class Types ----------------- -In Idris, types are a first class language construct, meaning that they-can be computed and manipulated (and passed to functions) just like any-other language construct. For example, we could write a function which-computes a type:+In Idris, types are first class, meaning that they can be computed and+manipulated (and passed to functions) just like any other language construct.+For example, we could write a function which computes a type:  .. code-block:: idris @@ -350,21 +398,24 @@  :: -    $ idris vbroken.idr --check-    vbroken.idr:9:23:When elaborating right hand side of Vect.++:-    When elaborating an application of constructor Vect.:::-        Type mismatch between-                Vect (k + k) a (Type of xs ++ xs)-        and-                Vect (plus k m) a (Expected type)+    $ idris VBroken.idr --check+    VBroken.idr:9:23-25:+    When checking right hand side of Vect.++ with expected type+            Vect (S k + m) a -        Specifically:-                Type mismatch between-                        plus k k-                and-                        plus k m+    When checking an application of constructor Vect.:::+            Type mismatch between+                    Vect (k + k) a (Type of xs ++ xs)+            and+                    Vect (plus k m) a (Expected type) +            Specifically:+                    Type mismatch between+                            plus k k+                    and+                            plus k m + This error message suggests that there is a length mismatch between two vectors — we needed a vector of length ``k + m``, but provided a vector of length ``k + k``.@@ -656,9 +707,9 @@  .. code-block:: idris -    ifThenElse : Bool -> a -> a -> a;-    ifThenElse True  t e = t;-    ifThenElse False t e = e;+    ifThenElse : Bool -> a -> a -> a+    ifThenElse True  t e = t+    ifThenElse False t e = e  This function uses one of the ``t`` or ``e`` arguments, but not both (in fact, this is used to implement the ``if...then...else`` construct@@ -681,19 +732,19 @@  .. code-block:: idris -    ifThenElse : Bool -> Lazy a -> Lazy a -> a;-    ifThenElse True  t e = t;-    ifThenElse False t e = e;+    ifThenElse : Bool -> Lazy a -> Lazy a -> a+    ifThenElse True  t e = t+    ifThenElse False t e = e  Codata Types ============ -Codata types are like regular data types, except that they allow for us to-define infinite data structures.  More precisely, for a type ``T``, each of its-constructor arguments of type ``T`` are transformed into a coinductive parameter-``Inf T``. This makes each of the ``T`` arguments lazy, and allows infinite data-structures of type ``T`` to be built. One example of a codata type is Stream,-which is defined as follows.+Codata types allow us to define infinite data structures by marking recursive+arguments as potentially infinite. For+a codata type ``T``, each of its constructor arguments of type ``T`` are transformed+into an argument of type ``Inf T``. This makes each of the ``T`` arguments+lazy, and allows infinite data structures of type ``T`` to be built. One+example of a codata type is Stream, which is defined as follows.  .. code-block:: idris @@ -778,7 +829,8 @@ =================  Idris includes a number of useful data types and library functions-(see the ``libs/`` directory in the distribution). This chapter+(see the ``libs/`` directory in the distribution, and the+`documentation <https://www.idris-lang.org/documentation/>`_). This section describes a few of these. The functions described here are imported automatically by every Idris program, as part of ``Prelude.idr``. @@ -836,7 +888,7 @@  :: -    *usefultypes> show (map double intVec)+    *UsefulTypes> show (map double intVec)     "[2, 4, 6, 8, 10]" : String  For more details of the functions available on ``List`` and@@ -850,9 +902,7 @@  -  ``libs/base/Data/VectType.idr`` -Functions include filtering, appending, reversing, and so on. Also-remember that Idris is still in development, so if you don’t see-the function you need, please feel free to add it and submit a patch!+Functions include filtering, appending, reversing, and so on.   Aside: Anonymous functions and operator sections ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~@@ -862,7 +912,7 @@  :: -    *usefultypes> show (map (\x => x * 2) intVec)+    *UsefulTypes> show (map (\x => x * 2) intVec)     "[2, 4, 6, 8, 10]" : String  The notation ``\x => val`` constructs an anonymous function which takes@@ -874,7 +924,7 @@  :: -    *usefultypes> show (map (* 2) intVec)+    *UsefulTypes> show (map (* 2) intVec)     "[2, 4, 6, 8, 10]" : String  ``(*2)`` is shorthand for a function which multiplies a number@@ -938,19 +988,18 @@  :: -    *usefultypes> fst jim+    *UsefulTypes> fst jim     "Jim" : String-    *usefultypes> snd jim+    *UsefulTypes> snd jim     (25, "Cambridge") : (Int, String)-    *usefultypes> jim == ("Jim", (25, "Cambridge"))+    *UsefulTypes> jim == ("Jim", (25, "Cambridge"))     True : Bool  Dependent Pairs ---------------  Dependent pairs allow the type of the second element of a pair to depend-on the value of the first element. Traditionally, these are referred to-as “sigma types”:+on the value of the first element.   .. code-block:: idris @@ -1021,6 +1070,7 @@  We will see more on ``with`` notation later. +Dependent pairs are sometimes referred to as “sigma types”.  Records -------@@ -1052,11 +1102,11 @@  :: -    *record> firstName fred+    *Record> firstName fred     "Fred" : String-    *record> age fred+    *Record> age fred     30 : Int-    *record> :t firstName+    *Record> :t firstName     firstName : Person -> String  We can also use the field names to update a record (or, more@@ -1065,9 +1115,9 @@  .. code-block:: bash -    *record> record { firstName = "Jim" } fred+    *Record> record { firstName = "Jim" } fred     MkPerson "Jim" "Joe" "Bloggs" 30 : Person-    *record> record { firstName = "Jim", age $= (+ 1) } fred+    *Record> record { firstName = "Jim", age $= (+ 1) } fred     MkPerson "Jim" "Joe" "Bloggs" 31 : Person  The syntax ``record { field = val, ... }`` generates a function which@@ -1098,10 +1148,16 @@  :: -    *record> addStudent fred (ClassInfo [] "CS")+    *Record> addStudent fred (ClassInfo [] "CS")     ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class +We could also use ``$=`` to define ``addStudent`` more concisely: +.. code-block:: idris++    addStudent' : Person -> Class -> Class+    addStudent' p c = record { students $= (p ::) } c+ Nested record update ~~~~~~~~~~~~~~~~~~~~ @@ -1123,12 +1179,13 @@      record { a->b->c } x +The ``$=`` notation is also valid for nested record updates.  Dependent Records ----------------- -Records can also be dependent on values. Records *parameters*, which-are not subject to field updates. The parameters appear as arguments+Records can also be dependent on values. Records have *parameters*, which+cannot be updated like the other fields. The parameters appear as arguments to the resulting type, and are written following the record type name. For example, a pair type could be defined as follows: @@ -1140,10 +1197,9 @@         snd : b  -Using the class record from the original introduction to records.  The-size of the class can be restricted using a ``Vect`` and the size-promoted to the type level by parameterising the record with the size.-For example:+Using the ``class`` record from earlier, the size of the class can be+restricted using a ``Vect`` and the size included in the type by parameterising+the record with the size.  For example:   .. code-block:: idris@@ -1258,9 +1314,9 @@  :: -    *usefultypes> lookup_default 2 [3,4,5,6] (-1)+    *UsefulTypes> lookup_default 2 [3,4,5,6] (-1)     5 : Integer-    *usefultypes> lookup_default 4 [3,4,5,6] (-1)+    *UsefulTypes> lookup_default 4 [3,4,5,6] (-1)     -1 : Integer  **Restrictions:** The ``case`` construct is intended for simple@@ -1278,75 +1334,25 @@ Totality ======== -A *total* function is a function that terminates for all possible-inputs, or one that is guaranteed to produce some output before making-a recursive call. For example, Idris' ``head`` function is total for-all lists:--::--    Idris> :t Prelude.List.head-    head : (l : List a) -> {auto ok : NonEmpty l} -> a--The ``{auto ok : NonEmpty l}`` tells us that Idris won't compile if we-try to call ``head`` on an empty list. The implementation is as follows:--.. code-block:: idris--    ||| Get the first element of a non-empty list-    ||| @ ok proof that the list is non-empty-    head : (l : List a) -> {auto ok : NonEmpty l} -> a-    head []      {ok=IsNonEmpty} impossible-    head (x::xs) {ok=p}    = x--(Note that this implementation is in contrast to Haskell's ``head``,-which is  *not* total and will fail at runtime rather than compile time.)-The following Idris code will compile:--.. code-block:: idris--    module Main--    main : IO ()-    main = do-      let x : Integer = head [1,2,3]-      print x--And will print ``1``. However, the same code with ``head []`` won't compile:--::--    test.idr:5:26:When checking right hand side of main with expected type-        IO ()--    When checking argument ok to function Prelude.List.head:-          Can't find a value of type-                  NonEmpty []--We can't bind and print ``x`` because ``head []`` doesn't type check.--However, we might imagine a function, ``unsafeHead``, that is identical to-Idris' ``head`` function except that it is *not* total: it will error out-at runtime if called on an empty list. (This is similar to the behavior of-Haskell's ``head`` function.) ``unsafeHead`` might look like this:--.. code-block:: idris--    -- Unsafe head example!-    unsafeHead : List a -> a-    unsafeHead (x::xs) = x+Idris distinguishes between *total* and *partial* functions.+A total function is a function that either: -And although it typechecks and compiles, it will not reduce (that is, evaluation-of the function will cause it to change):++ Terminates for all possible inputs, or ++ Produces a non-empty, finite, prefix of a possibly infinite result -::+If a function is total, we can consider its type a precise description of what+that function will do. For example, if we have a function with a return+type of ``String`` we know something different, depending on whether or not+it's total: -    unsafe> the Integer $ unsafeHead [1, 2, 3]-    1 : Integer-    unsafe> the Integer $ unsafeHead []-    unsafeHead [] : Integer++ If it's total, it will return a value of type ``String`` in finite time++ If it's partial, then as long as it doesn't crash or enter an infinite loop,+  it will return a ``String``. -Functions that are not total are known as *partial functions*. As-mentioned in the note about ``mutual`` blocks, non-total definitions-aren't reduced when type checking because they are not well-defined-for all possible inputs.+Idris makes this distinction so that it knows which functions are safe to+evaluate while type checking (as we've seen with :ref:`sect-fctypes`).  After all,+if it tries to evaluate a function during type checking which doesn't+terminate, then type checking won't terminate!+Therefore, only total functions will be evaluated during type checking.+Partial functions can still be used in types, but will not be evaluated+further.
docs/tutorial/views.rst view
@@ -89,7 +89,7 @@ ``j``—this is allowed because another argument has determined the form of these patterns. -We will return to this function in Section :ref:`sect-provisional` to+We will return to this function in the next section :ref:`sect-parity` to complete the definition of ``parity``.  With and proofs
idris.cabal view
@@ -1,5 +1,5 @@ Name:           idris-Version:        0.99.2+Version:        1.0 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -252,7 +252,7 @@                 , Tools_idris    Build-depends:  base >=4 && <5-                , aeson >= 0.6 && < 1.1+                , aeson >= 0.6 && < 1.2                 , annotated-wl-pprint >= 0.7 && < 0.8                 , ansi-terminal < 0.7                 , ansi-wl-pprint < 0.7@@ -287,7 +287,7 @@                 , uniplate >=1.6 && < 1.7                 , unordered-containers < 0.3                 , utf8-string < 1.1-                , vector < 0.12+                , vector < 0.13                 , vector-binary-instances < 0.3                 , zip-archive > 0.2.3.5 && < 0.4                 , fsnotify >= 0.2 && < 2.2
libs/contrib/Control/ST.idr view
@@ -39,14 +39,14 @@  {- Update an entry in a context with a new state -} public export-updateRes : (res : Resources) -> +updateRes : (res : Resources) ->              InState lbl st res -> Type -> Resources updateRes (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs) updateRes (r :: rs) (There x) ty = r :: updateRes rs x ty  {- Remove an entry from a context -} public export-drop : (res : Resources) -> (prf : InState lbl st res) -> +drop : (res : Resources) -> (prf : InState lbl st res) ->        Resources drop (MkRes lbl st :: rs) Here = rs drop (r :: rs) (There p) = r :: drop rs p@@ -128,10 +128,10 @@ updateWith new [] SubNil = new updateWith new [] (InRes el z) = absurd el -- Don't add the ones which were consumed by the subctxt-updateWith [] (x :: xs) (InRes el p) +updateWith [] (x :: xs) (InRes el p)     = updateWith [] (dropEl _ el) p -- A new item corresponding to an existing thing-updateWith (n :: ns) (x :: xs) (InRes el p) +updateWith (n :: ns) (x :: xs) (InRes el p)     = n :: updateWith ns (dropEl _ el) p updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p @@ -154,7 +154,7 @@  public export combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources-combineVarsIn {comp} res (InResVar el x) +combineVarsIn {comp} res (InResVar el x)      = ((comp ::: Composite (getCombineType x)) :: dropCombined (InResVar el x)) combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x @@ -172,7 +172,7 @@ lookupEnv Here (x :: xs) = x lookupEnv (There p) (x :: xs) = lookupEnv p xs -updateEnv : (prf : InState lbl ty res) -> Env res -> ty' -> +updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->             Env (updateRes res prf ty') updateEnv Here (x :: xs) val = val :: xs updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val@@ -205,20 +205,20 @@  mkComposite : Env res -> (prf : VarsIn vs res) -> Composite (getCombineType prf) mkComposite [] VarsNil = CompNil-mkComposite env (InResVar el z) +mkComposite env (InResVar el z)     = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z) mkComposite (x :: env) (SkipVar z) = mkComposite env z -rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) -> +rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->                 Env (combineVarsIn res prf)-rebuildVarsIn env (InResVar el p) +rebuildVarsIn env (InResVar el p)      = mkComposite (dropEntry env el) p :: dropVarsIn env (InResVar el p) rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p  {- Some things to make STrans interfaces look prettier -}  infix 6 :->-          + public export data Action : Type -> Type where      Stable : Var -> Type -> Action ty@@ -254,7 +254,7 @@ public export %error_reduce add : Type -> Action Var add ty = Add (\var => [var ::: ty])- + public export %error_reduce remove : Var -> Type -> Action ty remove = Remove@@ -285,17 +285,17 @@               (ty : Type) ->               Resources -> (ty -> Resources) ->               Type where-     Pure : (result : ty) -> +     Pure : (result : ty) ->             STrans m ty (out_fn result) out_fn      Bind : STrans m a st1 st2_fn ->-            ((result : a) -> +            ((result : a) ->                 STrans m b (st2_fn result) st3_fn) ->             STrans m b st1 st3_fn      Lift : Monad m => m t -> STrans m t res (const res)-     RunAs : Applicative m => STrans m t in_res (const out_res) -> +     RunAs : Applicative m => STrans m t in_res (const out_res) ->              STrans m (m t) in_res (const out_res) -     New : (val : state) -> +     New : (val : state) ->            STrans m Var res (\lbl => (lbl ::: state) :: res)      Delete : (lbl : Var) ->               (prf : InState lbl st res) ->@@ -305,8 +305,8 @@       Split : (lbl : Var) ->              (prf : InState lbl (Composite vars) res) ->-             STrans m (VarList vars) res -                   (\ vs => mkRes vs ++ +             STrans m (VarList vars) res+                   (\ vs => mkRes vs ++                             updateRes res prf (State ()))      Combine : (comp : Var) -> (vs : List Var) ->                (prf : VarsIn (comp :: vs) res) ->@@ -340,7 +340,7 @@ dropEnv : Env ys -> SubRes xs ys -> Env xs dropEnv [] SubNil = [] dropEnv [] (InRes idx rest) = absurd idx-dropEnv (z :: zs) (InRes idx rest) +dropEnv (z :: zs) (InRes idx rest)     = let [e] = envElem idx (z :: zs) in           e :: dropEnv (dropDups (z :: zs) idx) rest dropEnv (z :: zs) (Skip p) = dropEnv zs p@@ -355,25 +355,25 @@              Env (updateWith new old prf) rebuildEnv new [] SubNil = new rebuildEnv new [] (InRes el p) = absurd el-rebuildEnv [] (x :: xs) (InRes el p) +rebuildEnv [] (x :: xs) (InRes el p)     = rebuildEnv [] (dropDups (x :: xs) el) p-rebuildEnv (e :: es) (x :: xs) (InRes el p) +rebuildEnv (e :: es) (x :: xs) (InRes el p)     = e :: rebuildEnv es (dropDups (x :: xs) el) p rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p  runST : Env invars -> STrans m a invars outfn ->         ((x : a) -> Env (outfn x) -> m b) -> m b runST env (Pure result) k = k result env-runST env (Bind prog next) k +runST env (Bind prog next) k    = runST env prog (\prog', env' => runST env' (next prog') k)-runST env (Lift action) k +runST env (Lift action) k    = do res <- action         k res env runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env') runST env (New val) k = k MkVar (val :: env) runST env (Delete lbl prf) k = k () (dropVal prf env) runST env (DropSubRes prf) k = k (dropEnv env prf) (keepEnv env prf)-runST env (Split lbl prf) k = let val = lookupEnv prf env +runST env (Split lbl prf) k = let val = lookupEnv prf env                                   env' = updateEnv prf env (Value ()) in                                   k (mkVars val) (addToEnv val env')   where@@ -386,7 +386,7 @@     addToEnv (CompCons x xs) env = x :: addToEnv xs env runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env]) runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)-runST env (Call prog res_prf) k +runST env (Call prog res_prf) k    = let env' = dropEnv env res_prf in          runST env' prog                  (\prog', envk => k prog' (rebuildEnv envk env res_prf))@@ -404,15 +404,15 @@             (k : (x : a) -> Env (outfn x) -> m b) ->             (onDry : m b) -> m b runSTLoop Empty _ _ _ onDry = onDry-runSTLoop (More x) env (Bind prog next) k onDry +runSTLoop (More x) env (Bind prog next) k onDry     = runST env prog (\prog', env' => runSTLoop x env' (next prog') k onDry) runSTLoop (More x) env (Pure result) k onDry = k result env -export +export pure : (result : ty) -> STrans m ty (out_fn result) out_fn pure = Pure -export +export (>>=) : STrans m a st1 st2_fn ->         ((result : a) -> STrans m b (st2_fn result) st3_fn) ->         STrans m b st1 st3_fn@@ -423,19 +423,19 @@             STrans m ty res out_fn returning res prog = do prog                         pure res-  + export lift : Monad m => m t -> STrans m t res (const res) lift = Lift  export-runAs : Applicative m => STrans m t in_res (const out_res) -> +runAs : Applicative m => STrans m t in_res (const out_res) ->         STrans m (m t) in_res (const out_res) runAs = RunAs  export-new : (val : state) -> +new : (val : state) ->       STrans m Var res (\lbl => (lbl ::: State state) :: res) new val = New (Value val) @@ -455,8 +455,8 @@ export split : (lbl : Var) ->         {auto prf : InState lbl (Composite vars) res} ->-        STrans m (VarList vars) res -              (\ vs => mkRes vs ++ +        STrans m (VarList vars) res+              (\ vs => mkRes vs ++                        updateRes res prf (State ())) split lbl {prf} = Split lbl prf @@ -467,7 +467,7 @@           STrans m () res               (const (combineVarsIn res var_prf)) combine comp vs {var_prf} = Combine comp vs var_prf-     + export toEnd : (lbl : Var) ->         {auto prf : InState lbl state res} ->@@ -479,7 +479,7 @@        {auto res_prf : SubRes sub old} ->        STrans m t old (\res => updateWith (new_f res) old res_prf) call prog {res_prf} = Call prog res_prf- + export read : (lbl : Var) ->        {auto prf : InState lbl (State ty) res} ->@@ -493,7 +493,7 @@         (val : ty') ->         STrans m () res (const (updateRes res prf (State ty'))) write lbl {prf} val = Write lbl prf (Value val)-       + export update : (lbl : Var) ->          {auto prf : InState lbl (State ty) res} ->@@ -512,12 +512,12 @@    export    pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn    pure = Pure-    + public export %error_reduce out_res : ty -> (as : List (Action ty)) -> Resources out_res x [] = [] out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs-out_res x ((Trans lbl inr outr) :: xs) +out_res x ((Trans lbl inr outr) :: xs)     = (lbl ::: outr x) :: out_res x xs out_res x ((Remove lbl inr) :: xs) = out_res x xs out_res x (Add outf :: xs) = outf x ++ out_res x xs@@ -533,14 +533,14 @@ public export %error_reduce -- always evaluate this before showing errors ST : (m : Type -> Type) ->-     (ty : Type) -> +     (ty : Type) ->      List (Action ty) -> Type ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)  public export %error_reduce -- always evaluate this before showing errors STLoop : (m : Type -> Type) ->-         (ty : Type) -> +         (ty : Type) ->          List (Action ty) -> Type STLoop m ty xs = STransLoop m ty (in_res xs) (\result : ty => out_res result xs) @@ -550,22 +550,36 @@   putStr : String -> STrans m () xs (const xs)   getStr : STrans m String xs (const xs) +  putChar : Char -> STrans m () xs (const xs)+  getChar : STrans m Char xs (const xs)++ export putStrLn : ConsoleIO m => String -> STrans m () xs (const xs) putStrLn str = putStr (str ++ "\n")  export+print : (ConsoleIO m, Show a) => a -> STrans m () xs (const xs)+print a = putStr $ show a++export+printLn : (ConsoleIO m, Show a) => a -> STrans m () xs (const xs)+printLn a = putStrLn $ show a++export ConsoleIO IO where   putStr str = lift (Interactive.putStr str)   getStr = lift Interactive.getLine +  putChar c = lift $ Interactive.putChar c+  getChar = lift Interactive.getChar  export run : Applicative m => ST m a [] -> m a run prog = runST [] prog (\res, env' => pure res)  export-runLoop : Applicative m => Fuel -> STLoop m a [] -> +runLoop : Applicative m => Fuel -> STLoop m a [] ->           (onEmpty : m a) ->           m a runLoop fuel prog onEmpty@@ -580,16 +594,16 @@ ||| to ensure that it isn't duplicated. export runWith : {resf : _} ->-          Env res -> STrans IO a res (\result => resf result) -> +          Env res -> STrans IO a res (\result => resf result) ->           IO (result ** Env (resf result)) runWith env prog = runST env prog (\res, env' => pure (res ** env'))  export runWithLoop : {resf : _} ->-          Env res -> Fuel -> STransLoop IO a res (\result => resf result) -> +          Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->           IO (Maybe (result ** Env (resf result)))-runWithLoop env fuel prog -    = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env'))) +runWithLoop env fuel prog+    = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))                               (pure Nothing)  export@@ -602,7 +616,7 @@ export st_precondition : Err -> Maybe (List ErrorReportPart) st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)-   = pure +   = pure       [TextPart "'call' is not valid here. ",        TextPart "The operation has preconditions ",        TermPart sub,@@ -629,13 +643,13 @@     getPostconditions _ = Nothing      renderPre : TT -> TT -> List (ErrorReportPart)-    renderPre got req +    renderPre got req         = [SubReport [TextPart "Operation has preconditions: ",                       TermPart req],            SubReport [TextPart "States here are: ",                       TermPart got]]     renderPost : TT -> TT -> List (ErrorReportPart)-    renderPost got req +    renderPost got req         = [SubReport [TextPart "Operation has postconditions: ",                       TermPart req],            SubReport [TextPart "Required result states here are: ",
man/idris.1 view
@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "26 March 2017" "0.99.2" "Idris man page"+.TH man 1 "1 April 2017" "1.0" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS
rts/idris_main.c view
@@ -55,7 +55,7 @@     init_nullaries();     init_signals(); -    _idris__123_runMain0_125_(vm, NULL);+    _idris__123_runMain_95_0_125_(vm, NULL);  #ifdef IDRIS_DEBUG     if (opts.show_summary) {
rts/idris_rts.h view
@@ -213,7 +213,9 @@  typedef intptr_t i_int; -#define MKINT(x) ((void*)((i_int)(((x)<<1)+1)))+// Shifting a negative number left is undefined and (rightly) gives a warning,+// but we're only interested in shifting the bit pattern, so cast it+#define MKINT(x) ((void*)((i_int)((((uintptr_t)x)<<1)+1))) #define GETINT(x) ((i_int)(x)>>1) #define ISINT(x) ((((i_int)x)&1) == 1) #define ISSTR(x) (GETTY(x) == CT_STRING)
+ samples/tutorial/BMain.idr view
@@ -0,0 +1,8 @@+module Main++import BTree++main : IO ()+main = do let t = toTree [1,8,2,7,9,3]+          printLn (btree.toList t)+
+ samples/tutorial/BTree.idr view
@@ -0,0 +1,22 @@+module btree++public export+data BTree a = Leaf+             | Node (BTree a) a (BTree a)++export+insert : Ord a => a -> BTree a -> BTree a+insert x Leaf = Node Leaf x Leaf+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)+                                   else (Node l v (insert x r))++export+toList : BTree a -> List a+toList Leaf = []+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)++export+toTree : Ord a => List a -> BTree a+toTree [] = Leaf+toTree (x :: xs) = insert x (toTree xs)+
+ samples/tutorial/BTreeMod.idr view
@@ -0,0 +1,20 @@+module btree++abstract data BTree a = Leaf+                      | Node (BTree a) a (BTree a)++abstract+insert : Ord a => a -> BTree a -> BTree a+insert x Leaf = Node Leaf x Leaf+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)+                                   else (Node l v (insert x r))++abstract+toList : BTree a -> List a+toList Leaf = []+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)++abstract+toTree : Ord a => List a -> BTree a+toTree [] = Leaf+toTree (x :: xs) = insert x (toTree xs)
+ samples/tutorial/Foo.idr view
@@ -0,0 +1,10 @@+module foo++namespace x+  test : Int -> Int+  test x = x * 2++namespace y+  test : String -> String+  test x = x ++ x+
+ samples/tutorial/Hello.idr view
@@ -0,0 +1,5 @@+module Main++main : IO ()+main = putStrLn "Hello world"+
+ samples/tutorial/Idiom.idr view
@@ -0,0 +1,38 @@+module idiom++data Expr = Var String+          | Val Int+          | Add Expr Expr++data Eval : Type -> Type where+   MkEval : (List (String, Int) -> Maybe a) -> Eval a++fetch : String -> Eval Int+fetch x = MkEval fetchVal where+    fetchVal : List (String, Int) -> Maybe Int+    fetchVal [] = Nothing+    fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)++implementation Functor Eval where+    map f (MkEval g) = MkEval (\e => map f (g e))++implementation Applicative Eval where+    pure x = MkEval (\e => Just x)++    (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where+       app : Maybe (a -> b) -> Maybe a -> Maybe b+       app (Just fx) (Just gx) = Just (fx gx)+       app _         _         = Nothing++eval : Expr -> Eval Int+eval (Var x)   = fetch x+eval (Val x)   = [| x |]+eval (Add x y) = [| eval x + eval y |]++runEval : List (String, Int) -> Expr -> Maybe Int+runEval env e = case eval e of+    MkEval envFn => envFn env++m_add' : Maybe Int -> Maybe Int -> Maybe Int+m_add' x y = [| x + y |]+
+ samples/tutorial/Interfaces.idr view
@@ -0,0 +1,10 @@+m_add : Maybe Int -> Maybe Int -> Maybe Int+m_add x y = do x' <- x -- Extract value from x+               y' <- y -- Extract value from y+               pure (x' + y') -- Add them++m_add' : Maybe Int -> Maybe Int -> Maybe Int+m_add' x y = [ x' + y' | x' <- x, y' <- y ]++sortAndShow : (Ord a, Show a) => List a -> String+sortAndShow xs = show (sort xs)
+ samples/tutorial/Interp.idr view
@@ -0,0 +1,71 @@+module Main++import Data.Vect+import Data.Fin++data Ty = TyInt | TyBool| TyFun Ty Ty++interpTy : Ty -> Type+interpTy TyInt       = Int+interpTy TyBool      = Bool+interpTy (TyFun s t) = interpTy s -> interpTy t++using (G : Vect n Ty)++  data Env : Vect n Ty -> Type where+      Nil  : Env Nil+      (::) : interpTy a -> Env G -> Env (a :: G)++  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where+      Stop : HasType FZ (t :: G) t+      Pop  : HasType k G t -> HasType (FS k) (u :: G) t++  lookup : HasType i G t -> Env G -> interpTy t+  lookup Stop    (x :: xs) = x+  lookup (Pop k) (x :: xs) = lookup k xs++  data Expr : Vect n Ty -> Ty -> Type where+      Var : HasType i G t -> Expr G t+      Val : (x : Int) -> Expr G TyInt+      Lam : Expr (a :: G) t -> Expr G (TyFun a t)+      App : Expr G (TyFun a t) -> Expr G a -> Expr G t+      Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->+            Expr G c+      If  : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a++  interp : Env G -> (e : Expr G t) -> interpTy t+  interp env (Var i)     = lookup i env+  interp env (Val x)     = x+  interp env (Lam sc)    = \x => interp (x :: env) sc+  interp env (App f s)   = interp env f (interp env s)+  interp env (Op op x y) = op (interp env x) (interp env y)+  interp env (If x t e)  = if interp env x then interp env t+                                           else interp env e++  eId : Expr G (TyFun TyInt TyInt)+  eId = Lam (Var Stop)++  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))+  eAdd = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))++  eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))+  eEq = Lam (Lam (Op (==) (Var Stop) (Var (Pop Stop))))++  eDouble : Expr G (TyFun TyInt TyInt)+  eDouble = Lam (App (App eAdd (Var Stop)) (Var Stop))++  fact : Expr G (TyFun TyInt TyInt)+  fact = Lam (If (Op (==) (Var Stop) (Val 0))+                 (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1))) (Var Stop)))++testFac : Int+testFac = interp [] fact 4++-- unitTestFac : so (interp [] fact 4 == 24)+-- unitTestFac = oh++main : IO ()+main = do putStr "Enter a number: "+          x <- getLine+          printLn (interp [] fact (cast x))+
+ samples/tutorial/LetBind.idr view
@@ -0,0 +1,16 @@+module LetBind++mirror : List a -> List a+mirror xs = let xs' = reverse xs in+                xs ++ xs'++data Person = MkPerson String Int++showPerson : Person -> String+showPerson p = let MkPerson name age = p in+                   name ++ " is " ++ show age ++ " years old"++splitAt : Char -> String -> (String, String)+splitAt c x = case break (== c) x of+                  (x, y) => (x, strTail y)+
+ samples/tutorial/Prims.idr view
@@ -0,0 +1,14 @@+module Prims++x : Int+x = 42++foo : String+foo = "Sausage machine"++bar : Char+bar = 'Z'++quux : Bool+quux = False+
+ samples/tutorial/Record.idr view
@@ -0,0 +1,21 @@+import Data.Vect++record Person where+    constructor MkPerson+    firstName, middleName, lastName : String+    age : Int++fred : Person+fred = MkPerson "Fred" "Joe" "Bloggs" 30++record Class where+    constructor ClassInfo+    students : Vect n Person+    className : String++addStudent : Person -> Class -> Class+addStudent p c = record { students = p :: students c } c++addStudent' : Person -> Class -> Class+addStudent' p c = record { students $= (p ::) } c+
+ samples/tutorial/Theorems.idr view
@@ -0,0 +1,37 @@++fiveIsFive : 5 = 5+fiveIsFive = Refl++twoPlusTwo : 2 + 2 = 4+twoPlusTwo = Refl++total disjoint : (n : Nat) -> Z = S n -> Void+disjoint n p = replace {P = disjointTy} p ()+  where+    disjointTy : Nat -> Type+    disjointTy Z = ()+    disjointTy (S k) = Void++total acyclic : (n : Nat) -> n = S n -> Void+acyclic Z p = disjoint _ p+acyclic (S k) p = acyclic k (succInjective _ _ p)++empty1 : Void+empty1 = hd [] where+    hd : List a -> a+    hd (x :: xs) = x++empty2 : Void+empty2 = empty2++plusReduces : (n:Nat) -> plus Z n = n+plusReduces n = Refl++plusReducesZ : (n:Nat) -> n = plus n Z+plusReducesZ Z = Refl+plusReducesZ (S k) = cong (plusReducesZ k)++plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)+plusReducesS Z m = Refl+plusReducesS (S k) m = cong (plusReducesS k m)+
+ samples/tutorial/Universe.idr view
@@ -0,0 +1,7 @@+myid : (a : Type) -> a -> a+myid _ x = x++idid :  (a : Type) -> a -> a+idid = myid _ myid++
+ samples/tutorial/UsefulTypes.idr view
@@ -0,0 +1,21 @@+import Data.Vect++intVec : Vect 5 Int+intVec = [1, 2, 3, 4, 5]++double : Int -> Int+double x = x * 2++vec : (n ** Vect n Int)+vec = (_ ** [3, 4])++list_lookup : Nat -> List a -> Maybe a+list_lookup _     Nil         = Nothing+list_lookup Z     (x :: xs) = Just x+list_lookup (S k) (x :: xs) = list_lookup k xs++lookup_default : Nat -> List a -> a -> a+lookup_default i xs def = case list_lookup i xs of+                              Nothing => def+                              Just x => x+
+ samples/tutorial/VBroken.idr view
@@ -0,0 +1,10 @@+module Vect++data Vect : Nat -> Type -> Type where+     Nil : Vect Z a+     (::) : a -> Vect k a -> Vect (S k) a++(++) : Vect n a -> Vect m a -> Vect (n + m) a+(++) Nil       ys = ys+(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN+
+ samples/tutorial/Views.idr view
@@ -0,0 +1,25 @@+module views++data Parity : Nat -> Type where+   Even : Parity (n + n)+   Odd  : Parity (S (n + n))++helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))+helpEven j p = rewrite plusSuccRightSucc j j in p++helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))+helpOdd j p = rewrite plusSuccRightSucc j j in p++parity : (n:Nat) -> Parity n+parity Z     = Even {n=Z}+parity (S Z) = Odd {n=Z}+parity (S (S k)) with (parity k)+  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})+  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})++natToBin : Nat -> List Bool+natToBin Z = Nil+natToBin k with (parity k)+   natToBin (j + j)     | Even = False :: natToBin j+   natToBin (S (j + j)) | Odd  = True  :: natToBin j+
+ samples/tutorial/ViewsBroken.idr view
@@ -0,0 +1,12 @@++data Parity : Nat -> Type where+   Even : Parity (n + n)+   Odd  : Parity (S (n + n))++parity : (n:Nat) -> Parity n+parity Z     = Even {n=Z}+parity (S Z) = Odd {n=Z}+parity (S (S k)) with (parity k)+  parity (S (S (j + j)))     | Even = Even {n=S j}+  parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}+
+ samples/tutorial/Wheres.idr view
@@ -0,0 +1,14 @@+module Wheres++even : Nat -> Bool+even Z = True+even (S k) = odd k where+  odd Z = False+  odd (S k) = even k++test : List Nat+test = [c (S 1), c Z, d (S Z)]+  where c x = 42 + x+        d y = c (y + 1 + z y)+              where z w = y + w+
− samples/tutorial/binary.idr 
@@ -1,61 +0,0 @@-module Main--data Binary : Nat -> Type where-    bEnd : Binary Z-    bO : Binary n -> Binary (n + n)-    bI : Binary n -> Binary (S (n + n))--implementation Show (Binary n) where-    show (bO x) = show x ++ "0"-    show (bI x) = show x ++ "1"-    show bEnd = ""--data Parity : Nat -> Type where-   Even : Parity (n + n)-   Odd  : Parity (S (n + n))--parity : (n:Nat) -> Parity n-parity Z     = Even {n=Z}-parity (S Z) = Odd {n=Z}-parity (S (S k)) with (parity k)-    parity (S (S (j + j)))     | Even ?= Even {n=S j}-    parity (S (S (S (j + j)))) | Odd  ?= Odd {n=S j}--natToBin : (n:Nat) -> Binary n-natToBin Z = bEnd-natToBin (S k) with (parity k)-   natToBin (S (j + j))     | Even  = bI (natToBin j)-   natToBin (S (S (j + j))) | Odd  ?= bO (natToBin (S j))--intToNat : Int -> Nat-intToNat 0 = Z-intToNat x = if (x>0) then (S (intToNat (x-1))) else Z--main : IO ()-main = do putStr "Enter a number: "-          x <- getLine-          print (natToBin (fromInteger (cast x)))------------ Proofs ------------Main.natToBin_lemma_1 = proof-  intros-  rewrite plusSuccRightSucc j j-  rewrite sym (plusSuccRightSucc j j)-  trivial---parity_lemma_1 = proof-    intros-    rewrite sym (plusSuccRightSucc j j)-    trivial---parity_lemma_2 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--
− samples/tutorial/bmain.idr 
@@ -1,8 +0,0 @@-module Main--import btree--main : IO ()-main = do let t = toTree [1,8,2,7,9,3]-          print (btree.toList t)-
− samples/tutorial/btree.idr 
@@ -1,18 +0,0 @@-module btree--data BTree a = Leaf-             | Node (BTree a) a (BTree a)--insert : Ord a => a -> BTree a -> BTree a-insert x Leaf = Node Leaf x Leaf-insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)-                                   else (Node l v (insert x r))--toList : BTree a -> List a-toList Leaf = []-toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)--toTree : Ord a => List a -> BTree a-toTree [] = Leaf-toTree (x :: xs) = insert x (toTree xs)-
− samples/tutorial/btreemod.idr 
@@ -1,20 +0,0 @@-module btree--abstract data BTree a = Leaf-                      | Node (BTree a) a (BTree a)--abstract-insert : Ord a => a -> BTree a -> BTree a-insert x Leaf = Node Leaf x Leaf-insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)-                                   else (Node l v (insert x r))--abstract-toList : BTree a -> List a-toList Leaf = []-toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)--abstract-toTree : Ord a => List a -> BTree a-toTree [] = Leaf-toTree (x :: xs) = insert x (toTree xs)
− samples/tutorial/classes.idr 
@@ -1,10 +0,0 @@-m_add : Maybe Int -> Maybe Int -> Maybe Int-m_add x y = do x' <- x -- Extract value from x-               y' <- y -- Extract value from y-               pure (x' + y') -- Add them--m_add' : Maybe Int -> Maybe Int -> Maybe Int-m_add' x y = [ x' + y' | x' <- x, y' <- y ]--sortAndShow : (Ord a, Show a) => List a -> String-sortAndShow xs = show (sort xs)
− samples/tutorial/foo.idr 
@@ -1,10 +0,0 @@-module foo--namespace x-  test : Int -> Int-  test x = x * 2--namespace y-  test : String -> String-  test x = x ++ x-
− samples/tutorial/hello.idr 
@@ -1,5 +0,0 @@-module Main--main : IO ()-main = putStrLn "Hello world"-
− samples/tutorial/idiom.idr 
@@ -1,38 +0,0 @@-module idiom--data Expr = Var String-          | Val Int-          | Add Expr Expr--data Eval : Type -> Type where-   MkEval : (List (String, Int) -> Maybe a) -> Eval a--fetch : String -> Eval Int-fetch x = MkEval fetchVal where-    fetchVal : List (String, Int) -> Maybe Int-    fetchVal [] = Nothing-    fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)--implementation Functor Eval where-    map f (MkEval g) = MkEval (\e => map f (g e))--implementation Applicative Eval where-    pure x = MkEval (\e => Just x)--    (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where-       app : Maybe (a -> b) -> Maybe a -> Maybe b-       app (Just fx) (Just gx) = Just (fx gx)-       app _         _         = Nothing--eval : Expr -> Eval Int-eval (Var x)   = fetch x-eval (Val x)   = [| x |]-eval (Add x y) = [| eval x + eval y |]--runEval : List (String, Int) -> Expr -> Maybe Int-runEval env e = case eval e of-    MkEval envFn => envFn env--m_add' : Maybe Int -> Maybe Int -> Maybe Int-m_add' x y = [| x + y |]-
− samples/tutorial/interp.idr 
@@ -1,71 +0,0 @@-module Main--import Data.Vect-import Data.Fin--data Ty = TyInt | TyBool| TyFun Ty Ty--interpTy : Ty -> Type-interpTy TyInt       = Int-interpTy TyBool      = Bool-interpTy (TyFun s t) = interpTy s -> interpTy t--using (G : Vect n Ty)--  data Env : Vect n Ty -> Type where-      Nil  : Env Nil-      (::) : interpTy a -> Env G -> Env (a :: G)--  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where-      Stop : HasType FZ (t :: G) t-      Pop  : HasType k G t -> HasType (FS k) (u :: G) t--  lookup : HasType i G t -> Env G -> interpTy t-  lookup Stop    (x :: xs) = x-  lookup (Pop k) (x :: xs) = lookup k xs--  data Expr : Vect n Ty -> Ty -> Type where-      Var : HasType i G t -> Expr G t-      Val : (x : Int) -> Expr G TyInt-      Lam : Expr (a :: G) t -> Expr G (TyFun a t)-      App : Expr G (TyFun a t) -> Expr G a -> Expr G t-      Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->-            Expr G c-      If  : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a--  interp : Env G -> %static (e : Expr G t) -> interpTy t-  interp env (Var i)     = lookup i env-  interp env (Val x)     = x-  interp env (Lam sc)    = \x => interp (x :: env) sc-  interp env (App f s)   = interp env f (interp env s)-  interp env (Op op x y) = op (interp env x) (interp env y)-  interp env (If x t e)  = if interp env x then interp env t-                                           else interp env e--  eId : Expr G (TyFun TyInt TyInt)-  eId = Lam (Var Stop)--  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))-  eAdd = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))--  eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))-  eEq = Lam (Lam (Op (==) (Var Stop) (Var (Pop Stop))))--  eDouble : Expr G (TyFun TyInt TyInt)-  eDouble = Lam (App (App eAdd (Var Stop)) (Var Stop))--  fact : Expr G (TyFun TyInt TyInt)-  fact = Lam (If (Op (==) (Var Stop) (Val 0))-                 (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1))) (Var Stop)))--testFac : Int-testFac = interp [] fact 4---- unitTestFac : so (interp [] fact 4 == 24)--- unitTestFac = oh--main : IO ()-main = do putStr "Enter a number: "-          x <- getLine-          print (interp [] fact (cast x))-
− samples/tutorial/letbind.idr 
@@ -1,16 +0,0 @@-module letbind--mirror : List a -> List a-mirror xs = let xs' = reverse xs in-                xs ++ xs'--data Person = MkPerson String Int--showPerson : Person -> String-showPerson p = let MkPerson name age = p in-                   name ++ " is " ++ show age ++ " years old"--splitAt : Char -> String -> (String, String)-splitAt c x = case break (== c) x of-                  (x, y) => (x, strTail y)-
− samples/tutorial/prims.idr 
@@ -1,14 +0,0 @@-module prims--x : Int-x = 42--foo : String-foo = "Sausage machine"--bar : Char-bar = 'Z'--quux : Bool-quux = False-
− samples/tutorial/theorems.idr 
@@ -1,57 +0,0 @@--fiveIsFive : 5 = 5-fiveIsFive = Refl--twoPlusTwo : 2 + 2 = 4-twoPlusTwo = Refl--total disjoint : (n : Nat) -> Z = S n -> Void-disjoint n p = replace {P = disjointTy} p ()-  where-    disjointTy : Nat -> Type-    disjointTy Z = ()-    disjointTy (S k) = Void--total acyclic : (n : Nat) -> n = S n -> Void-acyclic Z p = disjoint _ p-acyclic (S k) p = acyclic k (succInjective _ _ p)--empty1 : Void-empty1 = hd [] where-    hd : List a -> a-    hd (x :: xs) = x--empty2 : Void-empty2 = empty2--plusReduces : (n:Nat) -> plus Z n = n-plusReduces n = Refl--plusReducesZ : (n:Nat) -> n = plus n Z-plusReducesZ Z = Refl-plusReducesZ (S k) = cong (plusReducesZ k)--plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)-plusReducesS Z m = Refl-plusReducesS (S k) m = cong (plusReducesS k m)--plusReducesZ' : (n:Nat) -> n = plus n Z-plusReducesZ' Z     = ?plusredZ_Z-plusReducesZ' (S k) = let ih = plusReducesZ' k in-                      ?plusredZ_S------------- Proofs ------------plusredZ_S = proof {-    intro;-    intro;-    rewrite ih;-    trivial;-}--plusredZ_Z = proof {-    compute;-    trivial;-}-
− samples/tutorial/universe.idr 
@@ -1,7 +0,0 @@-myid : (a : Type) -> a -> a-myid _ x = x--idid :  (a : Type) -> a -> a-idid = myid _ myid--
− samples/tutorial/usefultypes.idr 
@@ -1,20 +0,0 @@--intVec : Vect 5 Int-intVec = [1, 2, 3, 4, 5]--double : Int -> Int-double x = x * 2--vec : (n ** Vect n Int)-vec = (_ ** [3, 4])--list_lookup : Nat -> List a -> Maybe a-list_lookup _     Nil         = Nothing-list_lookup Z     (x :: xs) = Just x-list_lookup (S k) (x :: xs) = list_lookup k xs--lookup_default : Nat -> List a -> a -> a-lookup_default i xs def = case list_lookup i xs of-                              Nothing => def-                              Just x => x-
− samples/tutorial/vbroken.idr 
@@ -1,10 +0,0 @@-module Vect--data Vect : Nat -> Type -> Type where-     Nil : Vect Z a-     (::) : a -> Vect k a -> Vect (S k) a--(++) : Vect n a -> Vect m a -> Vect (n + m) a-(++) Nil       ys = ys-(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN-
− samples/tutorial/views.idr 
@@ -1,37 +0,0 @@-module views--data Parity : Nat -> Type where-   Even : Parity (n + n)-   Odd  : Parity (S (n + n))--parity : (n:Nat) -> Parity n-parity Z     = Even {n=Z}-parity (S Z) = Odd {n=Z}-parity (S (S k)) with (parity k)-  parity (S (S (j + j)))     | Even ?= Even {n=S j}-  parity (S (S (S (j + j)))) | Odd  ?= Odd {n=S j}--natToBin : Nat -> List Bool-natToBin Z = Nil-natToBin k with (parity k)-   natToBin (j + j)     | Even = False :: natToBin j-   natToBin (S (j + j)) | Odd  = True  :: natToBin j------------- Proofs ------------views.parity_lemma_2 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--views.parity_lemma_1 = proof {-    intro;-    intro;-    rewrite sym (plusSuccRightSucc j j);-    trivial;-}--
− samples/tutorial/viewsbroken.idr 
@@ -1,12 +0,0 @@--data Parity : Nat -> Type where-   Even : Parity (n + n)-   Odd  : Parity (S (n + n))--parity : (n:Nat) -> Parity n-parity Z     = Even {n=Z}-parity (S Z) = Odd {n=Z}-parity (S (S k)) with (parity k)-  parity (S (S (j + j)))     | Even = Even {n=S j}-  parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}-
− samples/tutorial/wheres.idr 
@@ -1,14 +0,0 @@-module wheres--even : Nat -> Bool-even Z = True-even (S k) = odd k where-  odd Z = False-  odd (S k) = even k--test : List Nat-test = [c (S 1), c Z, d (S Z)]-  where c x = 42 + x-        d y = c (y + 1 + z y)-              where z w = y + w-
src/IRTS/CodegenC.hs view
@@ -841,14 +841,14 @@                                             indent 1 ++ "STOREOLD;\n" ++                                             indent 1 ++ "BASETOP(0);\n" ++                                             indent 1 ++ "ADDTOP(2);\n" ++-                                            indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" +++                                            indent 1 ++ "CALL(_idris__123_APPLY_95_0_125_);\n" ++                                             indent 1 ++ "TOP(0)=REG1;\n" ++                                             applyArgs (y:xs)                         applyArgs x = push 1 x ++                                       indent 1 ++ "STOREOLD;\n" ++                                       indent 1 ++ "BASETOP(0);\n" ++                                       indent 1 ++ "ADDTOP(" ++ show (length x + 1) ++ ");\n" ++-                                      indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n"+                                      indent 1 ++ "CALL(_idris__123_APPLY_95_0_125_);\n"                         renderArgs [] = "void"                         renderArgs [((s, _), n)] = s ++ " a" ++ (show n)                         renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++
src/Idris/Core/Evaluate.hs view
@@ -640,14 +640,6 @@         | x `elem` holes || y `elem` holes = return True         | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True         | otherwise = sameDefs ps x y-    ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))-          = ceq ps x (substV (P Bound n t) y)-    ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y-          = ceq ps (substV (P Bound n t) x) y-    ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))-        | n == n' = ceq ps x y-    ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y-        | n == n' = ceq ps x y      ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y     ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc@@ -668,6 +660,16 @@             ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')             ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')             ceqB ps b b' = ceq ps (binderTy b) (binderTy b')++    ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))+          = ceq ps x (substV (P Bound n t) y)+    ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y+          = ceq ps (substV (P Bound n t) x) y+    ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))+        | n == n' = ceq ps x y+    ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y+        | n == n' = ceq ps x y+     -- Special case for 'case' blocks - size of scope causes complications,     -- we only want to check the blocks themselves are valid and identical     -- in the current scope. So, just check the bodies, and the additional
src/Idris/Core/TT.hs view
@@ -538,7 +538,7 @@     show (UN n) = str n     show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n     show (MN _ u) | u == txt "underscore" = "_"-    show (MN i s) = "{" ++ str s ++ show i ++ "}"+    show (MN i s) = "{" ++ str s ++ "_" ++ show i ++ "}"     show (SN s) = show s     show (SymRef i) = "##symbol" ++ show i ++ "##" @@ -559,7 +559,7 @@ showCG (UN n) = T.unpack n showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n showCG (MN _ u) | u == txt "underscore" = "_"-showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"+showCG (MN i s) = "{" ++ T.unpack s ++ "_" ++ show i ++ "}" showCG (SN s) = showCG' s   where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i         showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i
src/Idris/DataOpts.hs view
@@ -97,7 +97,7 @@ applyDataOptRT n tag arity uniq args     | length args == arity = doOpts n args     | otherwise = let extra = satArgs (arity - length args)-                      tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)+                      tm = doOpts n (map (weakenTm (length extra)) args ++ map (\n -> P Bound n Erased) extra)                   in bind extra tm   where     satArgs n = map (\i -> sMN i "sat") [1..n]
src/Idris/Elab/Implementation.hs view
@@ -99,6 +99,10 @@                                 (map fst $ interface_implementations ci)                           addImplementation intImpl True n iname             _ -> addImplementation intImpl False n iname++    ist <- getIState+    checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))+     when (what /= ETypes && (not (null ds && not emptyinterface))) $ do          -- Add the parent implementation names to the privileged set          oldOpen <- addOpenImpl parents@@ -212,7 +216,6 @@          setOpenImpl oldOpen --          totalityCheckBlock -         checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))          addIBC (IBCImplementation intImpl (isNothing expn) n iname)    where@@ -243,9 +246,6 @@                               (_:_) -> return True             _ -> return False -- couldn't find interface, just let elabImplementation fail later -    -- TODO: largely based upon elabType' - should try to abstract-    -- Issue #1614 in the issue tracker:-    --    https://github.com/idris-lang/Idris-dev/issues/1614     elabFindOverlapping i ci iname syn t         = do ty' <- addUsingConstraints syn fc t              -- TODO think: something more in info?@@ -506,7 +506,8 @@     isInj i (P _ n _) = isConName n (tt_ctxt i)     isInj i (App _ f a) = isInj i f && isInj i a     isInj i (V _) = True-    isInj i (Bind n b sc) = isInj i sc+    isInj i (Bind n b@(Pi{}) sc) = isInj i (binderTy b) && isInj i sc+    isInj i (Bind n b sc) = False     isInj _ _ = True      instantiateRetTy (Bind n (Pi _ _ _ _) sc)
stack-shell.nix view
@@ -2,7 +2,7 @@  let   # MUST match resolver in stack.yaml-  resolver = haskell.packages.lts-8_4.ghc;+  resolver = haskell.packages.lts-8_06.ghc;    native_libs = [     libffi
stack.yaml view
@@ -1,4 +1,4 @@-resolver: lts-8.04+resolver: lts-8.06  packages:   - location: .
test/dsl001/expected view
@@ -1,13 +1,13 @@ 24 12 testFac : Int-testFac = PE_interp_e04a79ff [] (PE_fromInteger_d6648df 4)-PE_interp_e04a79ff : Env G -> Int -> Int-PE_interp_e04a79ff (3arg) = \x =>+testFac = PE_interp_9b251b28 [] (PE_fromInteger_d6648df 4)+PE_interp_9b251b28 : Env G -> Int -> Int+PE_interp_9b251b28 (3arg) = \x =>                               ifThenElse (PE_==_ba2f651f x                                                          (PE_fromInteger_d6648df 0))                                          (Delay (PE_fromInteger_d6648df 1))-                                         (Delay (PE_*_ba2f651f (PE_interp_e04a79ff (x ::+                                         (Delay (PE_*_ba2f651f (PE_interp_9b251b28 (x ::                                                                                     (3arg))                                                                                    (PE_-_ba2f651f x                                                                                                   (PE_fromInteger_d6648df 1)))
test/dsl001/input view
@@ -1,2 +1,2 @@ :printdef testFac-:printdef PE_interp_e04a79ff+:printdef PE_interp_9b251b28
test/interactive010/expected view
@@ -4,9 +4,9 @@ Usage is :doc <functionname> Usage is :wc <functionname> Usage is :printdef <functionname>-pat {ty503} : Type toplevel.u. pat {__interface504} : Prelude.Interfaces.Fractional {ty503}. Prelude.Interfaces./ {ty503} {__interface504}+pat {ty_503} : Type toplevel.u. pat {__interface_504} : Prelude.Interfaces.Fractional {ty_503}. Prelude.Interfaces./ {ty_503} {__interface_504} - : pty {ty503} : Type toplevel.u. pty {__interface504} : Prelude.Interfaces.Fractional {ty503}. {ty503} -> {ty503} -> {ty503}+ : pty {ty_503} : Type toplevel.u. pty {__interface_504} : Prelude.Interfaces.Fractional {ty_503}. {ty_503} -> {ty_503} -> {ty_503} (input):1:1: error: expected: ":",     dependent type signature,     end of input
test/pkg001/expected view
@@ -11,7 +11,7 @@   -Elaborating {__Infer0}+Elaborating {__Infer_0} builtin Elaborating = builtin
test/proof009/expected view
@@ -2,20 +2,20 @@   ----------                 Goal:                  -----------{hole0} : Int -> Int -> Int+{hole_0} : Int -> Int -> Int -Main.arhs> ----------              Other goals:              -----------{hole0}+{hole_0} ----------              Assumptions:              ----------  x : Int ----------                 Goal:                  -----------{hole1} : Int -> Int+{hole_1} : Int -> Int -Main.arhs> ----------              Other goals:              -----------{hole1},{hole0}+{hole_1},{hole_0} ----------              Assumptions:              ----------  x : Int  y : Int ----------                 Goal:                  -----------{hole2} : Int+{hole_2} : Int -Main.arhs> arhs: No more goals. -Main.arhs> Proof completed! Main.arhs = proof
test/reg027/expected view
@@ -1,3 +1,2 @@ <<int fn>>-6 reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined
test/reg027/reg027.idr view
@@ -9,24 +9,9 @@ IntFn : Type -> Type IntFn = \x => Int -> x -implementation Functor IntFn where -- (\x => Int -> x) where-  map f intf = \x => f (intf x)--implementation Applicative (\x => Int -> x) where-  pure v = \x => v-  (<*>) f a = \x => f x (a x)--implementation Monad IntFn where -  f >>= k = \x => k (f x) x- dbl : IntFn Int dbl x = x * 2  -foo : Int -> String-foo = do val <- dbl-         \x => show val- main : IO ()-main = do printLn dbl-          putStrLn (foo 3)+main = printLn dbl