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

.gitignore+1

compare with master

unifiedsplit

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

28tags

29TAGS

30src/Version_idris.hs

31+.stack-work

CHANGELOG+3

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

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

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

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

27

30

28New in 0.9.18:

31New in 0.9.18:

29--------------

32--------------

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

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

29

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

31same 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:

33

34.. code:: idris

35

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

254 -- Single Line

255 {- Multiline -}

256 ||| Docstring (goes before definition)

257+

258+Multi line String literals

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

260+

261+::

262+

263+ foo = """

264+ this is a

265+ string literal"""

257

266

258Directives

267Directives

259----------

268----------

docs/tutorial/classes.rst+4−4

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

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

364

365Rather 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

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

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

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

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

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

369−Idris library):

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

370

371.. code-block:: idris

372

docs/tutorial/modules.rst+3−3

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

34

35

36Then, 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:

38

39.. code-block:: idris

40

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

50

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

52because 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:

54

55+ ``Btree.BTree``

56+ ``Btree.Leaf``

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

99.. note::

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

101

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

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

104

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

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

55 generates code.

56

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

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

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

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

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

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

60

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

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

docs/tutorial/testing.rst+31−11

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

4Testing Idris Packages

5**********************

6

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

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

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

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

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

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

10

11

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.

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

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.

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.

14

22

15

23

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

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

17

25

18.. code-block:: idris

26.. code-block:: idris

27+ :caption: Math/NumOps.idr

19

28

20 module Maths.NumOps

29 module Maths.NumOps

21

30

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

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

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

29

38

30.. code-block:: idris

39.. code-block:: idris

40+ :caption: Math/TestOps.idr

31

41

32 module Test.NumOps

42 module Test.NumOps

33

43

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

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

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

37 assertEq g e = if g == e

47 assertEq g e = if g == e

38 then putStrLn "Test Passed"

48 then putStrLn "Test Passed"

39− else putStrLn "Test failed"

49+ else putStrLn "Test Failed"

40

50

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

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

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

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

43 then putStrLn "Test Passed"

53 then putStrLn "Test Passed"

44− else putStrLn "Test failed"

54+ else putStrLn "Test Failed"

45

55

46 testDouble : IO ()

56 testDouble : IO ()

47 testDouble = assertEq (double 2) 4

57 testDouble = assertEq (double 2) 4

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

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

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

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

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

55

65

56− module maths

66+ package maths

57

67

58− module = Maths.NumOps

68+ modules = Maths.NumOps

59− , Test.NumOps

69+ , Test.NumOps

60

70

61 tests = Test.NumOps.testDouble

71 tests = Test.NumOps.testDouble

62 , Test.NumOps.testTriple

72 , Test.NumOps.testTriple

63

73

64

74

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:

103

104::

105

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

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

107

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

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

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

349 $ idris vbroken.idr --check

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

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

352− Type mismatch between

352+ Type mismatch between

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

354 and

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

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

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

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

444inferred 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

446as a parameter or index in a

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

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

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

912 showPerson p = let MkPerson name age = p in

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

914

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

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

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

918−

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

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

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

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

921pattern matching at the top level:

917pattern matching at the top level:

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

1021

1017

1022 record Person where

1018 record Person where

1023 constructor MkPerson

1019 constructor MkPerson

1024− name : String

1020+ firstName, middleName, lastName : String

1025 age : Int

1021 age : Int

1026

1022

1027 fred : Person

1023 fred : Person

1028− fred = MkPerson "Fred" 30

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

1029

1025

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

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

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

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

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

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

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

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

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

1032+access the field values:

1035

1033

1036::

1034::

1037

1035

1038− *record> name fred

1036+ *record> firstName fred

1039 "Fred" : String

1037 "Fred" : String

1040 *record> age fred

1038 *record> age fred

1041 30 : Int

1039 30 : Int

1042− *record> :t name

1040+ *record> :t firstName

1043− name : Person -> String

1041+ firstName : Person -> String

1044

1042

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

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

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

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

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

1048

1046

1049.. code-block:: bash

1047.. code-block:: bash

1050

1048

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

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

1052− MkPerson "Jim" 30 : Person

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

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

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

1054− MkPerson "Jim" 20 : Person

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

1055

1053

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

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

1057updates the given fields in a record.

1055updates the given fields in a record.

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

1078::

1076::

1079

1077

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

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

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

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

1082

1080

1083Nested record update

1081Nested record update

1084--------------------

1082--------------------

idris.cabal+6−3

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

118 libs/contrib/Data/*.idr

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

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

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

121 libs/contrib/Decidable/*.idr

122 libs/contrib/Decidable/*.idr

122 libs/contrib/Network/*.idr

123 libs/contrib/Network/*.idr

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

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

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

125 libs/effects/Makefile

126 libs/effects/Makefile

126 libs/effects/effects.ipkg

127 libs/effects/effects.ipkg

127 libs/effects/Effect/*.idr

128 libs/effects/Effect/*.idr

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

128 libs/effects/*.idr

130 libs/effects/*.idr

129

131

130 test/Makefile

132 test/Makefile

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

388 test/delab001/expected

390 test/delab001/expected

389 test/delab001/input

391 test/delab001/input

390

392

391− test/disambig001/run

392− test/disambig001/*.idr

393− test/disambig001/expected

394 test/disambig002/run

393 test/disambig002/run

395 test/disambig002/*.idr

394 test/disambig002/*.idr

396 test/disambig002/expected

395 test/disambig002/expected

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

424 test/effects004/*.idr

423 test/effects004/*.idr

425 test/effects004/expected

424 test/effects004/expected

426 test/effects004/input

425 test/effects004/input

426+ test/effects005/run

427+ test/effects005/*.idr

428+ test/effects005/expected

429+

427

430

428 test/error001/run

431 test/error001/run

429 test/error001/*.idr

432 test/error001/*.idr

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

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

27 plus_i = User 6

28

29

30−

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

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

32-- we can do:

31-- we can do:

33{-

32{-

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

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

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

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

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

63

62

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+

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

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

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

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

66instance Num (Complex Float) where

71instance Num (Complex Float) where

libs/base/Data/HVect.idr−1

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

1module Data.HVect

2

3−import Data.Fin

4import public Data.Vect

3import public Data.Vect

5

4

6%access public

5%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)

52mapElem Here = Here

53mapElem (There e) = There (mapElem e)

54

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

1module Data.VectType

2

3−import Data.Fin

3+import public Data.Fin

4

5%access public

6%default total

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

9

10infixr 7 ::

11

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

13+%elim

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

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

15+ ||| Empty vector

13 Nil : Vect Z a

16 Nil : Vect Z 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`.

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

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

15

20

16-- Hints for interactive editing

21-- Hints for interactive editing

17%name Vect xs,ys,zs,ws

22%name Vect xs,ys,zs,ws

libs/base/System.idr−16

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

4%default partial

5%access public

6

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−

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

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

24||| otherwise it returns Nothing.

8||| otherwise it returns Nothing.

25getEnv : String -> IO (Maybe String)

9getEnv : String -> IO (Maybe String)

libs/base/base.ipkg+1−1

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

5

6 Debug.Error, Debug.Trace,

7

8− System.Info, System.Interactive,

8+ System.Info,

9

10 Language.Reflection.Utils,

11

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

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

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

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

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

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

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

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

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

60class AbelianGroup a => Ring a where

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

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

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

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

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

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

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

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

86class Ring a => RingWithUnity a where

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

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

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

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

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

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

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

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

115class RingWithUnity a => Field a where

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

117

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

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

119−sum = foldr (<+>) neutral

119+sum' = concat

120

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

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

122−product = foldr (<.>) unity

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

123

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

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

125−power _ Z = unity

125+pow' _ Z = unity

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

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

127

128

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

1module Control.Algebra.NumericInstances

3module Control.Algebra.NumericInstances

2

4

3import Control.Algebra

5import Control.Algebra

6+import Control.Algebra.VectorSpace

4import Data.Complex

7import Data.Complex

5import Data.ZZ

8import Data.ZZ

6

9

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

102

105

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

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

104 unity = (unity :+ neutral)

107 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

1module Data.Matrix

3module Data.Matrix

2

4

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

11

6

12%default total

7%default total

13

8

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−

78||| Matrix with n rows and m columns

9||| Matrix with n rows and m columns

79Matrix : Nat -> Nat -> Type -> Type

10Matrix : Nat -> Nat -> Type -> Type

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

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

81

12

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

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

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

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

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

15+getCol f = map (index f)

85

16

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

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

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

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

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

19+getRow = index

89

20

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

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

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

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

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

23+deleteCol f = map (deleteAt f)

93

24

94−||| Matrix times a column vector

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

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

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

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

27+deleteRow = deleteAt

97

28

98−||| Matrix times a row vector

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

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

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

30+insertRow = insertAt

101

31

102−||| Matrix multiplication

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

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

33+insertCol f = zipWith (insertAt f)

104− Matrix k m a ->

105− Matrix n m a

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

107

34

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

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

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

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

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

37+indices f1 f2 = index f2 . index f1

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

115

38

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

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

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

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

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

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

119

42

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

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

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

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

122row r = [r]

45row r = [r]

123

46

124−||| Outer product between ring vectors

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

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

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

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

49+subMatrix r c = deleteRow r . deleteCol c

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

148

50

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

150

54

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,

9 Control.WellFounded,

10 Classes.Verified,

11 Data.Fun, Data.Rel,

12− Data.Hash, Data.Matrix,

12+ Data.Hash,

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

13 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,

14 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,

14 Data.ZZ, Data.Sign,

15 Data.ZZ, Data.Sign,

15 Data.BoundedList,

16 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

2

3import Effects

4import Data.Vect

5−import Data.Fin

6

5

7data Random : Effect where

6data Random : Effect where

8 getRandom : sig Random Integer Integer

7 getRandom : sig Random Integer Integer

libs/effects/effects.ipkg+15−4

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

1package effects

2

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

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

5

4

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

5+modules = Effects

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

6+ , Effect.Default

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

7+ , Effect.Monad

9

8

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

253 %used FFI_Prim prim

254

255 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)

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

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

259

libs/prelude/Prelude.idr+2−211

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

25import public Prelude.Stream

26import public Prelude.Providers

27import public Prelude.Show

28+import public Prelude.Interactive

29+import public Prelude.File

28import public Decidable.Equality

30import public Decidable.Equality

29import public Language.Reflection

31import public Language.Reflection

30import public Language.Reflection.Errors

32import public Language.Reflection.Errors

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

43instance Functor PrimIO where

45instance Functor PrimIO where

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

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

45

47

46−instance Functor (IO' ffi) where

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

48−

49instance Functor Maybe where

48instance Functor Maybe where

50 map f (Just x) = Just (f x)

49 map f (Just x) = Just (f x)

51 map f Nothing = Nothing

50 map f Nothing = Nothing

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

61

60

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

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

63

62

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−

70instance Applicative Maybe where

63instance Applicative Maybe where

71 pure = Just

64 pure = Just

72

65

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

103instance Monad PrimIO where

96instance Monad PrimIO where

104 b >>= k = prim_io_bind b k

97 b >>= k = prim_io_bind b k

105

98

106−instance Monad (IO' ffi) where

107− b >>= k = io_bind b k

108−

109instance Monad Maybe where

99instance Monad Maybe where

110 Nothing >>= k = Nothing

100 Nothing >>= k = Nothing

111 (Just x) >>= k = k x

101 (Just x) >>= k = k x

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

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

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

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

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

231

221

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−

409namespace JSNull

222namespace JSNull

410 ||| Check if a foreign pointer is null

223 ||| Check if a foreign pointer is null

411 partial

224 partial

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

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

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

426 return (eq /= 0)

239 return (eq /= 0)

427

240

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−

434||| Loop while some test is true

241||| Loop while some test is true

435|||

242|||

436||| @ test the condition of the loop

243||| @ test the condition of the loop

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

442 while t b

249 while t b

443 else return ()

250 else return ()

444

251

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−

461------- Some error rewriting

252------- Some error rewriting

462

253

463%language ErrorReflection

254%language ErrorReflection

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

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

15instance Cast String Int where

16 cast = prim__fromStrInt

17

18−instance Cast String Float where

18+instance Cast String Double where

19 cast = prim__strToFloat

20

21instance Cast String Integer where

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

26instance Cast Int String where

27 cast = prim__toStrInt

28

29−instance Cast Int Float where

29+instance Cast Int Double where

30 cast = prim__toFloatInt

31

32instance Cast Int Integer where

33 cast = prim__sextInt_BigInt

34

35−-- Float casts

35+-- Double casts

36

37−instance Cast Float String where

37+instance Cast Double String where

38 cast = prim__floatToStr

39

40−instance Cast Float Int where

40+instance Cast Double Int where

41 cast = prim__fromFloatInt

42

43+instance Cast Double Integer where

44+ cast = prim__fromFloatBigInt

45+

43-- Integer casts

46-- Integer casts

44

47

45instance Cast Integer String where

48instance Cast Integer String where

46 cast = prim__toStrBigInt

49 cast = prim__toStrBigInt

47

50

51+instance Cast Integer Double where

52+ cast = prim__toFloatBigInt

53+

48-- Char casts

54-- Char casts

49

55

50instance Cast Char Int where

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

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

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

6||| programming.

7−module System.Interactive

7+module Prelude.Interactive

8

9−{-

9+import Builtins

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

10+import Prelude.List

11−-}

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

12

83

13−import System

14

84

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

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

16||| @ state the input state

86||| @ state the input state

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

18||| output and a new state

88||| output and a new state

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

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

20||| to output

90||| to output

21−public partial

91+partial

22processHandle : File ->

92processHandle : File ->

23 (state : a) ->

93 (state : a) ->

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

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

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

38||| output and a new state

108||| output and a new state

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

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

40||| to output

110||| to output

41−public partial

111+partial

42processStdin : (state : a) ->

112processStdin : (state : a) ->

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

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

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

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

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

49||| @ prompt the prompt to show

119||| @ prompt the prompt to show

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

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

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

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

52−public partial

122+partial

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

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

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

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

55replWith acc prompt fn

125replWith acc prompt fn

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

64||| @ prompt the prompt to show

134||| @ prompt the prompt to show

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

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

66||| output

136||| output

67−public partial

137+partial

68repl : (prompt : String) ->

138repl : (prompt : String) ->

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

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

70repl prompt fn

140repl prompt fn

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

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

18infix 5 \\

19infixr 7 ::,++

20

21−||| Linked lists

21+||| Generic lists

22%elim data List elem =

23− ||| The empty list

23+ ||| Empty list

24 Nil |

25− ||| Cons cell

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

26+ ||| the list.

26 (::) elem (List elem)

27 (::) elem (List elem)

27

28

28-- Name hints for interactive editing

29-- Name hints for interactive editing

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

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

3-- Monads and Functors

4

5import Builtins

6−import Prelude.List

6+import Prelude.Functor

7import Prelude.Applicative

8import Prelude.Basics

9+import IO

9

10

10%access public

11%access public

11

12

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

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

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

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

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

24return = pure

25return = 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

12%access public

13%default total

14

15−||| Unary natural numbers

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

16+||| matched.

16%elim data Nat =

17%elim data Nat =

17 ||| Zero

18 ||| Zero

18 Z |

19 Z |

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

213instance Cast Integer Nat where

214instance Cast Integer Nat where

214 cast = fromInteger

215 cast = fromInteger

215

216

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 (*)

217record Multiplicative where

218record Multiplicative where

218 constructor getMultiplicative

219 constructor getMultiplicative

219 _ : Nat

220 _ : Nat

220

221

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 (+)

222record Additive where

223record Additive where

223 constructor getAdditive

224 constructor getAdditive

224 _ : Nat

225 _ : Nat

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

262instance Cast Nat Int where

263instance Cast Nat Int where

263 cast = toIntNat

264 cast = toIntNat

264

265

266+instance Cast Nat Double where

267+ cast = cast . toIntegerNat

268+

265--------------------------------------------------------------------------------

269--------------------------------------------------------------------------------

266-- Auxilliary notions

270-- Auxilliary notions

267--------------------------------------------------------------------------------

271--------------------------------------------------------------------------------

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

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

1module Prelude.Strings

2

3import Builtins

4+import IO

4

5

5import Prelude.Algebra

6import Prelude.Algebra

6import Prelude.Basics

7import Prelude.Basics

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

13import Prelude.Functor

14import Prelude.Functor

14import Prelude.List

15import Prelude.List

15import Prelude.Nat

16import Prelude.Nat

17+import Prelude.Monad

16import Decidable.Equality

18import Decidable.Equality

17

19

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+

18||| Appends two strings together.

29||| Appends two strings together.

19|||

30|||

20||| ```idris example

31||| ```idris example

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

247lines : String -> List String

258lines : String -> List String

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

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

249

260

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−

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

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

260|||

262|||

261||| ```idris example

263||| ```idris example

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

263||| ```

265||| ```

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

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

265unwords' [] = []

267unwords' [] = []

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

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

267− where

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

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

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

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

270

271

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

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

272|||

273|||

273||| ```idris example

274||| ```idris example

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

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

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

276unwords : List String -> String

277unwords : List String -> String

277unwords = pack . unwords' . map unpack

278unwords = pack . unwords' . map unpack

278

279

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+

279||| Returns the length of the string.

299||| Returns the length of the string.

280|||

300|||

281||| ```idris example

301||| ```idris example

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

287length : String -> Nat

307length : String -> Nat

288length = fromInteger . prim__zextInt_BigInt . prim_lenString

308length = fromInteger . prim__zextInt_BigInt . prim_lenString

289

309

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+

290||| Lowercases all characters in the string.

318||| Lowercases all characters in the string.

291|||

319|||

292||| ```idris example

320||| ```idris example

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

321

349

322isInfixOf : String -> String -> Bool

350isInfixOf : String -> String -> Bool

323isInfixOf a b = isInfixOf (unpack a) (unpack b)

351isInfixOf 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,

9 Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

12+ Prelude.Interactive, Prelude.File,

12

13

13 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

14 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

14

15

src/Idris/AbsSyntax.hs+9−3

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

597

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

599addDeferred' :: NameType

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

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

601 -- ^ The Name is the name being made into a metavar,

602 -- the Int is the number of vars that are part of a

603 -- putative proof context, the Maybe Name is the

@@ -606,10 +606,10 @@ addDeferred' :: NameType

606 -- allowed

607 -> Idris ()

608addDeferred' 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

610 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

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

613 idris_metavars i }

614 where

615 -- 'tidyNames' is to generate user accessible names in case they are

@@ -790,6 +790,12 @@ getNoBanner = do i <- getIState

790 let opts = idris_options i

791 return (opt_nobanner opts)

792

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+

793setQuiet :: Bool -> Idris ()

799setQuiet :: Bool -> Idris ()

794setQuiet q = do i <- getIState

800setQuiet q = do i <- getIState

795 let opts = idris_options i

801 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+35−11

@@ -89,7 +89,8 @@ data IOption = IOption { opt_logLevel :: Int,

89 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

90 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

91 opt_optimise :: [Optimisation],

92− opt_printdepth :: Maybe Int

92+ opt_printdepth :: Maybe Int,

93+ opt_evaltypes :: Bool -- ^ normalise types in :t

93 }

94 }

94 deriving (Show, Eq)

95 deriving (Show, Eq)

95

96

@@ -115,10 +116,12 @@ defaultOpts = IOption { opt_logLevel = 0

115 , opt_autoImport = []

116 , opt_autoImport = []

116 , opt_optimise = defaultOptimise

117 , opt_optimise = defaultOptimise

117 , opt_printdepth = Just 5000

118 , opt_printdepth = Just 5000

119+ , opt_evaltypes = True

118 }

120 }

119

121

120data PPOption = PPOption {

122data PPOption = PPOption {

121 ppopt_impl :: Bool -- ^^ whether to show implicits

123 ppopt_impl :: Bool -- ^^ whether to show implicits

124+ , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings

122 , ppopt_depth :: Maybe Int

125 , ppopt_depth :: Maybe Int

123} deriving (Show)

126} deriving (Show)

124

127

@@ -129,16 +132,21 @@ defaultOptimise = [PETransform]

129

132

130-- | Pretty printing options with default verbosity.

133-- | Pretty printing options with default verbosity.

131defaultPPOption :: PPOption

134defaultPPOption :: 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 }

133

138

134-- | Pretty printing options with the most verbosity.

139-- | Pretty printing options with the most verbosity.

135verbosePPOption :: PPOption

140verbosePPOption :: 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 }

137

144

138-- | Get pretty printing options from the big options record.

145-- | Get pretty printing options from the big options record.

139ppOption :: IOption -> PPOption

146ppOption :: IOption -> PPOption

140ppOption opt = PPOption {

147ppOption opt = PPOption {

141 ppopt_impl = opt_showimp opt,

148 ppopt_impl = opt_showimp opt,

149+ ppopt_pinames = False,

142 ppopt_depth = opt_printdepth opt

150 ppopt_depth = opt_printdepth opt

143}

151}

144

152

@@ -193,10 +201,11 @@ data IState = IState {

193 idris_name :: Int,

201 idris_name :: Int,

194 idris_lineapps :: [((FilePath, Int), PTerm)],

202 idris_lineapps :: [((FilePath, Int), PTerm)],

195 -- ^ Full application LHS on source line

203 -- ^ Full application LHS on source line

196− idris_metavars :: [(Name, (Maybe Name, Int, Bool))],

204+ idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],

197 -- ^ The currently defined but not proven metavariables. The Int

205 -- ^ The currently defined but not proven metavariables. The Int

198 -- is the number of vars to display as a context, the Maybe Name

206 -- is the number of vars to display as a context, the Maybe Name

207+ -- is its top-level function, the [Name] is the list of local variables

199− -- is its top-level function, and the Bool is whether :p is

208+ -- available for proof search and the Bool is whether :p is

200 -- allowed

209 -- allowed

201 idris_coercions :: [Name],

210 idris_coercions :: [Name],

202 idris_errRev :: [(Term, Term)],

211 idris_errRev :: [(Term, Term)],

@@ -400,10 +409,13 @@ data Command = Quit

400 | AddProofClauseFrom Bool Int Name

409 | AddProofClauseFrom Bool Int Name

401 | AddMissing Bool Int Name

410 | AddMissing Bool Int Name

402 | MakeWith Bool Int Name

411 | MakeWith Bool Int Name

412+ | MakeCase Bool Int Name

403 | MakeLemma Bool Int Name

413 | MakeLemma Bool Int Name

404− | DoProofSearch Bool Bool Int Name [Name]

414+ | DoProofSearch Bool -- update file

405− -- ^ the first bool is whether to update,

415+ Bool -- recursive search

406− -- the second is whether to search recursively (i.e. for the arguments)

416+ Int -- depth

417+ Name -- top level name

418+ [Name] -- hints

407 | SetOpt Opt

419 | SetOpt Opt

408 | UnsetOpt Opt

420 | UnsetOpt Opt

409 | NOP

421 | NOP

@@ -451,6 +463,7 @@ data Opt = Filename String

451 | DefaultPartial

463 | DefaultPartial

452 | WarnPartial

464 | WarnPartial

453 | WarnReach

465 | WarnReach

466+ | EvalTypes

454 | NoCoverage

467 | NoCoverage

455 | ErrContext

468 | ErrContext

456 | ShowImpl

469 | ShowImpl

@@ -978,7 +991,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

978 | MatchRefine Name

991 | MatchRefine Name

979 | LetTac Name t | LetTacTy Name t t

992 | LetTac Name t | LetTacTy Name t t

980 | Exact t | Compute | Trivial | TCInstance

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

982 -- ^ the bool is whether to search recursively

997 -- ^ the bool is whether to search recursively

983 | Solve

998 | Solve

984 | Attack

999 | Attack

@@ -1549,7 +1564,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1549 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

1564 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

1550 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

1565 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

1551 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)

1566 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 =

1553 depth d . bracket p startPrec . group $

1569 depth d . bracket p startPrec . group $

1554 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

1570 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

1555 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc

1571 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

1558 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>

1574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>

1559 group (prettySe (decD d) startPrec ((n, False):bnd) sc)

1575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)

1560 where

1576 where

1577+ uname (UN n) = case str n of

1578+ ('_':_) -> False

1579+ _ -> True

1580+ uname _ = False

1581+

1561 st =

1582 st =

1562 case s of

1583 case s of

1563 Static -> text "[static]" <> space

1584 Static -> text "[static]" <> space

@@ -1576,7 +1597,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1576 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1597 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1577 depth d . bracket p startPrec $

1598 depth d . bracket p startPrec $

1578 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1599 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) =

1580 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1601 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1581 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1602 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1582 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

1603 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

@@ -1996,6 +2017,9 @@ showTm ist = displayDecorated (consoleDecorate ist) .

1996showTmImpls :: PTerm -> String

2017showTmImpls :: PTerm -> String

1997showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

2018showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

1998

2019

2020+-- | Show a term with specific options

2021+showTmOpts :: PPOption -> PTerm -> String

2022+showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""

1999

2023

2000

2024

2001instance Sized PTerm where

2025instance Sized PTerm where

src/Idris/CaseSplit.hs+18−11

@@ -265,18 +265,23 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

265 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups

266

267 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

269 xs' <- updateRHSs i' xs

270 return (x' : xs')

271

272− updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs

272+ updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs

273− return ("?=" ++ xs', i')

273+ return ("?=" ++ xs', i')

274+ updateRHS last i ('?':xs)

274− updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) 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

275− (nm', i') <- getUniq nm i

280+ (nm', i') <- getUniq nm i

276− return ('?':nm' ++ rest, i')

281+ return ('?':nm' ++ rest, i')

277− updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs

282+ updateRHS last i (x : xs) = do (xs', i') <- updateRHS last i xs

278− return (x : xs', i')

283+ return (x : xs', i')

279− updateRHS i [] = return ("", i)

284+ updateRHS last i [] = return ("", i)

280

285

281

286

282 -- TMP HACK: If there are Nats, we don't want to show as numerals since

287 -- TMP HACK: If there are Nats, we don't want to show as numerals since

@@ -361,9 +366,11 @@ getClause l fn fp

361 getNameFrom i used (PApp fc f as) = getNameFrom i used f

366 getNameFrom i used (PApp fc f as) = getNameFrom i used f

362 getNameFrom i used (PRef fc _ f)

367 getNameFrom i used (PRef fc _ f)

363 = case getNameHints i f of

368 = case getNameHints i f of

364− [] -> uniqueName (sUN "x") used

369+ [] -> uniqueNameFrom (mkSupply [sUN "x", sUN "y",

370+ sUN "z"]) used

365 ns -> uniqueNameFrom (mkSupply ns) used

371 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

367

374

368 -- write method declarations, indent with 4 spaces

375 -- write method declarations, indent with 4 spaces

369 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

376 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

src/Idris/Completion.hs+1−1

@@ -52,7 +52,7 @@ names = do i <- get

52

53metavars :: Idris [String]

54metavars = 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

56

57

58modules :: Idris [String]

src/Idris/Core/Binary.hs+6−4

@@ -499,9 +499,10 @@ instance (Binary b) => Binary (Binder b) where

499 put x2

500 Hole x1 -> do putWord8 4

501 put x1

502− GHole x1 x2 -> do putWord8 5

502+ GHole x1 x2 x3 -> do putWord8 5

503− put x1

503+ put x1

504− put x2

504+ put x2

505+ put x3

505 Guess x1 x2 -> do putWord8 6

506 Guess x1 x2 -> do putWord8 6

506 put x1

507 put x1

507 put x2

508 put x2

@@ -528,7 +529,8 @@ instance (Binary b) => Binary (Binder b) where

528 return (Hole x1)

529 return (Hole x1)

529 5 -> do x1 <- get

530 5 -> do x1 <- get

530 x2 <- get

531 x2 <- get

532+ x3 <- get

531− return (GHole x1 x2)

533+ return (GHole x1 x2 x3)

532 6 -> do x1 <- get

534 6 -> do x1 <- get

533 x2 <- get

535 x2 <- get

534 return (Guess x1 x2)

536 return (Guess x1 x2)

src/Idris/Core/DeepSeq.hs+1−1

@@ -128,7 +128,7 @@ instance (NFData b) => NFData (Binder b) where

128 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

129 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

130 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` ()

132 rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

133 rnf (PVar x1) = rnf x1 `seq` ()

134 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

51 let p' = p { dontunify = n : dontunify p }

52 put (ES (p', a) s m)

53

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+

54saveState :: Elab' aux ()

68saveState :: Elab' aux ()

55saveState = do e@(ES p s _) <- get

69saveState = do e@(ES p s _) <- get

56 put (ES p s (Just e))

70 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

93 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

94 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

95 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

97 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

98 fixBinder (PVar t) = PVar <$> toTT t

99 fixBinder (PVTy t) = PVTy <$> toTT t

src/Idris/Core/ProofState.hs+7−4

@@ -39,6 +39,7 @@ data ProofState = PS { thname :: Name,

39 deferred :: [Name], -- ^ names we'll need to define

40 instances :: [Name], -- ^ instance arguments (for type classes)

41 autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes

42+ psnames :: [Name], -- ^ Local names okay to use in proof search

42 previous :: Maybe ProofState, -- ^ for undo

43 previous :: Maybe ProofState, -- ^ for undo

43 context :: Context,

44 context :: Context,

44 datatypes :: Ctxt TypeInfo,

45 datatypes :: Ctxt TypeInfo,

@@ -244,7 +245,8 @@ unify' ctxt env (topx, xfrom) (topy, yfrom) =

244 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)

245 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)

245 traceWhen (unifylog ps)

246 traceWhen (unifylog ps)

246 ("Now solved: " ++ show ns' ++

247 ("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))) $

248 put (ps { problems = probs' ++ probs_notu,

250 put (ps { problems = probs' ++ probs_notu,

249 unified = (h, ns'),

251 unified = (h, ns'),

250 injective = updateInj u (injective ps),

252 injective = updateInj u (injective ps),

@@ -300,7 +302,7 @@ newProof n ctxt datatypes ty =

300 in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

302 in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

301 (P Bound h ty'))) ty [] (h, []) [] []

303 (P Bound h ty'))) ty [] (h, []) [] []

302 Nothing [] []

304 Nothing [] []

303− [] [] []

305+ [] [] [] []

304 Nothing ctxt datatypes "" False False [] []

306 Nothing ctxt datatypes "" False False [] []

305

307

306type TState = ProofState -- [TacticAction])

308type TState = ProofState -- [TacticAction])

@@ -428,7 +430,8 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

428 do let env' = filter (\(n, t) -> n `notElem` dropped) env

430 do let env' = filter (\(n, t) -> n `notElem` dropped) env

429 action (\ps -> let hs = holes ps in

431 action (\ps -> let hs = holes ps in

430 ps { holes = hs \\ [x] })

432 ps { holes = hs \\ [x] })

433+ ps <- get

431− return (Bind n (GHole (length env') (mkTy (reverse env') t))

434+ return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

432 (mkApp (P Ref n ty) (map getP (reverse env'))))

435 (mkApp (P Ref n ty) (map getP (reverse env'))))

433 where

436 where

434 mkTy [] t = t

437 mkTy [] t = t

@@ -444,7 +447,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

444 ds = deferred ps in

447 ds = deferred ps in

445 ps { holes = hs \\ [x],

448 ps { holes = hs \\ [x],

446 deferred = n : ds })

449 deferred = n : ds })

447− return (Bind n (GHole 0 fty)

450+ return (Bind n (GHole 0 [] fty)

448 (mkApp (P Ref n ty) (map getP args)))

451 (mkApp (P Ref n ty) (map getP args)))

449 where

452 where

450 getP n = case lookup n env of

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

809 binderVal :: b }

810 | Hole { binderTy :: !b}

811 | GHole { envlen :: Int,

812+ localnames :: [Name],

812 binderTy :: !b}

813 binderTy :: !b}

813 | Guess { binderTy :: !b,

814 | Guess { binderTy :: !b,

814 binderVal :: b }

815 binderVal :: b }

@@ -827,7 +828,7 @@ instance Sized a => Sized (Binder a) where

827 size (Let ty val) = 1 + size ty + size val

828 size (Let ty val) = 1 + size ty + size val

828 size (NLet ty val) = 1 + size ty + size val

829 size (NLet ty val) = 1 + size ty + size val

829 size (Hole ty) = 1 + size ty

830 size (Hole ty) = 1 + size ty

830− size (GHole _ ty) = 1 + size ty

831+ size (GHole _ _ ty) = 1 + size ty

831 size (Guess ty val) = 1 + size ty + size val

832 size (Guess ty val) = 1 + size ty + size val

832 size (PVar ty) = 1 + size ty

833 size (PVar ty) = 1 + size ty

833 size (PVTy ty) = 1 + size ty

834 size (PVTy ty) = 1 + size ty

@@ -839,7 +840,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

839fmapMB f (Lam t) = liftM Lam (f t)

840fmapMB f (Lam t) = liftM Lam (f t)

840fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

841fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

841fmapMB f (Hole t) = liftM Hole (f t)

842fmapMB 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)

843fmapMB f (PVar t) = liftM PVar (f t)

844fmapMB f (PVar t) = liftM PVar (f t)

844fmapMB f (PVTy t) = liftM PVTy (f t)

845fmapMB f (PVTy t) = liftM PVTy (f t)

845

846

@@ -1494,7 +1495,7 @@ prettyEnv env t = prettyEnv' env t False

1494 -- Render a `Binder` and its name

1495 -- Render a `Binder` and its name

1495 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1496 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1496 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1497 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

1498 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t

1499 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t

1499 prettySb env n (PVar t) = prettyB env "pat" "." n t

1500 prettySb env n (PVar t) = prettyB env "pat" "." n t

1500 prettySb env n (PVTy t) = prettyB env "pty" "." n t

1501 prettySb env n (PVTy t) = prettyB env "pty" "." n t

@@ -1539,7 +1540,7 @@ showEnv' env t dbg = se 10 env t where

1539

1540

1540 sb env n (Lam t) = showb env "\\ " " => " n t

1541 sb env n (Lam t) = showb env "\\ " " => " n t

1541 sb env n (Hole t) = showb env "? " ". " n t

1542 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

1543 sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

1544 sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

1544 sb env n (Pi _ t _) = showb env "(" ") -> " n t

1545 sb env n (Pi _ t _) = showb env "(" ") -> " n t

1545 sb env n (PVar t) = showb env "pat " ". " n t

1546 sb env n (PVar t) = showb env "pat " ". " n t

@@ -1739,7 +1740,7 @@ pprintTT bound tm = pp startPrec bound tm

1739 ppb p bound n (Hole ty) sc =

1740 ppb p bound n (Hole ty) sc =

1740 bracket p startPrec . group . align . hang 2 $

1741 bracket p startPrec . group . align . hang 2 $

1741 text "?" <+> bindingOf n False <+> text "." <> line <> sc

1742 text "?" <+> bindingOf n False <+> text "." <> line <> sc

1742− ppb p bound n (GHole _ ty) sc =

1743+ ppb p bound n (GHole _ _ ty) sc =

1743 bracket p startPrec . group . align . hang 2 $

1744 bracket p startPrec . group . align . hang 2 $

1744 text "¿" <+> bindingOf n False <+> text "." <> line <> sc

1745 text "¿" <+> bindingOf n False <+> text "." <> line <> sc

1745 ppb p bound n (Guess ty val) sc =

1746 ppb p bound n (Guess ty val) sc =

@@ -1791,8 +1792,8 @@ pprintRaw bound (RBind n b body) =

1791 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

1792 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

1792 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

1793 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

1793 text "Hole" <$> pprintRaw bound ty

1794 text "Hole" <$> pprintRaw bound ty

1794− ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $

1795+ ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $

1795− text "GHole" <$> pprintRaw bound ty

1796+ text "GHole" <$> pprintRaw bound ty

1796 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1797 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1797 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1798 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1798 ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

1799 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

232 let tt' = normalise ctxt env tt

233 lift $ isType ctxt env tt'

234 return (Hole tv, tt')

235− checkBinder (GHole i t)

235+ checkBinder (GHole i ns t)

236 = do (tv, tt) <- chk u env t

237 let tv' = normalise ctxt env tv

238 let tt' = normalise ctxt env tt

239 lift $ isType ctxt env tt'

240− return (GHole i tv, tt')

240+ return (GHole i ns tv, tt')

241 checkBinder (Guess t v)

242 | not holes = lift $ tfail (IncompleteTerm undefined)

243 | otherwise

@@ -273,8 +273,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

273 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)

274 discharge n (Hole t) bt scv sct

275 = return (Bind n (Hole t) scv, sct)

276− discharge n (GHole i t) bt scv sct

276+ discharge n (GHole i ns t) bt scv sct

277− = return (Bind n (GHole i t) scv, sct)

277+ = return (Bind n (GHole i ns t) scv, sct)

278 discharge n (Guess t v) bt scv sct

279 = return (Bind n (Guess t v) scv, sct)

280 discharge n (PVar t) bt scv sct

src/Idris/DeepSeq.hs+2−2

@@ -295,8 +295,8 @@ instance (NFData t) => NFData (PTactic' t) where

295 rnf Compute = ()

296 rnf Trivial = ()

297 rnf TCInstance = ()

298− rnf (ProofSearch r r1 r2 x1 x2)

298+ rnf (ProofSearch r r1 r2 x1 x2 x3)

299− = rnf x1 `seq` rnf x2 `seq` ()

299+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

300 rnf Solve = ()

301 rnf Attack = ()

302 rnf ProofState = ()

src/Idris/Delaborate.hs+2−2

@@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

106 | Just n' <- lookup n env = PRef un [] n'

107 | otherwise

108 = case lookup n (idris_metavars ist) of

109− Just (Just _, mi, _) -> mkMVApp n []

109+ Just (Just _, mi, _, _) -> mkMVApp n []

110 _ -> PRef un [] n

111 de env _ (Bind n (Lam ty) sc)

112 = 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

169 = PApp un (de env [] f) (map pexp (map (de env []) args))

170 deFn env (P _ n _) args

171 | not mvs = case lookup n (idris_metavars ist) of

172− Just (Just _, mi, _) ->

172+ Just (Just _, mi, _, _) ->

173 mkMVApp n (drop mi (map (de env []) args))

174 _ -> mkPApp n (map (de env []) args)

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

543 let fn_is = case lookupCtxt fname (idris_implicits i) of

544 [t] -> t

545 _ -> []

546− let params = getParamsInType i [] fn_is fn_ty

546+ let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

547 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

548 propagateParams i params fn_ty (addImplPat i lhs_in)

549-- let lhs = mkLHSapp $

@@ -632,6 +632,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

632 ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-

633 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

634 (do pbinds ist lhs_tm

635+ -- proof search can use explicitly written names

636+ mapM_ addPSname (allNamesIn lhs_in)

635 mapM_ setinj (nub (params ++ inj))

637 mapM_ setinj (nub (params ++ inj))

636 setNextName

638 setNextName

637 (ElabResult _ _ is ctxt' newDecls highlights) <-

639 (ElabResult _ _ is ctxt' newDecls highlights) <-

@@ -656,9 +658,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

656 logLvl 5 "DONE CHECK"

658 logLvl 5 "DONE CHECK"

657 logLvl 4 $ "---> " ++ show rhs'

659 logLvl 4 $ "---> " ++ show rhs'

658 when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

660 when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

659− show (map (\ (n, (_,_,t)) -> (n, t)) defer)

661+ show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

660 def' <- checkDef fc (Elaborating "deferred type of ") defer

662 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'

662 addDeferred def''

664 addDeferred def''

663 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

665 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

664

666

@@ -790,7 +792,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

790 let fn_is = case lookupCtxt fname (idris_implicits i) of

792 let fn_is = case lookupCtxt fname (idris_implicits i) of

791 [t] -> t

793 [t] -> t

792 _ -> []

794 _ -> []

793− let params = getParamsInType i [] fn_is fn_ty

795+ let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

794 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

796 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

795 logLvl 2 ("LHS: " ++ show lhs)

797 logLvl 2 ("LHS: " ++ show lhs)

796 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

798 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

@@ -816,6 +818,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

816 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

818 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

817 (bindTyArgs PVTy bargs infP) initEState

819 (bindTyArgs PVTy bargs infP) initEState

818 (do pbinds i lhs_tm

820 (do pbinds i lhs_tm

821+ -- proof search can use explicitly written names

822+ mapM_ addPSname (allNamesIn lhs_in)

819 setNextName

823 setNextName

820 -- TODO: may want where here - see winfo abpve

824 -- TODO: may want where here - see winfo abpve

821 (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname

825 (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)

828 sendHighlighting highlights

832 sendHighlighting highlights

829

833

830 def' <- checkDef fc iderr defer

834 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'

832 addDeferred def''

836 addDeferred def''

833 mapM_ (elabCaseBlock info opts) is

837 mapM_ (elabCaseBlock info opts) is

834 logLvl 5 ("Checked wval " ++ show wval')

838 logLvl 5 ("Checked wval " ++ show wval')

@@ -890,8 +894,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

890 addIBC (IBCImp wname)

894 addIBC (IBCImp wname)

891 addIBC (IBCStatic wname)

895 addIBC (IBCStatic wname)

892

896

893− def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]

897+ def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]

894− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

898+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

895 addDeferred def''

899 addDeferred def''

896

900

897 -- in the subdecls, lhs becomes:

901 -- in the subdecls, lhs becomes:

@@ -932,7 +936,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

932 sendHighlighting highlights

936 sendHighlighting highlights

933

937

934 def' <- checkDef fc iderr defer

938 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'

936 addDeferred def''

940 addDeferred def''

937 mapM_ (elabCaseBlock info opts) is

941 mapM_ (elabCaseBlock info opts) is

938 logLvl 5 ("Checked RHS " ++ show rhs')

942 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

71 let constraint = PApp fc (PRef fc [] n) (map pexp ps)

72 let iname = mkiname n (namespace info) ps expn

73 let emptyclass = null (class_methods ci)

74− when (what /= EDefns || (null ds && not emptyclass)) $ do

74+ when (what /= EDefns) $ do

75 nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

76 -- if the instance type matches any of the instances we have already,

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

34

35-- | Elaborate a record declaration

36elabRecord :: ElabInfo

37+ -> ElabWhat

37 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

38 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

38 -> SyntaxInfo -> FC -> DataOpts

39 -> SyntaxInfo -> FC -> DataOpts

39 -> Name -- ^ The name of the type being defined

40 -> Name -- ^ The name of the type being defined

@@ -45,7 +46,7 @@ elabRecord :: ElabInfo

45 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

46 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

46 -> SyntaxInfo -- ^ Constructor SyntaxInfo

47 -> SyntaxInfo -- ^ Constructor SyntaxInfo

47 -> Idris ()

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

49 = do logLvl 1 $ "Building data declaration for " ++ show tyn

50 = do logLvl 1 $ "Building data declaration for " ++ show tyn

50 -- Type constructor

51 -- Type constructor

51 let tycon = generateTyConType params

52 let tycon = generateTyConType params

@@ -58,17 +59,20 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

58

59

59 -- Build data declaration for elaboration

60 -- Build data declaration for elaboration

60 logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

61 logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

62+ let datadecl = case what of

63+ ETypes -> PLaterdecl tyn NoFC tycon

61− let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

64+ _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

62 elabData info rsyn doc paramDocs fc opts datadecl

65 elabData info rsyn doc paramDocs fc opts datadecl

63

66

67+ when (what /= ETypes) $ do

64− logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

68+ logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

65− logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

69+ logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

66− elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

70+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

67

71

68− sendHighlighting $

72+ sendHighlighting $

69− [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

73+ [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

70− maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

74+ maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

71− [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

75+ [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

72

76

73 where

77 where

74 -- | Generates a type constructor.

78 -- | Generates a type constructor.

src/Idris/Elab/Term.hs+25−28

@@ -42,7 +42,7 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

42

43data ElabResult =

44 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

45− , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

45+ , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

46 -- ^ Information about new metavariables

47 , resultCaseDecls :: [PDecl]

48 -- ^ Deferred declarations as the meaning of case blocks

@@ -628,6 +628,7 @@ elab ist info emode opts fn tm

628 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")

629 checkPiGoal n

630 attack; intro (Just n);

631+ addPSname n -- okay for proof search

631 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

632 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

632 elabE (ina { e_inarg = True } ) (Just fc) sc; solve

633 elabE (ina { e_inarg = True } ) (Just fc) sc; solve

633 highlightSource nfc (AnnBoundName n False)

634 highlightSource nfc (AnnBoundName n False)

@@ -644,6 +645,7 @@ elab ist info emode opts fn tm

644 ptm <- get_term

645 ptm <- get_term

645 hs <- get_holes

646 hs <- get_holes

646 introTy (Var tyn) (Just n)

647 introTy (Var tyn) (Just n)

648+ addPSname n -- okay for proof search

647 focus tyn

649 focus tyn

648

650

649 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

651 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

@@ -652,6 +654,7 @@ elab ist info emode opts fn tm

652 highlightSource nfc (AnnBoundName n False)

654 highlightSource nfc (AnnBoundName n False)

653 elab' ina fc (PPi p n nfc Placeholder sc)

655 elab' ina fc (PPi p n nfc Placeholder sc)

654 = do attack; arg n (is_scoped p) (sMN 0 "ty")

656 = do attack; arg n (is_scoped p) (sMN 0 "ty")

657+ addPSname n -- okay for proof search

655 elabE (ina { e_inarg = True, e_intype = True }) fc sc

658 elabE (ina { e_inarg = True, e_intype = True }) fc sc

656 solve

659 solve

657 highlightSource nfc (AnnBoundName n False)

660 highlightSource nfc (AnnBoundName n False)

@@ -662,6 +665,7 @@ elab ist info emode opts fn tm

662 MN _ _ -> unique_hole n

665 MN _ _ -> unique_hole n

663 _ -> return n

666 _ -> return n

664 forall n' (is_scoped p) (Var tyn)

667 forall n' (is_scoped p) (Var tyn)

668+ addPSname n' -- okay for proof search

665 focus tyn

669 focus tyn

666 let ec' = ina { e_inarg = True, e_intype = True }

670 let ec' = ina { e_inarg = True, e_intype = True }

667 elabE ec' fc ty

671 elabE ec' fc ty

@@ -677,6 +681,7 @@ elab ist info emode opts fn tm

677 claim valn (Var tyn)

681 claim valn (Var tyn)

678 explicit valn

682 explicit valn

679 letbind n (Var tyn) (Var valn)

683 letbind n (Var tyn) (Var valn)

684+ addPSname n

680 case ty of

685 case ty of

681 Placeholder -> return ()

686 Placeholder -> return ()

682 _ -> do focus tyn

687 _ -> do focus tyn

@@ -902,7 +907,7 @@ elab ist info emode opts fn tm

902 case lookup n env of

907 case lookup n env of

903 Nothing -> return ()

908 Nothing -> return ()

904 Just b ->

909 Just b ->

905− case unApply (binderTy b) of

910+ case unApply (normalise (tt_ctxt ist) env (binderTy b)) of

906 (P _ c _, args) ->

911 (P _ c _, args) ->

907 case lookupCtxtExact c (idris_classes ist) of

912 case lookupCtxtExact c (idris_classes ist) of

908 Nothing -> return ()

913 Nothing -> return ()

@@ -962,6 +967,7 @@ elab ist info emode opts fn tm

962 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

967 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

963 let n' = metavarName (namespace info) n

968 let n' = metavarName (namespace info) n

964 attack

969 attack

970+ psns <- getPSnames

965 defer unique_used n'

971 defer unique_used n'

966 solve

972 solve

967 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

973 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

@@ -1621,7 +1627,7 @@ solveAuto ist fn ambigok n

1621 g <- goal

1627 g <- goal

1622 isg <- is_guess -- if it's a guess, we're working on it recursively, so stop

1628 isg <- is_guess -- if it's a guess, we're working on it recursively, so stop

1623 when (not isg) $

1629 when (not isg) $

1624− proofSearch' ist True ambigok 100 True Nothing fn []

1630+ proofSearch' ist True ambigok 100 True Nothing fn [] []

1625

1631

1626solveAutos :: IState -> Name -> Bool -> ElabD ()

1632solveAutos :: IState -> Name -> Bool -> ElabD ()

1627solveAutos ist fn ambigok

1633solveAutos ist fn ambigok

@@ -1630,12 +1636,12 @@ solveAutos ist fn ambigok

1630

1636

1631trivial' ist

1637trivial' ist

1632 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1638 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1633−trivialHoles' h ist

1639+trivialHoles' psn h ist

1634− = trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1640+ = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1635−proofSearch' ist rec ambigok depth prv top n hints

1641+proofSearch' ist rec ambigok depth prv top n psns hints

1636 = do unifyProblems

1642 = do unifyProblems

1637 proofSearch rec prv ambigok (not prv) depth

1643 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

1639

1645

1640-- | Resolve type classes. This will only pick up 'normal' instances, never

1646-- | Resolve type classes. This will only pick up 'normal' instances, never

1641-- named instances (which is enforced by 'findInstances').

1647-- named instances (which is enforced by 'findInstances').

@@ -1675,7 +1681,7 @@ resTC' tcs defaultOn topholes depth topg fn ist

1675 _ -> []

1681 _ -> []

1676

1682

1677 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1683 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1678− try' (trivialHoles' okholes ist)

1684+ try' (trivialHoles' [] okholes ist)

1679 (do addDefault t tc ttypes

1685 (do addDefault t tc ttypes

1680 let stk = map fst (filter snd $ elab_stack ist)

1686 let stk = map fst (filter snd $ elab_stack ist)

1681 let insts = findInstances ist t

1687 let insts = findInstances ist t

@@ -1800,11 +1806,11 @@ resTC' tcs defaultOn topholes depth topg fn ist

1800 isImp arg = (False, priority arg)

1806 isImp arg = (False, priority arg)

1801

1807

1802collectDeferred :: Maybe Name -> [Name] -> Context ->

1808collectDeferred :: Maybe Name -> [Name] -> Context ->

1803− Term -> State [(Name, (Int, Maybe Name, Type))] Term

1809+ Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

1804−collectDeferred top casenames ctxt (Bind n (GHole i t) app) =

1810+collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =

1805 do ds <- get

1811 do ds <- get

1806 t' <- collectDeferred top casenames ctxt t

1812 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))])

1808 collectDeferred top casenames ctxt app

1814 collectDeferred top casenames ctxt app

1809 where

1815 where

1810 -- Evaluate the top level functions in arguments, if possible, and if it's

1816 -- 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) =

1814 tidyArg env (Bind n b@(Pi im t k) sc)

1820 tidyArg env (Bind n b@(Pi im t k) sc)

1815 = Bind n (Pi im (tidy ctxt env t) k)

1821 = Bind n (Pi im (tidy ctxt env t) k)

1816 (tidyArg ((n, b) : env) sc)

1822 (tidyArg ((n, b) : env) sc)

1817− tidyArg env t = t

1823+ tidyArg env t = tidy ctxt env t

1818−

1824+

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)

1825+ tidy ctxt env t = normalise ctxt env t

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

1829

1826

1830 getFn (Bind n (Lam _) t) = getFn t

1827 getFn (Bind n (Lam _) t) = getFn t

1831 getFn t | (f, a) <- unApply t = f

1828 getFn t | (f, a) <- unApply t = f

@@ -2138,7 +2135,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2138 do actualHints <- mapM reifyTTName hs

2135 do actualHints <- mapM reifyTTName hs

2139 unifyProblems

2136 unifyProblems

2140 let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")

2137 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

2142 returnUnit

2139 returnUnit

2143 (Constant (I _), Nothing ) ->

2140 (Constant (I _), Nothing ) ->

2144 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

2141 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

@@ -2310,8 +2307,8 @@ runTac autoSolve ist perhapsFC fn tac

2310 runT Compute = compute

2307 runT Compute = compute

2311 runT Trivial = do trivial' ist; when autoSolve solveAll

2308 runT Trivial = do trivial' ist; when autoSolve solveAll

2312 runT TCInstance = runT (Exact (PResolveTC emptyFC))

2309 runT TCInstance = runT (Exact (PResolveTC emptyFC))

2313− runT (ProofSearch rec prover depth top hints)

2310+ runT (ProofSearch rec prover depth top psns hints)

2314− = do proofSearch' ist rec False depth prover top fn hints

2311+ = do proofSearch' ist rec False depth prover top fn psns hints

2315 when autoSolve solveAll

2312 when autoSolve solveAll

2316 runT (Focus n) = focus n

2313 runT (Focus n) = focus n

2317 runT Unfocus = do hs <- get_holes

2314 runT Unfocus = do hs <- get_holes

@@ -2519,7 +2516,7 @@ processTacticDecls info steps =

2519 updateIState $ \i -> i { idris_implicits =

2516 updateIState $ \i -> i { idris_implicits =

2520 addDef n impls (idris_implicits i) }

2517 addDef n impls (idris_implicits i) }

2521 addIBC (IBCImp n)

2518 addIBC (IBCImp n)

2522− ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]

2519+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))]

2523 addIBC (IBCDef n)

2520 addIBC (IBCDef n)

2524 ctxt <- getContext

2521 ctxt <- getContext

2525 case lookupDef n ctxt of

2522 case lookupDef n ctxt of

@@ -2528,7 +2525,7 @@ processTacticDecls info steps =

2528 -- then it must be added as a metavariable. This needs guarding

2525 -- then it must be added as a metavariable. This needs guarding

2529 -- to prevent overwriting case defs with a metavar, if the case

2526 -- to prevent overwriting case defs with a metavar, if the case

2530 -- defs come after the type decl in the same script!

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

2532 in addDeferred ds'

2529 in addDeferred ds'

2533 _ -> return ()

2530 _ -> return ()

2534 RAddInstance className instName ->

2531 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

159 -- Productivity checking now via checking for guarded 'Delay'

160 let opts' = opts -- if corec then (Coinductive : opts) else opts

161 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, []))]

163 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

165 addDeferred ds'

166 setFlags n opts'

167 checkDocs fc argDocs ty

src/Idris/Elab/Utils.hs+9−8

@@ -40,21 +40,21 @@ recheckC_borrowing uniq_check bs fc mkerr env t

40iderr :: Name -> Err -> Err

41iderr _ e = e

42

43−checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]

43+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))]

44− -> Idris [(Name, (Int, Maybe Name, Type))]

44+ -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

45checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

46

47checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

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

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

49− -> Idris [(Name, (Int, Maybe Name, Type))]

49+ -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

50checkAddDef 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)

52 = do ctxt <- getContext

53 (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))]

55 addIBC (IBCDef n)

56 ns' <- checkAddDef add toplvl fc mkerr ns

57− return ((n, (i, top, t')) : ns')

57+ return ((n, (i, top, t', psns)) : ns')

58

59-- | Get the list of (index, name) of inaccessible arguments from an elaborated

60-- type

@@ -137,7 +137,8 @@ decorateid decorate (PClauses f o n cs)

137pbinds :: IState -> Term -> ElabD ()

138pbinds i (Bind n (PVar t) sc)

139 = do attack; patbind n

140+ env <- get_env

140− case unApply t of

141+ case unApply (normalise (tt_ctxt i) env t) of

141 (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

142 (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

142 [] -> return ()

143 [] -> return ()

143 _ -> -- type class, set as injective

144 _ -> -- type class, set as injective

src/Idris/Elab/Value.hs+1−1

@@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in

76 let vtm = orderPats (getInferTerm tm')

77

78 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'

80 addDeferred def''

81 mapM_ (elabCaseBlock info []) is

82

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)

245 = do logLvl 1 $ "Elaborating instance " ++ show n

246 elabInstance info s doc argDocs what f cs n nfc ps t expn ds

247elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

248− | what /= ETypes

249 = do logLvl 1 $ "Elaborating record " ++ show name

248 = 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

251{-

250{-

252 | otherwise

251 | otherwise

253 = do logLvl 1 $ "Elaborating [type of] " ++ show tyn

252 = do logLvl 1 $ "Elaborating [type of] " ++ show tyn

src/Idris/IBC.hs+13−11

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 116

43+ibcVersion = 117

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -78,7 +78,7 @@ data IBCFile = IBCFile { ver :: Word16,

78 ibc_metainformation :: ![(Name, MetaInformation)],

79 ibc_errorhandlers :: ![Name],

80 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))],

82 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

83 ibc_postulates :: ![Name],

84 ibc_externs :: ![(Name, Int)],

@@ -365,7 +365,7 @@ timestampOlder :: FilePath -> FilePath -> Idris ()

365timestampOlder src ibc = do srct <- runIO $ getModificationTime src

366 ibct <- runIO $ getModificationTime ibc

367 if (srct > ibct)

368− then ifail "Needs reloading"

368+ then ifail $ "Needs reloading " ++ show (srct, ibct)

369 else return ()

370

371pPostulates :: [Name] -> Idris ()

@@ -610,7 +610,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

610pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->

611 addFunctionErrorHandlers fn arg [handler]) ns

612

613−pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

613+pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris ()

614pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

615

616----- For Cheapskate and docstrings

@@ -1869,12 +1869,13 @@ instance (Binary t) => Binary (PTactic' t) where

1869 put x1

1870 ByReflection x1 -> do putWord8 20

1871 put x1

1872− ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21

1872+ ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21

1873− put x1

1873+ put x1

1874− put x2

1874+ put x2

1875− put x3

1875+ put x3

1876− put x4

1876+ put x4

1877− put x5

1877+ put x5

1878+ put x6

1878 DoUnify -> putWord8 22

1879 DoUnify -> putWord8 22

1879 CaseTac x1 -> do putWord8 23

1880 CaseTac x1 -> do putWord8 23

1880 put x1

1881 put x1

@@ -1954,7 +1955,8 @@ instance (Binary t) => Binary (PTactic' t) where

1954 x3 <- get

1955 x3 <- get

1955 x4 <- get

1956 x4 <- get

1956 x5 <- get

1957 x5 <- get

1958+ x6 <- get

1957− return (ProofSearch x1 x2 x3 x4 x5)

1959+ return (ProofSearch x1 x2 x3 x4 x5 x6)

1958 22 -> return DoUnify

1960 22 -> return DoUnify

1959 23 -> do x1 <- get

1961 23 -> do x1 <- get

1960 return (CaseTac x1)

1962 return (CaseTac x1)

src/Idris/IdeMode.hs+2

@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String

229 | AddProofClause Int String

230 | AddMissing Int String

231 | MakeWithBlock Int String

232+ | MakeCaseBlock Int String

232 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

233 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

233 | MakeLemma Int String

234 | MakeLemma Int String

234 | LoadFile String (Maybe Int)

235 | LoadFile String (Maybe Int)

@@ -261,6 +262,7 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n

261sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

262sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

262sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

263sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

263sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

264sexpToCommand (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)

264-- The Boolean in ProofSearch means "search recursively"

266-- The Boolean in ProofSearch means "search recursively"

265-- If it's False, that means "refine", i.e. apply the name and fill in any

267-- If it's False, that means "refine", i.e. apply the name and fill in any

266-- arguments which can be done by unification.

268-- arguments which can be done by unification.

src/Idris/IdrisDoc.hs+2−2

@@ -360,8 +360,8 @@ extractPTactic (MatchRefine n) = [n]

360extractPTactic (LetTac n p) = n : extract p

361extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]

362extractPTactic (Exact p) = extract p

363−extractPTactic (ProofSearch _ _ _ m ns) | Just n <- m = n : ns

363+extractPTactic (ProofSearch _ _ _ m _ ns) | Just n <- m = n : ns

364−extractPTactic (ProofSearch _ _ _ _ ns) = ns

364+extractPTactic (ProofSearch _ _ _ _ _ ns) = ns

365extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2]

366extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2]

367extractPTactic (ApplyTactic p) = extract p

src/Idris/Interactive.hs+97−14

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

1{-# LANGUAGE PatternGuards #-}

2

3module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,

4− addMissing, makeWith, doProofSearch,

4+ addMissing, makeWith, makeCase, doProofSearch,

5 makeLemma) where

6

7{- Bits and pieces for editing source files interactively, called from

@@ -158,6 +158,47 @@ makeWith fn updatefile l n

158 else iPrintResult with

159 where getIndent s = length (takeWhile isSpace s)

160

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+

161

202

162doProofSearch :: FilePath -> Bool -> Bool ->

203doProofSearch :: FilePath -> Bool -> Bool ->

163 Int -> Name -> [Name] -> Maybe Int -> Idris ()

204 Int -> Name -> [Name] -> Maybe Int -> Idris ()

@@ -172,12 +213,13 @@ doProofSearch fn updatefile rec l n hints (Just depth)

172 [] -> return n

213 [] -> return n

173 ns -> ierror (CantResolveAlts ns)

214 ns -> ierror (CantResolveAlts ns)

174 i <- getIState

215 i <- getIState

216+ let (top, envlen, psnames, _)

175− let (top, envlen, _) = case lookup mn (idris_metavars i) of

217+ = case lookup mn (idris_metavars i) of

176− Just (t, e, False) -> (t, e, False)

218+ Just (t, e, ns, False) -> (t, e, ns, False)

177− _ -> (Nothing, 0, True)

219+ _ -> (Nothing, 0, [], True)

178 let fc = fileFC fn

220 let fc = fileFC fn

179− let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

221+ let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))

180− (ProofSearch rec False depth t hints)]

222+ (ProofSearch rec False depth t psnames hints)]

181 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

223 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

182 newmv <- idrisCatch

224 newmv <- idrisCatch

183 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

225 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

@@ -256,13 +298,17 @@ makeLemma fn updatefile l n

256 ns -> ierror (CantResolveAlts (map fst ns))

298 ns -> ierror (CantResolveAlts (map fst ns))

257 i <- getIState

299 i <- getIState

258 margs <- case lookup n (idris_metavars i) of

300 margs <- case lookup n (idris_metavars i) of

259− Just (_, arity, _) -> return arity

301+ Just (_, arity, _, _) -> return arity

260 _ -> return (-1)

302 _ -> return (-1)

261

303

262 if (not isProv) then do

304 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

264

307

308+ let lem = show n ++ " : " ++

309+ constraints i classes mty ++

310+ showTmOpts (defaultPPOption { ppopt_pinames = True })

265− let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))

311+ (stripMNBind skip (delab i mty))

266 let lem_app = show n ++ appArgs skip margs mty

312 let lem_app = show n ++ appArgs skip margs mty

267

313

268 if updatefile then

314 if updatefile then

@@ -312,15 +358,52 @@ makeLemma fn updatefile l n

312 stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

358 stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

313 stripMNBind skip t = t

359 stripMNBind skip t = t

314

360

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+

315 -- Guess which binders should be implicits in the generated lemma.

372 -- Guess which binders should be implicits in the generated lemma.

316 -- Make them implicit if they appear guarded by a top level constructor,

373 -- Make them implicit if they appear guarded by a top level constructor,

317 -- or at the top level themselves.

374 -- or at the top level themselves.

375+ -- Also, make type class instances implicit

318− guessImps :: Context -> Term -> [Name]

376+ guessImps :: IState -> Context -> Term -> [Name]

319− guessImps ctxt (Bind n (Pi _ _ _) sc)

377+ guessImps ist ctxt (Bind n (Pi _ ty _) sc)

320 | guarded ctxt n (substV (P Bound n Erased) sc)

378 | guarded ctxt n (substV (P Bound n Erased) sc)

321− = n : guessImps ctxt sc

379+ = n : guessImps ist ctxt sc

380+ | isClass ist ty

381+ = n : guessImps ist ctxt sc

322− | otherwise = guessImps ctxt sc

382+ | otherwise = guessImps ist ctxt sc

323− guessImps ctxt _ = []

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

324

407

325 guarded ctxt n (P _ n' _) | n == n' = True

408 guarded ctxt n (P _ n' _) | n == n' = True

326 guarded ctxt n ap@(App _ _ _)

409 guarded ctxt n ap@(App _ _ _)

src/Idris/ParseData.hs+18−17

@@ -86,25 +86,26 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

86

87 let constructorDoc' = annotate syn ist constructorDoc

88

89− fields <- many . indented $ field syn

89+ fields <- many . indented $ fieldLine syn

90

91− return (fields, constructorName, constructorDoc')

91+ return (concat fields, constructorName, constructorDoc')

92 where

93− field :: SyntaxInfo -> IdrisParser ((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

93+ fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

94+ fieldLine syn = do

94− field syn = do doc <- optional docComment

95+ doc <- optional docComment

95− c <- optional $ lchar '{'

96+ c <- optional $ lchar '{'

96− n <- (do (n, nfc) <- fnName

97+ let oneName = (do (n, nfc) <- fnName

97− return $ Just (expandNS syn n, nfc))

98+ return $ Just (expandNS syn n, nfc))

98− <|> (do symbol "_"

99− return Nothing)

99+ <|> (symbol "_" >> return Nothing)

100+ ns <- commaSeparated oneName

100− lchar ':'

101+ lchar ':'

101− t <- typeExpr (allowImp syn)

102+ t <- typeExpr (allowImp syn)

102− p <- endPlicity c

103+ p <- endPlicity c

103− ist <- get

104+ ist <- get

104− let doc' = case doc of -- Temp: Throws away any possible arg docs

105+ let doc' = case doc of -- Temp: Throws away any possible arg docs

105− Just (d,_) -> Just $ annotate syn ist d

106+ Just (d,_) -> Just $ annotate syn ist d

106− Nothing -> Nothing

107+ Nothing -> Nothing

107− return (n, p, t, doc')

108+ return $ map (\n -> (n, p, t, doc')) ns

108

109

109 constructor :: IdrisParser (Name, FC)

110 constructor :: IdrisParser (Name, FC)

110 constructor = (reservedHL "constructor") *> fnName

111 constructor = (reservedHL "constructor") *> fnName

src/Idris/ParseExpr.hs+2−2

@@ -971,7 +971,7 @@ autoImplicit opts st syn

971 sc <- expr syn

972 highlightP kw AnnKeyword

973 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)

975

976defaultImplicit opts st syn = do

977 kw <- reservedFC "default"

@@ -1436,7 +1436,7 @@ tactics =

1436 , noArgs ["unify"] DoUnify

1437 , (["search"], Nothing, const $

1438 do depth <- option 10 $ fst <$> natural

1439− return (ProofSearch True True (fromInteger depth) Nothing []))

1439+ return (ProofSearch True True (fromInteger depth) Nothing [] []))

1440 , noArgs ["instance"] TCInstance

1441 , noArgs ["solve"] Solve

1442 , noArgs ["attack"] Attack

src/Idris/ParseHelpers.hs+5

@@ -434,6 +434,11 @@ bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PT

434bindList b [] sc = sc

435bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)

436

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+

437{- * Layout helpers -}

442{- * Layout helpers -}

438

443

439-- | Push indentation to stack

444-- | Push indentation to stack

src/Idris/ProofSearch.hs+34−16

@@ -22,10 +22,10 @@ import Debug.Trace

22-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

23

24trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25−trivial = trivialHoles []

25+trivial = trivialHoles [] []

26

27−trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

27+trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28−trivialHoles ok elab ist

28+trivialHoles psnames ok elab ist

29 = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

30 return ())

31 (do env <- get_env

@@ -41,7 +41,7 @@ trivialHoles ok elab ist

41 g <- goal

42 -- anywhere but the top is okay for a hole, if holesOK set

43 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)

45 then try' (elab (PRef (fileFC "prf") [] x))

46 (tryAll xs) True

47 else tryAll xs

@@ -73,9 +73,11 @@ proofSearch :: Bool -> -- recursive search (False for 'refine')

73 Bool -> -- ambiguity ok

74 Bool -> -- defer on failure

75 Int -> -- maximum depth

76− (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

76+ (PTerm -> ElabD ()) -> Maybe Name -> Name ->

77+ [Name] ->

78+ [Name] ->

77 IState -> ElabD ()

79 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

79 = do -- get all possible versions of the name, take the first one that

81 = do -- get all possible versions of the name, take the first one that

80 -- works

82 -- works

81 let all_imps = lookupCtxtName fn (idris_implicits ist)

83 let all_imps = lookupCtxtName fn (idris_implicits ist)

@@ -106,7 +108,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

106

108

107 isImp (PImp p _ _ _ _) = (True, p)

109 isImp (PImp p _ _ _ _) = (True, p)

108 isImp arg = (True, priority arg) -- try to get all of them by unification

110 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

110 = do compute

112 = do compute

111 ty <- goal

113 ty <- goal

112 hs <- get_holes

114 hs <- get_holes

@@ -177,7 +179,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

177 ty <- goal

179 ty <- goal

178 when (S.member ty tys) $ fail "Been here before"

180 when (S.member ty tys) $ fail "Been here before"

179 let tys' = S.insert ty tys

181 let tys' = S.insert ty tys

180− try' (trivial elab ist)

182+ try' (trivialHoles psnames [] elab ist)

181 (try' (try' (resolveByCon (d - 1) locs tys')

183 (try' (try' (resolveByCon (d - 1) locs tys')

182 (resolveByLocals (d - 1) locs tys')

184 (resolveByLocals (d - 1) locs tys')

183 True)

185 True)

@@ -199,11 +201,13 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

199 Nothing -> []

201 Nothing -> []

200 Just hs -> hs

202 Just hs -> hs

201 case lookupCtxtExact n (idris_datatypes ist) of

203 case lookupCtxtExact n (idris_datatypes ist) of

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

202− Just t -> tryCons d locs tys

210+ tryCons d locs tys (others ++ getFn d fn)

203− (hints ++

204− con_names t ++

205− autohints ++

206− getFn d fn)

207 Nothing -> fail "Not a data type"

211 Nothing -> fail "Not a data type"

208 _ -> fail "Not a data type"

212 _ -> fail "Not a data type"

209

213

@@ -215,7 +219,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

215

219

216 tryLocals d locs tys [] = fail "Locals failed"

220 tryLocals d locs tys [] = fail "Locals failed"

217 tryLocals d locs tys ((x, t) : xs)

221 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

219 | otherwise = try' (tryLocal d (x : locs) tys x t)

223 | otherwise = try' (tryLocal d (x : locs) tys x t)

220 (tryLocals d locs tys xs) True

224 (tryLocals d locs tys xs) True

221

225

@@ -245,12 +249,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

245 ps' <- get_probs

249 ps' <- get_probs

246 hs' <- get_holes

250 hs' <- get_holes

247 when (length ps < length ps') $ fail "Can't apply constructor"

251 when (length ps < length ps') $ fail "Can't apply constructor"

252+ let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)

248 mapM_ (\ (_, h) -> do focus h

253 mapM_ (\ (_, h) -> do focus h

249 aty <- goal

254 aty <- goal

250− psRec True d locs tys)

255+ psRec True d locs tys) newhs

251− (filter (\ (x, y) -> not x) (zip (map fst imps) args))

252 solve

256 solve

253

257

254 isImp (PImp p _ _ _ _) = (True, p)

258 isImp (PImp p _ _ _ _) = (True, p)

255 isImp arg = (False, priority arg)

259 isImp arg = (False, priority arg)

256

260

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) =

366 process fn (AddMissing False line (sUN name))

367runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =

368 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))

369runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =

371runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =

370 doProofSearch fn False r line (sUN name) (map sUN hints) depth

372 doProofSearch fn False r line (sUN name) (map sUN hints) depth

371runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =

373runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =

@@ -632,6 +634,7 @@ idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClaus

632idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

634idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

633idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

635idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

634idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

636idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

637+idemodeProcess fn (MakeCase False pos str) = process fn (MakeCase False pos str)

635idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

638idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

636idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

639idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

637 iPrintResult ""

640 iPrintResult ""

@@ -901,8 +904,8 @@ process fn (Check (PRef _ _ n))

901 case lookupNames n ctxt of

904 case lookupNames n ctxt of

902 ts@(t:_) ->

905 ts@(t:_) ->

903 case lookup t (idris_metavars ist) of

906 case lookup t (idris_metavars ist) of

904− Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

907+ Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

905− showMetavarInfo ppo ist n i

908+ showMetavarInfo ppo ist n i

906 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

909 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

907 [] -> iPrintError $ "No such variable " ++ show n

910 [] -> iPrintError $ "No such variable " ++ show n

908 where

911 where

@@ -934,12 +937,14 @@ process fn (Check t)

934 ctxt <- getContext

937 ctxt <- getContext

935 ist <- getIState

938 ist <- getIState

936 let ppo = ppOptionIst ist

939 let ppo = ppOptionIst ist

940+ ty' = if opt_evaltypes (idris_options ist)

937− ty' = normaliseC ctxt [] ty

941+ then normaliseC ctxt [] ty

942+ else ty

938 case tm of

943 case tm of

939 TType _ ->

944 TType _ ->

940 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

945 iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

941 _ -> iPrintTermWithType (pprintDelab ist tm)

946 _ -> iPrintTermWithType (pprintDelab ist tm)

942− (pprintDelab ist ty)

947+ (pprintDelab ist ty')

943

948

944process fn (Core t)

949process fn (Core t)

945 = do (tm, ty) <- elabREPL recinfo ERHS t

950 = do (tm, ty) <- elabREPL recinfo ERHS t

@@ -1047,6 +1052,8 @@ process fn (AddMissing updatefile l n)

1047 = addMissing fn updatefile l n

1052 = addMissing fn updatefile l n

1048process fn (MakeWith updatefile l n)

1053process fn (MakeWith updatefile l n)

1049 = makeWith fn updatefile l n

1054 = makeWith fn updatefile l n

1055+process fn (MakeCase updatefile l n)

1056+ = makeCase fn updatefile l n

1050process fn (MakeLemma updatefile l n)

1057process fn (MakeLemma updatefile l n)

1051 = makeLemma fn updatefile l n

1058 = makeLemma fn updatefile l n

1052process fn (DoProofSearch updatefile rec l n hints)

1059process fn (DoProofSearch updatefile rec l n hints)

@@ -1072,7 +1079,7 @@ process fn (RmProof n')

1072 insertMetavar n =

1079 insertMetavar n =

1073 do i <- getIState

1080 do i <- getIState

1074 let ms = idris_metavars i

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

1076

1083

1077process fn' (AddProof prf)

1084process fn' (AddProof prf)

1078 = do fn <- do

1085 = do fn <- do

@@ -1125,8 +1132,8 @@ process fn (Prove mode n')

1125 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns

1132 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns

1126 n <- case metavars of

1133 n <- case metavars of

1127 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

1134 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

1128− [(n, (_,_,False))] -> return n

1135+ [(n, (_,_,_,False))] -> return n

1129− [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1136+ [(_, (_,_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1130 ns -> ierror (CantResolveAlts (map fst ns))

1137 ns -> ierror (CantResolveAlts (map fst ns))

1131 prover mode (lit fn) n

1138 prover mode (lit fn) n

1132 -- recheck totality

1139 -- recheck totality

@@ -1234,6 +1241,8 @@ process fn (SetOpt NoBanner) = setNoBanner True

1234process fn (UnsetOpt NoBanner) = setNoBanner False

1241process fn (UnsetOpt NoBanner) = setNoBanner False

1235process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1242process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1236process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1243process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1244+process fn (SetOpt EvalTypes) = setEvalTypes True

1245+process fn (UnsetOpt EvalTypes) = setEvalTypes False

1237

1246

1238process fn (SetOpt _) = iPrintError "Not a valid option"

1247process fn (SetOpt _) = iPrintError "Not a valid option"

1239process fn (UnsetOpt _) = iPrintError "Not a valid option"

1248process fn (UnsetOpt _) = iPrintError "Not a valid option"

src/Idris/REPLParser.hs+3

@@ -123,6 +123,8 @@ parserCommands =

123 ":am <line> <name> adds all missing pattern matches for the name on the line"

124 , proofArgCmd ["mw", "makewith"] MakeWith

125 ":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"

126 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

128 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

127 , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

129 , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

128 , (["lto", "loadto"], SeqArgs NumberArg FileArg

130 , (["lto", "loadto"], SeqArgs NumberArg FileArg

@@ -257,6 +259,7 @@ optArg cmd name = do

257 <|> do discard (P.symbol "autosolve"); return AutoSolve

259 <|> do discard (P.symbol "autosolve"); return AutoSolve

258 <|> do discard (P.symbol "nobanner") ; return NoBanner

260 <|> do discard (P.symbol "nobanner") ; return NoBanner

259 <|> do discard (P.symbol "warnreach"); return WarnReach

261 <|> do discard (P.symbol "warnreach"); return WarnReach

262+ <|> do discard (P.symbol "evaltypes"); return EvalTypes

260

263

261proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

264proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

262proofArg cmd name = do

265proofArg cmd name = do

src/Idris/Reflection.hs+5−5

@@ -82,7 +82,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)

82reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

83reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

84reifyApp _ t [Constant (I i)]

85− | t == reflm "Search" = return (ProofSearch True True i Nothing [])

85+ | t == reflm "Search" = return (ProofSearch True True i Nothing [] [])

86reifyApp _ t [x]

87 | t == reflm "Refine" = do n <- reifyTTName x

88 return $ Refine n []

@@ -313,7 +313,7 @@ reifyTTBinderApp reif f [x, y]

313reifyTTBinderApp reif f [t]

314 | f == reflm "Hole" = liftM Hole (reif t)

315reifyTTBinderApp reif f [t]

316− | f == reflm "GHole" = liftM (GHole 0) (reif t)

316+ | f == reflm "GHole" = liftM (GHole 0 []) (reif t)

317reifyTTBinderApp reif f [x, y]

318 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

319reifyTTBinderApp reif f [t]

@@ -339,7 +339,7 @@ reifyTTConstApp f (Constant c@(BI _))

339 | f == reflm "BI" = return $ c

340reifyTTConstApp f (Constant c@(Fl _))

341 | f == reflm "Fl" = return $ c

342−reifyTTConstApp f (Constant c@(I _))

342+reifyTTConstApp f (Constant c@(Ch _))

343 | f == reflm "Ch" = return $ c

344reifyTTConstApp f (Constant c@(Str _))

345 | f == reflm "Str" = return $ c

@@ -586,7 +586,7 @@ reflectBinderQuotePattern q ty unq (Hole t)

586 fill $ reflCall "Hole" [ty, Var t']

587 solve

588 focus t'; q unq t

589−reflectBinderQuotePattern q ty unq (GHole _ t)

589+reflectBinderQuotePattern q ty unq (GHole _ _ t)

590 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

591 fill $ reflCall "GHole" [ty, Var t']

592 solve

@@ -737,7 +737,7 @@ reflectBinderQuote q ty unq (NLet x y)

737 = reflCall "NLet" [Var ty, q unq x, q unq y]

738reflectBinderQuote q ty unq (Hole t)

739 = reflCall "Hole" [Var ty, q unq t]

740−reflectBinderQuote q ty unq (GHole _ t)

740+reflectBinderQuote q ty unq (GHole _ _ t)

741 = reflCall "GHole" [Var ty, q unq t]

742reflectBinderQuote q ty unq (Guess x y)

743 = reflCall "Guess" [Var ty, q unq x, q unq y]

src/Pkg/Package.hs+3−3

@@ -132,17 +132,17 @@ documentPkg fp =

132 do pkgdesc <- parseDesc fp

133 cd <- getCurrentDirectory

134 let pkgDir = cd </> takeDirectory fp

135− outputDir = cd </> (pkgname pkgdesc) ++ "_doc"

135+ outputDir = cd </> pkgname pkgdesc ++ "_doc"

136 opts = NoREPL : Verbose : idris_opts pkgdesc

137 mods = modules pkgdesc

138 fs = map (foldl1' (</>) . splitOn "." . showCG) mods

139 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

140 make (makefile pkgdesc)

141− setCurrentDirectory $ pkgDir

141+ setCurrentDirectory pkgDir

142 let run l = runExceptT . execStateT l

143 load [] = return ()

144 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

146 idrisInstance <- run loader idrisInit

147 setCurrentDirectory cd

148 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:

11 The function is Total

12Instances:

13 Functor List

14+ Functor (IO' ffi)

14 Functor Stream

15 Functor Stream

15 Functor Provider

16 Functor Provider

16 Functor Binder

17 Functor Binder

17 Functor PrimIO

18 Functor PrimIO

18− Functor (IO' ffi)

19 Functor Maybe

20 Functor (Either e)

21

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

2x :: app xs ys

3[]

4f x y :: vzipWith f xs ys

5+?word_length_rhs_3 :: word_length xs

test/interactive003/input+1

@@ -2,3 +2,4 @@

2:ps 5 app_rhs_2

3:ps 8 vzipWith_rhs_3

4: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

8vzipWith f [] [] = ?vzipWith_rhs_3

9vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1

10

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

29simple.append_lemma_2 = proof {

30 intros;

31 compute;

32− rewrite (plusSuccRightSucc m n);

32+ rewrite (plusSuccRightSucc m k);

33 trivial;

34}

35

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

1tutorial006a.idr:5:23-25:When checking right hand side of vapp:

2When checking argument xs to constructor Data.VectType.Vect.:::

3 Type mismatch between

4− Vect (n + n) a (Type of vapp xs xs)

4+ Vect (k + k) a (Type of vapp xs xs)

5 and

6− Vect (plus n m) a (Expected type)

6+ Vect (plus k m) a (Expected type)

7

8 Specifically:

9 Type mismatch between

10− plus n n

10+ plus k k

11 and

12− plus n m

12+ plus k m

13tutorial006b.idr:10:10:

14When checking right hand side of with block in Main.parity:

15Type mismatch between