Merge remote-tracking branch 'upstream/master' into wip/tactical

.gitignore

@@ -28,3 +28,4 @@ test/*[0-9][0-9][0-9]/*.exe
 tags
 TAGS
 src/Version_idris.hs
+.stack-work

CHANGELOG

@@ -24,6 +24,9 @@ New in 0.9.19:
 * More flexible 'case' construct, allowing each branch to target different
   types, provided that the case analysis does not affect the form of any
   variable used in the right hand side of the case.
+* Some improvements in interactive editing, particularly in lifting out
+  definitions and proof search.
+* Moved System.Interactive, along with getArgs to the Prelude.
 
 New in 0.9.18:
 --------------

docs/reference/syntax-guide.rst

@@ -29,7 +29,7 @@ Types
 
 In Idris, types are first class values. So a type declaration is the
 same as just declaration of a variable whose type is ``Type``. In Idris,
-variables that denote a type must being with a capital letter. Example:
+variables that denote a type must begin with a capital letter. Example:
 
 .. code:: idris
 
@@ -254,6 +254,15 @@ Comments
     -- Single Line
     {- Multiline -}
     ||| Docstring (goes before definition)
+    
+Multi line String literals
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+::
+
+    foo = """
+    this is a
+    string literal"""
 
 Directives
 ----------

docs/tutorial/classes.rst

@@ -363,10 +363,10 @@ alternative notion of function application, with explicit calls to
     m_add' x y = m_app (m_app (Just (+)) x) y
 
 Rather than having to insert ``m_app`` everywhere there is an
-application, we can use to do the job for us. To do this, we can make
+application, we can use idiom brackets to do the job for us.
-``Maybe`` an instance of ``Applicative`` as follows, where ``<*>`` is
+To do this, we can make ``Maybe`` an instance of ``Applicative``
-defined in the same way as ``m_app`` above (this is defined in the
+as follows, where ``<*>`` is defined in the same way as ``m_app``
-Idris library):
+above (this is defined in the Idris library):
 
 .. code-block:: idris
 

docs/tutorial/modules.rst

@@ -34,7 +34,7 @@ module which defines a binary tree type ``BTree`` (in a file
 
 
 Then, this gives a main program (in a file
-``bmain.idr``) which uses the ``bst`` module to sort a list:
+``bmain.idr``) which uses the ``Btree`` module to sort a list:
 
 .. code-block:: idris
 
@@ -50,7 +50,7 @@ Then, this gives a main program (in a file
 
 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 names defined in the ``Btree`` module are, in full:
 
 + ``Btree.BTree``
 + ``Btree.Leaf``
@@ -99,7 +99,7 @@ and classes to be marked as: ``public``, ``abstract`` or ``private``:
 .. note::
     If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
 
-For our ``btree`` module, it makes sense for the tree data type and the
+For our ``Btree`` module, it makes sense for the tree data type and the
 functions to be exported as ``abstract``, as we see below:
 
 .. code-block:: idris

docs/tutorial/packages.rst

@@ -54,9 +54,9 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile
   package only. This differs from build that type checks **and**
   generates code.
 
-+ ``idris --mathspkg maths.ipkg`` will compile and run any embedded
++ ``idris --testpkg maths.ipkg`` will compile and run any embedded
-  mathss you have specified in the ``tests`` paramater. More
+  tests you have specified in the ``tests`` paramater. More
-  information about mathsing is given in the next section.
+  information about testing is given in the next section.
 
 Once the maths package has been installed, the command line option
 ``--package maths`` makes it accessible (abbreviated to ``-p maths``).

docs/tutorial/testing.rst

@@ -4,18 +4,27 @@
 Testing Idris Packages
 **********************
 
-As part of the integrated build system a simple testing framework is provided.
+The integrated build system includes a simple testing framework.
-This framework will collect a list of named functions and construct an Idris executable in a fresh environment on your machine.
+This framework collects functions listed in the ``ipkg`` file under ``tests``.
-This executable lists the named functions under a single ``main`` function, and imports the complete list of modules for the package.
+All test functions must return ``IO ()``.
 
 
-It is up to the developer to ensure the correct reporting of test results, and the structure and nature of how the tests are run.
+When you enter ``idris --testpkg yourmodule.ipkg``,
-Further, all test functions must return ``IO ()``, and must be listed in the ``ipkg`` file under ``tests``, and rhe modules containing the test functions must also be listed in the modules section of the ``iPKG`` file.
+the build system creates a temporary file in a fresh environment on your machine
+by listing the ``tests`` functions under a single ``main`` function.
+It compiles this temporary file to an executable and then executes it.
+
+
+The tests themselves are responsible for reporting their success or failure.
+Test functions commonly use ``putStrLn`` to report test results.
+The test framework does not impose any standards for reporting and consequently
+does not aggregate test results.
 
 
 For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.
 
 .. code-block:: idris
+   :caption: Math/NumOps.idr
 
     module Maths.NumOps
 
@@ -28,6 +37,7 @@ For example, lets take the following list of functions that are defined in a mod
 A simple test module, with a qualified name of ``Test.NumOps`` can be declared as
 
 .. code-block:: idris
+   :caption: Math/TestOps.idr
 
     module Test.NumOps
 
@@ -36,12 +46,12 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
     assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
     assertEq g e = if g == e
         then putStrLn "Test Passed"
-        else putStrLn "Test failed"
+        else putStrLn "Test Failed"
 
     assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
     assertNotEq g e = if not (g == e)
         then putStrLn "Test Passed"
-        else putStrLn "Test failed"
+        else putStrLn "Test Failed"
 
     testDouble : IO ()
     testDouble = assertEq (double 2) 4
@@ -53,13 +63,23 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
 The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.
 The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::
 
-    module maths
+    package maths
 
-    module = Maths.NumOps
+    modules = Maths.NumOps
-           , Test.NumOps
+            , Test.NumOps
 
     tests = Test.NumOps.testDouble
           , Test.NumOps.testTriple
 
 
-The testing framework can be invoked using: ``idris --testpkg maths.ipkg``.
+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
+
+    > idris --testpkg maths.ipkg
+    Type checking ./Maths/NumOps.idr
+    Type checking ./Test/NumOps.idr
+    Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
+    Test Passed
+    Test Passed
+
+Note how both tests have reported success by printing ``Test Passed``
+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

docs/tutorial/typesfuns.rst

@@ -103,7 +103,7 @@ symbols:
 
 ::
 
-    :+-*/=_.?|&><!@$%^~.
+    :+-*\/=.?|&><!@$%^~#
 
 Some operators built from these symbols can't be user defined. These are
 ``:``,  ``=>``,  ``->``,  ``<-``,  ``=``,  ``?=``,  ``|``,  ``**``,
@@ -349,7 +349,7 @@ following:
     $ 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 
+        Type mismatch between
                 Vect (k + k) a (Type of xs ++ xs)
         and
                 Vect (plus k m) a (Expected type)
@@ -442,7 +442,7 @@ names, ``n`` and ``a``, which are not declared explicitly. These are
 Implicit arguments, given in braces ``{}`` in the type declaration,
 are not given in applications of ``index``; their values can be
 inferred from the types of the ``Fin n`` and ``Vect n a``
-arguments. Any name beginning with a lower case letter which appears 
+arguments. Any name beginning with a lower case letter which appears
 as a parameter or index in a
 type declaration, but which is otherwise unbound, will be automatically
 bound as an implicit argument. Implicit arguments can still be given
@@ -912,10 +912,6 @@ Intermediate values can be calculated using ``let`` bindings:
     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)
-
 We can do simple pattern matching in ``let`` bindings too. For
 example, we can extract fields from a record as follows, as well as by
 pattern matching at the top level:
@@ -1021,26 +1017,28 @@ example, we can represent a person's name and age in a record:
 
     record Person where
         constructor MkPerson
-        name : String
+        firstName, middleName, lastName : String
         age : Int
 
     fred : Person
-    fred = MkPerson "Fred" 30
+    fred = MkPerson "Fred" "Joe" "Bloggs" 30
 
 Records can have *parameters*, which are listed between the record
 name and the ``where`` keyword, and *fields*, which are in an indented
-block following the `where` keyword (here, ``name`` and ``age``). The
+block following the `where` keyword (here, ``firstName``, ``middleName``,
-constructor name is provided after the ``constructor`` keyword. The
+``lastName``, and ``age``). You can declare multiple fields on a single
-field names can be used to access the field values:
+line, provided that they have the same type. The constructor name is
+provided after the ``constructor`` keyword. The field names can be used to
+access the field values:
 
 ::
 
-    *record> name fred
+    *record> firstName fred
     "Fred" : String
     *record> age fred
     30 : Int
-    *record> :t name
+    *record> :t firstName
-    name : Person -> String
+    firstName : Person -> String
 
 We can also use the field names to update a record (or, more
 precisely, produce a copy of the record with the given fields
@@ -1048,10 +1046,10 @@ updated):
 
 .. code-block:: bash
 
-    *record> record { name = "Jim" } fred
+    *record> record { firstName = "Jim" } fred
-    MkPerson "Jim" 30 : Person
+    MkPerson "Jim" "Joe" "Bloggs" 30 : Person
-    *record> record { name = "Jim", age = 20 } fred
+    *record> record { firstName = "Jim", age = 20 } fred
-    MkPerson "Jim" 20 : Person
+    MkPerson "Jim" "Joe" "Bloggs" 20 : Person
 
 The syntax ``record { field = val, ... }`` generates a function which
 updates the given fields in a record.
@@ -1078,7 +1076,7 @@ length because it will not affect the type of the record:
 ::
 
     *record> addStudent fred (ClassInfo [] "CS")
-    ClassInfo [MkPerson "Fred" 30] "CS" : Class
+    ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
 
 Nested record update
 --------------------

idris.cabal

@@ -118,6 +118,7 @@ Extra-source-files:
                        libs/contrib/Data/*.idr
                        libs/contrib/Data/Nat/*.idr
                        libs/contrib/Data/Nat/DivMod/*.idr
+                       libs/contrib/Data/Matrix/*.idr
                        libs/contrib/Decidable/*.idr
                        libs/contrib/Network/*.idr
                        libs/contrib/System/Concurrency/*.idr
@@ -125,6 +126,7 @@ Extra-source-files:
                        libs/effects/Makefile
                        libs/effects/effects.ipkg
                        libs/effects/Effect/*.idr
+		       libs/effects/Effect/Logging/*.idr
                        libs/effects/*.idr
 
                        test/Makefile
@@ -388,9 +390,6 @@ Extra-source-files:
                        test/delab001/expected
                        test/delab001/input
 
-                       test/disambig001/run
-                       test/disambig001/*.idr
-                       test/disambig001/expected
                        test/disambig002/run
                        test/disambig002/*.idr
                        test/disambig002/expected
@@ -424,6 +423,10 @@ Extra-source-files:
                        test/effects004/*.idr
                        test/effects004/expected
                        test/effects004/input
+                       test/effects005/run
+                       test/effects005/*.idr
+                       test/effects005/expected
+
 
                        test/error001/run
                        test/error001/*.idr

libs/base/Data/Complex.idr

@@ -27,7 +27,6 @@ instance Show a => Show (Complex a) where
             plus_i = User 6
 
 
-
 -- when we have a type class 'Fractional' (which contains Float and Double),
 -- we can do:
 {-
@@ -61,6 +60,12 @@ phase (x:+y) = atan2 y x
 conjugate : Num a => Complex a -> Complex a
 conjugate (r:+i) = (r :+ (0-i))
 
+instance Functor Complex where
+  map f (r :+ i) = f r :+ f i
+
+instance Neg a => Neg (Complex a) where
+  negate = map negate
+
 -- We can't do "instance Num a => Num (Complex a)" because
 -- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
 instance Num (Complex Float) where

libs/base/Data/HVect.idr

@@ -1,6 +1,5 @@
 module Data.HVect
 
-import Data.Fin
 import public Data.Vect
 
 %access public

libs/base/Data/Vect.idr

@@ -52,3 +52,30 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
 mapElem Here = Here
 mapElem (There e) = There (mapElem e)
 
+-- Some convenience functions for testing lengths
+
+||| If the given Vect is the required length, return a Vect with that
+||| length in its type, otherwise return Nothing
+||| @len the required length
+||| @xs the vector with the desired length
+-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we 
+-- only know we don't know how to make a Vect n a, not that one can't exist.
+isLength : {m : Nat} -> -- expected at run-time
+           (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
+isLength {m} len xs with (decEq m len)
+  isLength {m = m} m xs | (Yes Refl) = Just xs
+  isLength {m = m} len xs | (No contra) = Nothing
+
+||| If the given Vect is at least the required length, return a Vect with
+||| at least that length in its type, otherwise return Nothing
+||| @len the required length
+||| @xs the vector with the desired length
+overLength : {m : Nat} -> -- expected at run-time
+             (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
+overLength {m} n xs with (cmp m n)
+  overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
+  overLength {m = m} m xs | CmpEQ
+         = Just (0 ** xs)
+  overLength {m = plus n (S x)} n xs | (CmpGT x)
+         = Just (S x ** rewrite plusCommutative (S x) n in xs)
+

libs/base/Data/VectType.idr

@@ -1,6 +1,6 @@
 module Data.VectType
 
-import Data.Fin
+import public Data.Fin
 
 %access public
 %default total
@@ -9,9 +9,14 @@ namespace Vect {
 
 infixr 7 ::
 
-%elim data Vect : Nat -> Type -> Type where
+||| Vectors: Generic lists with explicit length in the type
+%elim 
+data Vect : Nat -> Type -> Type where
+  ||| Empty vector 
   Nil  : Vect Z a
-  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
+  ||| A non-empty vector of length `S k`, consisting of a head element and 
+  ||| the rest of the list, of length `k`.
+  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
 
 -- Hints for interactive editing
 %name Vect xs,ys,zs,ws

libs/base/System.idr

@@ -4,22 +4,6 @@ module System
 %default partial
 %access public
 
-||| Get the command-line arguments that the program was called with.
-getArgs : IO (List String)
-getArgs = do n <- numArgs
-             ga' [] 0 n
-  where
-    numArgs : IO Int
-    numArgs = foreign FFI_C "idris_numArgs" (IO Int)
-
-    getArg : Int -> IO String
-    getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x
-
-    ga' : List String -> Int -> Int -> IO (List String)
-    ga' acc i n = if (i == n) then (return $ reverse acc) else
-                    do arg <- getArg i
-                       ga' (arg :: acc) (i+1) n
-
 ||| Retrieves an value from the environment, if the given key is present,
 ||| otherwise it returns Nothing.
 getEnv : String -> IO (Maybe String)

libs/base/base.ipkg

@@ -5,7 +5,7 @@ modules = System,
 
           Debug.Error, Debug.Trace,
 
-          System.Info, System.Interactive,
+          System.Info, 
 
           Language.Reflection.Utils,
 

libs/contrib/Control/Algebra.idr

@@ -54,7 +54,7 @@ class Group a => AbelianGroup a where { }
 |||     forall a,     inverse a <+> a == neutral
 ||| + Associativity of `<.>`:
 |||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
-||| + Distributivity of `<.>` and `<->`:
+||| + Distributivity of `<.>` and `<+>`:
 |||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
 |||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
 class AbelianGroup a => Ring a where
@@ -80,7 +80,7 @@ class AbelianGroup a => Ring a where
 ||| + Neutral for `<.>`:
 |||     forall a,     a <.> unity     == a
 |||     forall a,     unity <.> a     == a
-||| + Distributivity of `<.>` and `<->`:
+||| + Distributivity of `<.>` and `<+>`:
 |||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
 |||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
 class Ring a => RingWithUnity a where
@@ -109,21 +109,21 @@ class Ring a => RingWithUnity a where
 ||| + InverseM of `<.>`, except for neutral
 |||     forall a /= neutral,  a <.> inverseM a == unity
 |||     forall a /= neutral,  inverseM a <.> a == unity
-||| + Distributivity of `<.>` and `<->`:
+||| + Distributivity of `<.>` and `<+>`:
 |||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
 |||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
 class RingWithUnity a => Field a where
   inverseM : (x : a) -> Not (x = neutral) -> a
 
-sum : (Foldable t, Monoid a) => t a -> a
+sum' : (Foldable t, Monoid a) => t a -> a
-sum = foldr (<+>) neutral
+sum' = concat
 
-product : (Foldable t, RingWithUnity a) => t a -> a
+product' : (Foldable t, RingWithUnity a) => t a -> a
-product = foldr (<.>) unity
+product' = foldr (<.>) unity
 
-power : RingWithUnity a => a -> Nat -> a
+pow' : RingWithUnity a => a -> Nat -> a
-power _ Z     = unity
+pow' _ Z     = unity
-power x (S n) = x <.> (Algebra.power x n)
+pow' x (S n) = x <.> pow' x n
 
 
 -- XXX todo:

libs/contrib/Control/Algebra/NumericInstances.idr

@@ -1,6 +1,9 @@
+||| Instances of algebraic classes (group, ring, etc) for numeric data types,
+||| and Complex number types.
 module Control.Algebra.NumericInstances
 
 import Control.Algebra
+import Control.Algebra.VectorSpace
 import Data.Complex
 import Data.ZZ
 
@@ -102,3 +105,9 @@ instance Ring a => Ring (Complex a) where
 
 instance RingWithUnity a => RingWithUnity (Complex a) where
   unity = (unity :+ neutral)
+
+instance RingWithUnity a => Module a (Complex a) where
+  (<#>) x = map (x <.>)
+
+instance RingWithUnity a => InnerProductSpace a (Complex a) where
+  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z

libs/contrib/Data/Matrix.idr

@@ -1,150 +1,58 @@
+||| Basic matrix operations with dimensionalities enforced
+||| at the type level
 module Data.Matrix
 
-import        Control.Algebra
+import public Data.Vect
-import        Control.Algebra.VectorSpace
-import public Control.Algebra.NumericInstances
-
-import Data.Complex
-import Data.ZZ
-import Data.Fin
-import Data.Vect
 
 %default total
 
-infixr 2 <:>  -- vector inner product
-infixr 2 ><   -- vector outer product
-infixr 2 <<>> -- matrix commutator
-infixr 2 >><< -- matrix anticommutator
-infixl 3 <\>  -- row times a matrix
-infixr 4 </>  -- matrix times a column
-infixr 5 <>   -- matrix multiplication
-infixr 7 \&\  -- vector tensor product
-infixr 7 <&>  -- matrix tensor product
-
------------------------------------------------------------------------
---               Vectors as members of algebraic classes
------------------------------------------------------------------------
-
-instance Semigroup a => Semigroup (Vect n a) where
-  (<+>) v w = zipWith (<+>) v w
-
-instance Monoid a => Monoid (Vect n a) where
-  neutral {n} = replicate n neutral
-
-instance Group a => Group (Vect n a) where
-  inverse = map inverse
-
-instance AbelianGroup a => AbelianGroup (Vect n a) where {}
-
-instance Ring a => Ring (Vect n a) where
-  (<.>) v w = zipWith (<.>) v w
-
-instance RingWithUnity a => RingWithUnity (Vect n a) where
-  unity {n} = replicate n unity
-
---instance Field a => Field (Vect n a) where
-
-instance RingWithUnity a => Module a (Vect n a) where
-  (<#>) r v = map (r <.>) v
-
-instance RingWithUnity a => Module a (Vect n (Vect l a)) where
-  (<#>) r m = map (r <#>) m
--- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'
-
------------------------------------------------------------------------
---                       (Ring) Vector functions
------------------------------------------------------------------------
-
-||| Inner product of ring vectors
-(<:>) : Ring a => Vect n a -> Vect n a -> a
-(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)
-
-||| Tensor multiply (⊗) ring vectors
-(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
-(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
-  orep : (n : Nat) -> Vect m a -> Vect (n * m) a
-  orep n v = concat $ replicate n v
-  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
-  oextend n w = concat $ map (replicate n) w
-
-||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
-basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
-basis i = replaceAt i unity $ neutral
-
------------------------------------------------------------------------
---                          Matrix functions
------------------------------------------------------------------------
-
 ||| Matrix with n rows and m columns
 Matrix : Nat -> Nat -> Type -> Type
 Matrix n m a = Vect n (Vect m a)
 
-||| Gets the specified column of a matrix. For rows use the vector function 'index'
+||| Get the specified column of a matrix
 getCol : Fin m -> Matrix n m a -> Vect n a
-getCol fm q = map (index fm) q
+getCol f = map (index f)
 
-||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'
+||| Get the specified row of a matrix
+getRow : Fin n -> Matrix n m a -> Vect m a
+getRow = index
+
+||| Delete the specified column of a matrix
 deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a
-deleteCol f m = map (deleteAt f) m
+deleteCol f = map (deleteAt f)
+
+||| Delete the specified row of a matrix
+deleteRow : Fin (S n) -> Matrix (S n) m a -> Matrix n m a
+deleteRow = deleteAt
+
+insertRow : Fin (S n) -> Vect m a -> Matrix n m a -> Matrix (S n) m a
+insertRow = insertAt
+
+insertCol : Fin (S m) -> Vect n a -> Matrix n m a -> Matrix n (S m) a
+insertCol f = zipWith (insertAt f)
 
 ||| Matrix element at specified row and column indices
 indices : Fin n -> Fin m -> Matrix n m a -> a
-indices f1 f2 m = index f2 (index f1 m)
+indices f1 f2 = index f2 . index f1
-
-||| Matrix times a column vector
-(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
-(</>) m v = map (v <:>) m
-
-||| Matrix times a row vector
-(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
-(<\>) r m = map (r <:>) $ transpose m
-
-||| Matrix multiplication
-(<>) : Ring a => Matrix n k a ->
-                 Matrix k m a ->
-                 Matrix n m a
-(<>) m1 m2 = map (<\> m2) m1
-
-||| Tensor multiply (⊗) for ring matrices
-(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
-(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
-  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
-  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
-  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
-  stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
 
 ||| Cast a vector from a standard Vect to a proper n x 1 matrix
 col : Vect n a -> Matrix n 1 a
-col v = map (\x => [x]) v
+col = map (\x => [x])
 
 ||| Cast a row from a standard Vect to a proper 1 x n matrix
 row : Vect n a -> Matrix 1 n a
 row r = [r]
 
-||| Outer product between ring vectors
+||| Matrix formed by deleting specified row and col
-(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
+subMatrix : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) a -> Matrix n m a
-(><) x y = (col x) <> (row y)
+subMatrix r c = deleteRow r . deleteCol c
 
-||| All finite numbers up to the given bound
+||| Flatten a matrix of matrices
-allN : (n : Nat) -> Vect n (Fin n)
+concatMatrix : Matrix n m (Matrix x y a) -> Matrix (n * x) (m * y) a
-allN Z     = Nil
+concatMatrix = Vect.concat . map (map Vect.concat) . map transpose
-allN (S n) = FZ :: (map FS $ allN n)
-
-||| Identity matrix
-Id : RingWithUnity a => {d : Nat} -> Matrix d d a
-Id {d} = map (\n => basis n) $ allN d
-
-||| Matrix commutator
-(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
-(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
-
-||| Matrix anti-commutator
-(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
-(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
-
------------------------------------------------------------------------
---                      Matrix Algebra Properties
------------------------------------------------------------------------
-
--- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
 
+||| All finite numbers of the specified level
+fins : (n : Nat) -> Vect n (Fin n)
+fins Z     = Nil
+fins (S n) = FZ :: (map FS $ fins n)

libs/contrib/Data/Matrix/Algebraic.idr

@@ -0,0 +1,149 @@
+||| Matrix operations with vector space dimensionalities enforced
+||| at the type level. Uses operations from classes in `Control.Algebra`
+||| and `Control.Algebra.VectorSpace`.
+module Data.Matrix.Algebraic
+
+import public Control.Algebra
+import public Control.Algebra.VectorSpace
+import public Control.Algebra.NumericInstances
+
+import public Data.Matrix
+
+
+%default total
+
+infixr 2 <:>  -- vector inner product
+infixr 2 ><   -- vector outer product
+infixr 2 <<>> -- matrix commutator
+infixr 2 >><< -- matrix anticommutator
+infixl 3 <\>  -- row times a matrix
+infixr 4 </>  -- matrix times a column
+infixr 5 <>   -- matrix multiplication
+infixr 7 \&\  -- vector tensor product
+infixr 7 <&>  -- matrix tensor product
+
+-----------------------------------------------------------------------
+--               Vectors as members of algebraic classes
+-----------------------------------------------------------------------
+
+instance Semigroup a => Semigroup (Vect n a) where
+  (<+>)= zipWith (<+>)
+
+instance Monoid a => Monoid (Vect n a) where
+  neutral {n} = replicate n neutral
+
+instance Group a => Group (Vect n a) where
+  inverse = map inverse
+
+instance AbelianGroup a => AbelianGroup (Vect n a) where {}
+
+instance Ring a => Ring (Vect n a) where
+  (<.>) = zipWith (<.>)
+
+instance RingWithUnity a => RingWithUnity (Vect n a) where
+  unity {n} = replicate n unity
+
+instance RingWithUnity a => Module a (Vect n a) where
+  (<#>) r = map (r <.>)
+
+instance RingWithUnity a => Module a (Vect n (Vect l a)) where
+  (<#>) r = map (r <#>)
+-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'
+
+-----------------------------------------------------------------------
+--                        (Ring) Vector functions
+-----------------------------------------------------------------------
+
+||| Inner product of ring vectors
+(<:>) : Ring a => Vect n a -> Vect n a -> a
+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)
+
+||| Tensor multiply (⊗) ring vectors
+(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
+  orep : (n : Nat) -> Vect m a -> Vect (n * m) a
+  orep n v = concat $ replicate n v
+  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
+  oextend n w = concat $ map (replicate n) w
+
+||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
+basis : RingWithUnity a => (Fin d) -> Vect d a
+basis i = replaceAt i unity neutral
+
+-----------------------------------------------------------------------
+--                         Ring Matrix functions
+-----------------------------------------------------------------------
+
+||| Matrix times a column vector
+(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
+(</>) m v = map (v <:>) m
+
+||| Matrix times a row vector
+(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
+(<\>) r m = map (r <:>) $ transpose m
+
+||| Matrix multiplication
+(<>) : Ring a => Matrix n k a ->
+                 Matrix k m a ->
+                 Matrix n m a
+(<>) m1 m2 = map (<\> m2) m1
+
+||| Tensor multiply (⊗) for ring matrices
+(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
+  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
+  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
+  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
+  stepTwo {h1} m1 m2 = concat $ replicate h1 m2
+
+||| Outer product between ring vectors
+(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
+(><) x y = col x <> row y
+
+||| Matrix commutator
+(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
+(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)
+
+||| Matrix anti-commutator
+(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
+(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
+
+||| Identity matrix
+Id : RingWithUnity a => Matrix d d a
+Id = map (\n => basis n) (fins _)
+
+||| Square matrix from diagonal elements
+diag_ : Monoid a => Vect n a -> Matrix n n a
+diag_ = zipWith (\f => \x => replaceAt f x neutral) (fins _)
+
+||| Combine two matrices to make a new matrix in block diagonal form
+blockDiag : Monoid a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a
+blockDiag g h = map (++ replicate _ neutral) g ++ map ((replicate _ neutral) ++) h
+
+
+-----------------------------------------------------------------------
+--                           Determinants
+-----------------------------------------------------------------------
+
+||| Alternating sum
+altSum : Group a => Vect n a -> a
+altSum (x::y::zs) = (x <-> y) <+> altSum zs
+altSum [x]        = x
+altSum []         = neutral
+
+||| Determinant of a 2-by-2 matrix
+det2 : Ring a => Matrix 2 2 a -> a
+det2 [[x1,x2],[y1,y2]] = x1 <.> y2 <-> x2 <.> y1
+
+||| Determinant of a square matrix
+det : Ring a => Matrix (S (S n)) (S (S n)) a -> a
+det {n} m = case n of
+  Z     => det2 m
+  (S k) => altSum . map (\c => indices FZ c m <.> det (subMatrix FZ c m))
+         $ fins (S (S (S k)))
+
+-----------------------------------------------------------------------
+--                      Matrix Algebra Properties
+-----------------------------------------------------------------------
+
+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes

libs/contrib/Data/Matrix/Numeric.idr

@@ -0,0 +1,129 @@
+||| Matrix operations with vector space dimensionalities enforced
+||| at the type level. Uses operations from the Num type class.
+module Data.Matrix.Numeric
+
+import public Data.Matrix
+
+%default total
+
+infixr 2 <:>  -- vector inner product
+infixr 2 ><   -- vector outer product
+infixr 2 <<>> -- matrix commutator
+infixr 2 >><< -- matrix anticommutator
+infixl 3 <\>  -- row times a matrix
+infixr 4 </>  -- matrix times a column
+infixr 5 <>   -- matrix multiplication
+infixl 5 <#>  -- matrix rescale
+infixl 5 <#   -- vector rescale
+infixr 7 \&\  -- vector tensor product
+infixr 7 <&>  -- matrix tensor product
+
+-----------------------------------------------------------------------
+--                   Vectors as members of Num
+-----------------------------------------------------------------------
+
+instance Num a => Num (Vect n a) where
+  (+) = zipWith (+)
+  (-) = zipWith (+)
+  (*) = zipWith (*)
+  abs = id
+  fromInteger n = replicate _ (fromInteger n)
+
+-----------------------------------------------------------------------
+--                        Vector functions
+-----------------------------------------------------------------------
+
+||| Inner product of ring vectors
+(<:>) : Num a => Vect n a -> Vect n a -> a
+(<:>) w v = sum $ zipWith (*) w v
+
+||| Scale a numeric vector by a scalar
+(<#) : Num a => a -> Vect n a -> Vect n a
+(<#) r = map (r *)
+
+||| Tensor multiply (⊗) numeric vectors
+(\&\) : Num a => Vect n a -> Vect m a -> Vect (n * m) a
+(\&\) {n} {m} v w = zipWith (*) (oextend m v) (orep n w) where
+  orep : (n : Nat) -> Vect m a -> Vect (n * m) a
+  orep n v = concat $ replicate n v
+  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
+  oextend n w = concat $ map (replicate n) w
+
+||| Standard basis vector with one nonzero entry, numeric data type and vector-length unfixed
+basis : Num a => (Fin d) -> Vect d a
+basis i = replaceAt i 1 0
+
+-----------------------------------------------------------------------
+--                          Matrix functions
+-----------------------------------------------------------------------
+
+||| Matrix times a column vector
+(</>) : Num a => Matrix n m a -> Vect m a -> Vect n a
+(</>) m v = map (v <:>) m
+
+||| Matrix times a row vector
+(<\>) : Num a => Vect n a -> Matrix n m a -> Vect m a
+(<\>) r m = map (r <:>) $ transpose m
+
+||| Matrix multiplication
+(<>) : Num a => Matrix n k a ->
+                Matrix k m a ->
+                Matrix n m a
+(<>) m1 m2 = map (<\> m2) m1
+
+||| Scale matrix by a scalar
+(<#>) : Num a => a -> Matrix n m a -> Matrix n m a
+(<#>) r = map (r <#)
+
+||| Tensor multiply (⊗) for numeric matrices
+(<&>) : Num a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
+  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
+  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
+  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
+  stepTwo {h1} m1 m2 = concat $ replicate h1 m2
+
+||| Outer product between numeric vectors
+(><) : Num a => Vect n a -> Vect m a -> Matrix n m a
+(><) x y = col x <> row y
+
+||| Matrix commutator
+(<<>>) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a
+(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)
+
+||| Matrix anti-commutator
+(>><<) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a
+(>><<) m1 m2 = (m1 <> m2) + (m2 <> m1)
+
+||| Identity matrix
+Id : Num a => Matrix d d a
+Id = map (\n => basis n) (fins _)
+
+||| Square matrix from diagonal elements
+diag_ : Num a => Vect n a -> Matrix n n a
+diag_ = zipWith (\f => \x => replaceAt f x 0) (fins _)
+
+||| Combine two matrices to make a new matrix in block diagonal form
+blockDiag : Num a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a
+blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h
+
+-----------------------------------------------------------------------
+--                           Determinants
+-----------------------------------------------------------------------
+
+||| Alternating sum
+altSum : Num a => Vect n a -> a
+altSum (x::y::zs) = (x - y) + altSum zs
+altSum [x]        = x
+altSum []         = 0
+
+||| Determinant of a 2-by-2 matrix
+det2 : Num a => Matrix 2 2 a -> a
+det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1
+
+||| Determinant of a square matrix
+det : Num a => Matrix (S (S n)) (S (S n)) a -> a
+det {n} m = case n of
+  Z     => det2 m
+  (S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))
+         $ fins (S (S (S k)))

libs/contrib/contrib.ipkg

@@ -9,7 +9,8 @@ modules = Control.Algebra,
           Control.WellFounded,
           Classes.Verified,
           Data.Fun, Data.Rel,
-          Data.Hash, Data.Matrix,
+          Data.Hash,
+          Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,
           Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,
           Data.ZZ, Data.Sign,
           Data.BoundedList,

libs/effects/Effect/Logging/Default.idr

@@ -0,0 +1,57 @@
+-- ------------------------------------------------------------- [ Default.idr ]
+-- Module    : Default.idr
+-- Copyright : (c) The Idris Community
+-- License   : see LICENSE
+-- --------------------------------------------------------------------- [ EOH ]
+
+||| A logging effect that allows messages to be logged using both
+||| numerical levels and user specified categories. The higher the
+||| logging level the grater in verbosity the logging.
+|||
+||| In this effect the resource we are computing over is the logging
+||| level itself and the list of categories to show.
+|||
+module Effect.Logging.Default
+
+import Effects
+import public Effect.Logging.Level
+
+import Control.IOExcept -- TODO Add IOExcept Logger.
+
+||| A Logging effect to log levels and categories.
+data Logging : Effect where
+    Log : (Eq a, Show a) =>
+          (lvl : Nat)
+       -> (cats : List a)
+       -> (msg : String)
+       -> Logging () (Nat,List a) (\v => (Nat,List a))
+
+||| The Logging effect.
+|||
+||| @cTy The type used to differentiate categories.
+LOG : (cTy : Type) -> EFFECT
+LOG a = MkEff (Nat, List a) Logging
+
+instance Handler Logging IO where
+    handle (l,cs) (Log lvl cs' msg) k = do
+      case lvl <= l  of
+        False => k () (l,cs)
+        True  =>  do
+          let res = and $ map (\x => elem x cs') cs
+          let prompt = if isNil cs then "" else show cs
+          if res || isNil cs
+            then do
+              printLn $ unwords [show lvl, ":", prompt, ":", msg]
+              k () (l,cs)
+            else k () (l,cs)
+
+||| Log the given message at the given level and assign it the list of categories.
+|||
+||| @l The logging level.
+||| @cs The logging categories.
+||| @m THe message to be logged.
+log : (Show a, Eq a) => (l : Nat)
+    -> (cs : List a) -> (m : String) -> Eff () [LOG a]
+log lvl cs msg = call $ Log lvl cs msg
+
+-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Logging/Level.idr

@@ -0,0 +1,49 @@
+-- -------------------------------------------------------------- [ Levels.idr ]
+-- Module    : Levels.idr
+-- Copyright : (c) Jan de Muijnck-Hughes
+-- License   : see LICENSE
+-- --------------------------------------------------------------------- [ EOH ]
+||| Common aliases and definitions of Logging Levels.
+module Effect.Logging.Level
+
+%access public
+-- ---------------------------------------------- [ Nat Derived Logging Levels ]
+--
+-- Several aliases have been defined to aide in semantic use of the
+-- logging levels. These aliases have come from the Log4j family of
+-- loggers.
+
+||| No events will be logged.
+OFF : Nat
+OFF = 0
+
+||| A severe error that will prevent the application from continuing.
+FATAL : Nat
+FATAL = 1
+
+||| An error in the application, possibly recoverable.
+ERROR : Nat
+ERROR = 2
+
+||| An event that might possible lead to an error.
+WARN : Nat
+WARN = 3
+
+|||  An event for informational purposes.
+INFO : Nat
+INFO = 4
+
+||| A general debugging event.
+DEBUG : Nat
+DEBUG = 5
+
+||| A fine-grained debug message, typically capturing the flow through
+||| the application.
+TRACE : Nat
+TRACE = 6
+
+||| All events should be logged.
+ALL : Nat
+ALL = 7
+
+-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Logging/Simple.idr

@@ -0,0 +1,48 @@
+-- -------------------------------------------------------------- [ Simple.idr ]
+-- Module    : Logging.idr
+-- Copyright : (c) The Idris Community
+-- License   : see LICENSE
+--------------------------------------------------------------------- [ EOH ]
+
+||| A simple logging effect that allows messages to be logged at
+||| different numerical level. The higher the number the grater in
+||| verbosity the logging.
+|||
+||| In this effect the resource we are computing over is the logging
+||| level itself.
+|||
+module Effect.Logging.Simple
+
+import Effects
+import public Effect.Logging.Level
+
+import Control.IOExcept -- TODO Add IO Logging Handler
+
+||| A Logging effect that displays a logging message to be logged at a
+||| certain level.
+data Logging : Effect where
+    Log : (lvl : Nat)
+       -> (msg : String)
+       -> Logging () Nat (\v => Nat)
+
+||| A Logging Effect.
+LOG : EFFECT
+LOG = MkEff Nat Logging
+
+-- For logging in the IO context
+instance Handler Logging IO where
+    handle l (Log lvl msg) k = do
+      case lvl <= l  of
+        False   => k () l
+        True  =>  do
+          printLn $ unwords [show lvl, ":", msg]
+          k () l
+
+||| Log `msg` at the given level.
+|||
+||| @l The level to log.
+||| @m The message to log.
+log : (l : Nat) -> (m : String) -> Eff () [LOG]
+log lvl msg = call $ Log lvl msg
+
+-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Random.idr

@@ -2,7 +2,6 @@ module Effect.Random
 
 import Effects
 import Data.Vect
-import Data.Fin
 
 data Random : Effect where 
      getRandom : sig Random Integer Integer

libs/effects/effects.ipkg

@@ -1,9 +1,20 @@
 package effects
 
 opts    = "--nobasepkgs -i ../prelude -i ../base"
-modules = Effects, Effect.Default, Effect.Monad,
 
-          Effect.Exception, Effect.File, Effect.State,
+modules = Effects
-          Effect.Random, Effect.StdIO, Effect.Select,
+        , Effect.Default
-          Effect.Memory, Effect.System, Effect.Trans
+        , Effect.Monad
 
+        , Effect.Exception
+        , Effect.File
+        , Effect.State
+        , Effect.Random
+        , Effect.StdIO
+        , Effect.Select
+        , Effect.Memory
+        , Effect.System
+        , Effect.Trans
+        , Effect.Logging.Level
+        , Effect.Logging.Simple
+        , Effect.Logging.Default

libs/prelude/IO.idr

@@ -253,7 +253,7 @@ namespace FFI_Export
   %used FFI_Prim prim
 
   data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
-       FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
+       FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
        FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
        FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
 

libs/prelude/Prelude.idr

@@ -25,6 +25,8 @@ import public Prelude.Pairs
 import public Prelude.Stream
 import public Prelude.Providers
 import public Prelude.Show
+import public Prelude.Interactive
+import public Prelude.File
 import public Decidable.Equality
 import public Language.Reflection
 import public Language.Reflection.Errors
@@ -43,9 +45,6 @@ decAsBool (No _)  = False
 instance Functor PrimIO where
     map f io = prim_io_bind io (prim_io_return . f)
 
-instance Functor (IO' ffi) where
-    map f io = io_bind io (\b => io_return (f b))
-
 instance Functor Maybe where
     map f (Just x) = Just (f x)
     map f Nothing  = Nothing
@@ -61,12 +60,6 @@ instance Applicative PrimIO where
 
     am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
 
-instance Applicative (IO' ffi) where
-    pure x = io_return x
-    f <*> a = io_bind f (\f' =>
-                io_bind a (\a' =>
-                  io_return (f' a')))
-
 instance Applicative Maybe where
     pure = Just
 
@@ -103,9 +96,6 @@ instance Alternative List where
 instance Monad PrimIO where
     b >>= k = prim_io_bind b k
 
-instance Monad (IO' ffi) where
-    b >>= k = io_bind b k
-
 instance Monad Maybe where
     Nothing  >>= k = Nothing
     (Just x) >>= k = k x
@@ -229,183 +219,6 @@ curry f a b = f (a, b)
 uncurry : (a -> b -> c) -> (a, b) -> c
 uncurry f (a, b) = f a b
 
----- some basic io
-
-||| Output a string to stdout without a trailing newline
-putStr : String -> IO' ffi ()
-putStr x = do prim_write x
-              return ()
-
-||| Output a string to stdout with a trailing newline
-putStrLn : String -> IO' ffi ()
-putStrLn x = putStr (x ++ "\n")
-
-||| Output something showable to stdout, without a trailing newline
-partial
-print : Show a => a -> IO' ffi ()
-print x = putStr (show x)
-
-||| Output something showable to stdout, with a trailing newline
-partial
-printLn : Show a => a -> IO' ffi ()
-printLn x = putStrLn (show x)
-
-||| Read one line of input from stdin, without the trailing newline
-partial
-getLine : IO' ffi String
-getLine = do x <- prim_read
-             return (reverse (trimNL (reverse x)))
-  where trimNL : String -> String
-        trimNL str with (strM str)
-          trimNL "" | StrNil = ""
-          trimNL (strCons '\n' xs) | StrCons _ _ = xs
-          trimNL (strCons x xs)    | StrCons _ _ = strCons x xs
-
-||| Write a single character to stdout
-partial
-putChar : Char -> IO ()
-putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)
-
-||| Write a singel character to stdout, with a trailing newline
-partial
-putCharLn : Char -> IO ()
-putCharLn c = putStrLn (singleton c)
-
-||| Read a single character from stdin
-partial
-getChar : IO Char
-getChar = map cast $ foreign FFI_C "getchar" (IO Int)
-
----- some basic file handling
-
-||| A file handle
-abstract
-data File = FHandle Ptr
-
-||| Standard input
-stdin : File
-stdin = FHandle prim__stdin
-
-||| Standard output
-stdout : File
-stdout = FHandle prim__stdout
-
-||| Standard output
-stderr : File
-stderr = FHandle prim__stderr
-
-||| Call the RTS's file opening function
-do_fopen : String -> String -> IO Ptr
-do_fopen f m
-   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
-
-||| Open a file
-||| @ f the filename
-||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
-fopen : (f : String) -> (m : String) -> IO File
-fopen f m = do h <- do_fopen f m
-               return (FHandle h)
-
-||| Modes for opening files
-data Mode = Read | Write | ReadWrite
-
-||| Open a file
-||| @ f the filename
-||| @ m the mode
-partial
-openFile : (f : String) -> (m : Mode) -> IO File
-openFile f m = fopen f (modeStr m) where
-  modeStr Read  = "r"
-  modeStr Write = "w"
-  modeStr ReadWrite = "r+"
-
-partial
-do_fclose : Ptr -> IO ()
-do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
-
-partial
-closeFile : File -> IO ()
-closeFile (FHandle h) = do_fclose h
-
-partial
-do_fread : Ptr -> IO' l String
-do_fread h = prim_fread h
-
-fgetc : File -> IO Char
-fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))
-
-fgetc' : File -> IO (Maybe Char)
-fgetc' (FHandle h)
-   = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h
-        if (x < 0) then return Nothing
-                   else return (Just (cast x))
-
-fflush : File -> IO ()
-fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
-
-do_popen : String -> String -> IO Ptr
-do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
-
-popen : String -> Mode -> IO File
-popen f m = do ptr <- do_popen f (modeStr m)
-               return (FHandle ptr)
-  where
-    modeStr Read  = "r"
-    modeStr Write = "w"
-    modeStr ReadWrite = "r+"
-
-pclose : File -> IO ()
-pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
-
--- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
---                        prim__vm h
-
-partial
-fread : File -> IO' l String
-fread (FHandle h) = do_fread h
-
-partial
-do_fwrite : Ptr -> String -> IO ()
-do_fwrite h s = do prim_fwrite h s
-                   return ()
-
-partial
-fwrite : File -> String -> IO ()
-fwrite (FHandle h) s = do_fwrite h s
-
-partial
-do_feof : Ptr -> IO Int
-do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
-
-||| Check if a file handle has reached the end
-feof : File -> IO Bool
-feof (FHandle h) = do eof <- do_feof h
-                      return (not (eof == 0))
-
-partial
-do_ferror : Ptr -> IO Int
-do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
-
-ferror : File -> IO Bool
-ferror (FHandle h) = do err <- do_ferror h
-                        return (not (err == 0))
-
-fpoll : File -> IO Bool
-fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
-                       return (p > 0)
-
-||| Check if a foreign pointer is null
-partial
-nullPtr : Ptr -> IO Bool
-nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p
-               return (ok /= 0)
-
-||| Check if a supposed string was actually a null pointer
-partial
-nullStr : String -> IO Bool
-nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
-               return (ok /= 0)
-
 namespace JSNull
   ||| Check if a foreign pointer is null
   partial
@@ -425,12 +238,6 @@ eqPtr : Ptr -> Ptr -> IO Bool
 eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y
                return (eq /= 0)
 
-||| Check whether a file handle is actually a null pointer
-partial
-validFile : File -> IO Bool
-validFile (FHandle h) = do x <- nullPtr h
-                           return (not x)
-
 ||| Loop while some test is true
 |||
 ||| @ test the condition of the loop
@@ -442,22 +249,6 @@ while t b = do v <- t
                             while t b
                     else return ()
 
-||| Read the contents of a file into a string
-partial -- no error checking!
-readFile : String -> IO String
-readFile fn = do h <- openFile fn Read
-                 c <- readFile' h ""
-                 closeFile h
-                 return c
-  where
-    partial
-    readFile' : File -> String -> IO String
-    readFile' h contents =
-       do x <- feof h
-          if not x then do l <- fread h
-                           readFile' h (contents ++ l)
-                   else return contents
-
 ------- Some error rewriting
 
 %language ErrorReflection

libs/prelude/Prelude/Cast.idr

@@ -15,7 +15,7 @@ class Cast from to where
 instance Cast String Int where
     cast = prim__fromStrInt
 
-instance Cast String Float where
+instance Cast String Double where
     cast = prim__strToFloat
 
 instance Cast String Integer where
@@ -26,25 +26,31 @@ instance Cast String Integer where
 instance Cast Int String where
     cast = prim__toStrInt
 
-instance Cast Int Float where
+instance Cast Int Double where
     cast = prim__toFloatInt
 
 instance Cast Int Integer where
     cast = prim__sextInt_BigInt
 
--- Float casts
+-- Double casts
 
-instance Cast Float String where
+instance Cast Double String where
     cast = prim__floatToStr
 
-instance Cast Float Int where
+instance Cast Double Int where
     cast = prim__fromFloatInt
 
+instance Cast Double Integer where
+    cast = prim__fromFloatBigInt
+
 -- Integer casts
 
 instance Cast Integer String where
     cast = prim__toStrBigInt
 
+instance Cast Integer Double where
+    cast = prim__toFloatBigInt
+
 -- Char casts
 
 instance Cast Char Int where

libs/prelude/Prelude/File.idr

@@ -0,0 +1,156 @@
+module Prelude.File
+
+import Builtins
+import Prelude.List
+import Prelude.Maybe
+import Prelude.Monad
+import Prelude.Chars
+import Prelude.Strings
+import Prelude.Cast
+import Prelude.Bool
+import Prelude.Basics
+import Prelude.Classes
+import Prelude.Monad
+import IO
+
+%access public
+
+||| A file handle
+abstract
+data File = FHandle Ptr
+
+||| Standard input
+stdin : File
+stdin = FHandle prim__stdin
+
+||| Standard output
+stdout : File
+stdout = FHandle prim__stdout
+
+||| Standard output
+stderr : File
+stderr = FHandle prim__stderr
+
+||| Call the RTS's file opening function
+do_fopen : String -> String -> IO Ptr
+do_fopen f m
+   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m
+
+||| Open a file
+||| @ f the filename
+||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
+fopen : (f : String) -> (m : String) -> IO File
+fopen f m = do h <- do_fopen f m
+               return (FHandle h)
+
+||| Check whether a file handle is actually a null pointer
+partial
+validFile : File -> IO Bool
+validFile (FHandle h) = do x <- nullPtr h
+                           return (not x)
+
+||| Modes for opening files
+data Mode = Read | Write | ReadWrite
+
+||| Open a file
+||| @ f the filename
+||| @ m the mode
+partial
+openFile : (f : String) -> (m : Mode) -> IO File
+openFile f m = fopen f (modeStr m) where
+  modeStr Read  = "r"
+  modeStr Write = "w"
+  modeStr ReadWrite = "r+"
+
+partial
+do_fclose : Ptr -> IO ()
+do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
+
+partial
+closeFile : File -> IO ()
+closeFile (FHandle h) = do_fclose h
+
+partial
+do_fread : Ptr -> IO' l String
+do_fread h = prim_fread h
+
+fgetc : File -> IO Char
+fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))
+
+fgetc' : File -> IO (Maybe Char)
+fgetc' (FHandle h)
+   = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h
+        if (x < 0) then return Nothing
+                   else return (Just (cast x))
+
+fflush : File -> IO ()
+fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
+
+do_popen : String -> String -> IO Ptr
+do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
+
+popen : String -> Mode -> IO File
+popen f m = do ptr <- do_popen f (modeStr m)
+               return (FHandle ptr)
+  where
+    modeStr Read  = "r"
+    modeStr Write = "w"
+    modeStr ReadWrite = "r+"
+
+pclose : File -> IO ()
+pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
+
+-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
+--                        prim__vm h
+
+partial
+fread : File -> IO' l String
+fread (FHandle h) = do_fread h
+
+partial
+do_fwrite : Ptr -> String -> IO ()
+do_fwrite h s = do prim_fwrite h s
+                   return ()
+
+partial
+fwrite : File -> String -> IO ()
+fwrite (FHandle h) s = do_fwrite h s
+
+partial
+do_feof : Ptr -> IO Int
+do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
+
+||| Check if a file handle has reached the end
+feof : File -> IO Bool
+feof (FHandle h) = do eof <- do_feof h
+                      return (not (eof == 0))
+
+partial
+do_ferror : Ptr -> IO Int
+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
+
+ferror : File -> IO Bool
+ferror (FHandle h) = do err <- do_ferror h
+                        return (not (err == 0))
+
+fpoll : File -> IO Bool
+fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
+                       return (p > 0)
+
+||| Read the contents of a file into a string
+partial -- no error checking!
+readFile : String -> IO String
+readFile fn = do h <- openFile fn Read
+                 c <- readFile' h ""
+                 closeFile h
+                 return c
+  where
+    partial
+    readFile' : File -> String -> IO String
+    readFile' h contents =
+       do x <- feof h
+          if not x then do l <- fread h
+                           readFile' h (contents ++ l)
+                   else return contents
+
+

libs/prelude/Prelude/Interactive.idr

@@ -4,13 +4,83 @@
 ||| the easy creation of interactive programs without needing to teach IO
 ||| or Effects first, but they also capture some common patterns of interactive
 ||| programming.
-module System.Interactive
+module Prelude.Interactive
 
-{-
+import Builtins
-When the interfaces and names are stable, these are intended for the Prelude.
+import Prelude.List
--}
+import Prelude.File
+import Prelude.Bool
+import Prelude.Classes
+import Prelude.Strings
+import Prelude.Chars
+import Prelude.Show
+import Prelude.Cast
+import Prelude.Maybe
+import Prelude.Functor
+import Prelude.Monad
+import IO
+
+%access public
+
+---- some basic io
+
+||| Output a string to stdout without a trailing newline
+putStr : String -> IO' ffi ()
+putStr x = do prim_write x
+              return ()
+
+||| Output a string to stdout with a trailing newline
+putStrLn : String -> IO' ffi ()
+putStrLn x = putStr (x ++ "\n")
+
+||| Output something showable to stdout, without a trailing newline
+print : Show a => a -> IO' ffi ()
+print x = putStr (show x)
+
+||| Output something showable to stdout, with a trailing newline
+printLn : Show a => a -> IO' ffi ()
+printLn x = putStrLn (show x)
+
+||| Read one line of input from stdin, without the trailing newline
+getLine : IO' ffi String
+getLine = do x <- prim_read
+             return (reverse (trimNL (reverse x)))
+  where trimNL : String -> String
+        trimNL str with (strM str)
+          trimNL "" | StrNil = ""
+          trimNL (strCons '\n' xs) | StrCons _ _ = xs
+          trimNL (strCons x xs)    | StrCons _ _ = strCons x xs
+
+||| Write a single character to stdout
+putChar : Char -> IO ()
+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)
+
+||| Write a singel character to stdout, with a trailing newline
+putCharLn : Char -> IO ()
+putCharLn c = putStrLn (singleton c)
+
+||| Read a single character from stdin
+getChar : IO Char
+getChar = map cast $ foreign FFI_C "getchar" (IO Int)
+
+||| Get the command-line arguments that the program was called with.
+partial
+getArgs : IO (List String)
+getArgs = do n <- numArgs
+             ga' [] 0 n
+  where
+    numArgs : IO Int
+    numArgs = foreign FFI_C "idris_numArgs" (IO Int)
+
+    getArg : Int -> IO String
+    getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x
+
+    partial
+    ga' : List String -> Int -> Int -> IO (List String)
+    ga' acc i n = if (i == n) then (return $ reverse acc) else
+                    do arg <- getArg i
+                       ga' (arg :: acc) (i+1) n
 
-import System
 
 ||| Process input from an open file handle, while maintaining a state.
 ||| @ state the input state
@@ -18,7 +88,7 @@ import System
 ||| output and a new state
 ||| @ onEOF the function to run on reaching end of file, returning a String
 ||| to output
-public partial
+partial
 processHandle : File -> 
                 (state : a) ->
                 (onRead : a -> String -> (String, a)) -> 
@@ -38,7 +108,7 @@ processHandle h acc onRead onEOF
 ||| output and a new state
 ||| @ onEOI the function to run on reaching end of input, returning a String
 ||| to output
-public partial
+partial
 processStdin : (state : a) -> 
                (onRead : a -> String -> (String, a)) -> 
                (onEOI : a -> String) -> IO ()
@@ -49,7 +119,7 @@ processStdin = processHandle stdin
 ||| @ prompt the prompt to show 
 ||| @ onInput the function to run on reading input, returning a String to
 ||| output and a new state. Returns Nothing if the repl should exit
-public partial
+partial
 replWith : (state : a) -> (prompt : String) -> 
            (onInput : a -> String -> Maybe (String, a)) -> IO a
 replWith acc prompt fn 
@@ -64,7 +134,7 @@ replWith acc prompt fn
 ||| @ prompt the prompt to show 
 ||| @ onInput the function to run on reading input, returning a String to
 ||| output 
-public partial
+partial
 repl : (prompt : String) -> 
        (onInput : String -> String) -> IO ()
 repl prompt fn 

libs/prelude/Prelude/List.idr

@@ -18,11 +18,12 @@ import Prelude.Nat
 infix 5 \\
 infixr 7 ::,++
 
-||| Linked lists
+||| Generic lists
 %elim data List elem =
-  ||| The empty list
+  ||| Empty list
   Nil |
-  ||| Cons cell
+  ||| A non-empty list, consisting of a head element and the rest of
+  ||| the list.
   (::) elem (List elem)
 
 -- Name hints for interactive editing

libs/prelude/Prelude/Monad.idr

@@ -3,9 +3,10 @@ module Prelude.Monad
 -- Monads and Functors
 
 import Builtins
-import Prelude.List
+import Prelude.Functor
 import Prelude.Applicative
 import Prelude.Basics
+import IO
 
 %access public
 
@@ -22,3 +23,20 @@ flatten a = a >>= id
 ||| define `return` and `pure` differently!
 return : Monad m => a -> m a
 return = pure
+
+-- Annoyingly, these need to be here, so that we can use them in other
+-- Prelude modules other than the top level.
+
+instance Functor (IO' ffi) where
+    map f io = io_bind io (\b => io_return (f b))
+
+instance Applicative (IO' ffi) where
+    pure x = io_return x
+    f <*> a = io_bind f (\f' =>
+                io_bind a (\a' =>
+                  io_return (f' a')))
+
+
+instance Monad (IO' ffi) where
+    b >>= k = io_bind b k
+

libs/prelude/Prelude/Nat.idr

@@ -12,7 +12,8 @@ import Prelude.Uninhabited
 %access public
 %default total
 
-||| Unary natural numbers
+||| Natural numbers: unbounded, unsigned integers which can be pattern
+||| matched.
 %elim data Nat =
   ||| Zero
   Z |
@@ -213,12 +214,12 @@ instance MinBound Nat where
 instance Cast Integer Nat where
   cast = fromInteger
 
-||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
 record Multiplicative where
   constructor getMultiplicative
   _ : Nat
 
-||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
 record Additive where
   constructor getAdditive  
   _ : Nat
@@ -262,6 +263,9 @@ instance Cast Int Nat where
 instance Cast Nat Int where
   cast = toIntNat
 
+instance Cast Nat Double where
+  cast = cast . toIntegerNat
+
 --------------------------------------------------------------------------------
 -- Auxilliary notions
 --------------------------------------------------------------------------------

libs/prelude/Prelude/Strings.idr

@@ -1,6 +1,7 @@
 module Prelude.Strings
 
 import Builtins
+import IO
 
 import Prelude.Algebra
 import Prelude.Basics
@@ -13,8 +14,18 @@ import Prelude.Foldable
 import Prelude.Functor
 import Prelude.List
 import Prelude.Nat
+import Prelude.Monad
 import Decidable.Equality
 
+partial
+foldr1 : (a -> a -> a) -> List a -> a
+foldr1 _ [x] = x
+foldr1 f (x::xs) = f x (foldr1 f xs)
+
+partial
+foldl1 : (a -> a -> a) -> List a -> a
+foldl1 f (x::xs) = foldl f x xs
+
 ||| Appends two strings together.
 |||
 ||| ```idris example
@@ -247,15 +258,6 @@ lines' s = case dropWhile isNL s of
 lines : String -> List String
 lines s = map pack $ lines' $ unpack s
 
-partial
-foldr1 : (a -> a -> a) -> List a -> a
-foldr1 _ [x] = x
-foldr1 f (x::xs) = f x (foldr1 f xs)
-
-partial
-foldl1 : (a -> a -> a) -> List a -> a
-foldl1 f (x::xs) = foldl f x xs
-
 ||| Joins the character lists by spaces into a single character list.
 |||
 ||| ```idris example
@@ -263,12 +265,11 @@ foldl1 f (x::xs) = foldl f x xs
 ||| ```
 unwords' : List (List Char) -> List Char
 unwords' [] = []
-unwords' ws = assert_total (foldr1 addSpace ws)
+unwords' ws = assert_total (foldr1 addSpace ws) where
-        where
+  addSpace : List Char -> List Char -> List Char
-            addSpace : List Char -> List Char -> List Char
+  addSpace w s = w ++ (' ' :: s)
-            addSpace w s = w ++ (' ' :: s)
 
-||| Joins the strings by spaces into a single string. 
+||| Joins the strings by spaces into a single string.
 |||
 ||| ```idris example
 ||| unwords ["A", "BC", "D", "E"]
@@ -276,6 +277,25 @@ unwords' ws = assert_total (foldr1 addSpace ws)
 unwords : List String -> String
 unwords = pack . unwords' . map unpack
 
+||| Joins the character lists by newlines into a single character list.
+|||
+||| ```idris example
+||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
+||| ```
+unlines' : List (List Char) -> List Char
+unlines' [] = []
+unlines' ls = assert_total (foldr1 addLine ls) where
+  addLine : List Char -> List Char -> List Char
+  addLine l s = l ++ ('\n' :: s)
+
+||| Joins the strings by newlines into a single string.
+|||
+||| ```idris example
+||| unlines ["line", "line2", "ln3", "D"]
+||| ```
+unlines : List String -> String
+unlines = pack . unlines' . map unpack
+
 ||| Returns the length of the string.
 |||
 ||| ```idris example
@@ -287,6 +307,14 @@ unwords = pack . unwords' . map unpack
 length : String -> Nat
 length = fromInteger . prim__zextInt_BigInt . prim_lenString
 
+||| Returns a substring of a given string
+||| @index The (zero based) index of the string to extract. If this is
+||| beyond the end of the String, the function returns the empty string.
+||| @len The desired length of the substring. Truncated if this exceeds
+||| the length of the input.
+substr : (index : Nat) -> (len : Nat) -> String -> String
+substr i len = pack . List.take len . drop i . unpack
+
 ||| Lowercases all characters in the string.
 |||
 ||| ```idris example
@@ -321,3 +349,16 @@ isSuffixOf a b = isSuffixOf (unpack a) (unpack b)
 
 isInfixOf : String -> String -> Bool
 isInfixOf a b = isInfixOf (unpack a) (unpack b)
+
+||| Check if a foreign pointer is null
+partial
+nullPtr : Ptr -> IO Bool
+nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p
+               return (ok /= 0)
+
+||| Check if a supposed string was actually a null pointer
+partial
+nullStr : String -> IO Bool
+nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p
+               return (ok /= 0)
+

libs/prelude/prelude.ipkg

@@ -9,6 +9,7 @@ modules = Builtins, Prelude, IO,
           Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
           Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
           Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
+          Prelude.Interactive, Prelude.File,
 
           Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
 

src/Idris/AbsSyntax.hs

@@ -597,7 +597,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)
 
 -- | Save information about a name that is not yet defined
 addDeferred' :: NameType
-             -> [(Name, (Int, Maybe Name, Type, Bool))]
+             -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]
                 -- ^ The Name is the name being made into a metavar,
                 -- the Int is the number of vars that are part of a
                 -- putative proof context, the Maybe Name is the
@@ -606,10 +606,10 @@ addDeferred' :: NameType
                 -- allowed
              -> Idris ()
 addDeferred' nt ns
-  = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
+  = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
        mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
        i <- getIState
-       putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
+       putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++
                                             idris_metavars i }
   where
         -- 'tidyNames' is to generate user accessible names in case they are
@@ -790,6 +790,12 @@ getNoBanner = do i <- getIState
                  let opts = idris_options i
                  return (opt_nobanner opts)
 
+setEvalTypes :: Bool -> Idris ()
+setEvalTypes n = do i <- getIState
+                    let opts = idris_options i
+                    let opt' = opts { opt_evaltypes = n }
+                    putIState $ i { idris_options = opt' }
+
 setQuiet :: Bool -> Idris ()
 setQuiet q = do i <- getIState
                 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs

@@ -89,7 +89,8 @@ data IOption = IOption { opt_logLevel     :: Int,
                          opt_autoSolve    :: Bool, -- ^ automatically apply "solve" tactic in prover
                          opt_autoImport   :: [FilePath], -- ^ e.g. Builtins+Prelude
                          opt_optimise     :: [Optimisation],
-                         opt_printdepth   :: Maybe Int
+                         opt_printdepth   :: Maybe Int,
+                         opt_evaltypes    :: Bool -- ^ normalise types in :t
                        }
     deriving (Show, Eq)
 
@@ -115,10 +116,12 @@ defaultOpts = IOption { opt_logLevel   = 0
                       , opt_autoImport = []
                       , opt_optimise   = defaultOptimise
                       , opt_printdepth = Just 5000
+                      , opt_evaltypes  = True
                       }
 
 data PPOption = PPOption {
     ppopt_impl :: Bool -- ^^ whether to show implicits
+  , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings
   , ppopt_depth :: Maybe Int
 } deriving (Show)
 
@@ -129,16 +132,21 @@ defaultOptimise = [PETransform]
 
 -- | Pretty printing options with default verbosity.
 defaultPPOption :: PPOption
-defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
+defaultPPOption = PPOption { ppopt_impl = False, 
+                             ppopt_pinames = False,
+                             ppopt_depth = Just 200 }
 
 -- | Pretty printing options with the most verbosity.
 verbosePPOption :: PPOption
-verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
+verbosePPOption = PPOption { ppopt_impl = True,
+                             ppopt_pinames = True,
+                             ppopt_depth = Just 200 }
 
 -- | Get pretty printing options from the big options record.
 ppOption :: IOption -> PPOption
 ppOption opt = PPOption {
     ppopt_impl = opt_showimp opt,
+    ppopt_pinames = False,
     ppopt_depth = opt_printdepth opt
 }
 
@@ -193,10 +201,11 @@ data IState = IState {
     idris_name :: Int,
     idris_lineapps :: [((FilePath, Int), PTerm)],
           -- ^ Full application LHS on source line
-    idris_metavars :: [(Name, (Maybe Name, Int, Bool))],
+    idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],
     -- ^ The currently defined but not proven metavariables. The Int
     -- is the number of vars to display as a context, the Maybe Name
-    -- is its top-level function, and the Bool is whether :p is
+    -- is its top-level function, the [Name] is the list of local variables
+    -- available for proof search and the Bool is whether :p is
     -- allowed
     idris_coercions :: [Name],
     idris_errRev :: [(Term, Term)],
@@ -400,10 +409,13 @@ data Command = Quit
              | AddProofClauseFrom Bool Int Name
              | AddMissing Bool Int Name
              | MakeWith Bool Int Name
+             | MakeCase Bool Int Name
              | MakeLemma Bool Int Name
-             | DoProofSearch Bool Bool Int Name [Name]
+             | DoProofSearch Bool -- update file
-               -- ^ the first bool is whether to update,
+                             Bool -- recursive search
-               -- the second is whether to search recursively (i.e. for the arguments)
+                             Int -- depth
+                             Name -- top level name
+                             [Name] -- hints
              | SetOpt Opt
              | UnsetOpt Opt
              | NOP
@@ -451,6 +463,7 @@ data Opt = Filename String
          | DefaultPartial
          | WarnPartial
          | WarnReach
+         | EvalTypes
          | NoCoverage
          | ErrContext
          | ShowImpl
@@ -978,7 +991,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
                 | MatchRefine Name
                 | LetTac Name t | LetTacTy Name t t
                 | Exact t | Compute | Trivial | TCInstance
-                | ProofSearch Bool Bool Int (Maybe Name) [Name]
+                | ProofSearch Bool Bool Int (Maybe Name) 
+                              [Name] -- allowed local names
+                              [Name] -- hints
                   -- ^ the bool is whether to search recursively
                 | Solve
                 | Attack
@@ -1549,7 +1564,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
       kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
       kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
     prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
-      | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
+      | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs
+          || ppopt_pinames ppo && uname n =
           depth d . bracket p startPrec . group $
           enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
           st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
@@ -1558,6 +1574,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
           group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
           group (prettySe (decD d) startPrec ((n, False):bnd) sc)
       where
+        uname (UN n) = case str n of
+                            ('_':_) -> False
+                            _ -> True
+        uname _ = False
+
         st =
           case s of
             Static -> text "[static]" <> space
@@ -1576,7 +1597,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
     prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
       depth d . bracket p startPrec $
       prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
-    prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
+    prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
       lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
       rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
     prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
@@ -1996,6 +2017,9 @@ showTm ist = displayDecorated (consoleDecorate ist) .
 showTmImpls :: PTerm -> String
 showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
 
+-- | Show a term with specific options 
+showTmOpts :: PPOption -> PTerm -> String
+showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
 
 
 instance Sized PTerm where

src/Idris/CaseSplit.hs

@@ -265,18 +265,23 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
     rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
 
     updateRHSs i [] = return []
-    updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
+    updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x
                                xs' <- updateRHSs i' xs
                                return (x' : xs')
 
-    updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
+    updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs
-                                  return ("?=" ++ xs', i')
+                                       return ("?=" ++ xs', i')
-    updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
+    updateRHS last i ('?':xs) 
-                              (nm', i') <- getUniq nm i
+        = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'
-                              return ('?':nm' ++ rest, i')
+                                                              || x == '(')) xs
-    updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
+             let rest = if last then rest_in else
-                              return (x : xs', i')
+                           case span (not . (=='\n')) rest_in of
-    updateRHS i [] = return ("", i)
+                                (_, restnl) -> restnl
+             (nm', i') <- getUniq nm i
+             return ('?':nm' ++ rest, i')
+    updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs
+                                   return (x : xs', i')
+    updateRHS last i [] = return ("", i)
 
 
     -- TMP HACK: If there are Nats, we don't want to show as numerals since
@@ -361,9 +366,11 @@ getClause l fn fp
          getNameFrom i used (PApp fc f as) = getNameFrom i used f
          getNameFrom i used (PRef fc _ f)
             = case getNameHints i f of
-                   [] -> uniqueName (sUN "x") used
+                   [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",
+                                                   sUN "z"]) used
                    ns -> uniqueNameFrom (mkSupply ns) used
-         getNameFrom i used _ = uniqueName (sUN "x") used 
+         getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",
+                                                          sUN "z"]) used 
 
          -- write method declarations, indent with 4 spaces
          mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

src/Idris/Completion.hs

@@ -52,7 +52,7 @@ names = do i <- get
 
 metavars :: Idris [String]
 metavars = do i <- get
-              return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
+              return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t)) -> not t) (idris_metavars i)) \\ primDefs
 
 
 modules :: Idris [String]

src/Idris/Core/Binary.hs

@@ -499,9 +499,10 @@ instance (Binary b) => Binary (Binder b) where
                                  put x2
                 Hole x1 -> do putWord8 4
                               put x1
-                GHole x1 x2 -> do putWord8 5
+                GHole x1 x2 x3 -> do putWord8 5
-                                  put x1
+                                     put x1
-                                  put x2
+                                     put x2
+                                     put x3
                 Guess x1 x2 -> do putWord8 6
                                   put x1
                                   put x2
@@ -528,7 +529,8 @@ instance (Binary b) => Binary (Binder b) where
                            return (Hole x1)
                    5 -> do x1 <- get
                            x2 <- get
-                           return (GHole x1 x2)
+                           x3 <- get
+                           return (GHole x1 x2 x3)
                    6 -> do x1 <- get
                            x2 <- get
                            return (Guess x1 x2)

src/Idris/Core/DeepSeq.hs

@@ -128,7 +128,7 @@ instance (NFData b) => NFData (Binder b) where
         rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (Hole x1) = rnf x1 `seq` ()
-        rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
+        rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (PVar x1) = rnf x1 `seq` ()
         rnf (PVTy x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs

@@ -51,6 +51,20 @@ explicit n = do ES (p, a) s m <- get
                 let p' = p { dontunify = n : dontunify p }
                 put (ES (p', a) s m)
 
+-- Add a name that's okay to use in proof search (typically either because 
+-- it was given explicitly on the lhs, or intrduced as an explicit lambda
+-- or let binding)
+addPSname :: Name -> Elab' aux ()
+addPSname n@(UN _)
+     = do ES (p, a) s m <- get
+          let p' = p { psnames = n : psnames p }
+          put (ES (p', a) s m)
+addPSname _ = return () -- can only use user given names
+
+getPSnames :: Elab' aux [Name]
+getPSnames = do ES (p, a) s m <- get
+                return (psnames p)
+
 saveState :: Elab' aux ()
 saveState = do e@(ES p s _) <- get
                put (ES p s (Just e))

src/Idris/Core/Execute.hs

@@ -93,7 +93,7 @@ toTT (EBind n b body) = do n' <- newN n
           fixBinder (Let t1 t2)   = Let     <$> toTT t1 <*> toTT t2
           fixBinder (NLet t1 t2)  = NLet    <$> toTT t1 <*> toTT t2
           fixBinder (Hole t)      = Hole    <$> toTT t
-          fixBinder (GHole i t)   = GHole i <$> toTT t
+          fixBinder (GHole i ns t) = GHole i ns <$> toTT t
           fixBinder (Guess t1 t2) = Guess   <$> toTT t1 <*> toTT t2
           fixBinder (PVar t)      = PVar    <$> toTT t
           fixBinder (PVTy t)      = PVTy    <$> toTT t

src/Idris/Core/ProofState.hs

@@ -39,6 +39,7 @@ data ProofState = PS { thname   :: Name,
                        deferred :: [Name], -- ^ names we'll need to define
                        instances :: [Name], -- ^ instance arguments (for type classes)
                        autos    :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes
+                       psnames  :: [Name], -- ^ Local names okay to use in proof search
                        previous :: Maybe ProofState, -- ^ for undo
                        context  :: Context,
                        datatypes :: Ctxt TypeInfo,
@@ -244,7 +245,8 @@ unify' ctxt env (topx, xfrom) (topy, yfrom) =
            let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
            traceWhen (unifylog ps)
             ("Now solved: " ++ show ns' ++
-             "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $
+             "\nNow problems: " ++ qshow (probs' ++ probs_notu) ++
+             "\nNow injective: " ++ show (updateInj u (injective ps))) $
              put (ps { problems = probs' ++ probs_notu,
                        unified = (h, ns'),
                        injective = updateInj u (injective ps),
@@ -300,7 +302,7 @@ newProof n ctxt datatypes ty =
   in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
         (P Bound h ty'))) ty [] (h, []) [] []
         Nothing [] []
-        [] [] []
+        [] [] [] []
         Nothing ctxt datatypes "" False False [] []
 
 type TState = ProofState -- [TacticAction])
@@ -428,7 +430,8 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
     do let env' = filter (\(n, t) -> n `notElem` dropped) env
        action (\ps -> let hs = holes ps in
                           ps { holes = hs \\ [x] })
-       return (Bind n (GHole (length env') (mkTy (reverse env') t))
+       ps <- get
+       return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))
                       (mkApp (P Ref n ty) (map getP (reverse env'))))
   where
     mkTy []           t = t
@@ -444,7 +447,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
                           ds = deferred ps in
                           ps { holes = hs \\ [x],
                                deferred = n : ds })
-       return (Bind n (GHole 0 fty)
+       return (Bind n (GHole 0 [] fty)
                       (mkApp (P Ref n ty) (map getP args)))
   where
     getP n = case lookup n env of

src/Idris/Core/TT.hs

@@ -809,6 +809,7 @@ data Binder b = Lam   { binderTy  :: !b {-^ type annotation for bound variable-}
                         binderVal :: b }
               | Hole  { binderTy  :: !b}
               | GHole { envlen :: Int,
+                        localnames :: [Name],
                         binderTy  :: !b}
               | Guess { binderTy  :: !b,
                         binderVal :: b }
@@ -827,7 +828,7 @@ instance Sized a => Sized (Binder a) where
   size (Let ty val) = 1 + size ty + size val
   size (NLet ty val) = 1 + size ty + size val
   size (Hole ty) = 1 + size ty
-  size (GHole _ ty) = 1 + size ty
+  size (GHole _ _ ty) = 1 + size ty
   size (Guess ty val) = 1 + size ty + size val
   size (PVar ty) = 1 + size ty
   size (PVTy ty) = 1 + size ty
@@ -839,7 +840,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
 fmapMB f (Lam t)     = liftM Lam (f t)
 fmapMB f (Pi i t k)  = liftM2 (Pi i) (f t) (f k)
 fmapMB f (Hole t)    = liftM Hole (f t)
-fmapMB f (GHole i t) = liftM (GHole i) (f t)
+fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)
 fmapMB f (PVar t)    = liftM PVar (f t)
 fmapMB f (PVTy t)    = liftM PVTy (f t)
 
@@ -1494,7 +1495,7 @@ prettyEnv env t = prettyEnv' env t False
     -- Render a `Binder` and its name
     prettySb env n (Lam t) = prettyB env "λ" "=>" n t
     prettySb env n (Hole t) = prettyB env "?defer" "." n t
-    prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t
+    prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t
     prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t
     prettySb env n (PVar t) = prettyB env "pat" "." n t
     prettySb env n (PVTy t) = prettyB env "pty" "." n t
@@ -1539,7 +1540,7 @@ showEnv' env t dbg = se 10 env t where
 
     sb env n (Lam t)  = showb env "\\ " " => " n t
     sb env n (Hole t) = showb env "? " ". " n t
-    sb env n (GHole i t) = showb env "?defer " ". " n t
+    sb env n (GHole i ns t) = showb env "?defer " ". " n t
     sb env n (Pi (Just _) t _)   = showb env "{" "} -> " n t
     sb env n (Pi _ t _)   = showb env "(" ") -> " n t
     sb env n (PVar t) = showb env "pat " ". " n t
@@ -1739,7 +1740,7 @@ pprintTT bound tm = pp startPrec bound tm
     ppb p bound n (Hole ty) sc =
       bracket p startPrec . group . align . hang 2 $
       text "?" <+> bindingOf n False <+> text "." <> line <> sc
-    ppb p bound n (GHole _ ty) sc =
+    ppb p bound n (GHole _ _ ty) sc =
       bracket p startPrec . group . align . hang 2 $
       text "¿" <+> bindingOf n False <+> text "." <> line <> sc
     ppb p bound n (Guess ty val) sc =
@@ -1791,8 +1792,8 @@ pprintRaw bound (RBind n b body) =
                       vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]
     ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $
                     text "Hole" <$> pprintRaw bound ty
-    ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $
+    ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $
-                       text "GHole" <$> pprintRaw bound ty
+                         text "GHole" <$> pprintRaw bound ty
     ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $
                        vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]
     ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

src/Idris/Core/Typecheck.hs

@@ -232,12 +232,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
                         let tt' = normalise ctxt env tt
                         lift $ isType ctxt env tt'
                         return (Hole tv, tt')
-          checkBinder (GHole i t)
+          checkBinder (GHole i ns t)
             = do (tv, tt) <- chk u env t
                  let tv' = normalise ctxt env tv
                  let tt' = normalise ctxt env tt
                  lift $ isType ctxt env tt'
-                 return (GHole i tv, tt')
+                 return (GHole i ns tv, tt')
           checkBinder (Guess t v)
             | not holes = lift $ tfail (IncompleteTerm undefined)
             | otherwise
@@ -273,8 +273,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
             = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
           discharge n (Hole t) bt scv sct
             = return (Bind n (Hole t) scv, sct)
-          discharge n (GHole i t) bt scv sct
+          discharge n (GHole i ns t) bt scv sct
-            = return (Bind n (GHole i t) scv, sct)
+            = return (Bind n (GHole i ns t) scv, sct)
           discharge n (Guess t v) bt scv sct
             = return (Bind n (Guess t v) scv, sct)
           discharge n (PVar t) bt scv sct

src/Idris/DeepSeq.hs

@@ -295,8 +295,8 @@ instance (NFData t) => NFData (PTactic' t) where
         rnf Compute = ()
         rnf Trivial = ()
         rnf TCInstance = ()
-        rnf (ProofSearch r r1 r2 x1 x2)
+        rnf (ProofSearch r r1 r2 x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` ()
+          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf Solve = ()
         rnf Attack = ()
         rnf ProofState = ()

src/Idris/Delaborate.hs

@@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
                        | Just n' <- lookup n env = PRef un [] n'
                        | otherwise
                             = case lookup n (idris_metavars ist) of
-                                  Just (Just _, mi, _) -> mkMVApp n []
+                                  Just (Just _, mi, _, _) -> mkMVApp n []
                                   _ -> PRef un [] n
     de env _ (Bind n (Lam ty) sc)
           = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)
@@ -169,7 +169,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
               = PApp un (de env [] f) (map pexp (map (de env []) args))
     deFn env (P _ n _) args
          | not mvs = case lookup n (idris_metavars ist) of
-                        Just (Just _, mi, _) ->
+                        Just (Just _, mi, _, _) ->
                             mkMVApp n (drop mi (map (de env []) args))
                         _ -> mkPApp n (map (de env []) args)
          | otherwise = mkPApp n (map (de env []) args)

src/Idris/Elab/Clause.hs

@@ -543,7 +543,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         let fn_is = case lookupCtxt fname (idris_implicits i) of
                          [t] -> t
                          _ -> []
-        let params = getParamsInType i [] fn_is fn_ty
+        let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)
         let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
                     propagateParams i params fn_ty (addImplPat i lhs_in)
 --         let lhs = mkLHSapp $ 
@@ -632,6 +632,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-
            tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState
                     (do pbinds ist lhs_tm
+                        -- proof search can use explicitly written names
+                        mapM_ addPSname (allNamesIn lhs_in)
                         mapM_ setinj (nub (params ++ inj))
                         setNextName
                         (ElabResult _ _ is ctxt' newDecls highlights) <-
@@ -656,9 +658,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         logLvl 5 "DONE CHECK"
         logLvl 4 $ "---> " ++ show rhs'
         when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++
-                    show (map (\ (n, (_,_,t)) -> (n, t)) defer)
+                    show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
         def' <- checkDef fc (Elaborating "deferred type of ") defer
-        let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
+        let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
         addDeferred def''
         mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
 
@@ -790,7 +792,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         let fn_is = case lookupCtxt fname (idris_implicits i) of
                          [t] -> t
                          _ -> []
-        let params = getParamsInType i [] fn_is fn_ty
+        let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)
         let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)
         logLvl 2 ("LHS: " ++ show lhs)
         (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-
@@ -816,6 +818,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
             tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")
                         (bindTyArgs PVTy bargs infP) initEState
                         (do pbinds i lhs_tm
+                            -- proof search can use explicitly written names
+                            mapM_ addPSname (allNamesIn lhs_in)
                             setNextName
                             -- TODO: may want where here - see winfo abpve
                             (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname
@@ -828,7 +832,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         sendHighlighting highlights
 
         def' <- checkDef fc iderr defer
-        let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
+        let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
         addDeferred def''
         mapM_ (elabCaseBlock info opts) is
         logLvl 5 ("Checked wval " ++ show wval')
@@ -890,8 +894,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         addIBC (IBCImp wname)
         addIBC (IBCStatic wname)
 
-        def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]
+        def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]
-        let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
+        let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
         addDeferred def''
 
         -- in the subdecls, lhs becomes:
@@ -932,7 +936,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         sendHighlighting highlights
 
         def' <- checkDef fc iderr defer
-        let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
+        let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'
         addDeferred def''
         mapM_ (elabCaseBlock info opts) is
         logLvl 5 ("Checked RHS " ++ show rhs')

src/Idris/Elab/Instance.hs

@@ -71,7 +71,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do
     let constraint = PApp fc (PRef fc [] n) (map pexp ps)
     let iname = mkiname n (namespace info) ps expn
     let emptyclass = null (class_methods ci)
-    when (what /= EDefns || (null ds && not emptyclass)) $ do
+    when (what /= EDefns) $ do 
          nty <- elabType' True info syn doc argDocs fc [] iname NoFC t
          -- if the instance type matches any of the instances we have already,
          -- and it's not a named instance, then it's overlapping, so report an error

src/Idris/Elab/Record.hs

@@ -34,6 +34,7 @@ import Control.Monad
 
 -- | Elaborate a record declaration
 elabRecord :: ElabInfo
+           -> ElabWhat
            -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
            -> SyntaxInfo -> FC -> DataOpts
            -> Name  -- ^ The name of the type being defined
@@ -45,7 +46,7 @@ elabRecord :: ElabInfo
            -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc
            -> SyntaxInfo -- ^ Constructor SyntaxInfo
            -> Idris ()
-elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
+elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
   = do logLvl 1 $ "Building data declaration for " ++ show tyn
        -- Type constructor
        let tycon = generateTyConType params
@@ -58,17 +59,20 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
 
        -- Build data declaration for elaboration
        logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)
-       let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
+       let datadecl = case what of
+                           ETypes -> PLaterdecl tyn NoFC tycon
+                           _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
        elabData info rsyn doc paramDocs fc opts datadecl
 
-       logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
+       when (what /= ETypes) $ do
-       logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
+           logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
-       elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
+           logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
+           elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
 
-       sendHighlighting $
+           sendHighlighting $
-         [(nfc, AnnName tyn Nothing Nothing Nothing)] ++
+             [(nfc, AnnName tyn Nothing Nothing Nothing)] ++
-         maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++
+             maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++
-         [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]
+             [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]
 
   where
     -- | Generates a type constructor.

src/Idris/Elab/Term.hs

@@ -42,7 +42,7 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS
 
 data ElabResult =
   ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
-             , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
+             , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
                -- ^ Information about new metavariables
              , resultCaseDecls :: [PDecl]
                -- ^ Deferred declarations as the meaning of case blocks
@@ -628,6 +628,7 @@ elab ist info emode opts fn tm
                     lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
                checkPiGoal n
                attack; intro (Just n);
+               addPSname n -- okay for proof search
                -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
                elabE (ina { e_inarg = True } ) (Just fc) sc; solve
                highlightSource nfc (AnnBoundName n False)
@@ -644,6 +645,7 @@ elab ist info emode opts fn tm
                ptm <- get_term
                hs <- get_holes
                introTy (Var tyn) (Just n)
+               addPSname n -- okay for proof search
                focus tyn
                
                elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
@@ -652,6 +654,7 @@ elab ist info emode opts fn tm
                highlightSource nfc (AnnBoundName n False)
     elab' ina fc (PPi p n nfc Placeholder sc)
           = do attack; arg n (is_scoped p) (sMN 0 "ty")
+               addPSname n -- okay for proof search
                elabE (ina { e_inarg = True, e_intype = True }) fc sc
                solve
                highlightSource nfc (AnnBoundName n False)
@@ -662,6 +665,7 @@ elab ist info emode opts fn tm
                         MN _ _ -> unique_hole n
                         _ -> return n
                forall n' (is_scoped p) (Var tyn)
+               addPSname n' -- okay for proof search
                focus tyn
                let ec' = ina { e_inarg = True, e_intype = True }
                elabE ec' fc ty
@@ -677,6 +681,7 @@ elab ist info emode opts fn tm
                claim valn (Var tyn)
                explicit valn
                letbind n (Var tyn) (Var valn)
+               addPSname n
                case ty of
                    Placeholder -> return ()
                    _ -> do focus tyn
@@ -902,7 +907,7 @@ elab ist info emode opts fn tm
                 case lookup n env of
                      Nothing -> return ()
                      Just b ->
-                       case unApply (binderTy b) of
+                       case unApply (normalise (tt_ctxt ist) env (binderTy b)) of
                             (P _ c _, args) ->
                                 case lookupCtxtExact c (idris_classes ist) of
                                    Nothing -> return ()
@@ -962,6 +967,7 @@ elab ist info emode opts fn tm
              let unique_used = getUniqueUsed (tt_ctxt ist) ptm
              let n' = metavarName (namespace info) n
              attack
+             psns <- getPSnames
              defer unique_used n'
              solve
              highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
@@ -1621,7 +1627,7 @@ solveAuto ist fn ambigok n
                   g <- goal
                   isg <- is_guess -- if it's a guess, we're working on it recursively, so stop
                   when (not isg) $
-                    proofSearch' ist True ambigok 100 True Nothing fn []
+                    proofSearch' ist True ambigok 100 True Nothing fn [] []
 
 solveAutos :: IState -> Name -> Bool -> ElabD ()
 solveAutos ist fn ambigok
@@ -1630,12 +1636,12 @@ solveAutos ist fn ambigok
 
 trivial' ist
     = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
-trivialHoles' h ist
+trivialHoles' psn h ist
-    = trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
+    = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
-proofSearch' ist rec ambigok depth prv top n hints
+proofSearch' ist rec ambigok depth prv top n psns hints
     = do unifyProblems
          proofSearch rec prv ambigok (not prv) depth
-                     (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
+                     (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist
 
 -- | Resolve type classes. This will only pick up 'normal' instances, never
 -- named instances (which is enforced by 'findInstances').
@@ -1675,7 +1681,7 @@ resTC' tcs defaultOn topholes depth topg fn ist
                               _ -> []
 
            traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
-            try' (trivialHoles' okholes ist)
+            try' (trivialHoles' [] okholes ist)
                 (do addDefault t tc ttypes
                     let stk = map fst (filter snd $ elab_stack ist)
                     let insts = findInstances ist t
@@ -1800,11 +1806,11 @@ resTC' tcs defaultOn topholes depth topg fn ist
              isImp arg = (False, priority arg)
 
 collectDeferred :: Maybe Name -> [Name] -> Context ->
-                   Term -> State [(Name, (Int, Maybe Name, Type))] Term
+                   Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
-collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
+collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =
     do ds <- get
        t' <- collectDeferred top casenames ctxt t
-       when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])
+       when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])
        collectDeferred top casenames ctxt app
   where
     -- Evaluate the top level functions in arguments, if possible, and if it's
@@ -1814,18 +1820,9 @@ collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
     tidyArg env (Bind n b@(Pi im t k) sc) 
         = Bind n (Pi im (tidy ctxt env t) k)
                  (tidyArg ((n, b) : env) sc)
-    tidyArg env t = t
+    tidyArg env t = tidy ctxt env t
 
-    tidy ctxt env t | (f, args) <- unApply t,
+    tidy ctxt env t = normalise ctxt env t
-                      P _ specn _ <- getFn f,
-                      n `notElem` casenames
-        = fst $ specialise ctxt env [(specn, 99999)] t 
-    tidy ctxt env t@(Bind n (Let _ _) sct)
-                    | (f, args) <- unApply sct,
-                      P _ specn _ <- getFn f,
-                      n `notElem` casenames
-        = fst $ specialise ctxt env [(specn, 99999)] t 
-    tidy ctxt env t = t
 
     getFn (Bind n (Lam _) t) = getFn t
     getFn t | (f, a) <- unApply t = f
@@ -2138,7 +2135,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
                do actualHints <- mapM reifyTTName hs
                   unifyProblems
                   let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")
-                  proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist
+                  proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist
                   returnUnit
              (Constant (I _), Nothing ) ->
                lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
@@ -2310,8 +2307,8 @@ runTac autoSolve ist perhapsFC fn tac
     runT Compute = compute
     runT Trivial = do trivial' ist; when autoSolve solveAll
     runT TCInstance = runT (Exact (PResolveTC emptyFC))
-    runT (ProofSearch rec prover depth top hints)
+    runT (ProofSearch rec prover depth top psns hints)
-         = do proofSearch' ist rec False depth prover top fn hints
+         = do proofSearch' ist rec False depth prover top fn psns hints
               when autoSolve solveAll
     runT (Focus n) = focus n
     runT Unfocus = do hs <- get_holes
@@ -2519,7 +2516,7 @@ processTacticDecls info steps =
          updateIState $ \i -> i { idris_implicits =
                                     addDef n impls (idris_implicits i) }
          addIBC (IBCImp n)
-         ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
+         ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))]
          addIBC (IBCDef n)
          ctxt <- getContext
          case lookupDef n ctxt of
@@ -2528,7 +2525,7 @@ processTacticDecls info steps =
              -- then it must be added as a metavariable. This needs guarding
              -- to prevent overwriting case defs with a metavar, if the case
              -- defs come after the type decl in the same script!
-             let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
+             let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds
              in addDeferred ds'
            _ -> return ()
     RAddInstance className instName ->

src/Idris/Elab/Type.hs

@@ -159,9 +159,9 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
          -- Productivity checking now via checking for guarded 'Delay' 
          let opts' = opts -- if corec then (Coinductive : opts) else opts
          let usety = if norm then nty' else nty
-         ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]
+         ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]
          addIBC (IBCDef n)
-         let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds
+         let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds
          addDeferred ds'
          setFlags n opts'
          checkDocs fc argDocs ty

src/Idris/Elab/Utils.hs

@@ -40,21 +40,21 @@ recheckC_borrowing uniq_check bs fc mkerr env t
 iderr :: Name -> Err -> Err
 iderr _ e = e
 
-checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]
+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))]
-         -> Idris [(Name, (Int, Maybe Name, Type))]
+         -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
 checkDef fc mkerr ns = checkAddDef False True fc mkerr ns
 
 checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
-            -> [(Name, (Int, Maybe Name, Type))]
+            -> [(Name, (Int, Maybe Name, Type, [Name]))]
-            -> Idris [(Name, (Int, Maybe Name, Type))]
+            -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
 checkAddDef add toplvl fc mkerr [] = return []
-checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns) 
+checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns) 
                = do ctxt <- getContext
                     (t', _) <- recheckC fc (mkerr n) [] t
-                    when add $ do addDeferred [(n, (i, top, t, toplvl))]
+                    when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]
                                   addIBC (IBCDef n)
                     ns' <- checkAddDef add toplvl fc mkerr ns
-                    return ((n, (i, top, t')) : ns')
+                    return ((n, (i, top, t', psns)) : ns')
 
 -- | Get the list of (index, name) of inaccessible arguments from an elaborated
 -- type
@@ -137,7 +137,8 @@ decorateid decorate (PClauses f o n cs)
 pbinds :: IState -> Term -> ElabD ()
 pbinds i (Bind n (PVar t) sc) 
     = do attack; patbind n
-         case unApply t of
+         env <- get_env
+         case unApply (normalise (tt_ctxt i) env t) of
               (P _ c _, args) -> case lookupCtxt c (idris_classes i) of
                                    [] -> return ()
                                    _ -> -- type class, set as injective

src/Idris/Elab/Value.hs

@@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in
         let vtm = orderPats (getInferTerm tm')
 
         def' <- checkDef (fileFC "(input)") iderr defer
-        let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
+        let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) def'
         addDeferred def''
         mapM_ (elabCaseBlock info []) is
 

src/Idris/ElabDecls.hs

@@ -245,9 +245,8 @@ elabDecl' what info (PInstance doc argDocs s f cs n nfc ps t expn ds)
     = do logLvl 1 $ "Elaborating instance " ++ show n
          elabInstance info s doc argDocs what f cs n nfc ps t expn ds
 elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)
-  | what /= ETypes
     = do logLvl 1 $ "Elaborating record " ++ show name
-         elabRecord info doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn
+         elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn
 {-
   | otherwise
     = do logLvl 1 $ "Elaborating [type of] " ++ show tyn

src/Idris/IBC.hs

@@ -40,7 +40,7 @@ import System.Directory
 import Codec.Archive.Zip
 
 ibcVersion :: Word16
-ibcVersion = 116
+ibcVersion = 117
 
 data IBCFile = IBCFile { ver :: Word16,
                          sourcefile :: FilePath,
@@ -78,7 +78,7 @@ data IBCFile = IBCFile { ver :: Word16,
                          ibc_metainformation :: ![(Name, MetaInformation)],
                          ibc_errorhandlers :: ![Name],
                          ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler
-                         ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],
+                         ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],
                          ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],
                          ibc_postulates :: ![Name],
                          ibc_externs :: ![(Name, Int)],
@@ -365,7 +365,7 @@ timestampOlder :: FilePath -> FilePath -> Idris ()
 timestampOlder src ibc = do srct <- runIO $ getModificationTime src
                             ibct <- runIO $ getModificationTime ibc
                             if (srct > ibct)
-                               then ifail "Needs reloading"
+                               then ifail $ "Needs reloading " ++ show (srct, ibct)
                                else return ()
 
 pPostulates :: [Name] -> Idris ()
@@ -610,7 +610,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()
 pFunctionErrorHandlers ns =  mapM_ (\ (fn,arg,handler) ->
                                 addFunctionErrorHandlers fn arg [handler]) ns
 
-pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()
+pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris ()
 pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })
 
 ----- For Cheapskate and docstrings
@@ -1869,12 +1869,13 @@ instance (Binary t) => Binary (PTactic' t) where
                                    put x1
                 ByReflection x1 -> do putWord8 20
                                       put x1
-                ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21
+                ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21
-                                                 put x1
+                                                    put x1
-                                                 put x2
+                                                    put x2
-                                                 put x3
+                                                    put x3
-                                                 put x4
+                                                    put x4
-                                                 put x5
+                                                    put x5
+                                                    put x6
                 DoUnify -> putWord8 22
                 CaseTac x1 -> do putWord8 23
                                  put x1
@@ -1954,7 +1955,8 @@ instance (Binary t) => Binary (PTactic' t) where
                             x3 <- get
                             x4 <- get
                             x5 <- get
-                            return (ProofSearch x1 x2 x3 x4 x5)
+                            x6 <- get
+                            return (ProofSearch x1 x2 x3 x4 x5 x6)
                    22 -> return DoUnify
                    23 -> do x1 <- get
                             return (CaseTac x1)

src/Idris/IdeMode.hs

@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String
                     | AddProofClause Int String
                     | AddMissing Int String
                     | MakeWithBlock Int String
+                    | MakeCaseBlock Int String
                     | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
                     | MakeLemma Int String
                     | LoadFile String (Maybe Int)
@@ -261,6 +262,7 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n
 sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name])   = Just (AddProofClause (fromInteger line) name)
 sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name])  = Just (AddMissing (fromInteger line) name)
 sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name])    = Just (MakeWithBlock (fromInteger line) name)
+sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name])    = Just (MakeCaseBlock (fromInteger line) name)
 -- The Boolean in ProofSearch means "search recursively"
 -- If it's False, that means "refine", i.e. apply the name and fill in any
 -- arguments which can be done by unification.

src/Idris/IdrisDoc.hs

@@ -360,8 +360,8 @@ extractPTactic (MatchRefine n)    = [n]
 extractPTactic (LetTac n p)       = n : extract p
 extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]
 extractPTactic (Exact p)          = extract p
-extractPTactic (ProofSearch _ _ _ m ns) | Just n <- m = n : ns
+extractPTactic (ProofSearch _ _ _ m _ ns) | Just n <- m = n : ns
-extractPTactic (ProofSearch _ _ _ _ ns) = ns
+extractPTactic (ProofSearch _ _ _ _ _ ns) = ns
 extractPTactic (Try t1 t2)        = concatMap extractPTactic [t1, t2]
 extractPTactic (TSeq t1 t2)       = concatMap extractPTactic [t1, t2]
 extractPTactic (ApplyTactic p)    = extract p

src/Idris/Interactive.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE PatternGuards #-}
 
 module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
-                         addMissing, makeWith, doProofSearch,
+                         addMissing, makeWith, makeCase, doProofSearch,
                          makeLemma) where
 
 {- Bits and pieces for editing source files interactively, called from
@@ -158,6 +158,47 @@ makeWith fn updatefile l n
            else iPrintResult with
   where getIndent s = length (takeWhile isSpace s)
 
+-- Replace the given metavariable on the given line with a 'case'
+-- block, using a _ for the scrutinee
+makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
+makeCase fn updatefile l n
+   = do src <- runIO $ readSource fn
+        let (before, tyline : later) = splitAt (l-1) (lines src)
+        let newcase = addCaseSkel (show n) tyline
+
+        if updatefile then
+           do let fb = fn ++ "~"
+              runIO $ writeSource fb (unlines (before ++ newcase ++ later))
+              runIO $ copyFile fb fn
+           else iPrintResult (showSep "\n" newcase)
+  where addCaseSkel n line =
+            let b = brackets False line in
+            case findSubstr ('?':n) line of
+                 Just (before, pos, after) ->
+                      [before ++ (if b then "(" else "") ++ "case _ of",
+                       take (pos + (if b then 6 else 5)) (repeat ' ') ++ 
+                             "case_val => ?" ++ n ++ if b then ")" else "",
+                       after]
+                 Nothing -> fail "No such metavariable"
+
+        -- Assume case needs to be bracketed unless the metavariable is
+        -- on its own after an =
+        brackets eq line | line == '?' : show n = not eq
+        brackets eq ('=':ls) = brackets True ls
+        brackets eq (' ':ls) = brackets eq ls
+        brackets eq (l : ls) = brackets False ls
+        brackets eq [] = True
+
+        findSubstr n xs = findSubstr' [] 0 n xs
+
+        findSubstr' acc i n xs | take (length n) xs == n 
+                = Just (reverse acc, i, drop (length n) xs)
+        findSubstr' acc i n [] = Nothing
+        findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs
+
+
+
+
 
 doProofSearch :: FilePath -> Bool -> Bool -> 
                  Int -> Name -> [Name] -> Maybe Int -> Idris ()
@@ -172,12 +213,13 @@ doProofSearch fn updatefile rec l n hints (Just depth)
                     [] -> return n
                     ns -> ierror (CantResolveAlts ns)
          i <- getIState
-         let (top, envlen, _) = case lookup mn (idris_metavars i) of
+         let (top, envlen, psnames, _) 
-                                  Just (t, e, False) -> (t, e, False)
+              = case lookup mn (idris_metavars i) of
-                                  _ -> (Nothing, 0, True)
+                     Just (t, e, ns, False) -> (t, e, ns, False)
+                     _ -> (Nothing, 0, [], True)
          let fc = fileFC fn
-         let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))
+         let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
-                                  (ProofSearch rec False depth t hints)]
+                                  (ProofSearch rec False depth t psnames hints)]
          let def = PClause fc mn (PRef fc [] mn) [] (body top) []
          newmv <- idrisCatch
              (do elabDecl' EAll recinfo (PClauses fc [] mn [def])
@@ -256,13 +298,17 @@ makeLemma fn updatefile l n
                     ns -> ierror (CantResolveAlts (map fst ns))
         i <- getIState
         margs <- case lookup n (idris_metavars i) of
-                      Just (_, arity, _) -> return arity
+                      Just (_, arity, _, _) -> return arity
                       _ -> return (-1)
 
         if (not isProv) then do
-            let skip = guessImps (tt_ctxt i) mty
+            let skip = guessImps i (tt_ctxt i) mty
+            let classes = guessClasses i (tt_ctxt i) mty
 
-            let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
+            let lem = show n ++ " : " ++ 
+                            constraints i classes mty ++
+                            showTmOpts (defaultPPOption { ppopt_pinames = True })
+                                       (stripMNBind skip (delab i mty))
             let lem_app = show n ++ appArgs skip margs mty
 
             if updatefile then
@@ -312,15 +358,52 @@ makeLemma fn updatefile l n
         stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc
         stripMNBind skip t = t
 
+        constraints :: IState -> [Name] -> Type -> String
+        constraints i [] ty = ""
+        constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
+        constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
+
+        showConstraints i ns (Bind n (Pi _ ty _) sc)
+            | n `elem` ns = show (delab i ty) : 
+                              showConstraints i ns (substV (P Bound n Erased) sc)
+            | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
+        showConstraints _ _ _ = []
+
         -- Guess which binders should be implicits in the generated lemma.
         -- Make them implicit if they appear guarded by a top level constructor,
         -- or at the top level themselves.
-        guessImps :: Context -> Term -> [Name]
+        -- Also, make type class instances implicit
-        guessImps ctxt (Bind n (Pi _ _ _) sc)
+        guessImps :: IState -> Context -> Term -> [Name]
+        guessImps ist ctxt (Bind n (Pi _ ty _) sc)
            | guarded ctxt n (substV (P Bound n Erased) sc) 
-                = n : guessImps ctxt sc
+                = n : guessImps ist ctxt sc
-           | otherwise = guessImps ctxt sc
+           | isClass ist ty
-        guessImps ctxt _ = []
+                = n : guessImps ist ctxt sc
+           | otherwise = guessImps ist ctxt sc
+        guessImps ist ctxt _ = []
+
+        guessClasses :: IState -> Context -> Term -> [Name]
+        guessClasses ist ctxt (Bind n (Pi _ ty _) sc)
+           | isParamClass ist ty
+                = n : guessClasses ist ctxt sc
+           | otherwise = guessClasses ist ctxt sc
+        guessClasses ist ctxt _ = []
+
+        isClass ist t
+           | (P _ n _, args) <- unApply t
+                = case lookupCtxtExact n (idris_classes ist) of
+                       Just _ -> True
+                       _ -> False
+           | otherwise = False
+        
+        isParamClass ist t
+           | (P _ n _, args) <- unApply t
+                = case lookupCtxtExact n (idris_classes ist) of
+                       Just _ -> any isV args
+                       _ -> False
+           | otherwise = False
+          where isV (V _) = True
+                isV _ = False
 
         guarded ctxt n (P _ n' _) | n == n' = True
         guarded ctxt n ap@(App _ _ _)

src/Idris/ParseData.hs

@@ -86,25 +86,26 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
 
         let constructorDoc' = annotate syn ist constructorDoc
 
-        fields <- many . indented $ field syn
+        fields <- many . indented $ fieldLine syn
 
-        return (fields, constructorName, constructorDoc')
+        return (concat fields, constructorName, constructorDoc')
       where
-        field :: SyntaxInfo -> IdrisParser ((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))
+        fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
-        field syn = do doc <- optional docComment
+        fieldLine syn = do
-                       c <- optional $ lchar '{'
+            doc <- optional docComment
-                       n <- (do (n, nfc) <- fnName
+            c <- optional $ lchar '{'
-                                return $ Just (expandNS syn n, nfc))
+            let oneName = (do (n, nfc) <- fnName
-                        <|> (do symbol "_"
+                              return $ Just (expandNS syn n, nfc))
-                                return Nothing)
+                          <|> (symbol "_" >> return Nothing)
-                       lchar ':'
+            ns <- commaSeparated oneName
-                       t <- typeExpr (allowImp syn)
+            lchar ':'
-                       p <- endPlicity c
+            t <- typeExpr (allowImp syn)
-                       ist <- get
+            p <- endPlicity c
-                       let doc' = case doc of -- Temp: Throws away any possible arg docs
+            ist <- get
-                                   Just (d,_) -> Just $ annotate syn ist d
+            let doc' = case doc of -- Temp: Throws away any possible arg docs
-                                   Nothing    -> Nothing
+                        Just (d,_) -> Just $ annotate syn ist d
-                       return (n, p, t, doc')
+                        Nothing    -> Nothing
+            return $ map (\n -> (n, p, t, doc')) ns
 
         constructor :: IdrisParser (Name, FC)
         constructor = (reservedHL "constructor") *> fnName

src/Idris/ParseExpr.hs

@@ -971,7 +971,7 @@ autoImplicit opts st syn
         sc <- expr syn
         highlightP kw AnnKeyword
         return (bindList (PPi
-          (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc) 
+          (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc) 
 
 defaultImplicit opts st syn = do
    kw <- reservedFC "default"
@@ -1436,7 +1436,7 @@ tactics =
   , noArgs ["unify"] DoUnify
   , (["search"], Nothing, const $
       do depth <- option 10 $ fst <$> natural
-         return (ProofSearch True True (fromInteger depth) Nothing []))
+         return (ProofSearch True True (fromInteger depth) Nothing [] []))
   , noArgs ["instance"] TCInstance
   , noArgs ["solve"] Solve
   , noArgs ["attack"] Attack

src/Idris/ParseHelpers.hs

@@ -434,6 +434,11 @@ bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PT
 bindList b []              sc = sc
 bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)
 
+{- | @commaSeparated p@ parses one or more occurences of `p`,
+     separated by commas and optional whitespace. -}
+commaSeparated :: MonadicParsing m => m a -> m [a]
+commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)
+
 {- * Layout helpers -}
 
 -- | Push indentation to stack

src/Idris/ProofSearch.hs

@@ -22,10 +22,10 @@ import Debug.Trace
 -- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
 
 trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
-trivial = trivialHoles []
+trivial = trivialHoles [] []
 
-trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
+trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
-trivialHoles ok elab ist
+trivialHoles psnames ok elab ist
                  = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])
                             return ())
                         (do env <- get_env
@@ -41,7 +41,7 @@ trivialHoles ok elab ist
                 g <- goal
                 -- anywhere but the top is okay for a hole, if holesOK set
                 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
-                   holesOK hs (binderTy b)
+                   holesOK hs (binderTy b) && (null psnames || x `elem` psnames)
                    then try' (elab (PRef (fileFC "prf") [] x))
                              (tryAll xs) True
                    else tryAll xs
@@ -73,9 +73,11 @@ proofSearch :: Bool -> -- recursive search (False for 'refine')
                Bool -> -- ambiguity ok
                Bool -> -- defer on failure
                Int -> -- maximum depth
-               (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
+               (PTerm -> ElabD ()) -> Maybe Name -> Name -> 
+               [Name] ->
+               [Name] ->
                IState -> ElabD ()
-proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
+proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist
        = do -- get all possible versions of the name, take the first one that
             -- works
             let all_imps = lookupCtxtName fn (idris_implicits ist)
@@ -106,7 +108,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
 
     isImp (PImp p _ _ _ _) = (True, p)
     isImp arg = (True, priority arg) -- try to get all of them by unification
-proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist 
+proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist 
        = do compute
             ty <- goal
             hs <- get_holes
@@ -177,7 +179,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
                       ty <- goal
                       when (S.member ty tys) $ fail "Been here before"
                       let tys' = S.insert ty tys
-                      try' (trivial elab ist)
+                      try' (trivialHoles psnames [] elab ist)
                            (try' (try' (resolveByCon (d - 1) locs tys') 
                                        (resolveByLocals (d - 1) locs tys')
                                  True)
@@ -199,11 +201,13 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
                                            Nothing -> []
                                            Just hs -> hs
                       case lookupCtxtExact n (idris_datatypes ist) of
-                          Just t -> tryCons d locs tys 
+                          Just t -> do
-                                                   (hints ++ 
+                             let others = hints ++ con_names t ++ autohints
-                                                    con_names t ++ 
+                             when (not fromProver) -- in interactive mode,
-                                                    autohints ++ 
+                                   -- don't just guess (fine for 'auto',
-                                                    getFn d fn)
+                                   -- since that's part of the point...)
+                                   $ checkConstructor ist others
+                             tryCons d locs tys (others ++ getFn d fn)
                           Nothing -> fail "Not a data type"
                 _ -> fail "Not a data type"
 
@@ -215,7 +219,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
 
     tryLocals d locs tys [] = fail "Locals failed"
     tryLocals d locs tys ((x, t) : xs) 
-       | x `elem` locs = tryLocals d locs tys xs
+       | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
        | otherwise = try' (tryLocal d (x : locs) tys x t) 
                           (tryLocals d locs tys xs) True
 
@@ -245,12 +249,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
             ps' <- get_probs
             hs' <- get_holes
             when (length ps < length ps') $ fail "Can't apply constructor"
+            let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)
             mapM_ (\ (_, h) -> do focus h
                                   aty <- goal
-                                  psRec True d locs tys)
+                                  psRec True d locs tys) newhs      
-                  (filter (\ (x, y) -> not x) (zip (map fst imps) args))
             solve
 
     isImp (PImp p _ _ _ _) = (True, p)
     isImp arg = (False, priority arg) 
 
+-- In interactive mode, only search for things if there is some constructor
+-- index to help pick a relevant constructor
+checkConstructor :: IState -> [Name] -> ElabD ()
+checkConstructor ist [] = return ()
+checkConstructor ist (n : ns) =
+    case lookupTyExact n (tt_ctxt ist) of
+         Just t -> if not (conIndexed t)
+                      then fail "Overlapping constructor types"
+                      else checkConstructor ist ns
+  where
+    conIndexed t = let (_, args) = unApply (getRetTy t) in
+                       any conHead args
+    conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)
+              | otherwise = False

src/Idris/REPL.hs

@@ -366,6 +366,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =
   process fn (AddMissing False line (sUN name))
 runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =
   process fn (MakeWith False line (sUN name))
+runIdeModeCommand h id orig fn mods (IdeMode.MakeCaseBlock line name) =
+  process fn (MakeCase False line (sUN name))
 runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =
   doProofSearch fn False r line (sUN name) (map sUN hints) depth
 runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =
@@ -632,6 +634,7 @@ idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClaus
 idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)
 idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)
 idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)
+idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str)
 idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)
 idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)
                                            iPrintResult ""
@@ -901,8 +904,8 @@ process fn (Check (PRef _ _ n))
         case lookupNames n ctxt of
           ts@(t:_) ->
             case lookup t (idris_metavars ist) of
-                Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
+                Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
-                                  showMetavarInfo ppo ist n i
+                                     showMetavarInfo ppo ist n i
                 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
           [] -> iPrintError $ "No such variable " ++ show n
   where
@@ -934,12 +937,14 @@ process fn (Check t)
         ctxt <- getContext
         ist <- getIState
         let ppo = ppOptionIst ist
-            ty' = normaliseC ctxt [] ty
+            ty' = if opt_evaltypes (idris_options ist)
+                     then normaliseC ctxt [] ty
+                     else ty
         case tm of
            TType _ ->
              iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc
            _ -> iPrintTermWithType (pprintDelab ist tm)
-                                   (pprintDelab ist ty)
+                                   (pprintDelab ist ty')
 
 process fn (Core t)
    = do (tm, ty) <- elabREPL recinfo ERHS t
@@ -1047,6 +1052,8 @@ process fn (AddMissing updatefile l n)
     = addMissing fn updatefile l n
 process fn (MakeWith updatefile l n)
     = makeWith fn updatefile l n
+process fn (MakeCase updatefile l n)
+    = makeCase fn updatefile l n
 process fn (MakeLemma updatefile l n)
     = makeLemma fn updatefile l n
 process fn (DoProofSearch updatefile rec l n hints)
@@ -1072,7 +1079,7 @@ process fn (RmProof n')
                             insertMetavar n =
                               do i <- getIState
                                  let ms = idris_metavars i
-                                 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }
+                                 putIState $ i { idris_metavars = (n, (Nothing, 0, [], False)) : ms }
 
 process fn' (AddProof prf)
   = do fn <- do
@@ -1125,8 +1132,8 @@ process fn (Prove mode n')
           let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
           n <- case metavars of
               [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
-              [(n, (_,_,False))] -> return n
+              [(n, (_,_,_,False))] -> return n
-              [(_, (_,_,True))]  -> ierror (Msg $ "Declarations not solvable using prover")
+              [(_, (_,_,_,True))]  -> ierror (Msg $ "Declarations not solvable using prover")
               ns -> ierror (CantResolveAlts (map fst ns))
           prover mode (lit fn) n
           -- recheck totality
@@ -1234,6 +1241,8 @@ process fn (SetOpt NoBanner)      = setNoBanner True
 process fn (UnsetOpt NoBanner)    = setNoBanner False
 process fn (SetOpt WarnReach)     = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)
 process fn (UnsetOpt WarnReach)   = fmodifyState opts_idrisCmdline $ delete WarnReach
+process fn (SetOpt EvalTypes)     = setEvalTypes True
+process fn (UnsetOpt EvalTypes)   = setEvalTypes False
 
 process fn (SetOpt _) = iPrintError "Not a valid option"
 process fn (UnsetOpt _) = iPrintError "Not a valid option"

src/Idris/REPLParser.hs

@@ -123,6 +123,8 @@ parserCommands =
       ":am <line> <name> adds all missing pattern matches for the name on the line"
   , proofArgCmd ["mw", "makewith"] MakeWith
       ":mw <line> <name> adds a with clause for the definition of the name on the line"
+  , proofArgCmd ["mc", "makecase"] MakeCase
+      ":mc <line> <name> adds a case block for the definition of the metavariable on the line"
   , proofArgCmd ["ml", "makelemma"] MakeLemma "?"
   , (["log"], NumberArg, "Set logging verbosity level", cmd_log)
   , (["lto", "loadto"], SeqArgs NumberArg FileArg
@@ -257,6 +259,7 @@ optArg cmd name = do
               <|> do discard (P.symbol "autosolve"); return AutoSolve
               <|> do discard (P.symbol "nobanner") ; return NoBanner
               <|> do discard (P.symbol "warnreach"); return WarnReach
+              <|> do discard (P.symbol "evaltypes"); return EvalTypes
 
 proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)
 proofArg cmd name = do

src/Idris/Reflection.hs

@@ -82,7 +82,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)
 reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
 reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
 reifyApp _ t [Constant (I i)]
-           | t == reflm "Search" = return (ProofSearch True True i Nothing [])
+           | t == reflm "Search" = return (ProofSearch True True i Nothing [] [])
 reifyApp _ t [x]
            | t == reflm "Refine" = do n <- reifyTTName x
                                       return $ Refine n []
@@ -313,7 +313,7 @@ reifyTTBinderApp reif f [x, y]
 reifyTTBinderApp reif f [t]
                       | f == reflm "Hole" = liftM Hole (reif t)
 reifyTTBinderApp reif f [t]
-                      | f == reflm "GHole" = liftM (GHole 0) (reif t)
+                      | f == reflm "GHole" = liftM (GHole 0 []) (reif t)
 reifyTTBinderApp reif f [x, y]
                       | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
 reifyTTBinderApp reif f [t]
@@ -339,7 +339,7 @@ reifyTTConstApp f (Constant c@(BI _))
                 | f == reflm "BI"  = return $ c
 reifyTTConstApp f (Constant c@(Fl _))
                 | f == reflm "Fl"  = return $ c
-reifyTTConstApp f (Constant c@(I _))
+reifyTTConstApp f (Constant c@(Ch _))
                 | f == reflm "Ch"  = return $ c
 reifyTTConstApp f (Constant c@(Str _))
                 | f == reflm "Str" = return $ c
@@ -586,7 +586,7 @@ reflectBinderQuotePattern q ty unq (Hole t)
         fill $ reflCall "Hole" [ty, Var t']
         solve
         focus t'; q unq t
-reflectBinderQuotePattern q ty unq (GHole _ t)
+reflectBinderQuotePattern q ty unq (GHole _ _ t)
    = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
         fill $ reflCall "GHole" [ty, Var t']
         solve
@@ -737,7 +737,7 @@ reflectBinderQuote q ty unq (NLet x y)
    = reflCall "NLet" [Var ty, q unq x, q unq y]
 reflectBinderQuote q ty unq (Hole t)
    = reflCall "Hole" [Var ty, q unq t]
-reflectBinderQuote q ty unq (GHole _ t)
+reflectBinderQuote q ty unq (GHole _ _ t)
    = reflCall "GHole" [Var ty, q unq t]
 reflectBinderQuote q ty unq (Guess x y)
    = reflCall "Guess" [Var ty, q unq x, q unq y]

src/Pkg/Package.hs

@@ -132,17 +132,17 @@ documentPkg fp =
   do pkgdesc        <- parseDesc fp
      cd             <- getCurrentDirectory
      let pkgDir      = cd </> takeDirectory fp
-         outputDir   = cd </> (pkgname pkgdesc) ++ "_doc"
+         outputDir   = cd </> pkgname pkgdesc ++ "_doc"
          opts        = NoREPL : Verbose : idris_opts pkgdesc
          mods        = modules pkgdesc
          fs          = map (foldl1' (</>) . splitOn "." . showCG) mods
      setCurrentDirectory $ pkgDir </> sourcedir pkgdesc
      make (makefile pkgdesc)
-     setCurrentDirectory $ pkgDir
+     setCurrentDirectory pkgDir
      let run l       = runExceptT . execStateT l
          load []     = return ()
          load (f:fs) = do loadModule f; load fs
-         loader      = do idrisMain opts; load fs
+         loader      = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs
      idrisInstance  <- run loader idrisInit
      setCurrentDirectory cd
      case idrisInstance of

stack.yaml

@@ -0,0 +1,6 @@
+flags: {}
+packages:
+- '.'
+extra-deps: 
+- cheapskate-0.1.0.4
+resolver: nightly-2015-07-24

test/disambig001/disambig001.idr

@@ -1,12 +0,0 @@
-module Main
-
-import Prelude.Monad
-
-import System
-import Effect.System
-
-main : IO ()
-main = do 
-    args <- System.getArgs
-    putStrLn (concat (drop 1 args))
-

test/disambig001/expected

@@ -1 +0,0 @@
-foobar

test/disambig001/run

@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-idris $@ disambig001.idr -p effects -o disambig001
-./disambig001 foo bar
-rm -f disambig001 *.ibc

test/docs003/expected

@@ -11,11 +11,11 @@ Methods:
         The function is Total
 Instances:
     Functor List
+    Functor (IO' ffi)
     Functor Stream
     Functor Provider
     Functor Binder
     Functor PrimIO
-    Functor (IO' ffi)
     Functor Maybe
     Functor (Either e)
 

test/effects005/defaultlog.idr

@@ -0,0 +1,18 @@
+import Effects
+import Effect.Logging.Default
+
+func : Nat -> Eff () [LOG String]
+func x = do
+  log WARN Nil $ unwords ["I do nothing with", show x]
+  pure ()
+
+doubleFunc : Nat -> Eff Nat [LOG String]
+doubleFunc x = do
+  log WARN ["NumOPS"] $ unwords ["Doing the double with", show x ]
+  func x
+  pure (x+x)
+
+main : IO ()
+main = do
+   x <- runInit [(ALL,["NumOPS"])] (doubleFunc 3)
+   printLn x

test/effects005/expected

@@ -0,0 +1,5 @@
+"3 : Doing the double with 3"
+6
+8
+"3 : [\"NumOPS\"] : Doing the double with 3"
+6

test/effects005/run

@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+idris $@ simplelog.idr -o simple -p effects
+./simple
+idris $@ defaultlog.idr -o default -p effects
+./default
+rm -f simple default *.ibc

test/effects005/simplelog.idr

@@ -0,0 +1,14 @@
+import Effects
+import Effect.Logging.Simple
+
+doubleFunc : Nat -> Eff Nat [LOG]
+doubleFunc x = do
+  log WARN $ unwords ["Doing the double with", show x ]
+  pure (x+x)
+
+main : IO ()
+main = do
+   x <- runInit [ALL] (doubleFunc 3)
+   printLn x
+   y <- runInit [OFF] (doubleFunc 4)
+   printLn y

test/interactive003/expected

@@ -2,3 +2,4 @@ ys
 x :: app xs ys
 []
 f x y :: vzipWith f xs ys
+?word_length_rhs_3 :: word_length xs

test/interactive003/input

@@ -2,3 +2,4 @@
 :ps 5 app_rhs_2
 :ps 8 vzipWith_rhs_3
 :ps 9 vzipWith_rhs_1
+:ps 13 word_length_rhs_2

test/interactive003/interactive003.idr

@@ -8,3 +8,8 @@ vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
 vzipWith f [] [] = ?vzipWith_rhs_3
 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1
 
+word_length : Vect n String -> Vect n Nat
+word_length [] = []
+word_length (x :: xs) = ?word_length_rhs_2
+
+

test/proof001/test029.idr

@@ -29,7 +29,7 @@ append (x :: xs) ys ?= x :: append xs ys
 simple.append_lemma_2 = proof {
   intros;
   compute;
-  rewrite (plusSuccRightSucc m n);
+  rewrite (plusSuccRightSucc m k);
   trivial;
 }
 

test/records004/expected

@@ -0,0 +1,3 @@
+"Fred"
+"Joe"
+"Bloggs"

test/records004/records004.idr

@@ -0,0 +1,13 @@
+-- Test for multiple field declarations on one line with the same type
+
+record Person where
+  constructor MkPerson
+  firstName, middleName, lastName : String
+
+fred : Person
+fred = MkPerson "Fred" "Joe" "Bloggs"
+
+main : IO ()
+main = do printLn (firstName fred)
+          printLn (middleName fred)
+          printLn (lastName fred)

test/records004/run

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+idris $@ records004.idr -o records004
+./records004
+rm -f records004 *.ibc

test/tutorial006/expected

@@ -1,15 +1,15 @@
 tutorial006a.idr:5:23-25:When checking right hand side of vapp:
 When checking argument xs to constructor Data.VectType.Vect.:::
         Type mismatch between
-                Vect (n + n) a (Type of vapp xs xs)
+                Vect (k + k) a (Type of vapp xs xs)
         and
-                Vect (plus n m) a (Expected type)
+                Vect (plus k m) a (Expected type)
         
         Specifically:
                 Type mismatch between
-                        plus n n
+                        plus k k
                 and
-                        plus n m
+                        plus k m
 tutorial006b.idr:10:10:
 When checking right hand side of with block in Main.parity:
 Type mismatch between