763ac00 · Idris-dev · git.iko.soy

.gitignore+1

@@ -28,3 +28,4 @@ test/*[0-9][0-9][0-9]/*.exe

2828tags

2929TAGS

3030src/Version_idris.hs

31+.stack-work

CHANGELOG+3

@@ -24,6 +24,9 @@ New in 0.9.19:

2424* More flexible 'case' construct, allowing each branch to target different

2525 types, provided that the case analysis does not affect the form of any

2626 variable used in the right hand side of the case.

27+* Some improvements in interactive editing, particularly in lifting out

28+ definitions and proof search.

29+* Moved System.Interactive, along with getArgs to the Prelude.

2730

2831New in 0.9.18:

2932--------------

docs/reference/syntax-guide.rst+10−1

@@ -29,7 +29,7 @@ Types

2929

3030In Idris, types are first class values. So a type declaration is the

3131same as just declaration of a variable whose type is ``Type``. In Idris,

32−variables that denote a type must being with a capital letter. Example:

32+variables that denote a type must begin with a capital letter. Example:

3333

3434.. code:: idris

3535

@@ -254,6 +254,15 @@ Comments

254254 -- Single Line

255255 {- Multiline -}

256256 ||| Docstring (goes before definition)

257+

258+Multi line String literals

259+~~~~~~~~~~~~~~~~~~~~~~~~~~

260+

261+::

262+

263+ foo = """

264+ this is a

265+ string literal"""

257266

258267Directives

259268----------

docs/tutorial/classes.rst+4−4

@@ -363,10 +363,10 @@ alternative notion of function application, with explicit calls to

363363 m_add' x y = m_app (m_app (Just (+)) x) y

364364

365365Rather than having to insert ``m_app`` everywhere there is an

366−application, we can use to do the job for us. To do this, we can make

367−``Maybe`` an instance of ``Applicative`` as follows, where ``<*>`` is

368−defined in the same way as ``m_app`` above (this is defined in the

369−Idris library):

366+application, we can use idiom brackets to do the job for us.

367+To do this, we can make ``Maybe`` an instance of ``Applicative``

368+as follows, where ``<*>`` is defined in the same way as ``m_app``

369+above (this is defined in the Idris library):

370370

371371.. code-block:: idris

372372

docs/tutorial/modules.rst+3−3

@@ -34,7 +34,7 @@ module which defines a binary tree type ``BTree`` (in a file

3434

3535

3636Then, this gives a main program (in a file

37−``bmain.idr``) which uses the ``bst`` module to sort a list:

37+``bmain.idr``) which uses the ``Btree`` module to sort a list:

3838

3939.. code-block:: idris

4040

@@ -50,7 +50,7 @@ Then, this gives a main program (in a file

5050

5151The same names can be defined in multiple modules. This is possible

5252because in practice names are *qualified* with the name of the module.

53−The names defined in the ``btree`` module are, in full:

53+The names defined in the ``Btree`` module are, in full:

5454

5555+ ``Btree.BTree``

5656+ ``Btree.Leaf``

@@ -99,7 +99,7 @@ and classes to be marked as: ``public``, ``abstract`` or ``private``:

9999.. note::

100100 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.

101101

102−For our ``btree`` module, it makes sense for the tree data type and the

102+For our ``Btree`` module, it makes sense for the tree data type and the

103103functions to be exported as ``abstract``, as we see below:

104104

105105.. code-block:: idris

docs/tutorial/packages.rst+3−3

@@ -54,9 +54,9 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile

5454 package only. This differs from build that type checks **and**

5555 generates code.

5656

57−+ ``idris --mathspkg maths.ipkg`` will compile and run any embedded

58− mathss you have specified in the ``tests`` paramater. More

59− information about mathsing is given in the next section.

57++ ``idris --testpkg maths.ipkg`` will compile and run any embedded

58+ tests you have specified in the ``tests`` paramater. More

59+ information about testing is given in the next section.

6060

6161Once the maths package has been installed, the command line option

6262``--package maths`` makes it accessible (abbreviated to ``-p maths``).

docs/tutorial/testing.rst+31−11

@@ -4,18 +4,27 @@

44Testing Idris Packages

55**********************

66

7−As part of the integrated build system a simple testing framework is provided.

8−This framework will collect a list of named functions and construct an Idris executable in a fresh environment on your machine.

9−This executable lists the named functions under a single ``main`` function, and imports the complete list of modules for the package.

7+The integrated build system includes a simple testing framework.

8+This framework collects functions listed in the ``ipkg`` file under ``tests``.

9+All test functions must return ``IO ()``.

1010

1111

12−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.

13−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.

12+When you enter ``idris --testpkg yourmodule.ipkg``,

13+the build system creates a temporary file in a fresh environment on your machine

14+by listing the ``tests`` functions under a single ``main`` function.

15+It compiles this temporary file to an executable and then executes it.

16+

17+

18+The tests themselves are responsible for reporting their success or failure.

19+Test functions commonly use ``putStrLn`` to report test results.

20+The test framework does not impose any standards for reporting and consequently

21+does not aggregate test results.

1422

1523

1624For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

1725

1826.. code-block:: idris

27+ :caption: Math/NumOps.idr

1928

2029 module Maths.NumOps

2130

@@ -28,6 +37,7 @@ For example, lets take the following list of functions that are defined in a mod

2837A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

2938

3039.. code-block:: idris

40+ :caption: Math/TestOps.idr

3141

3242 module Test.NumOps

3343

@@ -36,12 +46,12 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a

3646 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()

3747 assertEq g e = if g == e

3848 then putStrLn "Test Passed"

39− else putStrLn "Test failed"

49+ else putStrLn "Test Failed"

4050

4151 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()

4252 assertNotEq g e = if not (g == e)

4353 then putStrLn "Test Passed"

44− else putStrLn "Test failed"

54+ else putStrLn "Test Failed"

4555

4656 testDouble : IO ()

4757 testDouble = assertEq (double 2) 4

@@ -53,13 +63,23 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a

5363The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.

5464The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::

5565

56− module maths

66+ package maths

5767

58− module = Maths.NumOps

59− , Test.NumOps

68+ modules = Maths.NumOps

69+ , Test.NumOps

6070

6171 tests = Test.NumOps.testDouble

6272 , Test.NumOps.testTriple

6373

6474

65−The testing framework can be invoked using: ``idris --testpkg maths.ipkg``.

75+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

76+

77+ > idris --testpkg maths.ipkg

78+ Type checking ./Maths/NumOps.idr

79+ Type checking ./Test/NumOps.idr

80+ Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr

81+ Test Passed

82+ Test Passed

83+

84+Note how both tests have reported success by printing ``Test Passed``

85+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

docs/tutorial/typesfuns.rst+18−20

@@ -103,7 +103,7 @@ symbols:

103103

104104::

105105

106− :+-*/=_.?|&><!@$%^~.

106+ :+-*\/=.?|&><!@$%^~#

107107

108108Some operators built from these symbols can't be user defined. These are

109109``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,

@@ -349,7 +349,7 @@ following:

349349 $ idris vbroken.idr --check

350350 vbroken.idr:9:23:When elaborating right hand side of Vect.++:

351351 When elaborating an application of constructor Vect.:::

352− Type mismatch between

352+ Type mismatch between

353353 Vect (k + k) a (Type of xs ++ xs)

354354 and

355355 Vect (plus k m) a (Expected type)

@@ -442,7 +442,7 @@ names, ``n`` and ``a``, which are not declared explicitly. These are

442442Implicit arguments, given in braces ``{}`` in the type declaration,

443443are not given in applications of ``index``; their values can be

444444inferred from the types of the ``Fin n`` and ``Vect n a``

445−arguments. Any name beginning with a lower case letter which appears

445+arguments. Any name beginning with a lower case letter which appears

446446as a parameter or index in a

447447type declaration, but which is otherwise unbound, will be automatically

448448bound as an implicit argument. Implicit arguments can still be given

@@ -912,10 +912,6 @@ Intermediate values can be calculated using ``let`` bindings:

912912 showPerson p = let MkPerson name age = p in

913913 name ++ " is " ++ show age ++ " years old"

914914

915− splitAt : Char -> String -> (String, String)

916− splitAt c x = case break (== c) x of

917− (x, y) => (x, strTail y)

918−

919915We can do simple pattern matching in ``let`` bindings too. For

920916example, we can extract fields from a record as follows, as well as by

921917pattern matching at the top level:

@@ -1021,26 +1017,28 @@ example, we can represent a person's name and age in a record:

10211017

10221018 record Person where

10231019 constructor MkPerson

1024− name : String

1020+ firstName, middleName, lastName : String

10251021 age : Int

10261022

10271023 fred : Person

1028− fred = MkPerson "Fred" 30

1024+ fred = MkPerson "Fred" "Joe" "Bloggs" 30

10291025

10301026Records can have *parameters*, which are listed between the record

10311027name and the ``where`` keyword, and *fields*, which are in an indented

1032−block following the `where` keyword (here, ``name`` and ``age``). The

1033−constructor name is provided after the ``constructor`` keyword. The

1034−field names can be used to access the field values:

1028+block following the `where` keyword (here, ``firstName``, ``middleName``,

1029+``lastName``, and ``age``). You can declare multiple fields on a single

1030+line, provided that they have the same type. The constructor name is

1031+provided after the ``constructor`` keyword. The field names can be used to

1032+access the field values:

10351033

10361034::

10371035

1038− *record> name fred

1036+ *record> firstName fred

10391037 "Fred" : String

10401038 *record> age fred

10411039 30 : Int

1042− *record> :t name

1043− name : Person -> String

1040+ *record> :t firstName

1041+ firstName : Person -> String

10441042

10451043We can also use the field names to update a record (or, more

10461044precisely, produce a copy of the record with the given fields

@@ -1048,10 +1046,10 @@ updated):

10481046

10491047.. code-block:: bash

10501048

1051− *record> record { name = "Jim" } fred

1052− MkPerson "Jim" 30 : Person

1053− *record> record { name = "Jim", age = 20 } fred

1054− MkPerson "Jim" 20 : Person

1049+ *record> record { firstName = "Jim" } fred

1050+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person

1051+ *record> record { firstName = "Jim", age = 20 } fred

1052+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person

10551053

10561054The syntax ``record { field = val, ... }`` generates a function which

10571055updates the given fields in a record.

@@ -1078,7 +1076,7 @@ length because it will not affect the type of the record:

10781076::

10791077

10801078 *record> addStudent fred (ClassInfo [] "CS")

1081− ClassInfo [MkPerson "Fred" 30] "CS" : Class

1079+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class

10821080

10831081Nested record update

10841082--------------------

idris.cabal+6−3

@@ -118,6 +118,7 @@ Extra-source-files:

118118 libs/contrib/Data/*.idr

119119 libs/contrib/Data/Nat/*.idr

120120 libs/contrib/Data/Nat/DivMod/*.idr

121+ libs/contrib/Data/Matrix/*.idr

121122 libs/contrib/Decidable/*.idr

122123 libs/contrib/Network/*.idr

123124 libs/contrib/System/Concurrency/*.idr

@@ -125,6 +126,7 @@ Extra-source-files:

125126 libs/effects/Makefile

126127 libs/effects/effects.ipkg

127128 libs/effects/Effect/*.idr

129+ libs/effects/Effect/Logging/*.idr

128130 libs/effects/*.idr

129131

130132 test/Makefile

@@ -388,9 +390,6 @@ Extra-source-files:

388390 test/delab001/expected

389391 test/delab001/input

390392

391− test/disambig001/run

392− test/disambig001/*.idr

393− test/disambig001/expected

394393 test/disambig002/run

395394 test/disambig002/*.idr

396395 test/disambig002/expected

@@ -424,6 +423,10 @@ Extra-source-files:

424423 test/effects004/*.idr

425424 test/effects004/expected

426425 test/effects004/input

426+ test/effects005/run

427+ test/effects005/*.idr

428+ test/effects005/expected

429+

427430

428431 test/error001/run

429432 test/error001/*.idr

libs/base/Data/Complex.idr+6−1

@@ -27,7 +27,6 @@ instance Show a => Show (Complex a) where

2727 plus_i = User 6

2828

2929

30−

3130-- when we have a type class 'Fractional' (which contains Float and Double),

3231-- we can do:

3332{-

@@ -61,6 +60,12 @@ phase (x:+y) = atan2 y x

6160conjugate : Num a => Complex a -> Complex a

6261conjugate (r:+i) = (r :+ (0-i))

6362

63+instance Functor Complex where

64+ map f (r :+ i) = f r :+ f i

65+

66+instance Neg a => Neg (Complex a) where

67+ negate = map negate

68+

6469-- We can't do "instance Num a => Num (Complex a)" because

6570-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float

6671instance Num (Complex Float) where

libs/base/Data/HVect.idr−1

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

11module Data.HVect

22

3−import Data.Fin

43import public Data.Vect

54

65%access public

libs/base/Data/Vect.idr+27

@@ -52,3 +52,30 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)

5252mapElem Here = Here

5353mapElem (There e) = There (mapElem e)

5454

55+-- Some convenience functions for testing lengths

56+

57+||| If the given Vect is the required length, return a Vect with that

58+||| length in its type, otherwise return Nothing

59+||| @len the required length

60+||| @xs the vector with the desired length

61+-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we

62+-- only know we don't know how to make a Vect n a, not that one can't exist.

63+isLength : {m : Nat} -> -- expected at run-time

64+ (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)

65+isLength {m} len xs with (decEq m len)

66+ isLength {m = m} m xs | (Yes Refl) = Just xs

67+ isLength {m = m} len xs | (No contra) = Nothing

68+

69+||| If the given Vect is at least the required length, return a Vect with

70+||| at least that length in its type, otherwise return Nothing

71+||| @len the required length

72+||| @xs the vector with the desired length

73+overLength : {m : Nat} -> -- expected at run-time

74+ (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)

75+overLength {m} n xs with (cmp m n)

76+ overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing

77+ overLength {m = m} m xs | CmpEQ

78+ = Just (0 ** xs)

79+ overLength {m = plus n (S x)} n xs | (CmpGT x)

80+ = Just (S x ** rewrite plusCommutative (S x) n in xs)

81+

libs/base/Data/VectType.idr+8−3

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

11module Data.VectType

22

3−import Data.Fin

3+import public Data.Fin

44

55%access public

66%default total

@@ -9,9 +9,14 @@ namespace Vect {

99

1010infixr 7 ::

1111

12−%elim data Vect : Nat -> Type -> Type where

12+||| Vectors: Generic lists with explicit length in the type

13+%elim

14+data Vect : Nat -> Type -> Type where

15+ ||| Empty vector

1316 Nil : Vect Z a

14− (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

17+ ||| A non-empty vector of length `S k`, consisting of a head element and

18+ ||| the rest of the list, of length `k`.

19+ (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

1520

1621-- Hints for interactive editing

1722%name Vect xs,ys,zs,ws

libs/base/System.idr−16

@@ -4,22 +4,6 @@ module System

44%default partial

55%access public

66

7−||| Get the command-line arguments that the program was called with.

8−getArgs : IO (List String)

9−getArgs = do n <- numArgs

10− ga' [] 0 n

11− where

12− numArgs : IO Int

13− numArgs = foreign FFI_C "idris_numArgs" (IO Int)

14−

15− getArg : Int -> IO String

16− getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x

17−

18− ga' : List String -> Int -> Int -> IO (List String)

19− ga' acc i n = if (i == n) then (return $ reverse acc) else

20− do arg <- getArg i

21− ga' (arg :: acc) (i+1) n

22−

237||| Retrieves an value from the environment, if the given key is present,

248||| otherwise it returns Nothing.

259getEnv : String -> IO (Maybe String)

libs/base/base.ipkg+1−1

@@ -5,7 +5,7 @@ modules = System,

55

66 Debug.Error, Debug.Trace,

77

8− System.Info, System.Interactive,

8+ System.Info,

99

1010 Language.Reflection.Utils,

1111

libs/contrib/Control/Algebra.idr+10−10

@@ -54,7 +54,7 @@ class Group a => AbelianGroup a where { }

5454||| forall a, inverse a <+> a == neutral

5555||| + Associativity of `<.>`:

5656||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

57−||| + Distributivity of `<.>` and `<->`:

57+||| + Distributivity of `<.>` and `<+>`:

5858||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

5959||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

6060class AbelianGroup a => Ring a where

@@ -80,7 +80,7 @@ class AbelianGroup a => Ring a where

8080||| + Neutral for `<.>`:

8181||| forall a, a <.> unity == a

8282||| forall a, unity <.> a == a

83−||| + Distributivity of `<.>` and `<->`:

83+||| + Distributivity of `<.>` and `<+>`:

8484||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

8585||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

8686class Ring a => RingWithUnity a where

@@ -109,21 +109,21 @@ class Ring a => RingWithUnity a where

109109||| + InverseM of `<.>`, except for neutral

110110||| forall a /= neutral, a <.> inverseM a == unity

111111||| forall a /= neutral, inverseM a <.> a == unity

112−||| + Distributivity of `<.>` and `<->`:

112+||| + Distributivity of `<.>` and `<+>`:

113113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

114114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

115115class RingWithUnity a => Field a where

116116 inverseM : (x : a) -> Not (x = neutral) -> a

117117

118−sum : (Foldable t, Monoid a) => t a -> a

119−sum = foldr (<+>) neutral

118+sum' : (Foldable t, Monoid a) => t a -> a

119+sum' = concat

120120

121−product : (Foldable t, RingWithUnity a) => t a -> a

122−product = foldr (<.>) unity

121+product' : (Foldable t, RingWithUnity a) => t a -> a

122+product' = foldr (<.>) unity

123123

124−power : RingWithUnity a => a -> Nat -> a

125−power _ Z = unity

126−power x (S n) = x <.> (Algebra.power x n)

124+pow' : RingWithUnity a => a -> Nat -> a

125+pow' _ Z = unity

126+pow' x (S n) = x <.> pow' x n

127127

128128

129129-- XXX todo:

libs/contrib/Control/Algebra/NumericInstances.idr+9

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

1+||| Instances of algebraic classes (group, ring, etc) for numeric data types,

2+||| and Complex number types.

13module Control.Algebra.NumericInstances

24

35import Control.Algebra

6+import Control.Algebra.VectorSpace

47import Data.Complex

58import Data.ZZ

69

@@ -102,3 +105,9 @@ instance Ring a => Ring (Complex a) where

102105

103106instance RingWithUnity a => RingWithUnity (Complex a) where

104107 unity = (unity :+ neutral)

108+

109+instance RingWithUnity a => Module a (Complex a) where

110+ (<#>) x = map (x <.>)

111+

112+instance RingWithUnity a => InnerProductSpace a (Complex a) where

113+ (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z

libs/contrib/Data/Matrix.idr+32−124

@@ -1,150 +1,58 @@

1+||| Basic matrix operations with dimensionalities enforced

2+||| at the type level

13module Data.Matrix

24

3−import Control.Algebra

4−import Control.Algebra.VectorSpace

5−import public Control.Algebra.NumericInstances

6−

7−import Data.Complex

8−import Data.ZZ

9−import Data.Fin

10−import Data.Vect

5+import public Data.Vect

116

127%default total

138

14−infixr 2 <:> -- vector inner product

15−infixr 2 >< -- vector outer product

16−infixr 2 <<>> -- matrix commutator

17−infixr 2 >><< -- matrix anticommutator

18−infixl 3 <\> -- row times a matrix

19−infixr 4 </> -- matrix times a column

20−infixr 5 <> -- matrix multiplication

21−infixr 7 \&\ -- vector tensor product

22−infixr 7 <&> -- matrix tensor product

23−

24−-----------------------------------------------------------------------

25−-- Vectors as members of algebraic classes

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

27−

28−instance Semigroup a => Semigroup (Vect n a) where

29− (<+>) v w = zipWith (<+>) v w

30−

31−instance Monoid a => Monoid (Vect n a) where

32− neutral {n} = replicate n neutral

33−

34−instance Group a => Group (Vect n a) where

35− inverse = map inverse

36−

37−instance AbelianGroup a => AbelianGroup (Vect n a) where {}

38−

39−instance Ring a => Ring (Vect n a) where

40− (<.>) v w = zipWith (<.>) v w

41−

42−instance RingWithUnity a => RingWithUnity (Vect n a) where

43− unity {n} = replicate n unity

44−

45−--instance Field a => Field (Vect n a) where

46−

47−instance RingWithUnity a => Module a (Vect n a) where

48− (<#>) r v = map (r <.>) v

49−

50−instance RingWithUnity a => Module a (Vect n (Vect l a)) where

51− (<#>) r m = map (r <#>) m

52−-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'

53−

54−-----------------------------------------------------------------------

55−-- (Ring) Vector functions

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

57−

58−||| Inner product of ring vectors

59−(<:>) : Ring a => Vect n a -> Vect n a -> a

60−(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)

61−

62−||| Tensor multiply (⊗) ring vectors

63−(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a

64−(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where

65− orep : (n : Nat) -> Vect m a -> Vect (n * m) a

66− orep n v = concat $ replicate n v

67− oextend : (n : Nat) -> Vect k a -> Vect (k * n) a

68− oextend n w = concat $ map (replicate n) w

69−

70−||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed

71−basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a

72−basis i = replaceAt i unity $ neutral

73−

74−-----------------------------------------------------------------------

75−-- Matrix functions

76−-----------------------------------------------------------------------

77−

789||| Matrix with n rows and m columns

7910Matrix : Nat -> Nat -> Type -> Type

8011Matrix n m a = Vect n (Vect m a)

8112

82−||| Gets the specified column of a matrix. For rows use the vector function 'index'

13+||| Get the specified column of a matrix

8314getCol : Fin m -> Matrix n m a -> Vect n a

84−getCol fm q = map (index fm) q

15+getCol f = map (index f)

8516

86−||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'

87−deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a

88−deleteCol f m = map (deleteAt f) m

17+||| Get the specified row of a matrix

18+getRow : Fin n -> Matrix n m a -> Vect m a

19+getRow = index

8920

90−||| Matrix element at specified row and column indices

91−indices : Fin n -> Fin m -> Matrix n m a -> a

92−indices f1 f2 m = index f2 (index f1 m)

21+||| Delete the specified column of a matrix

22+deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a

23+deleteCol f = map (deleteAt f)

9324

94−||| Matrix times a column vector

95−(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a

96−(</>) m v = map (v <:>) m

25+||| Delete the specified row of a matrix

26+deleteRow : Fin (S n) -> Matrix (S n) m a -> Matrix n m a

27+deleteRow = deleteAt

9728

98−||| Matrix times a row vector

99−(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a

100−(<\>) r m = map (r <:>) $ transpose m

29+insertRow : Fin (S n) -> Vect m a -> Matrix n m a -> Matrix (S n) m a

30+insertRow = insertAt

10131

102−||| Matrix multiplication

103−(<>) : Ring a => Matrix n k a ->

104− Matrix k m a ->

105− Matrix n m a

106−(<>) m1 m2 = map (<\> m2) m1

32+insertCol : Fin (S m) -> Vect n a -> Matrix n m a -> Matrix n (S m) a

33+insertCol f = zipWith (insertAt f)

10734

108−||| Tensor multiply (⊗) for ring matrices

109−(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a

110−(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where

111− stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a

112− stepOne {h2} m1 m2 = concat $ map (replicate h2) m1

113− stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a

114− stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2

35+||| Matrix element at specified row and column indices

36+indices : Fin n -> Fin m -> Matrix n m a -> a

37+indices f1 f2 = index f2 . index f1

11538

11639||| Cast a vector from a standard Vect to a proper n x 1 matrix

11740col : Vect n a -> Matrix n 1 a

118−col v = map (\x => [x]) v

41+col = map (\x => [x])

11942

12043||| Cast a row from a standard Vect to a proper 1 x n matrix

12144row : Vect n a -> Matrix 1 n a

12245row r = [r]

12346

124−||| Outer product between ring vectors

125−(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a

126−(><) x y = (col x) <> (row y)

127−

128−||| All finite numbers up to the given bound

129−allN : (n : Nat) -> Vect n (Fin n)

130−allN Z = Nil

131−allN (S n) = FZ :: (map FS $ allN n)

132−

133−||| Identity matrix

134−Id : RingWithUnity a => {d : Nat} -> Matrix d d a

135−Id {d} = map (\n => basis n) $ allN d

136−

137−||| Matrix commutator

138−(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a

139−(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)

140−

141−||| Matrix anti-commutator

142−(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a

143−(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)

144−

145−-----------------------------------------------------------------------

146−-- Matrix Algebra Properties

147−-----------------------------------------------------------------------

47+||| Matrix formed by deleting specified row and col

48+subMatrix : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) a -> Matrix n m a

49+subMatrix r c = deleteRow r . deleteCol c

14850

149−-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes

51+||| Flatten a matrix of matrices

52+concatMatrix : Matrix n m (Matrix x y a) -> Matrix (n * x) (m * y) a

53+concatMatrix = Vect.concat . map (map Vect.concat) . map transpose

15054

55+||| All finite numbers of the specified level

56+fins : (n : Nat) -> Vect n (Fin n)

57+fins Z = Nil

58+fins (S n) = FZ :: (map FS $ fins n)

libs/contrib/Data/Matrix/Algebraic.idrnew file+149

@@ -0,0 +1,149 @@

1+||| Matrix operations with vector space dimensionalities enforced

2+||| at the type level. Uses operations from classes in `Control.Algebra`

3+||| and `Control.Algebra.VectorSpace`.

4+module Data.Matrix.Algebraic

5+

6+import public Control.Algebra

7+import public Control.Algebra.VectorSpace

8+import public Control.Algebra.NumericInstances

9+

10+import public Data.Matrix

11+

12+

13+%default total

14+

15+infixr 2 <:> -- vector inner product

16+infixr 2 >< -- vector outer product

17+infixr 2 <<>> -- matrix commutator

18+infixr 2 >><< -- matrix anticommutator

19+infixl 3 <\> -- row times a matrix

20+infixr 4 </> -- matrix times a column

21+infixr 5 <> -- matrix multiplication

22+infixr 7 \&\ -- vector tensor product

23+infixr 7 <&> -- matrix tensor product

24+

25+-----------------------------------------------------------------------

26+-- Vectors as members of algebraic classes

27+-----------------------------------------------------------------------

28+

29+instance Semigroup a => Semigroup (Vect n a) where

30+ (<+>)= zipWith (<+>)

31+

32+instance Monoid a => Monoid (Vect n a) where

33+ neutral {n} = replicate n neutral

34+

35+instance Group a => Group (Vect n a) where

36+ inverse = map inverse

37+

38+instance AbelianGroup a => AbelianGroup (Vect n a) where {}

39+

40+instance Ring a => Ring (Vect n a) where

41+ (<.>) = zipWith (<.>)

42+

43+instance RingWithUnity a => RingWithUnity (Vect n a) where

44+ unity {n} = replicate n unity

45+

46+instance RingWithUnity a => Module a (Vect n a) where

47+ (<#>) r = map (r <.>)

48+

49+instance RingWithUnity a => Module a (Vect n (Vect l a)) where

50+ (<#>) r = map (r <#>)

51+-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'

52+

53+-----------------------------------------------------------------------

54+-- (Ring) Vector functions

55+-----------------------------------------------------------------------

56+

57+||| Inner product of ring vectors

58+(<:>) : Ring a => Vect n a -> Vect n a -> a

59+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)

60+

61+||| Tensor multiply (⊗) ring vectors

62+(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a

63+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where

64+ orep : (n : Nat) -> Vect m a -> Vect (n * m) a

65+ orep n v = concat $ replicate n v

66+ oextend : (n : Nat) -> Vect k a -> Vect (k * n) a

67+ oextend n w = concat $ map (replicate n) w

68+

69+||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed

70+basis : RingWithUnity a => (Fin d) -> Vect d a

71+basis i = replaceAt i unity neutral

72+

73+-----------------------------------------------------------------------

74+-- Ring Matrix functions

75+-----------------------------------------------------------------------

76+

77+||| Matrix times a column vector

78+(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a

79+(</>) m v = map (v <:>) m

80+

81+||| Matrix times a row vector

82+(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a

83+(<\>) r m = map (r <:>) $ transpose m

84+

85+||| Matrix multiplication

86+(<>) : Ring a => Matrix n k a ->

87+ Matrix k m a ->

88+ Matrix n m a

89+(<>) m1 m2 = map (<\> m2) m1

90+

91+||| Tensor multiply (⊗) for ring matrices

92+(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a

93+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where

94+ stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a

95+ stepOne {h2} m1 m2 = concat $ map (replicate h2) m1

96+ stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a

97+ stepTwo {h1} m1 m2 = concat $ replicate h1 m2

98+

99+||| Outer product between ring vectors

100+(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a

101+(><) x y = col x <> row y

102+

103+||| Matrix commutator

104+(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a

105+(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)

106+

107+||| Matrix anti-commutator

108+(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a

109+(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)

110+

111+||| Identity matrix

112+Id : RingWithUnity a => Matrix d d a

113+Id = map (\n => basis n) (fins _)

114+

115+||| Square matrix from diagonal elements

116+diag_ : Monoid a => Vect n a -> Matrix n n a

117+diag_ = zipWith (\f => \x => replaceAt f x neutral) (fins _)

118+

119+||| Combine two matrices to make a new matrix in block diagonal form

120+blockDiag : Monoid a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a

121+blockDiag g h = map (++ replicate _ neutral) g ++ map ((replicate _ neutral) ++) h

122+

123+

124+-----------------------------------------------------------------------

125+-- Determinants

126+-----------------------------------------------------------------------

127+

128+||| Alternating sum

129+altSum : Group a => Vect n a -> a

130+altSum (x::y::zs) = (x <-> y) <+> altSum zs

131+altSum [x] = x

132+altSum [] = neutral

133+

134+||| Determinant of a 2-by-2 matrix

135+det2 : Ring a => Matrix 2 2 a -> a

136+det2 [[x1,x2],[y1,y2]] = x1 <.> y2 <-> x2 <.> y1

137+

138+||| Determinant of a square matrix

139+det : Ring a => Matrix (S (S n)) (S (S n)) a -> a

140+det {n} m = case n of

141+ Z => det2 m

142+ (S k) => altSum . map (\c => indices FZ c m <.> det (subMatrix FZ c m))

143+ $ fins (S (S (S k)))

144+

145+-----------------------------------------------------------------------

146+-- Matrix Algebra Properties

147+-----------------------------------------------------------------------

148+

149+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes

libs/contrib/Data/Matrix/Numeric.idrnew file+129

@@ -0,0 +1,129 @@

1+||| Matrix operations with vector space dimensionalities enforced

2+||| at the type level. Uses operations from the Num type class.

3+module Data.Matrix.Numeric

4+

5+import public Data.Matrix

6+

7+%default total

8+

9+infixr 2 <:> -- vector inner product

10+infixr 2 >< -- vector outer product

11+infixr 2 <<>> -- matrix commutator

12+infixr 2 >><< -- matrix anticommutator

13+infixl 3 <\> -- row times a matrix

14+infixr 4 </> -- matrix times a column

15+infixr 5 <> -- matrix multiplication

16+infixl 5 <#> -- matrix rescale

17+infixl 5 <# -- vector rescale

18+infixr 7 \&\ -- vector tensor product

19+infixr 7 <&> -- matrix tensor product

20+

21+-----------------------------------------------------------------------

22+-- Vectors as members of Num

23+-----------------------------------------------------------------------

24+

25+instance Num a => Num (Vect n a) where

26+ (+) = zipWith (+)

27+ (-) = zipWith (+)

28+ (*) = zipWith (*)

29+ abs = id

30+ fromInteger n = replicate _ (fromInteger n)

31+

32+-----------------------------------------------------------------------

33+-- Vector functions

34+-----------------------------------------------------------------------

35+

36+||| Inner product of ring vectors

37+(<:>) : Num a => Vect n a -> Vect n a -> a

38+(<:>) w v = sum $ zipWith (*) w v

39+

40+||| Scale a numeric vector by a scalar

41+(<#) : Num a => a -> Vect n a -> Vect n a

42+(<#) r = map (r *)

43+

44+||| Tensor multiply (⊗) numeric vectors

45+(\&\) : Num a => Vect n a -> Vect m a -> Vect (n * m) a

46+(\&\) {n} {m} v w = zipWith (*) (oextend m v) (orep n w) where

47+ orep : (n : Nat) -> Vect m a -> Vect (n * m) a

48+ orep n v = concat $ replicate n v

49+ oextend : (n : Nat) -> Vect k a -> Vect (k * n) a

50+ oextend n w = concat $ map (replicate n) w

51+

52+||| Standard basis vector with one nonzero entry, numeric data type and vector-length unfixed

53+basis : Num a => (Fin d) -> Vect d a

54+basis i = replaceAt i 1 0

55+

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

57+-- Matrix functions

58+-----------------------------------------------------------------------

59+

60+||| Matrix times a column vector

61+(</>) : Num a => Matrix n m a -> Vect m a -> Vect n a

62+(</>) m v = map (v <:>) m

63+

64+||| Matrix times a row vector

65+(<\>) : Num a => Vect n a -> Matrix n m a -> Vect m a

66+(<\>) r m = map (r <:>) $ transpose m

67+

68+||| Matrix multiplication

69+(<>) : Num a => Matrix n k a ->

70+ Matrix k m a ->

71+ Matrix n m a

72+(<>) m1 m2 = map (<\> m2) m1

73+

74+||| Scale matrix by a scalar

75+(<#>) : Num a => a -> Matrix n m a -> Matrix n m a

76+(<#>) r = map (r <#)

77+

78+||| Tensor multiply (⊗) for numeric matrices

79+(<&>) : Num a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a

80+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where

81+ stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a

82+ stepOne {h2} m1 m2 = concat $ map (replicate h2) m1

83+ stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a

84+ stepTwo {h1} m1 m2 = concat $ replicate h1 m2

85+

86+||| Outer product between numeric vectors

87+(><) : Num a => Vect n a -> Vect m a -> Matrix n m a

88+(><) x y = col x <> row y

89+

90+||| Matrix commutator

91+(<<>>) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a

92+(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)

93+

94+||| Matrix anti-commutator

95+(>><<) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a

96+(>><<) m1 m2 = (m1 <> m2) + (m2 <> m1)

97+

98+||| Identity matrix

99+Id : Num a => Matrix d d a

100+Id = map (\n => basis n) (fins _)

101+

102+||| Square matrix from diagonal elements

103+diag_ : Num a => Vect n a -> Matrix n n a

104+diag_ = zipWith (\f => \x => replaceAt f x 0) (fins _)

105+

106+||| Combine two matrices to make a new matrix in block diagonal form

107+blockDiag : Num a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a

108+blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h

109+

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

111+-- Determinants

112+-----------------------------------------------------------------------

113+

114+||| Alternating sum

115+altSum : Num a => Vect n a -> a

116+altSum (x::y::zs) = (x - y) + altSum zs

117+altSum [x] = x

118+altSum [] = 0

119+

120+||| Determinant of a 2-by-2 matrix

121+det2 : Num a => Matrix 2 2 a -> a

122+det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1

123+

124+||| Determinant of a square matrix

125+det : Num a => Matrix (S (S n)) (S (S n)) a -> a

126+det {n} m = case n of

127+ Z => det2 m

128+ (S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))

129+ $ fins (S (S (S k)))

libs/contrib/contrib.ipkg+2−1

@@ -9,7 +9,8 @@ modules = Control.Algebra,

99 Control.WellFounded,

1010 Classes.Verified,

1111 Data.Fun, Data.Rel,

12− Data.Hash, Data.Matrix,

12+ Data.Hash,

13+ Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,

1314 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,

1415 Data.ZZ, Data.Sign,

1516 Data.BoundedList,

libs/effects/Effect/Logging/Default.idrnew file+57

@@ -0,0 +1,57 @@

1+-- ------------------------------------------------------------- [ Default.idr ]

2+-- Module : Default.idr

3+-- Copyright : (c) The Idris Community

4+-- License : see LICENSE

5+-- --------------------------------------------------------------------- [ EOH ]

6+

7+||| A logging effect that allows messages to be logged using both

8+||| numerical levels and user specified categories. The higher the

9+||| logging level the grater in verbosity the logging.

10+|||

11+||| In this effect the resource we are computing over is the logging

12+||| level itself and the list of categories to show.

13+|||

14+module Effect.Logging.Default

15+

16+import Effects

17+import public Effect.Logging.Level

18+

19+import Control.IOExcept -- TODO Add IOExcept Logger.

20+

21+||| A Logging effect to log levels and categories.

22+data Logging : Effect where

23+ Log : (Eq a, Show a) =>

24+ (lvl : Nat)

25+ -> (cats : List a)

26+ -> (msg : String)

27+ -> Logging () (Nat,List a) (\v => (Nat,List a))

28+

29+||| The Logging effect.

30+|||

31+||| @cTy The type used to differentiate categories.

32+LOG : (cTy : Type) -> EFFECT

33+LOG a = MkEff (Nat, List a) Logging

34+

35+instance Handler Logging IO where

36+ handle (l,cs) (Log lvl cs' msg) k = do

37+ case lvl <= l of

38+ False => k () (l,cs)

39+ True => do

40+ let res = and $ map (\x => elem x cs') cs

41+ let prompt = if isNil cs then "" else show cs

42+ if res || isNil cs

43+ then do

44+ printLn $ unwords [show lvl, ":", prompt, ":", msg]

45+ k () (l,cs)

46+ else k () (l,cs)

47+

48+||| Log the given message at the given level and assign it the list of categories.

49+|||

50+||| @l The logging level.

51+||| @cs The logging categories.

52+||| @m THe message to be logged.

53+log : (Show a, Eq a) => (l : Nat)

54+ -> (cs : List a) -> (m : String) -> Eff () [LOG a]

55+log lvl cs msg = call $ Log lvl cs msg

56+

57+-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Logging/Level.idrnew file+49

@@ -0,0 +1,49 @@

1+-- -------------------------------------------------------------- [ Levels.idr ]

2+-- Module : Levels.idr

3+-- Copyright : (c) Jan de Muijnck-Hughes

4+-- License : see LICENSE

5+-- --------------------------------------------------------------------- [ EOH ]

6+||| Common aliases and definitions of Logging Levels.

7+module Effect.Logging.Level

8+

9+%access public

10+-- ---------------------------------------------- [ Nat Derived Logging Levels ]

11+--

12+-- Several aliases have been defined to aide in semantic use of the

13+-- logging levels. These aliases have come from the Log4j family of

14+-- loggers.

15+

16+||| No events will be logged.

17+OFF : Nat

18+OFF = 0

19+

20+||| A severe error that will prevent the application from continuing.

21+FATAL : Nat

22+FATAL = 1

23+

24+||| An error in the application, possibly recoverable.

25+ERROR : Nat

26+ERROR = 2

27+

28+||| An event that might possible lead to an error.

29+WARN : Nat

30+WARN = 3

31+

32+||| An event for informational purposes.

33+INFO : Nat

34+INFO = 4

35+

36+||| A general debugging event.

37+DEBUG : Nat

38+DEBUG = 5

39+

40+||| A fine-grained debug message, typically capturing the flow through

41+||| the application.

42+TRACE : Nat

43+TRACE = 6

44+

45+||| All events should be logged.

46+ALL : Nat

47+ALL = 7

48+

49+-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Logging/Simple.idrnew file+48

@@ -0,0 +1,48 @@

1+-- -------------------------------------------------------------- [ Simple.idr ]

2+-- Module : Logging.idr

3+-- Copyright : (c) The Idris Community

4+-- License : see LICENSE

5+--------------------------------------------------------------------- [ EOH ]

6+

7+||| A simple logging effect that allows messages to be logged at

8+||| different numerical level. The higher the number the grater in

9+||| verbosity the logging.

10+|||

11+||| In this effect the resource we are computing over is the logging

12+||| level itself.

13+|||

14+module Effect.Logging.Simple

15+

16+import Effects

17+import public Effect.Logging.Level

18+

19+import Control.IOExcept -- TODO Add IO Logging Handler

20+

21+||| A Logging effect that displays a logging message to be logged at a

22+||| certain level.

23+data Logging : Effect where

24+ Log : (lvl : Nat)

25+ -> (msg : String)

26+ -> Logging () Nat (\v => Nat)

27+

28+||| A Logging Effect.

29+LOG : EFFECT

30+LOG = MkEff Nat Logging

31+

32+-- For logging in the IO context

33+instance Handler Logging IO where

34+ handle l (Log lvl msg) k = do

35+ case lvl <= l of

36+ False => k () l

37+ True => do

38+ printLn $ unwords [show lvl, ":", msg]

39+ k () l

40+

41+||| Log `msg` at the given level.

42+|||

43+||| @l The level to log.

44+||| @m The message to log.

45+log : (l : Nat) -> (m : String) -> Eff () [LOG]

46+log lvl msg = call $ Log lvl msg

47+

48+-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Random.idr−1

@@ -2,7 +2,6 @@ module Effect.Random

22

33import Effects

44import Data.Vect

5−import Data.Fin

65

76data Random : Effect where

87 getRandom : sig Random Integer Integer

libs/effects/effects.ipkg+15−4

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

11package effects

22

33opts = "--nobasepkgs -i ../prelude -i ../base"

4−modules = Effects, Effect.Default, Effect.Monad,

54

6− Effect.Exception, Effect.File, Effect.State,

7− Effect.Random, Effect.StdIO, Effect.Select,

8− Effect.Memory, Effect.System, Effect.Trans

5+modules = Effects

6+ , Effect.Default

7+ , Effect.Monad

98

9+ , Effect.Exception

10+ , Effect.File

11+ , Effect.State

12+ , Effect.Random

13+ , Effect.StdIO

14+ , Effect.Select

15+ , Effect.Memory

16+ , Effect.System

17+ , Effect.Trans

18+ , Effect.Logging.Level

19+ , Effect.Logging.Simple

20+ , Effect.Logging.Default

libs/prelude/IO.idr+1−1

@@ -253,7 +253,7 @@ namespace FFI_Export

253253 %used FFI_Prim prim

254254

255255 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where

256− FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)

256+ FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)

257257 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)

258258 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t

259259

libs/prelude/Prelude.idr+2−211

@@ -25,6 +25,8 @@ import public Prelude.Pairs

2525import public Prelude.Stream

2626import public Prelude.Providers

2727import public Prelude.Show

28+import public Prelude.Interactive

29+import public Prelude.File

2830import public Decidable.Equality

2931import public Language.Reflection

3032import public Language.Reflection.Errors

@@ -43,9 +45,6 @@ decAsBool (No _) = False

4345instance Functor PrimIO where

4446 map f io = prim_io_bind io (prim_io_return . f)

4547

46−instance Functor (IO' ffi) where

47− map f io = io_bind io (\b => io_return (f b))

48−

4948instance Functor Maybe where

5049 map f (Just x) = Just (f x)

5150 map f Nothing = Nothing

@@ -61,12 +60,6 @@ instance Applicative PrimIO where

6160

6261 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

6362

64−instance Applicative (IO' ffi) where

65− pure x = io_return x

66− f <*> a = io_bind f (\f' =>

67− io_bind a (\a' =>

68− io_return (f' a')))

69−

7063instance Applicative Maybe where

7164 pure = Just

7265

@@ -103,9 +96,6 @@ instance Alternative List where

10396instance Monad PrimIO where

10497 b >>= k = prim_io_bind b k

10598

106−instance Monad (IO' ffi) where

107− b >>= k = io_bind b k

108−

10999instance Monad Maybe where

110100 Nothing >>= k = Nothing

111101 (Just x) >>= k = k x

@@ -229,183 +219,6 @@ curry f a b = f (a, b)

229219uncurry : (a -> b -> c) -> (a, b) -> c

230220uncurry f (a, b) = f a b

231221

232−---- some basic io

233−

234−||| Output a string to stdout without a trailing newline

235−putStr : String -> IO' ffi ()

236−putStr x = do prim_write x

237− return ()

238−

239−||| Output a string to stdout with a trailing newline

240−putStrLn : String -> IO' ffi ()

241−putStrLn x = putStr (x ++ "\n")

242−

243−||| Output something showable to stdout, without a trailing newline

244−partial

245−print : Show a => a -> IO' ffi ()

246−print x = putStr (show x)

247−

248−||| Output something showable to stdout, with a trailing newline

249−partial

250−printLn : Show a => a -> IO' ffi ()

251−printLn x = putStrLn (show x)

252−

253−||| Read one line of input from stdin, without the trailing newline

254−partial

255−getLine : IO' ffi String

256−getLine = do x <- prim_read

257− return (reverse (trimNL (reverse x)))

258− where trimNL : String -> String

259− trimNL str with (strM str)

260− trimNL "" | StrNil = ""

261− trimNL (strCons '\n' xs) | StrCons _ _ = xs

262− trimNL (strCons x xs) | StrCons _ _ = strCons x xs

263−

264−||| Write a single character to stdout

265−partial

266−putChar : Char -> IO ()

267−putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

268−

269−||| Write a singel character to stdout, with a trailing newline

270−partial

271−putCharLn : Char -> IO ()

272−putCharLn c = putStrLn (singleton c)

273−

274−||| Read a single character from stdin

275−partial

276−getChar : IO Char

277−getChar = map cast $ foreign FFI_C "getchar" (IO Int)

278−

279−---- some basic file handling

280−

281−||| A file handle

282−abstract

283−data File = FHandle Ptr

284−

285−||| Standard input

286−stdin : File

287−stdin = FHandle prim__stdin

288−

289−||| Standard output

290−stdout : File

291−stdout = FHandle prim__stdout

292−

293−||| Standard output

294−stderr : File

295−stderr = FHandle prim__stderr

296−

297−||| Call the RTS's file opening function

298−do_fopen : String -> String -> IO Ptr

299−do_fopen f m

300− = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

301−

302−||| Open a file

303−||| @ f the filename

304−||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

305−fopen : (f : String) -> (m : String) -> IO File

306−fopen f m = do h <- do_fopen f m

307− return (FHandle h)

308−

309−||| Modes for opening files

310−data Mode = Read | Write | ReadWrite

311−

312−||| Open a file

313−||| @ f the filename

314−||| @ m the mode

315−partial

316−openFile : (f : String) -> (m : Mode) -> IO File

317−openFile f m = fopen f (modeStr m) where

318− modeStr Read = "r"

319− modeStr Write = "w"

320− modeStr ReadWrite = "r+"

321−

322−partial

323−do_fclose : Ptr -> IO ()

324−do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

325−

326−partial

327−closeFile : File -> IO ()

328−closeFile (FHandle h) = do_fclose h

329−

330−partial

331−do_fread : Ptr -> IO' l String

332−do_fread h = prim_fread h

333−

334−fgetc : File -> IO Char

335−fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))

336−

337−fgetc' : File -> IO (Maybe Char)

338−fgetc' (FHandle h)

339− = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h

340− if (x < 0) then return Nothing

341− else return (Just (cast x))

342−

343−fflush : File -> IO ()

344−fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

345−

346−do_popen : String -> String -> IO Ptr

347−do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m

348−

349−popen : String -> Mode -> IO File

350−popen f m = do ptr <- do_popen f (modeStr m)

351− return (FHandle ptr)

352− where

353− modeStr Read = "r"

354− modeStr Write = "w"

355− modeStr ReadWrite = "r+"

356−

357−pclose : File -> IO ()

358−pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

359−

360−-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))

361−-- prim__vm h

362−

363−partial

364−fread : File -> IO' l String

365−fread (FHandle h) = do_fread h

366−

367−partial

368−do_fwrite : Ptr -> String -> IO ()

369−do_fwrite h s = do prim_fwrite h s

370− return ()

371−

372−partial

373−fwrite : File -> String -> IO ()

374−fwrite (FHandle h) s = do_fwrite h s

375−

376−partial

377−do_feof : Ptr -> IO Int

378−do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

379−

380−||| Check if a file handle has reached the end

381−feof : File -> IO Bool

382−feof (FHandle h) = do eof <- do_feof h

383− return (not (eof == 0))

384−

385−partial

386−do_ferror : Ptr -> IO Int

387−do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

388−

389−ferror : File -> IO Bool

390−ferror (FHandle h) = do err <- do_ferror h

391− return (not (err == 0))

392−

393−fpoll : File -> IO Bool

394−fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

395− return (p > 0)

396−

397−||| Check if a foreign pointer is null

398−partial

399−nullPtr : Ptr -> IO Bool

400−nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

401− return (ok /= 0)

402−

403−||| Check if a supposed string was actually a null pointer

404−partial

405−nullStr : String -> IO Bool

406−nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p

407− return (ok /= 0)

408−

409222namespace JSNull

410223 ||| Check if a foreign pointer is null

411224 partial

@@ -425,12 +238,6 @@ eqPtr : Ptr -> Ptr -> IO Bool

425238eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y

426239 return (eq /= 0)

427240

428−||| Check whether a file handle is actually a null pointer

429−partial

430−validFile : File -> IO Bool

431−validFile (FHandle h) = do x <- nullPtr h

432− return (not x)

433−

434241||| Loop while some test is true

435242|||

436243||| @ test the condition of the loop

@@ -442,22 +249,6 @@ while t b = do v <- t

442249 while t b

443250 else return ()

444251

445−||| Read the contents of a file into a string

446−partial -- no error checking!

447−readFile : String -> IO String

448−readFile fn = do h <- openFile fn Read

449− c <- readFile' h ""

450− closeFile h

451− return c

452− where

453− partial

454− readFile' : File -> String -> IO String

455− readFile' h contents =

456− do x <- feof h

457− if not x then do l <- fread h

458− readFile' h (contents ++ l)

459− else return contents

460−

461252------- Some error rewriting

462253

463254%language ErrorReflection

libs/prelude/Prelude/Cast.idr+11−5

@@ -15,7 +15,7 @@ class Cast from to where

1515instance Cast String Int where

1616 cast = prim__fromStrInt

1717

18−instance Cast String Float where

18+instance Cast String Double where

1919 cast = prim__strToFloat

2020

2121instance Cast String Integer where

@@ -26,25 +26,31 @@ instance Cast String Integer where

2626instance Cast Int String where

2727 cast = prim__toStrInt

2828

29−instance Cast Int Float where

29+instance Cast Int Double where

3030 cast = prim__toFloatInt

3131

3232instance Cast Int Integer where

3333 cast = prim__sextInt_BigInt

3434

35−-- Float casts

35+-- Double casts

3636

37−instance Cast Float String where

37+instance Cast Double String where

3838 cast = prim__floatToStr

3939

40−instance Cast Float Int where

40+instance Cast Double Int where

4141 cast = prim__fromFloatInt

4242

43+instance Cast Double Integer where

44+ cast = prim__fromFloatBigInt

45+

4346-- Integer casts

4447

4548instance Cast Integer String where

4649 cast = prim__toStrBigInt

4750

51+instance Cast Integer Double where

52+ cast = prim__toFloatBigInt

53+

4854-- Char casts

4955

5056instance Cast Char Int where

libs/prelude/Prelude/File.idrnew file+156

@@ -0,0 +1,156 @@

1+module Prelude.File

2+

3+import Builtins

4+import Prelude.List

5+import Prelude.Maybe

6+import Prelude.Monad

7+import Prelude.Chars

8+import Prelude.Strings

9+import Prelude.Cast

10+import Prelude.Bool

11+import Prelude.Basics

12+import Prelude.Classes

13+import Prelude.Monad

14+import IO

15+

16+%access public

17+

18+||| A file handle

19+abstract

20+data File = FHandle Ptr

21+

22+||| Standard input

23+stdin : File

24+stdin = FHandle prim__stdin

25+

26+||| Standard output

27+stdout : File

28+stdout = FHandle prim__stdout

29+

30+||| Standard output

31+stderr : File

32+stderr = FHandle prim__stderr

33+

34+||| Call the RTS's file opening function

35+do_fopen : String -> String -> IO Ptr

36+do_fopen f m

37+ = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

38+

39+||| Open a file

40+||| @ f the filename

41+||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

42+fopen : (f : String) -> (m : String) -> IO File

43+fopen f m = do h <- do_fopen f m

44+ return (FHandle h)

45+

46+||| Check whether a file handle is actually a null pointer

47+partial

48+validFile : File -> IO Bool

49+validFile (FHandle h) = do x <- nullPtr h

50+ return (not x)

51+

52+||| Modes for opening files

53+data Mode = Read | Write | ReadWrite

54+

55+||| Open a file

56+||| @ f the filename

57+||| @ m the mode

58+partial

59+openFile : (f : String) -> (m : Mode) -> IO File

60+openFile f m = fopen f (modeStr m) where

61+ modeStr Read = "r"

62+ modeStr Write = "w"

63+ modeStr ReadWrite = "r+"

64+

65+partial

66+do_fclose : Ptr -> IO ()

67+do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

68+

69+partial

70+closeFile : File -> IO ()

71+closeFile (FHandle h) = do_fclose h

72+

73+partial

74+do_fread : Ptr -> IO' l String

75+do_fread h = prim_fread h

76+

77+fgetc : File -> IO Char

78+fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))

79+

80+fgetc' : File -> IO (Maybe Char)

81+fgetc' (FHandle h)

82+ = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h

83+ if (x < 0) then return Nothing

84+ else return (Just (cast x))

85+

86+fflush : File -> IO ()

87+fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

88+

89+do_popen : String -> String -> IO Ptr

90+do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m

91+

92+popen : String -> Mode -> IO File

93+popen f m = do ptr <- do_popen f (modeStr m)

94+ return (FHandle ptr)

95+ where

96+ modeStr Read = "r"

97+ modeStr Write = "w"

98+ modeStr ReadWrite = "r+"

99+

100+pclose : File -> IO ()

101+pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

102+

103+-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))

104+-- prim__vm h

105+

106+partial

107+fread : File -> IO' l String

108+fread (FHandle h) = do_fread h

109+

110+partial

111+do_fwrite : Ptr -> String -> IO ()

112+do_fwrite h s = do prim_fwrite h s

113+ return ()

114+

115+partial

116+fwrite : File -> String -> IO ()

117+fwrite (FHandle h) s = do_fwrite h s

118+

119+partial

120+do_feof : Ptr -> IO Int

121+do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

122+

123+||| Check if a file handle has reached the end

124+feof : File -> IO Bool

125+feof (FHandle h) = do eof <- do_feof h

126+ return (not (eof == 0))

127+

128+partial

129+do_ferror : Ptr -> IO Int

130+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

131+

132+ferror : File -> IO Bool

133+ferror (FHandle h) = do err <- do_ferror h

134+ return (not (err == 0))

135+

136+fpoll : File -> IO Bool

137+fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

138+ return (p > 0)

139+

140+||| Read the contents of a file into a string

141+partial -- no error checking!

142+readFile : String -> IO String

143+readFile fn = do h <- openFile fn Read

144+ c <- readFile' h ""

145+ closeFile h

146+ return c

147+ where

148+ partial

149+ readFile' : File -> String -> IO String

150+ readFile' h contents =

151+ do x <- feof h

152+ if not x then do l <- fread h

153+ readFile' h (contents ++ l)

154+ else return contents

155+

156+

libs/base/System/Interactive.idr → libs/prelude/Prelude/Interactive.idrrenamed+79−9

@@ -4,13 +4,83 @@

44||| the easy creation of interactive programs without needing to teach IO

55||| or Effects first, but they also capture some common patterns of interactive

66||| programming.

7−module System.Interactive

7+module Prelude.Interactive

88

9−{-

10−When the interfaces and names are stable, these are intended for the Prelude.

11−-}

9+import Builtins

10+import Prelude.List

11+import Prelude.File

12+import Prelude.Bool

13+import Prelude.Classes

14+import Prelude.Strings

15+import Prelude.Chars

16+import Prelude.Show

17+import Prelude.Cast

18+import Prelude.Maybe

19+import Prelude.Functor

20+import Prelude.Monad

21+import IO

22+

23+%access public

24+

25+---- some basic io

26+

27+||| Output a string to stdout without a trailing newline

28+putStr : String -> IO' ffi ()

29+putStr x = do prim_write x

30+ return ()

31+

32+||| Output a string to stdout with a trailing newline

33+putStrLn : String -> IO' ffi ()

34+putStrLn x = putStr (x ++ "\n")

35+

36+||| Output something showable to stdout, without a trailing newline

37+print : Show a => a -> IO' ffi ()

38+print x = putStr (show x)

39+

40+||| Output something showable to stdout, with a trailing newline

41+printLn : Show a => a -> IO' ffi ()

42+printLn x = putStrLn (show x)

43+

44+||| Read one line of input from stdin, without the trailing newline

45+getLine : IO' ffi String

46+getLine = do x <- prim_read

47+ return (reverse (trimNL (reverse x)))

48+ where trimNL : String -> String

49+ trimNL str with (strM str)

50+ trimNL "" | StrNil = ""

51+ trimNL (strCons '\n' xs) | StrCons _ _ = xs

52+ trimNL (strCons x xs) | StrCons _ _ = strCons x xs

53+

54+||| Write a single character to stdout

55+putChar : Char -> IO ()

56+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

57+

58+||| Write a singel character to stdout, with a trailing newline

59+putCharLn : Char -> IO ()

60+putCharLn c = putStrLn (singleton c)

61+

62+||| Read a single character from stdin

63+getChar : IO Char

64+getChar = map cast $ foreign FFI_C "getchar" (IO Int)

65+

66+||| Get the command-line arguments that the program was called with.

67+partial

68+getArgs : IO (List String)

69+getArgs = do n <- numArgs

70+ ga' [] 0 n

71+ where

72+ numArgs : IO Int

73+ numArgs = foreign FFI_C "idris_numArgs" (IO Int)

74+

75+ getArg : Int -> IO String

76+ getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x

77+

78+ partial

79+ ga' : List String -> Int -> Int -> IO (List String)

80+ ga' acc i n = if (i == n) then (return $ reverse acc) else

81+ do arg <- getArg i

82+ ga' (arg :: acc) (i+1) n

1283

13−import System

1484

1585||| Process input from an open file handle, while maintaining a state.

1686||| @ state the input state

@@ -18,7 +88,7 @@ import System

1888||| output and a new state

1989||| @ onEOF the function to run on reaching end of file, returning a String

2090||| to output

21−public partial

91+partial

2292processHandle : File ->

2393 (state : a) ->

2494 (onRead : a -> String -> (String, a)) ->

@@ -38,7 +108,7 @@ processHandle h acc onRead onEOF

38108||| output and a new state

39109||| @ onEOI the function to run on reaching end of input, returning a String

40110||| to output

41−public partial

111+partial

42112processStdin : (state : a) ->

43113 (onRead : a -> String -> (String, a)) ->

44114 (onEOI : a -> String) -> IO ()

@@ -49,7 +119,7 @@ processStdin = processHandle stdin

49119||| @ prompt the prompt to show

50120||| @ onInput the function to run on reading input, returning a String to

51121||| output and a new state. Returns Nothing if the repl should exit

52−public partial

122+partial

53123replWith : (state : a) -> (prompt : String) ->

54124 (onInput : a -> String -> Maybe (String, a)) -> IO a

55125replWith acc prompt fn

@@ -64,7 +134,7 @@ replWith acc prompt fn

64134||| @ prompt the prompt to show

65135||| @ onInput the function to run on reading input, returning a String to

66136||| output

67−public partial

137+partial

68138repl : (prompt : String) ->

69139 (onInput : String -> String) -> IO ()

70140repl prompt fn

libs/prelude/Prelude/List.idr+4−3

@@ -18,11 +18,12 @@ import Prelude.Nat

1818infix 5 \\

1919infixr 7 ::,++

2020

21−||| Linked lists

21+||| Generic lists

2222%elim data List elem =

23− ||| The empty list

23+ ||| Empty list

2424 Nil |

25− ||| Cons cell

25+ ||| A non-empty list, consisting of a head element and the rest of

26+ ||| the list.

2627 (::) elem (List elem)

2728

2829-- Name hints for interactive editing

libs/prelude/Prelude/Monad.idr+19−1

@@ -3,9 +3,10 @@ module Prelude.Monad

33-- Monads and Functors

44

55import Builtins

6−import Prelude.List

6+import Prelude.Functor

77import Prelude.Applicative

88import Prelude.Basics

9+import IO

910

1011%access public

1112

@@ -22,3 +23,20 @@ flatten a = a >>= id

2223||| define `return` and `pure` differently!

2324return : Monad m => a -> m a

2425return = pure

26+

27+-- Annoyingly, these need to be here, so that we can use them in other

28+-- Prelude modules other than the top level.

29+

30+instance Functor (IO' ffi) where

31+ map f io = io_bind io (\b => io_return (f b))

32+

33+instance Applicative (IO' ffi) where

34+ pure x = io_return x

35+ f <*> a = io_bind f (\f' =>

36+ io_bind a (\a' =>

37+ io_return (f' a')))

38+

39+

40+instance Monad (IO' ffi) where

41+ b >>= k = io_bind b k

42+

libs/prelude/Prelude/Nat.idr+7−3

@@ -12,7 +12,8 @@ import Prelude.Uninhabited

1212%access public

1313%default total

1414

15−||| Unary natural numbers

15+||| Natural numbers: unbounded, unsigned integers which can be pattern

16+||| matched.

1617%elim data Nat =

1718 ||| Zero

1819 Z |

@@ -213,12 +214,12 @@ instance MinBound Nat where

213214instance Cast Integer Nat where

214215 cast = fromInteger

215216

216−||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

217+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

217218record Multiplicative where

218219 constructor getMultiplicative

219220 _ : Nat

220221

221−||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

222+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

222223record Additive where

223224 constructor getAdditive

224225 _ : Nat

@@ -262,6 +263,9 @@ instance Cast Int Nat where

262263instance Cast Nat Int where

263264 cast = toIntNat

264265

266+instance Cast Nat Double where

267+ cast = cast . toIntegerNat

268+

265269--------------------------------------------------------------------------------

266270-- Auxilliary notions

267271--------------------------------------------------------------------------------

libs/prelude/Prelude/Strings.idr+55−14

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

11module Prelude.Strings

22

33import Builtins

4+import IO

45

56import Prelude.Algebra

67import Prelude.Basics

@@ -13,8 +14,18 @@ import Prelude.Foldable

1314import Prelude.Functor

1415import Prelude.List

1516import Prelude.Nat

17+import Prelude.Monad

1618import Decidable.Equality

1719

20+partial

21+foldr1 : (a -> a -> a) -> List a -> a

22+foldr1 _ [x] = x

23+foldr1 f (x::xs) = f x (foldr1 f xs)

24+

25+partial

26+foldl1 : (a -> a -> a) -> List a -> a

27+foldl1 f (x::xs) = foldl f x xs

28+

1829||| Appends two strings together.

1930|||

2031||| ```idris example

@@ -247,15 +258,6 @@ lines' s = case dropWhile isNL s of

247258lines : String -> List String

248259lines s = map pack $ lines' $ unpack s

249260

250−partial

251−foldr1 : (a -> a -> a) -> List a -> a

252−foldr1 _ [x] = x

253−foldr1 f (x::xs) = f x (foldr1 f xs)

254−

255−partial

256−foldl1 : (a -> a -> a) -> List a -> a

257−foldl1 f (x::xs) = foldl f x xs

258−

259261||| Joins the character lists by spaces into a single character list.

260262|||

261263||| ```idris example

@@ -263,12 +265,11 @@ foldl1 f (x::xs) = foldl f x xs

263265||| ```

264266unwords' : List (List Char) -> List Char

265267unwords' [] = []

266−unwords' ws = assert_total (foldr1 addSpace ws)

267− where

268− addSpace : List Char -> List Char -> List Char

269− addSpace w s = w ++ (' ' :: s)

268+unwords' ws = assert_total (foldr1 addSpace ws) where

269+ addSpace : List Char -> List Char -> List Char

270+ addSpace w s = w ++ (' ' :: s)

270271

271−||| Joins the strings by spaces into a single string.

272+||| Joins the strings by spaces into a single string.

272273|||

273274||| ```idris example

274275||| unwords ["A", "BC", "D", "E"]

@@ -276,6 +277,25 @@ unwords' ws = assert_total (foldr1 addSpace ws)

276277unwords : List String -> String

277278unwords = pack . unwords' . map unpack

278279

280+||| Joins the character lists by newlines into a single character list.

281+|||

282+||| ```idris example

283+||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]

284+||| ```

285+unlines' : List (List Char) -> List Char

286+unlines' [] = []

287+unlines' ls = assert_total (foldr1 addLine ls) where

288+ addLine : List Char -> List Char -> List Char

289+ addLine l s = l ++ ('\n' :: s)

290+

291+||| Joins the strings by newlines into a single string.

292+|||

293+||| ```idris example

294+||| unlines ["line", "line2", "ln3", "D"]

295+||| ```

296+unlines : List String -> String

297+unlines = pack . unlines' . map unpack

298+

279299||| Returns the length of the string.

280300|||

281301||| ```idris example

@@ -287,6 +307,14 @@ unwords = pack . unwords' . map unpack

287307length : String -> Nat

288308length = fromInteger . prim__zextInt_BigInt . prim_lenString

289309

310+||| Returns a substring of a given string

311+||| @index The (zero based) index of the string to extract. If this is

312+||| beyond the end of the String, the function returns the empty string.

313+||| @len The desired length of the substring. Truncated if this exceeds

314+||| the length of the input.

315+substr : (index : Nat) -> (len : Nat) -> String -> String

316+substr i len = pack . List.take len . drop i . unpack

317+

290318||| Lowercases all characters in the string.

291319|||

292320||| ```idris example

@@ -321,3 +349,16 @@ isSuffixOf a b = isSuffixOf (unpack a) (unpack b)

321349

322350isInfixOf : String -> String -> Bool

323351isInfixOf a b = isInfixOf (unpack a) (unpack b)

352+

353+||| Check if a foreign pointer is null

354+partial

355+nullPtr : Ptr -> IO Bool

356+nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p

357+ return (ok /= 0)

358+

359+||| Check if a supposed string was actually a null pointer

360+partial

361+nullStr : String -> IO Bool

362+nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p

363+ return (ok /= 0)

364+

libs/prelude/prelude.ipkg+1

@@ -9,6 +9,7 @@ modules = Builtins, Prelude, IO,

99 Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,

1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

1111 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

12+ Prelude.Interactive, Prelude.File,

1213

1314 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

1415

src/Idris/AbsSyntax.hs+9−3

@@ -597,7 +597,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

597597

598598-- | Save information about a name that is not yet defined

599599addDeferred' :: NameType

600− -> [(Name, (Int, Maybe Name, Type, Bool))]

600+ -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]

601601 -- ^ The Name is the name being made into a metavar,

602602 -- the Int is the number of vars that are part of a

603603 -- putative proof context, the Maybe Name is the

@@ -606,10 +606,10 @@ addDeferred' :: NameType

606606 -- allowed

607607 -> Idris ()

608608addDeferred' nt ns

609− = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

609+ = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

610610 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

611611 i <- getIState

612− putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

612+ putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++

613613 idris_metavars i }

614614 where

615615 -- 'tidyNames' is to generate user accessible names in case they are

@@ -790,6 +790,12 @@ getNoBanner = do i <- getIState

790790 let opts = idris_options i

791791 return (opt_nobanner opts)

792792

793+setEvalTypes :: Bool -> Idris ()

794+setEvalTypes n = do i <- getIState

795+ let opts = idris_options i

796+ let opt' = opts { opt_evaltypes = n }

797+ putIState $ i { idris_options = opt' }

798+

793799setQuiet :: Bool -> Idris ()

794800setQuiet q = do i <- getIState

795801 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+35−11

@@ -89,7 +89,8 @@ data IOption = IOption { opt_logLevel :: Int,

8989 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

9090 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

9191 opt_optimise :: [Optimisation],

92− opt_printdepth :: Maybe Int

92+ opt_printdepth :: Maybe Int,

93+ opt_evaltypes :: Bool -- ^ normalise types in :t

9394 }

9495 deriving (Show, Eq)

9596

@@ -115,10 +116,12 @@ defaultOpts = IOption { opt_logLevel = 0

115116 , opt_autoImport = []

116117 , opt_optimise = defaultOptimise

117118 , opt_printdepth = Just 5000

119+ , opt_evaltypes = True

118120 }

119121

120122data PPOption = PPOption {

121123 ppopt_impl :: Bool -- ^^ whether to show implicits

124+ , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings

122125 , ppopt_depth :: Maybe Int

123126} deriving (Show)

124127

@@ -129,16 +132,21 @@ defaultOptimise = [PETransform]

129132

130133-- | Pretty printing options with default verbosity.

131134defaultPPOption :: PPOption

132−defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }

135+defaultPPOption = PPOption { ppopt_impl = False,

136+ ppopt_pinames = False,

137+ ppopt_depth = Just 200 }

133138

134139-- | Pretty printing options with the most verbosity.

135140verbosePPOption :: PPOption

136−verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }

141+verbosePPOption = PPOption { ppopt_impl = True,

142+ ppopt_pinames = True,

143+ ppopt_depth = Just 200 }

137144

138145-- | Get pretty printing options from the big options record.

139146ppOption :: IOption -> PPOption

140147ppOption opt = PPOption {

141148 ppopt_impl = opt_showimp opt,

149+ ppopt_pinames = False,

142150 ppopt_depth = opt_printdepth opt

143151}

144152

@@ -193,10 +201,11 @@ data IState = IState {

193201 idris_name :: Int,

194202 idris_lineapps :: [((FilePath, Int), PTerm)],

195203 -- ^ Full application LHS on source line

196− idris_metavars :: [(Name, (Maybe Name, Int, Bool))],

204+ idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],

197205 -- ^ The currently defined but not proven metavariables. The Int

198206 -- is the number of vars to display as a context, the Maybe Name

199− -- is its top-level function, and the Bool is whether :p is

207+ -- is its top-level function, the [Name] is the list of local variables

208+ -- available for proof search and the Bool is whether :p is

200209 -- allowed

201210 idris_coercions :: [Name],

202211 idris_errRev :: [(Term, Term)],

@@ -400,10 +409,13 @@ data Command = Quit

400409 | AddProofClauseFrom Bool Int Name

401410 | AddMissing Bool Int Name

402411 | MakeWith Bool Int Name

412+ | MakeCase Bool Int Name

403413 | MakeLemma Bool Int Name

404− | DoProofSearch Bool Bool Int Name [Name]

405− -- ^ the first bool is whether to update,

406− -- the second is whether to search recursively (i.e. for the arguments)

414+ | DoProofSearch Bool -- update file

415+ Bool -- recursive search

416+ Int -- depth

417+ Name -- top level name

418+ [Name] -- hints

407419 | SetOpt Opt

408420 | UnsetOpt Opt

409421 | NOP

@@ -451,6 +463,7 @@ data Opt = Filename String

451463 | DefaultPartial

452464 | WarnPartial

453465 | WarnReach

466+ | EvalTypes

454467 | NoCoverage

455468 | ErrContext

456469 | ShowImpl

@@ -978,7 +991,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

978991 | MatchRefine Name

979992 | LetTac Name t | LetTacTy Name t t

980993 | Exact t | Compute | Trivial | TCInstance

981− | ProofSearch Bool Bool Int (Maybe Name) [Name]

994+ | ProofSearch Bool Bool Int (Maybe Name)

995+ [Name] -- allowed local names

996+ [Name] -- hints

982997 -- ^ the bool is whether to search recursively

983998 | Solve

984999 | Attack

@@ -1549,7 +1564,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

15491564 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

15501565 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

15511566 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)

1552− | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1567+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs

1568+ || ppopt_pinames ppo && uname n =

15531569 depth d . bracket p startPrec . group $

15541570 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

15551571 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

15581574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>

15591575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)

15601576 where

1577+ uname (UN n) = case str n of

1578+ ('_':_) -> False

1579+ _ -> True

1580+ uname _ = False

1581+

15611582 st =

15621583 case s of

15631584 Static -> text "[static]" <> space

@@ -1576,7 +1597,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

15761597 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

15771598 depth d . bracket p startPrec $

15781599 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1579− prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =

1600+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =

15801601 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

15811602 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

15821603 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

@@ -1996,6 +2017,9 @@ showTm ist = displayDecorated (consoleDecorate ist) .

19962017showTmImpls :: PTerm -> String

19972018showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

19982019

2020+-- | Show a term with specific options

2021+showTmOpts :: PPOption -> PTerm -> String

2022+showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""

19992023

20002024

20012025instance Sized PTerm where

src/Idris/CaseSplit.hs+18−11

@@ -265,18 +265,23 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

265265 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups

266266

267267 updateRHSs i [] = return []

268− updateRHSs i (x : xs) = do (x', i') <- updateRHS i x

268+ updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x

269269 xs' <- updateRHSs i' xs

270270 return (x' : xs')

271271

272− updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs

273− return ("?=" ++ xs', i')

274− updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs

275− (nm', i') <- getUniq nm i

276− return ('?':nm' ++ rest, i')

277− updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs

278− return (x : xs', i')

279− updateRHS i [] = return ("", i)

272+ updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs

273+ return ("?=" ++ xs', i')

274+ updateRHS last i ('?':xs)

275+ = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'

276+ || x == '(')) xs

277+ let rest = if last then rest_in else

278+ case span (not . (=='\n')) rest_in of

279+ (_, restnl) -> restnl

280+ (nm', i') <- getUniq nm i

281+ return ('?':nm' ++ rest, i')

282+ updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs

283+ return (x : xs', i')

284+ updateRHS last i [] = return ("", i)

280285

281286

282287 -- TMP HACK: If there are Nats, we don't want to show as numerals since

@@ -361,9 +366,11 @@ getClause l fn fp

361366 getNameFrom i used (PApp fc f as) = getNameFrom i used f

362367 getNameFrom i used (PRef fc _ f)

363368 = case getNameHints i f of

364− [] -> uniqueName (sUN "x") used

369+ [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",

370+ sUN "z"]) used

365371 ns -> uniqueNameFrom (mkSupply ns) used

366− getNameFrom i used _ = uniqueName (sUN "x") used

372+ getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",

373+ sUN "z"]) used

367374

368375 -- write method declarations, indent with 4 spaces

369376 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

src/Idris/Completion.hs+1−1

@@ -52,7 +52,7 @@ names = do i <- get

5252

5353metavars :: Idris [String]

5454metavars = do i <- get

55− return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs

55+ return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t)) -> not t) (idris_metavars i)) \\ primDefs

5656

5757

5858modules :: Idris [String]

src/Idris/Core/Binary.hs+6−4

@@ -499,9 +499,10 @@ instance (Binary b) => Binary (Binder b) where

499499 put x2

500500 Hole x1 -> do putWord8 4

501501 put x1

502− GHole x1 x2 -> do putWord8 5

503− put x1

504− put x2

502+ GHole x1 x2 x3 -> do putWord8 5

503+ put x1

504+ put x2

505+ put x3

505506 Guess x1 x2 -> do putWord8 6

506507 put x1

507508 put x2

@@ -528,7 +529,8 @@ instance (Binary b) => Binary (Binder b) where

528529 return (Hole x1)

529530 5 -> do x1 <- get

530531 x2 <- get

531− return (GHole x1 x2)

532+ x3 <- get

533+ return (GHole x1 x2 x3)

532534 6 -> do x1 <- get

533535 x2 <- get

534536 return (Guess x1 x2)

src/Idris/Core/DeepSeq.hs+1−1

@@ -128,7 +128,7 @@ instance (NFData b) => NFData (Binder b) where

128128 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

129129 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

130130 rnf (Hole x1) = rnf x1 `seq` ()

131− rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

131+ rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

132132 rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

133133 rnf (PVar x1) = rnf x1 `seq` ()

134134 rnf (PVTy x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+14

@@ -51,6 +51,20 @@ explicit n = do ES (p, a) s m <- get

5151 let p' = p { dontunify = n : dontunify p }

5252 put (ES (p', a) s m)

5353

54+-- Add a name that's okay to use in proof search (typically either because

55+-- it was given explicitly on the lhs, or intrduced as an explicit lambda

56+-- or let binding)

57+addPSname :: Name -> Elab' aux ()

58+addPSname n@(UN _)

59+ = do ES (p, a) s m <- get

60+ let p' = p { psnames = n : psnames p }

61+ put (ES (p', a) s m)

62+addPSname _ = return () -- can only use user given names

63+

64+getPSnames :: Elab' aux [Name]

65+getPSnames = do ES (p, a) s m <- get

66+ return (psnames p)

67+

5468saveState :: Elab' aux ()

5569saveState = do e@(ES p s _) <- get

5670 put (ES p s (Just e))

src/Idris/Core/Execute.hs+1−1

@@ -93,7 +93,7 @@ toTT (EBind n b body) = do n' <- newN n

9393 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

9494 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

9595 fixBinder (Hole t) = Hole <$> toTT t

96− fixBinder (GHole i t) = GHole i <$> toTT t

96+ fixBinder (GHole i ns t) = GHole i ns <$> toTT t

9797 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

9898 fixBinder (PVar t) = PVar <$> toTT t

9999 fixBinder (PVTy t) = PVTy <$> toTT t

src/Idris/Core/ProofState.hs+7−4

@@ -39,6 +39,7 @@ data ProofState = PS { thname :: Name,

3939 deferred :: [Name], -- ^ names we'll need to define

4040 instances :: [Name], -- ^ instance arguments (for type classes)

4141 autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes

42+ psnames :: [Name], -- ^ Local names okay to use in proof search

4243 previous :: Maybe ProofState, -- ^ for undo

4344 context :: Context,

4445 datatypes :: Ctxt TypeInfo,

@@ -244,7 +245,8 @@ unify' ctxt env (topx, xfrom) (topy, yfrom) =

244245 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)

245246 traceWhen (unifylog ps)

246247 ("Now solved: " ++ show ns' ++

247− "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

248+ "\nNow problems: " ++ qshow (probs' ++ probs_notu) ++

249+ "\nNow injective: " ++ show (updateInj u (injective ps))) $

248250 put (ps { problems = probs' ++ probs_notu,

249251 unified = (h, ns'),

250252 injective = updateInj u (injective ps),

@@ -300,7 +302,7 @@ newProof n ctxt datatypes ty =

300302 in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

301303 (P Bound h ty'))) ty [] (h, []) [] []

302304 Nothing [] []

303− [] [] []

305+ [] [] [] []

304306 Nothing ctxt datatypes "" False False [] []

305307

306308type TState = ProofState -- [TacticAction])

@@ -428,7 +430,8 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

428430 do let env' = filter (\(n, t) -> n `notElem` dropped) env

429431 action (\ps -> let hs = holes ps in

430432 ps { holes = hs \\ [x] })

431− return (Bind n (GHole (length env') (mkTy (reverse env') t))

433+ ps <- get

434+ return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

432435 (mkApp (P Ref n ty) (map getP (reverse env'))))

433436 where

434437 mkTy [] t = t

@@ -444,7 +447,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

444447 ds = deferred ps in

445448 ps { holes = hs \\ [x],

446449 deferred = n : ds })

447− return (Bind n (GHole 0 fty)

450+ return (Bind n (GHole 0 [] fty)

448451 (mkApp (P Ref n ty) (map getP args)))

449452 where

450453 getP n = case lookup n env of

src/Idris/Core/TT.hs+8−7

@@ -809,6 +809,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

809809 binderVal :: b }

810810 | Hole { binderTy :: !b}

811811 | GHole { envlen :: Int,

812+ localnames :: [Name],

812813 binderTy :: !b}

813814 | Guess { binderTy :: !b,

814815 binderVal :: b }

@@ -827,7 +828,7 @@ instance Sized a => Sized (Binder a) where

827828 size (Let ty val) = 1 + size ty + size val

828829 size (NLet ty val) = 1 + size ty + size val

829830 size (Hole ty) = 1 + size ty

830− size (GHole _ ty) = 1 + size ty

831+ size (GHole _ _ ty) = 1 + size ty

831832 size (Guess ty val) = 1 + size ty + size val

832833 size (PVar ty) = 1 + size ty

833834 size (PVTy ty) = 1 + size ty

@@ -839,7 +840,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

839840fmapMB f (Lam t) = liftM Lam (f t)

840841fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

841842fmapMB f (Hole t) = liftM Hole (f t)

842−fmapMB f (GHole i t) = liftM (GHole i) (f t)

843+fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)

843844fmapMB f (PVar t) = liftM PVar (f t)

844845fmapMB f (PVTy t) = liftM PVTy (f t)

845846

@@ -1494,7 +1495,7 @@ prettyEnv env t = prettyEnv' env t False

14941495 -- Render a `Binder` and its name

14951496 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

14961497 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1497− prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t

1498+ prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t

14981499 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t

14991500 prettySb env n (PVar t) = prettyB env "pat" "." n t

15001501 prettySb env n (PVTy t) = prettyB env "pty" "." n t

@@ -1539,7 +1540,7 @@ showEnv' env t dbg = se 10 env t where

15391540

15401541 sb env n (Lam t) = showb env "\\ " " => " n t

15411542 sb env n (Hole t) = showb env "? " ". " n t

1542− sb env n (GHole i t) = showb env "?defer " ". " n t

1543+ sb env n (GHole i ns t) = showb env "?defer " ". " n t

15431544 sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

15441545 sb env n (Pi _ t _) = showb env "(" ") -> " n t

15451546 sb env n (PVar t) = showb env "pat " ". " n t

@@ -1739,7 +1740,7 @@ pprintTT bound tm = pp startPrec bound tm

17391740 ppb p bound n (Hole ty) sc =

17401741 bracket p startPrec . group . align . hang 2 $

17411742 text "?" <+> bindingOf n False <+> text "." <> line <> sc

1742− ppb p bound n (GHole _ ty) sc =

1743+ ppb p bound n (GHole _ _ ty) sc =

17431744 bracket p startPrec . group . align . hang 2 $

17441745 text "¿" <+> bindingOf n False <+> text "." <> line <> sc

17451746 ppb p bound n (Guess ty val) sc =

@@ -1791,8 +1792,8 @@ pprintRaw bound (RBind n b body) =

17911792 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

17921793 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

17931794 text "Hole" <$> pprintRaw bound ty

1794− ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $

1795− text "GHole" <$> pprintRaw bound ty

1795+ ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $

1796+ text "GHole" <$> pprintRaw bound ty

17961797 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

17971798 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

17981799 ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

src/Idris/Core/Typecheck.hs+4−4

@@ -232,12 +232,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

232232 let tt' = normalise ctxt env tt

233233 lift $ isType ctxt env tt'

234234 return (Hole tv, tt')

235− checkBinder (GHole i t)

235+ checkBinder (GHole i ns t)

236236 = do (tv, tt) <- chk u env t

237237 let tv' = normalise ctxt env tv

238238 let tt' = normalise ctxt env tt

239239 lift $ isType ctxt env tt'

240− return (GHole i tv, tt')

240+ return (GHole i ns tv, tt')

241241 checkBinder (Guess t v)

242242 | not holes = lift $ tfail (IncompleteTerm undefined)

243243 | otherwise

@@ -273,8 +273,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

273273 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)

274274 discharge n (Hole t) bt scv sct

275275 = return (Bind n (Hole t) scv, sct)

276− discharge n (GHole i t) bt scv sct

277− = return (Bind n (GHole i t) scv, sct)

276+ discharge n (GHole i ns t) bt scv sct

277+ = return (Bind n (GHole i ns t) scv, sct)

278278 discharge n (Guess t v) bt scv sct

279279 = return (Bind n (Guess t v) scv, sct)

280280 discharge n (PVar t) bt scv sct

src/Idris/DeepSeq.hs+2−2

@@ -295,8 +295,8 @@ instance (NFData t) => NFData (PTactic' t) where

295295 rnf Compute = ()

296296 rnf Trivial = ()

297297 rnf TCInstance = ()

298− rnf (ProofSearch r r1 r2 x1 x2)

299− = rnf x1 `seq` rnf x2 `seq` ()

298+ rnf (ProofSearch r r1 r2 x1 x2 x3)

299+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

300300 rnf Solve = ()

301301 rnf Attack = ()

302302 rnf ProofState = ()

src/Idris/Delaborate.hs+2−2

@@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

106106 | Just n' <- lookup n env = PRef un [] n'

107107 | otherwise

108108 = case lookup n (idris_metavars ist) of

109− Just (Just _, mi, _) -> mkMVApp n []

109+ Just (Just _, mi, _, _) -> mkMVApp n []

110110 _ -> PRef un [] n

111111 de env _ (Bind n (Lam ty) sc)

112112 = 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

169169 = PApp un (de env [] f) (map pexp (map (de env []) args))

170170 deFn env (P _ n _) args

171171 | not mvs = case lookup n (idris_metavars ist) of

172− Just (Just _, mi, _) ->

172+ Just (Just _, mi, _, _) ->

173173 mkMVApp n (drop mi (map (de env []) args))

174174 _ -> mkPApp n (map (de env []) args)

175175 | otherwise = mkPApp n (map (de env []) args)

src/Idris/Elab/Clause.hs+12−8

@@ -543,7 +543,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

543543 let fn_is = case lookupCtxt fname (idris_implicits i) of

544544 [t] -> t

545545 _ -> []

546− let params = getParamsInType i [] fn_is fn_ty

546+ let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

547547 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

548548 propagateParams i params fn_ty (addImplPat i lhs_in)

549549-- let lhs = mkLHSapp $

@@ -632,6 +632,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

632632 ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-

633633 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

634634 (do pbinds ist lhs_tm

635+ -- proof search can use explicitly written names

636+ mapM_ addPSname (allNamesIn lhs_in)

635637 mapM_ setinj (nub (params ++ inj))

636638 setNextName

637639 (ElabResult _ _ is ctxt' newDecls highlights) <-

@@ -656,9 +658,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

656658 logLvl 5 "DONE CHECK"

657659 logLvl 4 $ "---> " ++ show rhs'

658660 when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

659− show (map (\ (n, (_,_,t)) -> (n, t)) defer)

661+ show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

660662 def' <- checkDef fc (Elaborating "deferred type of ") defer

661− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

663+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

662664 addDeferred def''

663665 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

664666

@@ -790,7 +792,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

790792 let fn_is = case lookupCtxt fname (idris_implicits i) of

791793 [t] -> t

792794 _ -> []

793− let params = getParamsInType i [] fn_is fn_ty

795+ let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

794796 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

795797 logLvl 2 ("LHS: " ++ show lhs)

796798 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

@@ -816,6 +818,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

816818 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

817819 (bindTyArgs PVTy bargs infP) initEState

818820 (do pbinds i lhs_tm

821+ -- proof search can use explicitly written names

822+ mapM_ addPSname (allNamesIn lhs_in)

819823 setNextName

820824 -- TODO: may want where here - see winfo abpve

821825 (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)

828832 sendHighlighting highlights

829833

830834 def' <- checkDef fc iderr defer

831− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

835+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

832836 addDeferred def''

833837 mapM_ (elabCaseBlock info opts) is

834838 logLvl 5 ("Checked wval " ++ show wval')

@@ -890,8 +894,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

890894 addIBC (IBCImp wname)

891895 addIBC (IBCStatic wname)

892896

893− def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]

894− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

897+ def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]

898+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

895899 addDeferred def''

896900

897901 -- in the subdecls, lhs becomes:

@@ -932,7 +936,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

932936 sendHighlighting highlights

933937

934938 def' <- checkDef fc iderr defer

935− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

939+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

936940 addDeferred def''

937941 mapM_ (elabCaseBlock info opts) is

938942 logLvl 5 ("Checked RHS " ++ show rhs')

src/Idris/Elab/Instance.hs+1−1

@@ -71,7 +71,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

7171 let constraint = PApp fc (PRef fc [] n) (map pexp ps)

7272 let iname = mkiname n (namespace info) ps expn

7373 let emptyclass = null (class_methods ci)

74− when (what /= EDefns || (null ds && not emptyclass)) $ do

74+ when (what /= EDefns) $ do

7575 nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

7676 -- if the instance type matches any of the instances we have already,

7777 -- and it's not a named instance, then it's overlapping, so report an error

src/Idris/Elab/Record.hs+13−9

@@ -34,6 +34,7 @@ import Control.Monad

3434

3535-- | Elaborate a record declaration

3636elabRecord :: ElabInfo

37+ -> ElabWhat

3738 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

3839 -> SyntaxInfo -> FC -> DataOpts

3940 -> Name -- ^ The name of the type being defined

@@ -45,7 +46,7 @@ elabRecord :: ElabInfo

4546 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

4647 -> SyntaxInfo -- ^ Constructor SyntaxInfo

4748 -> Idris ()

48−elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

49+elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

4950 = do logLvl 1 $ "Building data declaration for " ++ show tyn

5051 -- Type constructor

5152 let tycon = generateTyConType params

@@ -58,17 +59,20 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

5859

5960 -- Build data declaration for elaboration

6061 logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

61− let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

62+ let datadecl = case what of

63+ ETypes -> PLaterdecl tyn NoFC tycon

64+ _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

6265 elabData info rsyn doc paramDocs fc opts datadecl

6366

64− logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

65− logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

66− elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

67+ when (what /= ETypes) $ do

68+ logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

69+ logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

70+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

6771

68− sendHighlighting $

69− [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

70− maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

71− [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

72+ sendHighlighting $

73+ [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

74+ maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

75+ [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

7276

7377 where

7478 -- | Generates a type constructor.

src/Idris/Elab/Term.hs+25−28

@@ -42,7 +42,7 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

4242

4343data ElabResult =

4444 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

45− , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

45+ , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

4646 -- ^ Information about new metavariables

4747 , resultCaseDecls :: [PDecl]

4848 -- ^ Deferred declarations as the meaning of case blocks

@@ -628,6 +628,7 @@ elab ist info emode opts fn tm

628628 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")

629629 checkPiGoal n

630630 attack; intro (Just n);

631+ addPSname n -- okay for proof search

631632 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

632633 elabE (ina { e_inarg = True } ) (Just fc) sc; solve

633634 highlightSource nfc (AnnBoundName n False)

@@ -644,6 +645,7 @@ elab ist info emode opts fn tm

644645 ptm <- get_term

645646 hs <- get_holes

646647 introTy (Var tyn) (Just n)

648+ addPSname n -- okay for proof search

647649 focus tyn

648650

649651 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

@@ -652,6 +654,7 @@ elab ist info emode opts fn tm

652654 highlightSource nfc (AnnBoundName n False)

653655 elab' ina fc (PPi p n nfc Placeholder sc)

654656 = do attack; arg n (is_scoped p) (sMN 0 "ty")

657+ addPSname n -- okay for proof search

655658 elabE (ina { e_inarg = True, e_intype = True }) fc sc

656659 solve

657660 highlightSource nfc (AnnBoundName n False)

@@ -662,6 +665,7 @@ elab ist info emode opts fn tm

662665 MN _ _ -> unique_hole n

663666 _ -> return n

664667 forall n' (is_scoped p) (Var tyn)

668+ addPSname n' -- okay for proof search

665669 focus tyn

666670 let ec' = ina { e_inarg = True, e_intype = True }

667671 elabE ec' fc ty

@@ -677,6 +681,7 @@ elab ist info emode opts fn tm

677681 claim valn (Var tyn)

678682 explicit valn

679683 letbind n (Var tyn) (Var valn)

684+ addPSname n

680685 case ty of

681686 Placeholder -> return ()

682687 _ -> do focus tyn

@@ -902,7 +907,7 @@ elab ist info emode opts fn tm

902907 case lookup n env of

903908 Nothing -> return ()

904909 Just b ->

905− case unApply (binderTy b) of

910+ case unApply (normalise (tt_ctxt ist) env (binderTy b)) of

906911 (P _ c _, args) ->

907912 case lookupCtxtExact c (idris_classes ist) of

908913 Nothing -> return ()

@@ -962,6 +967,7 @@ elab ist info emode opts fn tm

962967 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

963968 let n' = metavarName (namespace info) n

964969 attack

970+ psns <- getPSnames

965971 defer unique_used n'

966972 solve

967973 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

@@ -1621,7 +1627,7 @@ solveAuto ist fn ambigok n

16211627 g <- goal

16221628 isg <- is_guess -- if it's a guess, we're working on it recursively, so stop

16231629 when (not isg) $

1624− proofSearch' ist True ambigok 100 True Nothing fn []

1630+ proofSearch' ist True ambigok 100 True Nothing fn [] []

16251631

16261632solveAutos :: IState -> Name -> Bool -> ElabD ()

16271633solveAutos ist fn ambigok

@@ -1630,12 +1636,12 @@ solveAutos ist fn ambigok

16301636

16311637trivial' ist

16321638 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1633−trivialHoles' h ist

1634− = trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1635−proofSearch' ist rec ambigok depth prv top n hints

1639+trivialHoles' psn h ist

1640+ = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1641+proofSearch' ist rec ambigok depth prv top n psns hints

16361642 = do unifyProblems

16371643 proofSearch rec prv ambigok (not prv) depth

1638− (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist

1644+ (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist

16391645

16401646-- | Resolve type classes. This will only pick up 'normal' instances, never

16411647-- named instances (which is enforced by 'findInstances').

@@ -1675,7 +1681,7 @@ resTC' tcs defaultOn topholes depth topg fn ist

16751681 _ -> []

16761682

16771683 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1678− try' (trivialHoles' okholes ist)

1684+ try' (trivialHoles' [] okholes ist)

16791685 (do addDefault t tc ttypes

16801686 let stk = map fst (filter snd $ elab_stack ist)

16811687 let insts = findInstances ist t

@@ -1800,11 +1806,11 @@ resTC' tcs defaultOn topholes depth topg fn ist

18001806 isImp arg = (False, priority arg)

18011807

18021808collectDeferred :: Maybe Name -> [Name] -> Context ->

1803− Term -> State [(Name, (Int, Maybe Name, Type))] Term

1804−collectDeferred top casenames ctxt (Bind n (GHole i t) app) =

1809+ Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

1810+collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =

18051811 do ds <- get

18061812 t' <- collectDeferred top casenames ctxt t

1807− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])

1813+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])

18081814 collectDeferred top casenames ctxt app

18091815 where

18101816 -- 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) =

18141820 tidyArg env (Bind n b@(Pi im t k) sc)

18151821 = Bind n (Pi im (tidy ctxt env t) k)

18161822 (tidyArg ((n, b) : env) sc)

1817− tidyArg env t = t

1818−

1819− tidy ctxt env t | (f, args) <- unApply t,

1820− P _ specn _ <- getFn f,

1821− n `notElem` casenames

1822− = fst $ specialise ctxt env [(specn, 99999)] t

1823− tidy ctxt env t@(Bind n (Let _ _) sct)

1824− | (f, args) <- unApply sct,

1825− P _ specn _ <- getFn f,

1826− n `notElem` casenames

1827− = fst $ specialise ctxt env [(specn, 99999)] t

1828− tidy ctxt env t = t

1823+ tidyArg env t = tidy ctxt env t

1824+

1825+ tidy ctxt env t = normalise ctxt env t

18291826

18301827 getFn (Bind n (Lam _) t) = getFn t

18311828 getFn t | (f, a) <- unApply t = f

@@ -2138,7 +2135,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

21382135 do actualHints <- mapM reifyTTName hs

21392136 unifyProblems

21402137 let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")

2141− proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist

2138+ proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist

21422139 returnUnit

21432140 (Constant (I _), Nothing ) ->

21442141 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

@@ -2310,8 +2307,8 @@ runTac autoSolve ist perhapsFC fn tac

23102307 runT Compute = compute

23112308 runT Trivial = do trivial' ist; when autoSolve solveAll

23122309 runT TCInstance = runT (Exact (PResolveTC emptyFC))

2313− runT (ProofSearch rec prover depth top hints)

2314− = do proofSearch' ist rec False depth prover top fn hints

2310+ runT (ProofSearch rec prover depth top psns hints)

2311+ = do proofSearch' ist rec False depth prover top fn psns hints

23152312 when autoSolve solveAll

23162313 runT (Focus n) = focus n

23172314 runT Unfocus = do hs <- get_holes

@@ -2519,7 +2516,7 @@ processTacticDecls info steps =

25192516 updateIState $ \i -> i { idris_implicits =

25202517 addDef n impls (idris_implicits i) }

25212518 addIBC (IBCImp n)

2522− ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]

2519+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))]

25232520 addIBC (IBCDef n)

25242521 ctxt <- getContext

25252522 case lookupDef n ctxt of

@@ -2528,7 +2525,7 @@ processTacticDecls info steps =

25282525 -- then it must be added as a metavariable. This needs guarding

25292526 -- to prevent overwriting case defs with a metavar, if the case

25302527 -- defs come after the type decl in the same script!

2531− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

2528+ let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds

25322529 in addDeferred ds'

25332530 _ -> return ()

25342531 RAddInstance className instName ->

src/Idris/Elab/Type.hs+2−2

@@ -159,9 +159,9 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

159159 -- Productivity checking now via checking for guarded 'Delay'

160160 let opts' = opts -- if corec then (Coinductive : opts) else opts

161161 let usety = if norm then nty' else nty

162− ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

162+ ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]

163163 addIBC (IBCDef n)

164− let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds

164+ let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds

165165 addDeferred ds'

166166 setFlags n opts'

167167 checkDocs fc argDocs ty

src/Idris/Elab/Utils.hs+9−8

@@ -40,21 +40,21 @@ recheckC_borrowing uniq_check bs fc mkerr env t

4040iderr :: Name -> Err -> Err

4141iderr _ e = e

4242

43−checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]

44− -> Idris [(Name, (Int, Maybe Name, Type))]

43+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))]

44+ -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

4545checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

4646

4747checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

48− -> [(Name, (Int, Maybe Name, Type))]

49− -> Idris [(Name, (Int, Maybe Name, Type))]

48+ -> [(Name, (Int, Maybe Name, Type, [Name]))]

49+ -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

5050checkAddDef add toplvl fc mkerr [] = return []

51−checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)

51+checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)

5252 = do ctxt <- getContext

5353 (t', _) <- recheckC fc (mkerr n) [] t

54− when add $ do addDeferred [(n, (i, top, t, toplvl))]

54+ when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]

5555 addIBC (IBCDef n)

5656 ns' <- checkAddDef add toplvl fc mkerr ns

57− return ((n, (i, top, t')) : ns')

57+ return ((n, (i, top, t', psns)) : ns')

5858

5959-- | Get the list of (index, name) of inaccessible arguments from an elaborated

6060-- type

@@ -137,7 +137,8 @@ decorateid decorate (PClauses f o n cs)

137137pbinds :: IState -> Term -> ElabD ()

138138pbinds i (Bind n (PVar t) sc)

139139 = do attack; patbind n

140− case unApply t of

140+ env <- get_env

141+ case unApply (normalise (tt_ctxt i) env t) of

141142 (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

142143 [] -> return ()

143144 _ -> -- type class, set as injective

src/Idris/Elab/Value.hs+1−1

@@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in

7676 let vtm = orderPats (getInferTerm tm')

7777

7878 def' <- checkDef (fileFC "(input)") iderr defer

79− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

79+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) def'

8080 addDeferred def''

8181 mapM_ (elabCaseBlock info []) is

8282

src/Idris/ElabDecls.hs+1−2

@@ -245,9 +245,8 @@ elabDecl' what info (PInstance doc argDocs s f cs n nfc ps t expn ds)

245245 = do logLvl 1 $ "Elaborating instance " ++ show n

246246 elabInstance info s doc argDocs what f cs n nfc ps t expn ds

247247elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

248− | what /= ETypes

249248 = do logLvl 1 $ "Elaborating record " ++ show name

250− elabRecord info doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

249+ elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

251250{-

252251 | otherwise

253252 = do logLvl 1 $ "Elaborating [type of] " ++ show tyn

src/Idris/IBC.hs+13−11

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 116

43+ibcVersion = 117

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -78,7 +78,7 @@ data IBCFile = IBCFile { ver :: Word16,

7878 ibc_metainformation :: ![(Name, MetaInformation)],

7979 ibc_errorhandlers :: ![Name],

8080 ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler

81− ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],

81+ ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],

8282 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

8383 ibc_postulates :: ![Name],

8484 ibc_externs :: ![(Name, Int)],

@@ -365,7 +365,7 @@ timestampOlder :: FilePath -> FilePath -> Idris ()

365365timestampOlder src ibc = do srct <- runIO $ getModificationTime src

366366 ibct <- runIO $ getModificationTime ibc

367367 if (srct > ibct)

368− then ifail "Needs reloading"

368+ then ifail $ "Needs reloading " ++ show (srct, ibct)

369369 else return ()

370370

371371pPostulates :: [Name] -> Idris ()

@@ -610,7 +610,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

610610pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->

611611 addFunctionErrorHandlers fn arg [handler]) ns

612612

613−pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

613+pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris ()

614614pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

615615

616616----- For Cheapskate and docstrings

@@ -1869,12 +1869,13 @@ instance (Binary t) => Binary (PTactic' t) where

18691869 put x1

18701870 ByReflection x1 -> do putWord8 20

18711871 put x1

1872− ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21

1873− put x1

1874− put x2

1875− put x3

1876− put x4

1877− put x5

1872+ ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21

1873+ put x1

1874+ put x2

1875+ put x3

1876+ put x4

1877+ put x5

1878+ put x6

18781879 DoUnify -> putWord8 22

18791880 CaseTac x1 -> do putWord8 23

18801881 put x1

@@ -1954,7 +1955,8 @@ instance (Binary t) => Binary (PTactic' t) where

19541955 x3 <- get

19551956 x4 <- get

19561957 x5 <- get

1957− return (ProofSearch x1 x2 x3 x4 x5)

1958+ x6 <- get

1959+ return (ProofSearch x1 x2 x3 x4 x5 x6)

19581960 22 -> return DoUnify

19591961 23 -> do x1 <- get

19601962 return (CaseTac x1)

src/Idris/IdeMode.hs+2

@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String

229229 | AddProofClause Int String

230230 | AddMissing Int String

231231 | MakeWithBlock Int String

232+ | MakeCaseBlock Int String

232233 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

233234 | MakeLemma Int String

234235 | LoadFile String (Maybe Int)

@@ -261,6 +262,7 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n

261262sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

262263sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

263264sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

265+sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name]) = Just (MakeCaseBlock (fromInteger line) name)

264266-- The Boolean in ProofSearch means "search recursively"

265267-- If it's False, that means "refine", i.e. apply the name and fill in any

266268-- arguments which can be done by unification.

src/Idris/IdrisDoc.hs+2−2

@@ -360,8 +360,8 @@ extractPTactic (MatchRefine n) = [n]

360360extractPTactic (LetTac n p) = n : extract p

361361extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]

362362extractPTactic (Exact p) = extract p

363−extractPTactic (ProofSearch _ _ _ m ns) | Just n <- m = n : ns

364−extractPTactic (ProofSearch _ _ _ _ ns) = ns

363+extractPTactic (ProofSearch _ _ _ m _ ns) | Just n <- m = n : ns

364+extractPTactic (ProofSearch _ _ _ _ _ ns) = ns

365365extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2]

366366extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2]

367367extractPTactic (ApplyTactic p) = extract p

src/Idris/Interactive.hs+97−14

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

11{-# LANGUAGE PatternGuards #-}

22

33module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,

4− addMissing, makeWith, doProofSearch,

4+ addMissing, makeWith, makeCase, doProofSearch,

55 makeLemma) where

66

77{- Bits and pieces for editing source files interactively, called from

@@ -158,6 +158,47 @@ makeWith fn updatefile l n

158158 else iPrintResult with

159159 where getIndent s = length (takeWhile isSpace s)

160160

161+-- Replace the given metavariable on the given line with a 'case'

162+-- block, using a _ for the scrutinee

163+makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()

164+makeCase fn updatefile l n

165+ = do src <- runIO $ readSource fn

166+ let (before, tyline : later) = splitAt (l-1) (lines src)

167+ let newcase = addCaseSkel (show n) tyline

168+

169+ if updatefile then

170+ do let fb = fn ++ "~"

171+ runIO $ writeSource fb (unlines (before ++ newcase ++ later))

172+ runIO $ copyFile fb fn

173+ else iPrintResult (showSep "\n" newcase)

174+ where addCaseSkel n line =

175+ let b = brackets False line in

176+ case findSubstr ('?':n) line of

177+ Just (before, pos, after) ->

178+ [before ++ (if b then "(" else "") ++ "case _ of",

179+ take (pos + (if b then 6 else 5)) (repeat ' ') ++

180+ "case_val => ?" ++ n ++ if b then ")" else "",

181+ after]

182+ Nothing -> fail "No such metavariable"

183+

184+ -- Assume case needs to be bracketed unless the metavariable is

185+ -- on its own after an =

186+ brackets eq line | line == '?' : show n = not eq

187+ brackets eq ('=':ls) = brackets True ls

188+ brackets eq (' ':ls) = brackets eq ls

189+ brackets eq (l : ls) = brackets False ls

190+ brackets eq [] = True

191+

192+ findSubstr n xs = findSubstr' [] 0 n xs

193+

194+ findSubstr' acc i n xs | take (length n) xs == n

195+ = Just (reverse acc, i, drop (length n) xs)

196+ findSubstr' acc i n [] = Nothing

197+ findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs

198+

199+

200+

201+

161202

162203doProofSearch :: FilePath -> Bool -> Bool ->

163204 Int -> Name -> [Name] -> Maybe Int -> Idris ()

@@ -172,12 +213,13 @@ doProofSearch fn updatefile rec l n hints (Just depth)

172213 [] -> return n

173214 ns -> ierror (CantResolveAlts ns)

174215 i <- getIState

175− let (top, envlen, _) = case lookup mn (idris_metavars i) of

176− Just (t, e, False) -> (t, e, False)

177− _ -> (Nothing, 0, True)

216+ let (top, envlen, psnames, _)

217+ = case lookup mn (idris_metavars i) of

218+ Just (t, e, ns, False) -> (t, e, ns, False)

219+ _ -> (Nothing, 0, [], True)

178220 let fc = fileFC fn

179− let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

180− (ProofSearch rec False depth t hints)]

221+ let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))

222+ (ProofSearch rec False depth t psnames hints)]

181223 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

182224 newmv <- idrisCatch

183225 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

@@ -256,13 +298,17 @@ makeLemma fn updatefile l n

256298 ns -> ierror (CantResolveAlts (map fst ns))

257299 i <- getIState

258300 margs <- case lookup n (idris_metavars i) of

259− Just (_, arity, _) -> return arity

301+ Just (_, arity, _, _) -> return arity

260302 _ -> return (-1)

261303

262304 if (not isProv) then do

263− let skip = guessImps (tt_ctxt i) mty

305+ let skip = guessImps i (tt_ctxt i) mty

306+ let classes = guessClasses i (tt_ctxt i) mty

264307

265− let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))

308+ let lem = show n ++ " : " ++

309+ constraints i classes mty ++

310+ showTmOpts (defaultPPOption { ppopt_pinames = True })

311+ (stripMNBind skip (delab i mty))

266312 let lem_app = show n ++ appArgs skip margs mty

267313

268314 if updatefile then

@@ -312,15 +358,52 @@ makeLemma fn updatefile l n

312358 stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

313359 stripMNBind skip t = t

314360

361+ constraints :: IState -> [Name] -> Type -> String

362+ constraints i [] ty = ""

363+ constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "

364+ constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "

365+

366+ showConstraints i ns (Bind n (Pi _ ty _) sc)

367+ | n `elem` ns = show (delab i ty) :

368+ showConstraints i ns (substV (P Bound n Erased) sc)

369+ | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)

370+ showConstraints _ _ _ = []

371+

315372 -- Guess which binders should be implicits in the generated lemma.

316373 -- Make them implicit if they appear guarded by a top level constructor,

317374 -- or at the top level themselves.

318− guessImps :: Context -> Term -> [Name]

319− guessImps ctxt (Bind n (Pi _ _ _) sc)

375+ -- Also, make type class instances implicit

376+ guessImps :: IState -> Context -> Term -> [Name]

377+ guessImps ist ctxt (Bind n (Pi _ ty _) sc)

320378 | guarded ctxt n (substV (P Bound n Erased) sc)

321− = n : guessImps ctxt sc

322− | otherwise = guessImps ctxt sc

323− guessImps ctxt _ = []

379+ = n : guessImps ist ctxt sc

380+ | isClass ist ty

381+ = n : guessImps ist ctxt sc

382+ | otherwise = guessImps ist ctxt sc

383+ guessImps ist ctxt _ = []

384+

385+ guessClasses :: IState -> Context -> Term -> [Name]

386+ guessClasses ist ctxt (Bind n (Pi _ ty _) sc)

387+ | isParamClass ist ty

388+ = n : guessClasses ist ctxt sc

389+ | otherwise = guessClasses ist ctxt sc

390+ guessClasses ist ctxt _ = []

391+

392+ isClass ist t

393+ | (P _ n _, args) <- unApply t

394+ = case lookupCtxtExact n (idris_classes ist) of

395+ Just _ -> True

396+ _ -> False

397+ | otherwise = False

398+

399+ isParamClass ist t

400+ | (P _ n _, args) <- unApply t

401+ = case lookupCtxtExact n (idris_classes ist) of

402+ Just _ -> any isV args

403+ _ -> False

404+ | otherwise = False

405+ where isV (V _) = True

406+ isV _ = False

324407

325408 guarded ctxt n (P _ n' _) | n == n' = True

326409 guarded ctxt n ap@(App _ _ _)

src/Idris/ParseData.hs+18−17

@@ -86,25 +86,26 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

8686

8787 let constructorDoc' = annotate syn ist constructorDoc

8888

89− fields <- many . indented $ field syn

89+ fields <- many . indented $ fieldLine syn

9090

91− return (fields, constructorName, constructorDoc')

91+ return (concat fields, constructorName, constructorDoc')

9292 where

93− field :: SyntaxInfo -> IdrisParser ((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

94− field syn = do doc <- optional docComment

95− c <- optional $ lchar '{'

96− n <- (do (n, nfc) <- fnName

97− return $ Just (expandNS syn n, nfc))

98− <|> (do symbol "_"

99− return Nothing)

100− lchar ':'

101− t <- typeExpr (allowImp syn)

102− p <- endPlicity c

103− ist <- get

104− let doc' = case doc of -- Temp: Throws away any possible arg docs

105− Just (d,_) -> Just $ annotate syn ist d

106− Nothing -> Nothing

107− return (n, p, t, doc')

93+ fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

94+ fieldLine syn = do

95+ doc <- optional docComment

96+ c <- optional $ lchar '{'

97+ let oneName = (do (n, nfc) <- fnName

98+ return $ Just (expandNS syn n, nfc))

99+ <|> (symbol "_" >> return Nothing)

100+ ns <- commaSeparated oneName

101+ lchar ':'

102+ t <- typeExpr (allowImp syn)

103+ p <- endPlicity c

104+ ist <- get

105+ let doc' = case doc of -- Temp: Throws away any possible arg docs

106+ Just (d,_) -> Just $ annotate syn ist d

107+ Nothing -> Nothing

108+ return $ map (\n -> (n, p, t, doc')) ns

108109

109110 constructor :: IdrisParser (Name, FC)

110111 constructor = (reservedHL "constructor") *> fnName

src/Idris/ParseExpr.hs+2−2

@@ -971,7 +971,7 @@ autoImplicit opts st syn

971971 sc <- expr syn

972972 highlightP kw AnnKeyword

973973 return (bindList (PPi

974− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)

974+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

975975

976976defaultImplicit opts st syn = do

977977 kw <- reservedFC "default"

@@ -1436,7 +1436,7 @@ tactics =

14361436 , noArgs ["unify"] DoUnify

14371437 , (["search"], Nothing, const $

14381438 do depth <- option 10 $ fst <$> natural

1439− return (ProofSearch True True (fromInteger depth) Nothing []))

1439+ return (ProofSearch True True (fromInteger depth) Nothing [] []))

14401440 , noArgs ["instance"] TCInstance

14411441 , noArgs ["solve"] Solve

14421442 , noArgs ["attack"] Attack

src/Idris/ParseHelpers.hs+5

@@ -434,6 +434,11 @@ bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PT

434434bindList b [] sc = sc

435435bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)

436436

437+{- | @commaSeparated p@ parses one or more occurences of `p`,

438+ separated by commas and optional whitespace. -}

439+commaSeparated :: MonadicParsing m => m a -> m [a]

440+commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)

441+

437442{- * Layout helpers -}

438443

439444-- | Push indentation to stack

src/Idris/ProofSearch.hs+34−16

@@ -22,10 +22,10 @@ import Debug.Trace

2222-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

2323

2424trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25−trivial = trivialHoles []

25+trivial = trivialHoles [] []

2626

27−trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28−trivialHoles ok elab ist

27+trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28+trivialHoles psnames ok elab ist

2929 = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

3030 return ())

3131 (do env <- get_env

@@ -41,7 +41,7 @@ trivialHoles ok elab ist

4141 g <- goal

4242 -- anywhere but the top is okay for a hole, if holesOK set

4343 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

44− holesOK hs (binderTy b)

44+ holesOK hs (binderTy b) && (null psnames || x `elem` psnames)

4545 then try' (elab (PRef (fileFC "prf") [] x))

4646 (tryAll xs) True

4747 else tryAll xs

@@ -73,9 +73,11 @@ proofSearch :: Bool -> -- recursive search (False for 'refine')

7373 Bool -> -- ambiguity ok

7474 Bool -> -- defer on failure

7575 Int -> -- maximum depth

76− (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

76+ (PTerm -> ElabD ()) -> Maybe Name -> Name ->

77+ [Name] ->

78+ [Name] ->

7779 IState -> ElabD ()

78−proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

80+proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist

7981 = do -- get all possible versions of the name, take the first one that

8082 -- works

8183 let all_imps = lookupCtxtName fn (idris_implicits ist)

@@ -106,7 +108,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

106108

107109 isImp (PImp p _ _ _ _) = (True, p)

108110 isImp arg = (True, priority arg) -- try to get all of them by unification

109−proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

111+proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist

110112 = do compute

111113 ty <- goal

112114 hs <- get_holes

@@ -177,7 +179,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

177179 ty <- goal

178180 when (S.member ty tys) $ fail "Been here before"

179181 let tys' = S.insert ty tys

180− try' (trivial elab ist)

182+ try' (trivialHoles psnames [] elab ist)

181183 (try' (try' (resolveByCon (d - 1) locs tys')

182184 (resolveByLocals (d - 1) locs tys')

183185 True)

@@ -199,11 +201,13 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

199201 Nothing -> []

200202 Just hs -> hs

201203 case lookupCtxtExact n (idris_datatypes ist) of

202− Just t -> tryCons d locs tys

203− (hints ++

204− con_names t ++

205− autohints ++

206− getFn d fn)

204+ Just t -> do

205+ let others = hints ++ con_names t ++ autohints

206+ when (not fromProver) -- in interactive mode,

207+ -- don't just guess (fine for 'auto',

208+ -- since that's part of the point...)

209+ $ checkConstructor ist others

210+ tryCons d locs tys (others ++ getFn d fn)

207211 Nothing -> fail "Not a data type"

208212 _ -> fail "Not a data type"

209213

@@ -215,7 +219,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

215219

216220 tryLocals d locs tys [] = fail "Locals failed"

217221 tryLocals d locs tys ((x, t) : xs)

218− | x `elem` locs = tryLocals d locs tys xs

222+ | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs

219223 | otherwise = try' (tryLocal d (x : locs) tys x t)

220224 (tryLocals d locs tys xs) True

221225

@@ -245,12 +249,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

245249 ps' <- get_probs

246250 hs' <- get_holes

247251 when (length ps < length ps') $ fail "Can't apply constructor"

252+ let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)

248253 mapM_ (\ (_, h) -> do focus h

249254 aty <- goal

250− psRec True d locs tys)

251− (filter (\ (x, y) -> not x) (zip (map fst imps) args))

255+ psRec True d locs tys) newhs

252256 solve

253257

254258 isImp (PImp p _ _ _ _) = (True, p)

255259 isImp arg = (False, priority arg)

256260

261+-- In interactive mode, only search for things if there is some constructor

262+-- index to help pick a relevant constructor

263+checkConstructor :: IState -> [Name] -> ElabD ()

264+checkConstructor ist [] = return ()

265+checkConstructor ist (n : ns) =

266+ case lookupTyExact n (tt_ctxt ist) of

267+ Just t -> if not (conIndexed t)

268+ then fail "Overlapping constructor types"

269+ else checkConstructor ist ns

270+ where

271+ conIndexed t = let (_, args) = unApply (getRetTy t) in

272+ any conHead args

273+ conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)

274+ | otherwise = False

src/Idris/REPL.hs+16−7

@@ -366,6 +366,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =

366366 process fn (AddMissing False line (sUN name))

367367runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =

368368 process fn (MakeWith False line (sUN name))

369+runIdeModeCommand h id orig fn mods (IdeMode.MakeCaseBlock line name) =

370+ process fn (MakeCase False line (sUN name))

369371runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =

370372 doProofSearch fn False r line (sUN name) (map sUN hints) depth

371373runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =

@@ -632,6 +634,7 @@ idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClaus

632634idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

633635idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

634636idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

637+idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str)

635638idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

636639idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

637640 iPrintResult ""

@@ -901,8 +904,8 @@ process fn (Check (PRef _ _ n))

901904 case lookupNames n ctxt of

902905 ts@(t:_) ->

903906 case lookup t (idris_metavars ist) of

904− Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

905− showMetavarInfo ppo ist n i

907+ Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

908+ showMetavarInfo ppo ist n i

906909 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

907910 [] -> iPrintError $ "No such variable " ++ show n

908911 where

@@ -934,12 +937,14 @@ process fn (Check t)

934937 ctxt <- getContext

935938 ist <- getIState

936939 let ppo = ppOptionIst ist

937− ty' = normaliseC ctxt [] ty

940+ ty' = if opt_evaltypes (idris_options ist)

941+ then normaliseC ctxt [] ty

942+ else ty

938943 case tm of

939944 TType _ ->

940945 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

941946 _ -> iPrintTermWithType (pprintDelab ist tm)

942− (pprintDelab ist ty)

947+ (pprintDelab ist ty')

943948

944949process fn (Core t)

945950 = do (tm, ty) <- elabREPL recinfo ERHS t

@@ -1047,6 +1052,8 @@ process fn (AddMissing updatefile l n)

10471052 = addMissing fn updatefile l n

10481053process fn (MakeWith updatefile l n)

10491054 = makeWith fn updatefile l n

1055+process fn (MakeCase updatefile l n)

1056+ = makeCase fn updatefile l n

10501057process fn (MakeLemma updatefile l n)

10511058 = makeLemma fn updatefile l n

10521059process fn (DoProofSearch updatefile rec l n hints)

@@ -1072,7 +1079,7 @@ process fn (RmProof n')

10721079 insertMetavar n =

10731080 do i <- getIState

10741081 let ms = idris_metavars i

1075− putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

1082+ putIState $ i { idris_metavars = (n, (Nothing, 0, [], False)) : ms }

10761083

10771084process fn' (AddProof prf)

10781085 = do fn <- do

@@ -1125,8 +1132,8 @@ process fn (Prove mode n')

11251132 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns

11261133 n <- case metavars of

11271134 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

1128− [(n, (_,_,False))] -> return n

1129− [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1135+ [(n, (_,_,_,False))] -> return n

1136+ [(_, (_,_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

11301137 ns -> ierror (CantResolveAlts (map fst ns))

11311138 prover mode (lit fn) n

11321139 -- recheck totality

@@ -1234,6 +1241,8 @@ process fn (SetOpt NoBanner) = setNoBanner True

12341241process fn (UnsetOpt NoBanner) = setNoBanner False

12351242process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

12361243process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1244+process fn (SetOpt EvalTypes) = setEvalTypes True

1245+process fn (UnsetOpt EvalTypes) = setEvalTypes False

12371246

12381247process fn (SetOpt _) = iPrintError "Not a valid option"

12391248process fn (UnsetOpt _) = iPrintError "Not a valid option"

src/Idris/REPLParser.hs+3

@@ -123,6 +123,8 @@ parserCommands =

123123 ":am <line> <name> adds all missing pattern matches for the name on the line"

124124 , proofArgCmd ["mw", "makewith"] MakeWith

125125 ":mw <line> <name> adds a with clause for the definition of the name on the line"

126+ , proofArgCmd ["mc", "makecase"] MakeCase

127+ ":mc <line> <name> adds a case block for the definition of the metavariable on the line"

126128 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

127129 , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

128130 , (["lto", "loadto"], SeqArgs NumberArg FileArg

@@ -257,6 +259,7 @@ optArg cmd name = do

257259 <|> do discard (P.symbol "autosolve"); return AutoSolve

258260 <|> do discard (P.symbol "nobanner") ; return NoBanner

259261 <|> do discard (P.symbol "warnreach"); return WarnReach

262+ <|> do discard (P.symbol "evaltypes"); return EvalTypes

260263

261264proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

262265proofArg cmd name = do

src/Idris/Reflection.hs+5−5

@@ -82,7 +82,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)

8282reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

8383reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

8484reifyApp _ t [Constant (I i)]

85− | t == reflm "Search" = return (ProofSearch True True i Nothing [])

85+ | t == reflm "Search" = return (ProofSearch True True i Nothing [] [])

8686reifyApp _ t [x]

8787 | t == reflm "Refine" = do n <- reifyTTName x

8888 return $ Refine n []

@@ -313,7 +313,7 @@ reifyTTBinderApp reif f [x, y]

313313reifyTTBinderApp reif f [t]

314314 | f == reflm "Hole" = liftM Hole (reif t)

315315reifyTTBinderApp reif f [t]

316− | f == reflm "GHole" = liftM (GHole 0) (reif t)

316+ | f == reflm "GHole" = liftM (GHole 0 []) (reif t)

317317reifyTTBinderApp reif f [x, y]

318318 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

319319reifyTTBinderApp reif f [t]

@@ -339,7 +339,7 @@ reifyTTConstApp f (Constant c@(BI _))

339339 | f == reflm "BI" = return $ c

340340reifyTTConstApp f (Constant c@(Fl _))

341341 | f == reflm "Fl" = return $ c

342−reifyTTConstApp f (Constant c@(I _))

342+reifyTTConstApp f (Constant c@(Ch _))

343343 | f == reflm "Ch" = return $ c

344344reifyTTConstApp f (Constant c@(Str _))

345345 | f == reflm "Str" = return $ c

@@ -586,7 +586,7 @@ reflectBinderQuotePattern q ty unq (Hole t)

586586 fill $ reflCall "Hole" [ty, Var t']

587587 solve

588588 focus t'; q unq t

589−reflectBinderQuotePattern q ty unq (GHole _ t)

589+reflectBinderQuotePattern q ty unq (GHole _ _ t)

590590 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

591591 fill $ reflCall "GHole" [ty, Var t']

592592 solve

@@ -737,7 +737,7 @@ reflectBinderQuote q ty unq (NLet x y)

737737 = reflCall "NLet" [Var ty, q unq x, q unq y]

738738reflectBinderQuote q ty unq (Hole t)

739739 = reflCall "Hole" [Var ty, q unq t]

740−reflectBinderQuote q ty unq (GHole _ t)

740+reflectBinderQuote q ty unq (GHole _ _ t)

741741 = reflCall "GHole" [Var ty, q unq t]

742742reflectBinderQuote q ty unq (Guess x y)

743743 = reflCall "Guess" [Var ty, q unq x, q unq y]

src/Pkg/Package.hs+3−3

@@ -132,17 +132,17 @@ documentPkg fp =

132132 do pkgdesc <- parseDesc fp

133133 cd <- getCurrentDirectory

134134 let pkgDir = cd </> takeDirectory fp

135− outputDir = cd </> (pkgname pkgdesc) ++ "_doc"

135+ outputDir = cd </> pkgname pkgdesc ++ "_doc"

136136 opts = NoREPL : Verbose : idris_opts pkgdesc

137137 mods = modules pkgdesc

138138 fs = map (foldl1' (</>) . splitOn "." . showCG) mods

139139 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

140140 make (makefile pkgdesc)

141− setCurrentDirectory $ pkgDir

141+ setCurrentDirectory pkgDir

142142 let run l = runExceptT . execStateT l

143143 load [] = return ()

144144 load (f:fs) = do loadModule f; load fs

145− loader = do idrisMain opts; load fs

145+ loader = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs

146146 idrisInstance <- run loader idrisInit

147147 setCurrentDirectory cd

148148 case idrisInstance of

stack.yamlnew file+6

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

1+flags: {}

2+packages:

3+- '.'

4+extra-deps:

5+- cheapskate-0.1.0.4

6+resolver: nightly-2015-07-24

test/disambig001/disambig001.idrdeleted−12

@@ -1,12 +0,0 @@

1−module Main

2−

3−import Prelude.Monad

4−

5−import System

6−import Effect.System

7−

8−main : IO ()

9−main = do

10− args <- System.getArgs

11− putStrLn (concat (drop 1 args))

12−

test/disambig001/expecteddeleted−1

@@ -1 +0,0 @@

1−foobar

test/disambig001/rundeleted−4

@@ -1,4 +0,0 @@

1−#!/usr/bin/env bash

2−idris $@ disambig001.idr -p effects -o disambig001

3−./disambig001 foo bar

4−rm -f disambig001 *.ibc

test/docs003/expected+1−1

@@ -11,11 +11,11 @@ Methods:

1111 The function is Total

1212Instances:

1313 Functor List

14+ Functor (IO' ffi)

1415 Functor Stream

1516 Functor Provider

1617 Functor Binder

1718 Functor PrimIO

18− Functor (IO' ffi)

1919 Functor Maybe

2020 Functor (Either e)

2121

test/effects005/defaultlog.idrnew file+18

@@ -0,0 +1,18 @@

1+import Effects

2+import Effect.Logging.Default

3+

4+func : Nat -> Eff () [LOG String]

5+func x = do

6+ log WARN Nil $ unwords ["I do nothing with", show x]

7+ pure ()

8+

9+doubleFunc : Nat -> Eff Nat [LOG String]

10+doubleFunc x = do

11+ log WARN ["NumOPS"] $ unwords ["Doing the double with", show x ]

12+ func x

13+ pure (x+x)

14+

15+main : IO ()

16+main = do

17+ x <- runInit [(ALL,["NumOPS"])] (doubleFunc 3)

18+ printLn x

test/effects005/expectednew file+5

@@ -0,0 +1,5 @@

1+"3 : Doing the double with 3"

2+6

3+8

4+"3 : [\"NumOPS\"] : Doing the double with 3"

5+6

test/effects005/runnew file+6

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

1+#!/usr/bin/env bash

2+idris $@ simplelog.idr -o simple -p effects

3+./simple

4+idris $@ defaultlog.idr -o default -p effects

5+./default

6+rm -f simple default *.ibc

test/effects005/simplelog.idrnew file+14

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

1+import Effects

2+import Effect.Logging.Simple

3+

4+doubleFunc : Nat -> Eff Nat [LOG]

5+doubleFunc x = do

6+ log WARN $ unwords ["Doing the double with", show x ]

7+ pure (x+x)

8+

9+main : IO ()

10+main = do

11+ x <- runInit [ALL] (doubleFunc 3)

12+ printLn x

13+ y <- runInit [OFF] (doubleFunc 4)

14+ printLn y

test/interactive003/expected+1

@@ -2,3 +2,4 @@ ys

22x :: app xs ys

33[]

44f x y :: vzipWith f xs ys

5+?word_length_rhs_3 :: word_length xs

test/interactive003/input+1

@@ -2,3 +2,4 @@

22:ps 5 app_rhs_2

33:ps 8 vzipWith_rhs_3

44:ps 9 vzipWith_rhs_1

5+:ps 13 word_length_rhs_2

test/interactive003/interactive003.idr+5

@@ -8,3 +8,8 @@ vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

88vzipWith f [] [] = ?vzipWith_rhs_3

99vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1

1010

11+word_length : Vect n String -> Vect n Nat

12+word_length [] = []

13+word_length (x :: xs) = ?word_length_rhs_2

14+

15+

test/proof001/test029.idr+1−1

@@ -29,7 +29,7 @@ append (x :: xs) ys ?= x :: append xs ys

2929simple.append_lemma_2 = proof {

3030 intros;

3131 compute;

32− rewrite (plusSuccRightSucc m n);

32+ rewrite (plusSuccRightSucc m k);

3333 trivial;

3434}

3535

test/records004/expectednew file+3

@@ -0,0 +1,3 @@

1+"Fred"

2+"Joe"

3+"Bloggs"

test/records004/records004.idrnew file+13

@@ -0,0 +1,13 @@

1+-- Test for multiple field declarations on one line with the same type

2+

3+record Person where

4+ constructor MkPerson

5+ firstName, middleName, lastName : String

6+

7+fred : Person

8+fred = MkPerson "Fred" "Joe" "Bloggs"

9+

10+main : IO ()

11+main = do printLn (firstName fred)

12+ printLn (middleName fred)

13+ printLn (lastName fred)

test/records004/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ records004.idr -o records004

3+./records004

4+rm -f records004 *.ibc

test/tutorial006/expected+4−4

@@ -1,15 +1,15 @@

11tutorial006a.idr:5:23-25:When checking right hand side of vapp:

22When checking argument xs to constructor Data.VectType.Vect.:::

33 Type mismatch between

4− Vect (n + n) a (Type of vapp xs xs)

4+ Vect (k + k) a (Type of vapp xs xs)

55 and

6− Vect (plus n m) a (Expected type)

6+ Vect (plus k m) a (Expected type)

77

88 Specifically:

99 Type mismatch between

10− plus n n

10+ plus k k

1111 and

12− plus n m

12+ plus k m

1313tutorial006b.idr:10:10:

1414When checking right hand side of with block in Main.parity:

1515Type mismatch between