diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +# New in 1.0 + ++ It's about time + # New in 0.99.2 ## Library Updates diff --git a/CONTRIBUTORS b/CONTRIBUTORS --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -171,7 +171,7 @@ Philip Rasmussen PoroCYon raichoo -Reynir Reynisson +Reynir Björnsson Ricky Elrod Robert Clipsham Robert Edström diff --git a/INSTALL.md b/INSTALL.md --- a/INSTALL.md +++ b/INSTALL.md @@ -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 -``` +``` diff --git a/docs/conf.py b/docs/conf.py --- a/docs/conf.py +++ b/docs/conf.py @@ -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. diff --git a/docs/listing/idris-prompt-helloworld.txt b/docs/listing/idris-prompt-helloworld.txt --- a/docs/listing/idris-prompt-helloworld.txt +++ b/docs/listing/idris-prompt-helloworld.txt @@ -1,7 +1,7 @@ $ idris hello.idr ____ __ _ / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 0.99.2 + / // __ / ___/ / ___/ Version 1.0 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help diff --git a/docs/listing/idris-prompt-interp.txt b/docs/listing/idris-prompt-interp.txt --- a/docs/listing/idris-prompt-interp.txt +++ b/docs/listing/idris-prompt-interp.txt @@ -1,7 +1,7 @@ $ idris interp.idr ____ __ _ / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 0.99.2 + / // __ / ___/ / ___/ Version 1.0 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help diff --git a/docs/listing/idris-prompt-start.txt b/docs/listing/idris-prompt-start.txt --- a/docs/listing/idris-prompt-start.txt +++ b/docs/listing/idris-prompt-start.txt @@ -1,7 +1,7 @@ $ idris ____ __ _ / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 0.99.2 + / // __ / ___/ / ___/ Version 1.0 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help diff --git a/docs/tutorial/index.rst b/docs/tutorial/index.rst --- a/docs/tutorial/index.rst +++ b/docs/tutorial/index.rst @@ -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 diff --git a/docs/tutorial/interfaces.rst b/docs/tutorial/interfaces.rst --- a/docs/tutorial/interfaces.rst +++ b/docs/tutorial/interfaces.rst @@ -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 ====================== diff --git a/docs/tutorial/introduction.rst b/docs/tutorial/introduction.rst --- a/docs/tutorial/introduction.rst +++ b/docs/tutorial/introduction.rst @@ -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 `_ +by Edwin Brady, available from `Manning `_. + Example Code ============ diff --git a/docs/tutorial/miscellany.rst b/docs/tutorial/miscellany.rst --- a/docs/tutorial/miscellany.rst +++ b/docs/tutorial/miscellany.rst @@ -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 ==================== diff --git a/docs/tutorial/modules.rst b/docs/tutorial/modules.rst --- a/docs/tutorial/modules.rst +++ b/docs/tutorial/modules.rst @@ -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. diff --git a/docs/tutorial/packages.rst b/docs/tutorial/packages.rst --- a/docs/tutorial/packages.rst +++ b/docs/tutorial/packages.rst @@ -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 ================ diff --git a/docs/tutorial/starting.rst b/docs/tutorial/starting.rst --- a/docs/tutorial/starting.rst +++ b/docs/tutorial/starting.rst @@ -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 `_. 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. diff --git a/docs/tutorial/theorems.rst b/docs/tutorial/theorems.rst --- a/docs/tutorial/theorems.rst +++ b/docs/tutorial/theorems.rst @@ -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, diff --git a/docs/tutorial/typesfuns.rst b/docs/tutorial/typesfuns.rst --- a/docs/tutorial/typesfuns.rst +++ b/docs/tutorial/typesfuns.rst @@ -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 `_). 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. diff --git a/docs/tutorial/views.rst b/docs/tutorial/views.rst --- a/docs/tutorial/views.rst +++ b/docs/tutorial/views.rst @@ -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 diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -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 diff --git a/libs/contrib/Control/ST.idr b/libs/contrib/Control/ST.idr --- a/libs/contrib/Control/ST.idr +++ b/libs/contrib/Control/ST.idr @@ -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: ", diff --git a/man/idris.1 b/man/idris.1 --- a/man/idris.1 +++ b/man/idris.1 @@ -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 diff --git a/rts/idris_main.c b/rts/idris_main.c --- a/rts/idris_main.c +++ b/rts/idris_main.c @@ -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) { diff --git a/rts/idris_rts.h b/rts/idris_rts.h --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -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) diff --git a/samples/tutorial/BMain.idr b/samples/tutorial/BMain.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/BMain.idr @@ -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) + diff --git a/samples/tutorial/BTree.idr b/samples/tutorial/BTree.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/BTree.idr @@ -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) + diff --git a/samples/tutorial/BTreeMod.idr b/samples/tutorial/BTreeMod.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/BTreeMod.idr @@ -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) diff --git a/samples/tutorial/Foo.idr b/samples/tutorial/Foo.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Foo.idr @@ -0,0 +1,10 @@ +module foo + +namespace x + test : Int -> Int + test x = x * 2 + +namespace y + test : String -> String + test x = x ++ x + diff --git a/samples/tutorial/Hello.idr b/samples/tutorial/Hello.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Hello.idr @@ -0,0 +1,5 @@ +module Main + +main : IO () +main = putStrLn "Hello world" + diff --git a/samples/tutorial/Idiom.idr b/samples/tutorial/Idiom.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Idiom.idr @@ -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 |] + diff --git a/samples/tutorial/Interfaces.idr b/samples/tutorial/Interfaces.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Interfaces.idr @@ -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) diff --git a/samples/tutorial/Interp.idr b/samples/tutorial/Interp.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Interp.idr @@ -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)) + diff --git a/samples/tutorial/LetBind.idr b/samples/tutorial/LetBind.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/LetBind.idr @@ -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) + diff --git a/samples/tutorial/Prims.idr b/samples/tutorial/Prims.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Prims.idr @@ -0,0 +1,14 @@ +module Prims + +x : Int +x = 42 + +foo : String +foo = "Sausage machine" + +bar : Char +bar = 'Z' + +quux : Bool +quux = False + diff --git a/samples/tutorial/Record.idr b/samples/tutorial/Record.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Record.idr @@ -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 + diff --git a/samples/tutorial/Theorems.idr b/samples/tutorial/Theorems.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Theorems.idr @@ -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) + diff --git a/samples/tutorial/Universe.idr b/samples/tutorial/Universe.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Universe.idr @@ -0,0 +1,7 @@ +myid : (a : Type) -> a -> a +myid _ x = x + +idid : (a : Type) -> a -> a +idid = myid _ myid + + diff --git a/samples/tutorial/UsefulTypes.idr b/samples/tutorial/UsefulTypes.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/UsefulTypes.idr @@ -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 + diff --git a/samples/tutorial/VBroken.idr b/samples/tutorial/VBroken.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/VBroken.idr @@ -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 + diff --git a/samples/tutorial/Views.idr b/samples/tutorial/Views.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Views.idr @@ -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 + diff --git a/samples/tutorial/ViewsBroken.idr b/samples/tutorial/ViewsBroken.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/ViewsBroken.idr @@ -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} + diff --git a/samples/tutorial/Wheres.idr b/samples/tutorial/Wheres.idr new file mode 100644 --- /dev/null +++ b/samples/tutorial/Wheres.idr @@ -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 + diff --git a/samples/tutorial/binary.idr b/samples/tutorial/binary.idr deleted file mode 100644 --- a/samples/tutorial/binary.idr +++ /dev/null @@ -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; -} - - diff --git a/samples/tutorial/bmain.idr b/samples/tutorial/bmain.idr deleted file mode 100644 --- a/samples/tutorial/bmain.idr +++ /dev/null @@ -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) - diff --git a/samples/tutorial/btree.idr b/samples/tutorial/btree.idr deleted file mode 100644 --- a/samples/tutorial/btree.idr +++ /dev/null @@ -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) - diff --git a/samples/tutorial/btreemod.idr b/samples/tutorial/btreemod.idr deleted file mode 100644 --- a/samples/tutorial/btreemod.idr +++ /dev/null @@ -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) diff --git a/samples/tutorial/classes.idr b/samples/tutorial/classes.idr deleted file mode 100644 --- a/samples/tutorial/classes.idr +++ /dev/null @@ -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) diff --git a/samples/tutorial/foo.idr b/samples/tutorial/foo.idr deleted file mode 100644 --- a/samples/tutorial/foo.idr +++ /dev/null @@ -1,10 +0,0 @@ -module foo - -namespace x - test : Int -> Int - test x = x * 2 - -namespace y - test : String -> String - test x = x ++ x - diff --git a/samples/tutorial/hello.idr b/samples/tutorial/hello.idr deleted file mode 100644 --- a/samples/tutorial/hello.idr +++ /dev/null @@ -1,5 +0,0 @@ -module Main - -main : IO () -main = putStrLn "Hello world" - diff --git a/samples/tutorial/idiom.idr b/samples/tutorial/idiom.idr deleted file mode 100644 --- a/samples/tutorial/idiom.idr +++ /dev/null @@ -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 |] - diff --git a/samples/tutorial/interp.idr b/samples/tutorial/interp.idr deleted file mode 100644 --- a/samples/tutorial/interp.idr +++ /dev/null @@ -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)) - diff --git a/samples/tutorial/letbind.idr b/samples/tutorial/letbind.idr deleted file mode 100644 --- a/samples/tutorial/letbind.idr +++ /dev/null @@ -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) - diff --git a/samples/tutorial/prims.idr b/samples/tutorial/prims.idr deleted file mode 100644 --- a/samples/tutorial/prims.idr +++ /dev/null @@ -1,14 +0,0 @@ -module prims - -x : Int -x = 42 - -foo : String -foo = "Sausage machine" - -bar : Char -bar = 'Z' - -quux : Bool -quux = False - diff --git a/samples/tutorial/theorems.idr b/samples/tutorial/theorems.idr deleted file mode 100644 --- a/samples/tutorial/theorems.idr +++ /dev/null @@ -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; -} - diff --git a/samples/tutorial/universe.idr b/samples/tutorial/universe.idr deleted file mode 100644 --- a/samples/tutorial/universe.idr +++ /dev/null @@ -1,7 +0,0 @@ -myid : (a : Type) -> a -> a -myid _ x = x - -idid : (a : Type) -> a -> a -idid = myid _ myid - - diff --git a/samples/tutorial/usefultypes.idr b/samples/tutorial/usefultypes.idr deleted file mode 100644 --- a/samples/tutorial/usefultypes.idr +++ /dev/null @@ -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 - diff --git a/samples/tutorial/vbroken.idr b/samples/tutorial/vbroken.idr deleted file mode 100644 --- a/samples/tutorial/vbroken.idr +++ /dev/null @@ -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 - diff --git a/samples/tutorial/views.idr b/samples/tutorial/views.idr deleted file mode 100644 --- a/samples/tutorial/views.idr +++ /dev/null @@ -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; -} - - diff --git a/samples/tutorial/viewsbroken.idr b/samples/tutorial/viewsbroken.idr deleted file mode 100644 --- a/samples/tutorial/viewsbroken.idr +++ /dev/null @@ -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} - diff --git a/samples/tutorial/wheres.idr b/samples/tutorial/wheres.idr deleted file mode 100644 --- a/samples/tutorial/wheres.idr +++ /dev/null @@ -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 - diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs --- a/src/IRTS/CodegenC.hs +++ b/src/IRTS/CodegenC.hs @@ -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) ++ ", " ++ diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs --- a/src/Idris/Core/Evaluate.hs +++ b/src/Idris/Core/Evaluate.hs @@ -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 diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs --- a/src/Idris/Core/TT.hs +++ b/src/Idris/Core/TT.hs @@ -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 diff --git a/src/Idris/DataOpts.hs b/src/Idris/DataOpts.hs --- a/src/Idris/DataOpts.hs +++ b/src/Idris/DataOpts.hs @@ -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] diff --git a/src/Idris/Elab/Implementation.hs b/src/Idris/Elab/Implementation.hs --- a/src/Idris/Elab/Implementation.hs +++ b/src/Idris/Elab/Implementation.hs @@ -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) diff --git a/stack-shell.nix b/stack-shell.nix --- a/stack-shell.nix +++ b/stack-shell.nix @@ -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 diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-8.04 +resolver: lts-8.06 packages: - location: . diff --git a/test/dsl001/expected b/test/dsl001/expected --- a/test/dsl001/expected +++ b/test/dsl001/expected @@ -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))) diff --git a/test/dsl001/input b/test/dsl001/input --- a/test/dsl001/input +++ b/test/dsl001/input @@ -1,2 +1,2 @@ :printdef testFac -:printdef PE_interp_e04a79ff +:printdef PE_interp_9b251b28 diff --git a/test/interactive010/expected b/test/interactive010/expected --- a/test/interactive010/expected +++ b/test/interactive010/expected @@ -4,9 +4,9 @@ Usage is :doc Usage is :wc Usage is :printdef -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 diff --git a/test/pkg001/expected b/test/pkg001/expected --- a/test/pkg001/expected +++ b/test/pkg001/expected @@ -11,7 +11,7 @@ -Elaborating {__Infer0} +Elaborating {__Infer_0} builtin Elaborating = builtin diff --git a/test/proof009/expected b/test/proof009/expected --- a/test/proof009/expected +++ b/test/proof009/expected @@ -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 diff --git a/test/reg027/expected b/test/reg027/expected --- a/test/reg027/expected +++ b/test/reg027/expected @@ -1,3 +1,2 @@ <> -6 reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined diff --git a/test/reg027/reg027.idr b/test/reg027/reg027.idr --- a/test/reg027/reg027.idr +++ b/test/reg027/reg027.idr @@ -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