8226a75 · Idris-dev · git.iko.soy

CHANGELOG+9

compare with master

unifiedsplit

@@ -19,6 +19,8 @@ Language updates

19* Name binding in patterns follows the same rule as name binding for implicits

20 in types: names which begin with lower case letters, not applied to any

21 arguments, are treated as bound pattern variables.

22+* Added %deprecate directive, which gives a warning and a message when a

23+ deprecated name is referenced.

22

24

23Library updates

25Library updates

24---------------

26---------------

@@ -37,6 +39,9 @@ Library updates

37 from Effectful programs.

39 from Effectful programs.

38* Some constructors that never actually occurred have been removed from

40* Some constructors that never actually occurred have been removed from

39 the TT and Raw reflection datatypes in Language.Reflection.

41 the TT and Raw reflection datatypes in Language.Reflection.

42+* File IO operations (for example openFile/fread/fwrite) now return

43+ 'Either FileError ty' where the return type was previously 'ty' to indicate

44+ that they may fail.

40

45

41Tool updates

46Tool updates

42------------

47------------

@@ -45,6 +50,10 @@ Tool updates

45* iPKG files have a new option `pkgs` which takes a comma-separated list

50* iPKG files have a new option `pkgs` which takes a comma-separated list

46 of package names that the idris project depends on. This reduces bloat

51 of package names that the idris project depends on. This reduces bloat

47 in the `opts` option with multiple package declarations.

52 in the `opts` option with multiple package declarations.

53+* iPKG files now allow `executable = "your filename here"` in addition to

54+ the existing `executable = yourFilenameHere` style. While the unquoted

55+ version is limited to filenames that look like namespaced Idris identifiers

56+ (`your.filename.here`), the quoted version accepts any valid filename.

48* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now

57* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now

49 adds missing clauses if there is already a definition.

58 adds missing clauses if there is already a definition.

50

59

CONTRIBUTORS+1

@@ -15,6 +15,7 @@ Jason Dagit

15Guglielmo Fachini

16Simon Fowler

17Google

18+Zack Grannan

18Cezar Ionescu

19Cezar Ionescu

19Heath Johns

20Heath Johns

20Irene Knapp

21Irene Knapp

Makefile+1−1

@@ -43,7 +43,7 @@ relib: lib_clean

43 $(CABAL) install $(CABALFLAGS)

44

45linecount:

46− wc -l src/Idris/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

46+ wc -l src/Idris/*.hs src/Idris/Elab/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs src/Util/*.hs

47

48#Note: this doesn't yet link to Hackage properly

49doc: dist/setup-config

docs/effects/depeff.rst+2−2

@@ -48,7 +48,7 @@ express this as follows:

48 readInt = do let x = trim !getStr

49 putM (cast x :: !get)

50

51−The notation ``{ xs ==> xs’ } Eff a`` in a type means that the operation

51+The type ``Eff a xs xs'`` means that the operation

52begins with effects ``xs`` available, and ends with effects ``xs’``

53available. We have used ``putM`` to update the state, where the ``M``

54suffix indicates that the *type* is being updated as well as the value.

@@ -96,7 +96,7 @@ value read from the user was valid. We can express this in the type:

96 else [STATE (Vect n Int), STDIO])

97 readInt = do let x = trim !getStr

98 case all isDigit (unpack x) of

99− False => pure False

99+ False => pureM False

100 True => do putM (cast x :: !get)

101 pureM True

102

docs/effects/hangman.rst+8−9

@@ -108,16 +108,15 @@ effect signature:

108 Guess : (x : Char) ->

109 sig MysteryRules Bool

110 (Mystery (Running (S g) (S w)))

111− (\inword =>

111+ (\inword => if inword

112− Mystery (case inword of

113− True => (Running (S g) w)

112+ then Mystery (Running (S g) w)

114− False => (Running g (S w))))

113+ else Mystery (Running g (S w)))

115 Won : sig MysteryRules () (Mystery (Running g 0))

114 Won : sig MysteryRules () (Mystery (Running g 0))

116 (Mystery NotRunning)

115 (Mystery NotRunning)

117 Lost : sig MysteryRules () (Mystery (Running 0 g))

116 Lost : sig MysteryRules () (Mystery (Running 0 g))

118 (Mystery NotRunning)

117 (Mystery NotRunning)

119 NewWord : (w : String) ->

118 NewWord : (w : String) ->

120− sig MysteryRules () h (Mystery (Running 6 (length (letters w))))

119+ sig MysteryRules () (Mystery NotRunning) (Mystery (Running 6 (length (letters w))))

121 Get : sig MysteryRules String (Mystery h)

120 Get : sig MysteryRules String (Mystery h)

122

121

123This description says nothing about how the rules are implemented. In

122This description says nothing about how the rules are implemented. In

@@ -243,11 +242,11 @@ running ``game``:

243.. code-block:: idris

242.. code-block:: idris

244

243

245 runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]

244 runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]

246− runGame = do srand (cast !time)

245+ runGame = do srand !time

247− let w = index !(rndFin WEWEWE) words

246+ let w = index !(rndFin _) words

248− NewWord w

247+ call $ NewWord w

249 game

248 game

250− putStrLn !Get

249+ putStrLn !(call Get)

251

250

252We use the system time (``time`` from the ``SYSTEM`` effect; see

251We use the system time (``time`` from the ``SYSTEM`` effect; see

253Appendix :ref:`sect-appendix`) to initialise the random number

252Appendix :ref:`sect-appendix`) to initialise the random number

docs/effects/simpleeff.rst+23−22

@@ -382,7 +382,7 @@ definition:

382

383 vadd : Vect n Int -> Vect n Int -> Vect n Int

384 vadd [] [] = []

385− vadd (x :: idris xs) (y :: ys) = x + y :: vadd xs ys

385+ vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys

386

387Using , we can set up a program so that it reads input from a user,

388checks that the input is valid (i.e both vectors contain integers, and

@@ -410,10 +410,28 @@ following type:

410

411This returns a dependent pair of a length, and a vector of that

412length, because we cannot know in advance how many integers the user

413−is going to input. One way to implement this function, using ``-1`` to

414−indicate the end of input, is shown in Listing [readvec]. This uses a

413+is going to input. We can use ``-1`` to indicate the end of input:

414+

415+.. code-block:: idris

416+

417+ read_vec : Eff (p ** Vect p Int) [STDIO]

418+ read_vec = do putStr "Number (-1 when done): "

419+ case run (parseNumber (trim !getStr)) of

420+ Nothing => do putStrLn "Input error"

421+ read_vec

422+ Just v => if (v /= -1)

423+ then do (_ ** xs) <- read_vec

424+ pure (_ ** v :: xs)

425+ else pure (_ ** [])

426+ where

427+ parseNumber : String -> Eff Int [EXCEPTION String]

428+ parseNumber str

429+ = if all (\x => isDigit x || x == '-') (unpack str)

430+ then pure (cast str)

431+ else raise "Not a number"

432+

415−variation on ``parseNumber`` which does not require a number to be

433+This uses a variation on ``parseNumber`` which does not require a

416−within range.

434+number to be within range.

417

435

418Finally, we write a program which reads two vectors and prints the

436Finally, we write a program which reads two vectors and prints the

419result of pairwise addition of them, throwing an exception if the

437result of pairwise addition of them, throwing an exception if the

@@ -434,23 +452,6 @@ equal. This does not stop us reading vectors from user input, but it

434does require that the lengths are checked and any discrepancy is dealt

452does require that the lengths are checked and any discrepancy is dealt

435with gracefully.

453with gracefully.

436

454

437−.. code-block:: idris

438−

439− read_vec : Eff (p ** Vect p Int) [STDIO]

440− read_vec = do putStr "Number (-1 when done): "

441− case run (parseNumber (trim !getStr)) of

442− Nothing => do putStrLn "Input error"

443− read_vec

444− Just v => if (v /= -1)

445− then do (_ ** xs) <- read_vec

446− pure (_ ** v :: xs)

447− else pure (_ ** [])

448− where

449− parseNumber : String -> Eff Int [EXCEPTION String]

450− parseNumber str

451− = if all (\x => isDigit x || x == '-') (unpack str)

452− then pure (cast str)

453− else raise "Not a number"

454

455

455Example: An Expression Calculator

456Example: An Expression Calculator

456=================================

457=================================

docs/faq/faq.rst+53

@@ -103,6 +103,59 @@ the difference between:

103 Idris> \n, m => n + (S m)

104 \n => \m => plus n (S m) : Nat -> Nat -> Nat

105

106+

107+Why can't I use a function with no arguments in a type?

108+=======================================================

109+

110+If you use a name in a type which begins with a lower case letter, and which is

111+not applied to any arguments, then Idris will treat it as an implicitly

112+bound argument. For example:

113+

114+.. code-block:: idris

115+

116+ append : Vect n ty -> Vect m ty -> Vect (n + m) ty

117+

118+Here, ``n``, ``m``, and ``ty`` are implicitly bound. This rule applies even

119+if there are functions defined elsewhere with any of these names. For example,

120+you may also have:

121+

122+.. code-block:: idris

123+

124+ ty : Type

125+ ty = String

126+

127+Even in this case, ``ty`` is still considered implicitly bound in the definition

128+of ``append``, rather than making the type of ``append`` equivalent to...

129+

130+.. code-block:: idris

131+

132+ append : Vect n String -> Vect m String -> Vect (n + m) String

133+

134+...which is probably not what was intended! The reason for this rule is so

135+that it is clear just from looking at the type of ``append``, and no other

136+context, what the implicitly bound names are.

137+

138+If you want to use an unapplied name in a type, you have two options. You

139+can either explicitly qualify it, for example, if ``ty`` is defined in the

140+namespace ``Main`` you can do the following:

141+

142+.. code-block:: idris

143+

144+ append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty

145+

146+Alternatively, you can use a name which does not begin with a lower case

147+letter, which will never be implicitly bound:

148+

149+.. code-block:: idris

150+

151+ Ty : Type

152+ Ty = String

153+

154+ append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty

155+

156+As a convention, if a name is intended to be used as a type synonym, it is

157+best for it to begin with a capital letter to avoid this restriction.

158+

106I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?

159I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?

107=============================================================================================

160=============================================================================================

108

161

docs/reference/repl.rst+2−1

@@ -128,7 +128,8 @@ The current set of supported commands are:

128+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

129|:? :h :help | | Display this help text |

130+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

131−|:set | <option> | Set an option (errorcontext, showimplicits) |

131+|:set | <option> | Set an option (errorcontext, showimplicits, originalerrors, autosolve, nobanner, warnreach, evaltypes, |

132+| | | desugarnats) |

132+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

133+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

133|:unset | <option> | Unset an option |

134|:unset | <option> | Unset an option |

134+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

135+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

@@ -112,7 +112,7 @@ Types

112

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

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

115−variables that denote a type must begin with a capital letter. Example:

115+variables that denote a type need not be capitalised. Example:

116

117.. code:: idris

118

@@ -126,6 +126,9 @@ a more interesting example:

126 MyListType : Type

127 MyListType = List Int

128

129+While capitalising types is not required, the rules for generating implicit

130+arguments mean it is often a good idea.

131+

129.. _syntax-data-types:

132.. _syntax-data-types:

130

133

131Data types

134Data types

docs/tutorial/interp.rst+3−1

@@ -36,7 +36,9 @@ We’re going to define a representation of our language in such a way

36that only well-typed programs can be represented. We’ll index the

37representations of expressions by their type and the types of local

38variables (the context), which we’ll be using regularly as an implicit

39−argument, so we define everything in a ``using`` block:

39+argument, so we define everything in a ``using`` block (keep in mind

40+that everything after this point needs to be indented so as to be

41+inside the ``using`` block):

40

42

41.. code-block:: idris

43.. code-block:: idris

42

44

docs/tutorial/introduction.rst+1−1

@@ -15,7 +15,7 @@ respectively:

15Correspondingly, the following values are examples of inhabitants of

16those types:

17

18−- ``42``, ``’a’``, ``Hello world!``, ``[2,3,4,5,6]``

18+- ``42``, ``’a’``, ``"Hello world!"``, ``[2,3,4,5,6]``

19

20In a language with *dependent types*, however, the distinction is less

21clear. Dependent types allow types to “depend” on values — in other

docs/tutorial/syntax.rst+3−3

@@ -122,7 +122,7 @@ hard to program this way in practice. Recall the factorial program in

122

123 fact : Expr G (TyFun TyInt TyInt)

124 fact = Lam (If (Op (==) (Var Stop) (Val 0))

125− (Val 1) (Op (*) (app fact (Op (-) (Var Stop) (Val 1)))

125+ (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))

126 (Var Stop)))

127

128Since this is a particularly useful pattern, Idris provides syntax

@@ -162,8 +162,8 @@ declaring:

162

163.. code-block:: idris

164

165− (<$>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t

165+ (<*>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t

166− (<$>) f a = App f a

166+ (<*>) f a = App f a

167

168 pure : Expr G a -> Expr G a

169 pure = id

docs/tutorial/typesfuns.rst+23−10

@@ -56,7 +56,7 @@ answer. For example:

56::

57

58 *prims> 6*6+6

59− 42 : Int

59+ 42 : Integer

60 *prims> x == 6*6+6

61 True : Bool

62

@@ -792,12 +792,12 @@ providing a default value:

792

793.. code-block:: idris

794

795− maybe : Lazy b -> (a -> b) -> Maybe a -> b

795+ maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

796

797−Note that the type of the first argument is ``Lazy b`` rather than

797+Note that the types of the first two arguments are wrapped in

798−simply ``b``. Since the default value might not be used, we mark it as

798+``Lazy``. Since only one of the two arguments will actually be used,

799−``Lazy`` in case it is a large expression where evaluating it then

799+we mark them as ``Lazy`` in case they are large expressions where it

800−discarding it would be wasteful.

800+would be wasteful to compute and then discard them.

801

802Tuples

803------

@@ -820,6 +820,15 @@ contain an arbitrary number of values, represented as nested pairs:

820 jim : (String, Int, String)

821 jim = ("Jim", 25, "Cambridge")

822

823+::

824+

825+ *usefultypes> fst jim

826+ "Jim" : String

827+ *usefultypes> snd jim

828+ (25, "Cambridge") : (Int, String)

829+ *usefultypes> jim == ("Jim", (25, "Cambridge"))

830+ True : Bool

831+

823Dependent Pairs

832Dependent Pairs

824---------------

833---------------

825

834

@@ -1025,7 +1034,11 @@ For example:

1025 className : String

1034 className : String

1026

1035

1027**Note** that it is no longer possible to use the ``addStudent``

1036**Note** that it is no longer possible to use the ``addStudent``

1028−method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremented using the successor constructor.

1037+function from earlier, since that would change the size of the class. A

1038+function to add a student must now specify in the type that the

1039+size of the class has been increased by one. As the size is specified

1040+using natural numbers, the new value can be incremented using the

1041+``S`` constructor.

1029

1042

1030.. code-block:: idris

1043.. code-block:: idris

1031

1044

@@ -1137,8 +1150,8 @@ auxiliary functions, and is also used internally to implement pattern

1137matching ``let`` and lambda bindings. It will *only* work if:

1150matching ``let`` and lambda bindings. It will *only* work if:

1138

1151

1139- Each branch *matches* a value of the same type, and *returns* a

1152- Each branch *matches* a value of the same type, and *returns* a

1140− value of the same type.

1153+ value of the same type.

1141

1154

1142- The type of the result is "known". i.e. the type of the expression

1155- The type of the result is "known". i.e. the type of the expression

1143− can be determined *without* type checking the ``case``-expression

1156+ can be determined *without* type checking the ``case``-expression

1144− itself.

1157+ itself.

idris.cabal+13−1

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

1Name: idris

2−Version: 0.9.19.1

2+Version: 0.9.20.1

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -538,6 +538,17 @@ Extra-source-files:

538 test/interactive009/input

539 test/interactive009/*.idr

540 test/interactive009/expected

541+ test/interactive010/expected

542+ test/interactive010/input

543+ test/interactive010/run

544+ test/interactive011/expected

545+ test/interactive011/input

546+ test/interactive011/run

547+ test/interactive011/*.idr

548+ test/interactive012/expected

549+ test/interactive012/input

550+ test/interactive012/run

551+ test/interactive012/*.idr

541

552

542 test/io001/run

553 test/io001/run

543 test/io001/*.idr

554 test/io001/*.idr

@@ -993,6 +1004,7 @@ Library

993 cpp-options: -DIDRIS_FFI

1004 cpp-options: -DIDRIS_FFI

994 if flag(GMP)

1005 if flag(GMP)

995 build-depends: libffi < 0.2

1006 build-depends: libffi < 0.2

1007+ extra-libraries: gmp

996 cpp-options: -DIDRIS_GMP

1008 cpp-options: -DIDRIS_GMP

997 if flag(curses)

1009 if flag(curses)

998 build-depends: hscurses < 1.5

1010 build-depends: hscurses < 1.5

iif/adder.iifdeleted−30

@@ -1,30 +0,0 @@

1−data O 0

2−data S 1

3−

4−fun plus(x, y) = case x of {

5− O => y

6− | S(k) => S (plus(k, y))

7− }

8−

9−fun natToInt(x) = case x of {

10− O => 0

11− | S(k) => let y = natToInt(k) in y + 1

12− }

13−

14−fun adder(arity, acc) = case arity of {

15− O => acc

16− | S(k) => adderAux(k, acc)

17− }

18−

19−fun adderAux(k, acc, n) = adder(k, plus(acc, n))

20−

21−fun zero() = O

22−fun one() = S(zero)

23−fun two() = S(one)

24−fun three() = S(two)

25−fun four() = S(three)

26−fun five() = S(four)

27−

28−fun main() = %WriteInt(natToInt(adder(three, two, three, four, five)))

29−

30−

iif/big.iifdeleted−7

@@ -1,7 +0,0 @@

1−fun fact(x) = case (x ==: 0:) of {

2− 0 => x *: fact(x - 1)

3− | _ => 1:

4− }

5−

6−fun main() = let f = fact(200:) in

7− %WriteString(%BigString(f) ++ "\n")

iif/ctest.cdeleted−106

@@ -1,106 +0,0 @@

1−#include <idris_rts.h>

2−

3−void plus(VM* vm, VAL* oldbase) {

4− INITFRAME;

5− RESERVE(2);

6− ADDTOP(2);

7−

8− switch(TAG(LOC(0))) {

9− case 0:

10− PROJECT(vm, LOC(0), 2, 0);

11− RVAL = LOC(1);

12− TOPBASE(0);

13− REBASE;

14− break;

15− case 1:

16− PROJECT(vm, LOC(0), 2, 1);

17− RESERVE(2);

18− TOP(0) = LOC(2);

19− TOP(1) = LOC(1);

20− STOREOLD;

21− BASETOP(0);

22− ADDTOP(2);

23− CALL(plus);

24− LOC(3) = RVAL;

25− RVAL = MKCON(vm, 1, 1, LOC(3));

26− TOPBASE(0);

27− REBASE;

28− break;

29− }

30−}

31−

32−void natToInt(VM* vm, VAL* oldbase) {

33− INITFRAME;

34− RESERVE(3);

35− ADDTOP(3);

36−

37− switch(TAG(LOC(0))) {

38− case 0:

39− PROJECT(vm, LOC(0), 2, 0);

40− RVAL = MKINT(0);

41− TOPBASE(0);

42− REBASE;

43− break;

44− case 1:

45− PROJECT(vm, LOC(0), 1, 1);

46− RESERVE(1);

47− TOP(0) = LOC(1);

48− STOREOLD;

49− BASETOP(0);

50− ADDTOP(1);

51− CALL(natToInt);

52− LOC(2) = RVAL;

53− RVAL = ADD(LOC(2), MKINT(1));

54− TOPBASE(0);

55− REBASE;

56− break;

57− }

58−}

59−

60−int do_main(VM* vm, VAL* oldbase) {

61− INITFRAME;

62− RESERVE(2);

63− ADDTOP(2);

64−

65− LOC(0) = MKCON(vm, 0, 0);

66− LOC(0) = MKCON(vm, 1, 1, LOC(0));

67− LOC(0) = MKCON(vm, 1, 1, LOC(0));

68−

69− dumpVal(LOC(0));

70− printf("\n");

71−

72− LOC(1) = MKCON(vm, 0, 0);

73− LOC(1) = MKCON(vm, 1, 1, LOC(1));

74− LOC(1) = MKCON(vm, 1, 1, LOC(1));

75−

76− RESERVE(2);

77− TOP(0) = LOC(0);

78− TOP(1) = LOC(1);

79−

80− STOREOLD;

81− BASETOP(0);

82− ADDTOP(2);

83− CALL(plus);

84− LOC(0) = RVAL;

85−

86− RESERVE(1);

87− TOP(0) = LOC(0);

88− SLIDE(vm, 1);

89− TOPBASE(1);

90− TAILCALL(natToInt);

91−/* STOREOLD;

92− BASETOP(0);

93− ADDTOP(1);

94− CALL(natToInt);

95− TOPBASE(0);

96− REBASE; */

97−}

98−

99−int main() {

100− VM* vm = init_vm(100,100);

101−

102− do_main(vm, NULL);

103− printf("%ld\n", GETINT(RVAL));

104−

105− printf("%d %d %d\n", vm->valstack, vm->valstack_base, vm->valstack_top);

106−}

iif/lazy.iifdeleted−21

@@ -1,21 +0,0 @@

1−data Nil 0

2−data Cons 2

3−

4−fun countFrom(x) = Cons(x, countFrom@(x+1))

5−

6−fun take(n, xs) = case n of {

7− 0 => Nil

8− | _ => case xs of {

9− Nil => Nil

10− | Cons(y, ys) => Cons(y, take(n-1, ys))

11− }

12− }

13−

14−fun dumpList(xs) = case xs of {

15− Nil => "END"

16− | Cons(y, ys) => %IntString(y) ++ ", " ++ dumpList(ys)

17− }

18−

19−fun double(x) = x + x

20−

21−fun main() = %WriteString(dumpList(take(5, countFrom(10))))

iif/testmap.iifdeleted−30

@@ -1,30 +0,0 @@

1−data Nil 0

2−data Cons 2

3−

4−fun twice(f, x) = f(f(x))

5−

6−fun map(f, xs) = case xs of {

7− Nil => Nil

8− | Cons(y, ys) => Cons(f(y), map(f, ys))

9− }

10−

11−fun dumpList(xs) = case xs of {

12− Nil => "END"

13− | Cons(y, ys) => %IntString(y) ++ ", " ++ dumpList(ys)

14− }

15−

16−fun countFrom(x) = Cons(x, countFrom@(x+1))

17−

18−fun take(n, xs) = case n of {

19− 0 => Nil

20− | _ => case xs of {

21− Nil => Nil

22− | Cons(y, ys) => Cons(y, take(n-1, ys))

23− }

24− }

25−

26−fun double(x) = x + x

27−

28−fun main() = let mult = 2 in

29− %WriteString(dumpList(map(twice(\ x => x*mult), take(1010, countFrom(10)))))

30−

iif/testvm.iifdeleted−32

@@ -1,32 +0,0 @@

1−data O 0

2−data S 1

3−

4−fun plus(x, y) = case x of {

5− O => y

6− | S(k) => S (plus(k, y))

7− }

8−

9−fun fact(x) = factAux(x, 1)

10−

11−fun factAux(x, acc) = case (x == 1) of {

12− 0 => factAux(x-1, acc * x)

13− | 1 => acc

14− }

15−

16−fun natToInt(x) = case x of {

17− O => 0

18− | S(k) => let y = natToInt(k) in y + 1

19− }

20−

21−fun intToNat(x) = case x of {

22− 0 => O

23− | _ => S (intToNat (x - 1))

24− }

25−

26−fun sin(x) = foreign C Float "sin" (Float x)

27−

28−fun main() = let val = natToInt(plus(intToNat(fact(6)), S(S(O)))) in

29− let sval = sin(1.0) in

30− %WriteString("Answer: " ++ %IntString(val)

31− ++ " " ++ %FloatString(sval))

32−

libs/base/Control/Catchable.idr+2−2

@@ -16,14 +16,14 @@ instance Catchable (Either a) a where

16 catch (Left err) h = h err

17 catch (Right x) h = (Right x)

18

19− throw x = Left x

19+ throw = Left

20

21instance Catchable (IOExcept err) err where

22 catch (IOM prog) h = IOM (do p' <- prog

23 case p' of

24 Left e => let IOM he = h e in he

25 Right val => return (Right val))

26− throw x = IOM (return (Left x))

26+ throw = ioe_fail

27

28instance Catchable List () where

29 catch [] h = h ()

libs/base/Control/IOExcept.idr+8−17

@@ -2,34 +2,25 @@ module Control.IOExcept

2

3-- An IO monad with exception handling

4

5−data IOExcept : Type -> Type -> Type where

5+record IOExcept err a where

6+ constructor IOM

6− IOM : IO (Either err a) -> IOExcept err a

7+ runIOExcept : IO (Either err a)

7

8

8instance Functor (IOExcept e) where

9instance Functor (IOExcept e) where

9 map f (IOM fn) = IOM (map (map f) fn)

10 map f (IOM fn) = IOM (map (map f) fn)

10

11

11instance Applicative (IOExcept e) where

12instance Applicative (IOExcept e) where

12 pure x = IOM (pure (pure x))

13 pure x = IOM (pure (pure x))

13− (IOM f) <*> (IOM a) = IOM (do f' <- f; a' <- a

14+ (IOM f) <*> (IOM a) = IOM [| f <*> a |]

14− return (f' <*> a'))

15

16instance Monad (IOExcept e) where

17− (IOM x) >>= k = IOM (do x' <- x;

17+ (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)

18− case x' of

19− Right a => let (IOM ka) = k a in

20− ka

21− Left err => return (Left err))

22

18

23ioe_lift : IO a -> IOExcept err a

19ioe_lift : IO a -> IOExcept err a

24−ioe_lift op = IOM (do op' <- op

20+ioe_lift op = IOM $ map Right op

25− return (Right op'))

26

21

27ioe_fail : err -> IOExcept err a

22ioe_fail : err -> IOExcept err a

28−ioe_fail e = IOM (return (Left e))

23+ioe_fail e = IOM $ pure (Left e)

29

24

30ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b

25ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b

31−ioe_run (IOM act) err ok = do act' <- act

26+ioe_run (IOM act) err ok = either err ok !act

32− case act' of

33− Left e => err e

34− Right v => ok v

35−

libs/base/Data/Complex.idr+8−8

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

25 plus_i = User 6

26

27

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

28+-- when we have a type class 'Fractional' (which contains Double),

29-- we can do:

30{-

31instance Fractional a => Fractional (Complex a) where

@@ -40,16 +40,16 @@ instance Fractional a => Fractional (Complex a) where

40

41------------------------------ Polarform

42

43−mkPolar : Float -> Float -> Complex Float

43+mkPolar : Double -> Double -> Complex Double

44mkPolar radius angle = radius * cos angle :+ radius * sin angle

45

46−cis : Float -> Complex Float

46+cis : Double -> Complex Double

47cis angle = cos angle :+ sin angle

48

49−magnitude : Complex Float -> Float

49+magnitude : Complex Double -> Double

50magnitude (r:+i) = sqrt (r*r+i*i)

51

52−phase : Complex Float -> Float

52+phase : Complex Double -> Double

53phase (x:+y) = atan2 y x

54

55

@@ -62,13 +62,13 @@ instance Functor Complex where

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

63

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

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

65+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double

66−instance Num (Complex Float) where

66+instance Num (Complex Double) where

67 (+) (a:+b) (c:+d) = ((a+c):+(b+d))

68 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))

69 fromInteger x = (fromInteger x:+0)

70

71−instance Neg (Complex Float) where

71+instance Neg (Complex Double) where

72 negate = map negate

73 (-) (a:+b) (c:+d) = ((a-c):+(b-d))

74 abs (a:+b) = (magnitude (a:+b):+0)

libs/base/Data/Vect.idr+5−5

@@ -614,11 +614,11 @@ mapElem (There e) = There (mapElem e)

614||| @xs the vector with the desired length

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

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

617−isLength : {m : Nat} -> -- expected at run-time

617+exactLength : {m : Nat} -> -- expected at run-time

618− (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)

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

619−isLength {m} len xs with (decEq m len)

619+exactLength {m} len xs with (decEq m len)

620− isLength {m = m} m xs | (Yes Refl) = Just xs

620+ exactLength {m = m} m xs | (Yes Refl) = Just xs

621− isLength {m = m} len xs | (No contra) = Nothing

621+ exactLength {m = m} len xs | (No contra) = Nothing

622

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

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

libs/base/Language/Reflection/Utils.idr+2−2

@@ -129,7 +129,7 @@ instance Show IntTy where

129

130instance Show ArithTy where

131 showPrec d (ATInt t) = showCon d "ATInt" $ showArg t

132− showPrec d ATFloat = "ATFloat"

132+ showPrec d ATDouble = "ATDouble"

133

134instance Show Const where

135 showPrec d (I i) = showCon d "I" $ showArg i

@@ -162,7 +162,7 @@ instance Eq Reflection.IntTy where

162

163instance Eq ArithTy where

164 (ATInt x) == (ATInt y) = x == y

165− ATFloat == ATFloat = True

165+ ATDouble == ATDouble = True

166 _ == _ = False

167

168instance Eq Const where

libs/contrib/Control/Algebra/NumericInstances.idr+7−7

@@ -44,24 +44,24 @@ instance RingWithUnity Int where

44 unity = 1

45

46

47−instance Semigroup Float where

47+instance Semigroup Double where

48 (<+>) = (+)

49

50−instance Monoid Float where

50+instance Monoid Double where

51 neutral = 0

52

53−instance Group Float where

53+instance Group Double where

54 inverse = (* -1)

55

56−instance AbelianGroup Float

56+instance AbelianGroup Double

57

58−instance Ring Float where

58+instance Ring Double where

59 (<.>) = (*)

60

61−instance RingWithUnity Float where

61+instance RingWithUnity Double where

62 unity = 1

63

64−instance Field Float where

64+instance Field Double where

65 inverseM f _ = 1 / f

66

67

libs/contrib/Network/Socket.idr−4

@@ -143,10 +143,6 @@ record Socket where

143 socketType : SocketType

144 protocalNumber : ProtocolNumber

145

146−||| Get the C error number

147−getErrno : IO Int

148−getErrno = foreign FFI_C "idrnet_errno" (IO Int)

149−

150||| Creates a UNIX socket with the given family, socket type and protocol

146||| Creates a UNIX socket with the given family, socket type and protocol

151||| number. Returns either a socket or an error.

147||| number. Returns either a socket or an error.

152socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

148socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

libs/effects/Effect/Default.idr+1−1

@@ -11,7 +11,7 @@ instance Default Int where

11instance Default Integer where

12 default = 0

13

14−instance Default Float where

14+instance Default Double where

15 default = 0

16

17instance Default Nat where

libs/effects/Effect/Exception.idr+1−1

@@ -18,7 +18,7 @@ instance Show a => Handler (Exception a) IO where

18 believe_me (exit 1)

19

20instance Handler (Exception a) (IOExcept a) where

21− handle _ (Raise e) k = IOM (return (Left e))

21+ handle _ (Raise e) k = ioe_fail e

22

23instance Handler (Exception a) (Either a) where

24 handle _ (Raise e) k = Left e

libs/effects/Effect/File.idr+16−12

@@ -74,29 +74,33 @@ data FileIO : Effect where

74

75--- An implementation of the resource access protocol for the IO Context.

76instance Handler FileIO IO where

77− handle () (Open fname m) k = do h <- openFile fname m

77+ handle () (Open fname m) k = do Right h <- openFile fname m

78− valid <- validFile h

78+ | Left err => k False ()

79− if valid then k True (FH h)

79+ k True (FH h)

80− else k False ()

81 handle (FH h) Close k = do closeFile h

80 handle (FH h) Close k = do closeFile h

82 k () ()

81 k () ()

83− handle (FH h) ReadLine k = do str <- fread h

82+ handle (FH h) ReadLine k = do Right str <- fread h

83+ -- Need proper error handling!

84+ | Left err => k "" (FH h)

84 k str (FH h)

85 k str (FH h)

85− handle (FH h) (WriteString str) k = do fwrite h str

86+ handle (FH h) (WriteString str) k = do Right () <- fwrite h str

87+ | Left err => k () (FH h)

86 k () (FH h)

88 k () (FH h)

87 handle (FH h) EOF k = do e <- feof h

89 handle (FH h) EOF k = do e <- feof h

88 k e (FH h)

90 k e (FH h)

89

91

90instance Handler FileIO (IOExcept a) where

92instance Handler FileIO (IOExcept a) where

91− handle () (Open fname m) k = do h <- ioe_lift $ openFile fname m

93+ handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m

92− valid <- ioe_lift $ validFile h

94+ | Left err => k False ()

93− if valid then k True (FH h)

95+ k True (FH h)

94− else k False ()

95 handle (FH h) Close k = do ioe_lift $ closeFile h

96 handle (FH h) Close k = do ioe_lift $ closeFile h

96 k () ()

97 k () ()

97− handle (FH h) ReadLine k = do str <- ioe_lift $ fread h

98+ handle (FH h) ReadLine k = do Right str <- ioe_lift $ fread h

99+ -- Need proper error handling!

100+ | Left err => k "" (FH h)

98 k str (FH h)

101 k str (FH h)

99− handle (FH h) (WriteString str) k = do ioe_lift $ fwrite h str

102+ handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str

103+ | Left err => k () (FH h)

100 k () (FH h)

104 k () (FH h)

101 handle (FH h) EOF k = do e <- ioe_lift $ feof h

105 handle (FH h) EOF k = do e <- ioe_lift $ feof h

102 k e (FH h)

106 k e (FH h)

libs/effects/Effects.idr+7−2

@@ -12,9 +12,9 @@ import Data.Vect

12||| The Effect type describes effectful computations.

13|||

14||| This type is parameterised by:

15−||| + The input resource.

16||| + The return type of the computation.

15||| + The return type of the computation.

16+||| + The input resource.

17−||| + The computation to run on the resource.

17+||| + The computation to run on the resource given the return value.

18Effect : Type

19Effect = (x : Type) -> Type -> (x -> Type) -> Type

20

@@ -245,6 +245,11 @@ pureM = Value

245(<*>) prog v = do fn <- prog

246 arg <- v

247 return (fn arg)

248+

249+(*>) : EffM m a xs (\v => xs) ->

250+ EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)

251+a *> b = do a

252+ b

248

253

249new : Handler e' m => (e : EFFECT) -> resTy ->

254new : Handler e' m => (e : EFFECT) -> resTy ->

250 {auto prf : e = MkEff resTy e'} ->

255 {auto prf : e = MkEff resTy e'} ->

libs/oldeffects/Effect/Default.idr+1−1

@@ -9,7 +9,7 @@ instance Default Int where

9instance Default Integer where

10 default = 0

11

12−instance Default Float where

12+instance Default Double where

13 default = 0

14

15instance Default Nat where

libs/prelude/Builtins.idr+3−1

@@ -152,9 +152,11 @@ public %assert_total

152really_believe_me : a -> b

153really_believe_me x = prim__believe_me _ _ x

154

155−-- Deprecated - for backward compatibility

155+||| Deprecated alias for `Double`, for the purpose of backwards

156+||| compatibility. Idris does not support 32 bit floats at present.

156Float : Type

157Float : Type

157Float = Double

158Float = Double

159+%deprecate Float

158

160

159-- Pointers as external primitive; there's no literals for these, so no

161-- Pointers as external primitive; there's no literals for these, so no

160-- need for them to be part of the compiler.

162-- need for them to be part of the compiler.

libs/prelude/IO.idr+10−6

@@ -36,7 +36,6 @@ record FFI where

36||| The IO type, parameterised over the FFI that is available within

37||| it.

38abstract

39−%error_reverse

40data IO' : (lang : FFI) -> Type -> Type where

39data IO' : (lang : FFI) -> Type -> Type where

41 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

40 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

42

41

@@ -117,11 +116,11 @@ io_return x = MkIO (\w => prim_io_return x)

117liftPrimIO : (World -> PrimIO a) -> IO' l a

116liftPrimIO : (World -> PrimIO a) -> IO' l a

118liftPrimIO = MkIO

117liftPrimIO = MkIO

119

118

120−call__IO : IO' l a -> PrimIO a

119+call__IO : IO' ffi a -> PrimIO a

121call__IO (MkIO f) = f (TheWorld prim__TheWorld)

120call__IO (MkIO f) = f (TheWorld prim__TheWorld)

122

121

123-- Concrete type makes it easier to elaborate at top level

122-- Concrete type makes it easier to elaborate at top level

124−run__IO : IO' l () -> PrimIO ()

123+run__IO : IO' ffi () -> PrimIO ()

125run__IO f = call__IO f

124run__IO f = call__IO f

126

125

127unsafePerformIO : IO' ffi a -> a

126unsafePerformIO : IO' ffi a -> a

@@ -163,7 +162,7 @@ namespace FFI_C

163 ||| Supported C foreign types

162 ||| Supported C foreign types

164 data C_Types : Type -> Type where

163 data C_Types : Type -> Type where

165 C_Str : C_Types String

164 C_Str : C_Types String

166− C_Float : C_Types Float

165+ C_Float : C_Types Double

167 C_Ptr : C_Types Ptr

166 C_Ptr : C_Types Ptr

168 C_MPtr : C_Types ManagedPtr

167 C_MPtr : C_Types ManagedPtr

169 C_Unit : C_Types ()

168 C_Unit : C_Types ()

@@ -176,8 +175,10 @@ namespace FFI_C

176 FFI_C : FFI

175 FFI_C : FFI

177 FFI_C = MkFFI C_Types String String

176 FFI_C = MkFFI C_Types String String

178

177

178+||| Interactive programs, describing I/O actions and returning a value.

179+||| @res The result type of the program

179%error_reverse

180%error_reverse

180−IO : Type -> Type

181+IO : (res : Type) -> Type

181IO = IO' FFI_C

182IO = IO' FFI_C

182

183

183-- Cannot be relaxed as is used by type providers and they expect IO a

184-- Cannot be relaxed as is used by type providers and they expect IO a

@@ -198,6 +199,9 @@ namespace IO

198 forceGC : IO ()

199 forceGC : IO ()

199 forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

200 forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

200

201

202+ getErrno : IO Int

203+ getErrno = foreign FFI_C "idris_errno" (IO Int)

204+

201--------- The Javascript/Node FFI

205--------- The Javascript/Node FFI

202

206

203

207

@@ -217,7 +221,7 @@ mutual

217

221

218 data JS_Types : Type -> Type where

222 data JS_Types : Type -> Type where

219 JS_Str : JS_Types String

223 JS_Str : JS_Types String

220− JS_Float : JS_Types Float

224+ JS_Float : JS_Types Double

221 JS_Ptr : JS_Types Ptr

225 JS_Ptr : JS_Types Ptr

222 JS_Unit : JS_Types ()

226 JS_Unit : JS_Types ()

223 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)

227 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)

libs/prelude/Language/Reflection.idr+9−9

@@ -70,10 +70,10 @@ data NativeTy = IT8 | IT16 | IT32 | IT64

70

71data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

72

73−data ArithTy = ATInt Language.Reflection.IntTy | ATFloat

73+data ArithTy = ATInt Language.Reflection.IntTy | ATDouble

74

75||| Primitive constants

76−data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

76+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

77 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

78 | AType ArithTy | StrType

79 | VoidType | Forgot

@@ -89,7 +89,7 @@ instance ReflConst Int where

89instance ReflConst Integer where

90 toConst = BI

91

92−instance ReflConst Float where

92+instance ReflConst Double where

93 toConst = Fl

94

95instance ReflConst Char where

@@ -366,12 +366,12 @@ instance Quotable Int Raw where

366 quotedTy = `(Int)

367 quote x = RConstant (I x)

368

369−instance Quotable Float TT where

369+instance Quotable Double TT where

370− quotedTy = `(Float)

370+ quotedTy = `(Double)

371 quote x = TConst (Fl x)

372

373−instance Quotable Float Raw where

373+instance Quotable Double Raw where

374− quotedTy = `(Float)

374+ quotedTy = `(Double)

375 quote x = RConstant (Fl x)

376

377instance Quotable Char TT where

@@ -541,12 +541,12 @@ instance Quotable Reflection.IntTy Raw where

541instance Quotable ArithTy TT where

542 quotedTy = `(ArithTy)

543 quote (ATInt x) = `(ATInt ~(quote x))

544− quote ATFloat = `(ATFloat)

544+ quote ATDouble = `(ATDouble)

545

546instance Quotable ArithTy Raw where

547 quotedTy = `(ArithTy)

548 quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))

549− quote ATFloat = `(ATFloat)

549+ quote ATDouble = `(ATDouble)

550

551instance Quotable Const TT where

552 quotedTy = `(Const)

libs/prelude/Prelude/Classes.idr+6−6

@@ -37,7 +37,7 @@ instance Eq Int where

37instance Eq Integer where

38 (==) = boolOp prim__eqBigInt

39

40−instance Eq Float where

40+instance Eq Double where

41 (==) = boolOp prim__eqFloat

42

43instance Eq Char where

@@ -118,7 +118,7 @@ instance Ord Integer where

118 GT

119

120

121−instance Ord Float where

121+instance Ord Double where

122 compare x y = if (x == y) then EQ else

123 if (boolOp prim__sltFloat x y) then LT else

124 GT

@@ -170,7 +170,7 @@ instance Num Int where

170 fromInteger = prim__truncBigInt_Int

171

172

173−instance Num Float where

173+instance Num Double where

174 (+) = prim__addFloat

175 (*) = prim__mulFloat

176

@@ -215,7 +215,7 @@ instance Neg Int where

215 (-) = prim__subInt

216 abs x = if x < (prim__truncBigInt_Int 0) then -x else x

217

218−instance Neg Float where

218+instance Neg Double where

219 negate x = prim__negFloat x

220 (-) = prim__subFloat

221 abs x = if x < (prim__toFloatBigInt 0) then -x else x

@@ -306,8 +306,8 @@ instance MaxBound Bits64 where

306

307-- ------------------------------------------------------------- [ Fractionals ]

308

309−||| Fractional division of two Floats.

309+||| Fractional division of two Doubles.

310−(/) : Float -> Float -> Float

310+(/) : Double -> Double -> Double

311(/) = prim__divFloat

312

313

libs/prelude/Prelude/File.idr+84−47

@@ -10,7 +10,8 @@ import Prelude.Cast

10import Prelude.Bool

11import Prelude.Basics

12import Prelude.Classes

13−import Prelude.Monad

13+import Prelude.Either

14+import Prelude.Show

14import IO

15import IO

15

16

16%access public

17%access public

@@ -19,6 +20,30 @@ import IO

19abstract

20abstract

20data File = FHandle Ptr

21data File = FHandle Ptr

21

22

23+||| An error from a file operation

24+-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure

25+-- the values correspond!

26+data FileError = FileReadError

27+ | FileWriteError

28+ | FileNotFound

29+ | PermissionDenied

30+ | GenericFileError Int -- errno

31+

32+private

33+strError : Int -> String

34+strError err = unsafePerformIO -- yeah, yeah...

35+ (foreign FFI_C "idris_showerror" (Int -> IO String) err)

36+

37+getFileError : IO FileError

38+getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"

39+ (Ptr -> IO (Raw FileError)) prim__vm

40+ return err

41+

42+instance Show FileError where

43+ show FileNotFound = "File Not Found"

44+ show PermissionDenied = "Permission Denied"

45+ show (GenericFileError errno) = strError errno

46+

22||| Standard input

47||| Standard input

23stdin : File

48stdin : File

24stdin = FHandle prim__stdin

49stdin = FHandle prim__stdin

@@ -31,6 +56,13 @@ stdout = FHandle prim__stdout

31stderr : File

56stderr : File

32stderr = FHandle prim__stderr

57stderr = FHandle prim__stderr

33

58

59+do_ferror : Ptr -> IO Int

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

61+

62+ferror : File -> IO Bool

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

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

65+

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

66||| Call the RTS's file opening function

35do_fopen : String -> String -> IO Ptr

67do_fopen : String -> String -> IO Ptr

36do_fopen f m

68do_fopen f m

@@ -39,12 +71,14 @@ do_fopen f m

39||| Open a file

71||| Open a file

40||| @ f the filename

72||| @ f the filename

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

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

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

74+fopen : (f : String) -> (m : String) -> IO (Either FileError File)

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

75fopen f m = do h <- do_fopen f m

76+ if !(nullPtr h)

77+ then do err <- getFileError

44− return (FHandle h)

78+ return (Left err)

79+ else return (Right (FHandle h))

45

80

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

81||| Check whether a file handle is actually a null pointer

47−partial

48validFile : File -> IO Bool

82validFile : File -> IO Bool

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

83validFile (FHandle h) = do x <- nullPtr h

50 return (not x)

84 return (not x)

@@ -55,33 +89,26 @@ data Mode = Read | Write | ReadWrite

55||| Open a file

89||| Open a file

56||| @ f the filename

90||| @ f the filename

57||| @ m the mode

91||| @ m the mode

58−partial

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

92+openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

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

93openFile f m = fopen f (modeStr m) where

61 modeStr Read = "r"

94 modeStr Read = "r"

62 modeStr Write = "w"

95 modeStr Write = "w"

63 modeStr ReadWrite = "r+"

96 modeStr ReadWrite = "r+"

64

97

65−partial

66do_fclose : Ptr -> IO ()

98do_fclose : Ptr -> IO ()

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

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

68

100

69−partial

70closeFile : File -> IO ()

101closeFile : File -> IO ()

71closeFile (FHandle h) = do_fclose h

102closeFile (FHandle h) = do_fclose h

72

103

73−partial

74do_fread : Ptr -> IO' l String

104do_fread : Ptr -> IO' l String

75do_fread h = prim_fread h

105do_fread h = prim_fread h

76

106

77−fgetc : File -> IO Char

107+fgetc : File -> IO (Either FileError 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

108+fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)

109+ if !(ferror (FHandle h))

83− if (x < 0) then return Nothing

110+ then return (Left FileReadError)

84− else return (Just (cast x))

111+ else return (Right c)

85

112

86fflush : File -> IO ()

113fflush : File -> IO ()

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

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

@@ -89,9 +116,12 @@ fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

89do_popen : String -> String -> IO Ptr

116do_popen : String -> String -> IO Ptr

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

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

91

118

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

119+popen : String -> Mode -> IO (Either FileError File)

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

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

121+ if !(nullPtr ptr)

122+ then do err <- getFileError

123+ return (Left err)

94− return (FHandle ptr)

124+ else return (Right (FHandle ptr))

95 where

125 where

96 modeStr Read = "r"

126 modeStr Read = "r"

97 modeStr Write = "w"

127 modeStr Write = "w"

@@ -103,20 +133,25 @@ pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h

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

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

104-- prim__vm h

134-- prim__vm h

105

135

106−partial

107−fread : File -> IO' l String

136+fread : File -> IO (Either FileError String)

108−fread (FHandle h) = do_fread h

137+fread (FHandle h) = do str <- do_fread h

109−

138+ if !(ferror (FHandle h))

110−partial

139+ then return (Left FileReadError)

140+ else return (Right str)

141+

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

142+do_fwrite : Ptr -> String -> IO (Either FileError ())

112−do_fwrite h s = do prim_fwrite h s

143+do_fwrite h s = do res <- prim_fwrite h s

113− return ()

144+ if (res /= 0)

114−

145+ then do errno <- getErrno

115−partial

146+ if errno == 0

147+ then return (Left FileWriteError)

148+ else do err <- getFileError

149+ return (Left err)

150+ else return (Right ())

151+

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

152+fwrite : File -> String -> IO (Either FileError ())

117fwrite (FHandle h) s = do_fwrite h s

153fwrite (FHandle h) s = do_fwrite h s

118

154

119−partial

120do_feof : Ptr -> IO Int

155do_feof : Ptr -> IO Int

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

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

122

157

@@ -125,32 +160,34 @@ feof : File -> IO Bool

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

160feof (FHandle h) = do eof <- do_feof h

126 return (not (eof == 0))

161 return (not (eof == 0))

127

162

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−

136fpoll : File -> IO Bool

163fpoll : File -> IO Bool

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

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

138 return (p > 0)

165 return (p > 0)

139

166

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

167||| Read the contents of a file into a string

141−partial -- no error checking!

168+partial -- might be reading something infinitely long like /dev/null ...

169+covering

142−readFile : String -> IO String

170+readFile : String -> IO (Either FileError String)

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

171+readFile fn = do Right h <- openFile fn Read

172+ | Left err => return (Left err)

144 c <- readFile' h ""

173 c <- readFile' h ""

145 closeFile h

174 closeFile h

146 return c

175 return c

147 where

176 where

148 partial

177 partial

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

178+ readFile' : File -> String -> IO (Either FileError String)

150 readFile' h contents =

179 readFile' h contents =

151 do x <- feof h

180 do x <- feof h

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

181+ if not x then do Right l <- fread h

182+ | Left err => return (Left err)

153 readFile' h (contents ++ l)

183 readFile' h (contents ++ l)

154− else return contents

184+ else return (Right contents)

155−

185+

156−

186+||| Write a string to a file

187+writeFile : (filepath : String) -> (contents : String) ->

188+ IO (Either FileError ())

189+writeFile fn contents = do

190+ Right h <- openFile fn Write | Left err => return (Left err)

191+ Right () <- fwrite h contents | Left err => return (Left err)

192+ closeFile h

193+ return (Right ())

libs/prelude/Prelude/Interactive.idr+42−15

@@ -17,6 +17,7 @@ import Prelude.Show

17import Prelude.Cast

18import Prelude.Maybe

19import Prelude.Functor

20+import Prelude.Either

20import Prelude.Monad

21import Prelude.Monad

21import IO

22import IO

22

23

@@ -24,33 +25,58 @@ import IO

24

25

25---- some basic io

26---- some basic io

26

27

28+||| Output a string to stdout without a trailing newline, for any FFI

29+||| descriptor

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

31+putStr' x = do prim_write x

32+ return ()

33+

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

34||| Output a string to stdout without a trailing newline

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

35+putStr : String -> IO ()

29−putStr x = do prim_write x

36+putStr = putStr'

30− return ()

37+

38+||| Output a string to stdout with a trailing newline, for any FFI

39+||| descriptor

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

41+putStrLn' x = putStr' (x ++ "\n")

31

42

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

43||| Output a string to stdout with a trailing newline

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

44+putStrLn : String -> IO ()

45+putStrLn = putStrLn'

46+

47+||| Output something showable to stdout, without a trailing newline, for any FFI

48+||| descriptor

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

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

50+print' x = putStr' (show x)

35

51

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

52||| Output something showable to stdout, without a trailing newline

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

53+print : Show a => a -> IO ()

38−print x = putStr (show x)

54+print = print'

39

55

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

56+||| Output something showable to stdout, with a trailing newline, for any FFI

57+||| descriptor

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

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

42−printLn x = putStrLn (show x)

59+printLn' x = putStrLn' (show x)

43

60

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

62+printLn : Show a => a -> IO ()

63+printLn = printLn'

64+

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

65+||| Read one line of input from stdin, without the trailing newline, for any FFI

66+||| descriptor

45−getLine : IO' ffi String

67+getLine' : IO' ffi String

46−getLine = do x <- prim_read

68+getLine' = do x <- prim_read

47− return (reverse (trimNL (reverse x)))

69+ return (reverse (trimNL (reverse x)))

48 where trimNL : String -> String

70 where trimNL : String -> String

49 trimNL str with (strM str)

71 trimNL str with (strM str)

50 trimNL "" | StrNil = ""

72 trimNL "" | StrNil = ""

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

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

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

74 trimNL (strCons x xs) | StrCons _ _ = strCons x xs

53

75

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

77+getLine : IO String

78+getLine = getLine'

79+

54||| Write a single character to stdout

80||| Write a single character to stdout

55putChar : Char -> IO ()

81putChar : Char -> IO ()

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

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

@@ -97,7 +123,8 @@ processHandle : File ->

97processHandle h acc onRead onEOF

123processHandle h acc onRead onEOF

98 = if !(feof h)

124 = if !(feof h)

99 then putStr (onEOF acc)

125 then putStr (onEOF acc)

100− else do x <- fread h

126+ else do Right x <- fread h

127+ | Left err => putStr (onEOF acc)

101 let (out, acc') = onRead acc x

128 let (out, acc') = onRead acc x

102 putStr out

129 putStr out

103 processHandle h acc' onRead onEOF

130 processHandle h acc' onRead onEOF

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

@@ -13,7 +13,7 @@ import IO

13infixl 5 >>=

14

15class Applicative m => Monad (m : Type -> Type) where

16− (>>=) : m a -> (a -> m b) -> m b

16+ (>>=) : m a -> ((result : a) -> m b) -> m b

17

18||| Also called `join` or mu

19flatten : Monad m => m (m a) -> m a

libs/prelude/Prelude/Show.idr+5

@@ -10,6 +10,7 @@ import Prelude.Chars

10import Prelude.Classes

11import Prelude.List

12import Prelude.Maybe

13+import Prelude.Either

13import Prelude.Nat

14import Prelude.Nat

14import Prelude.Strings

15import Prelude.Strings

15

16

@@ -185,6 +186,10 @@ instance Show a => Show (Maybe a) where

185 showPrec d Nothing = "Nothing"

186 showPrec d Nothing = "Nothing"

186 showPrec d (Just x) = showCon d "Just" $ showArg x

187 showPrec d (Just x) = showCon d "Just" $ showArg x

187

188

189+instance (Show a, Show b) => Show (Either a b) where

190+ showPrec d (Left x) = showCon d "Left" $ showArg x

191+ showPrec d (Right x) = showCon d "Right" $ showArg x

192+

188instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

193instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

189 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

190

195

rts/Makefile+4−3

@@ -1,7 +1,8 @@

1include ../config.mk

2

3OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \

4− idris_opts.o idris_stats.o idris_utf8.o mini-gmp.o getline.o

4+ idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o mini-gmp.o \

5+ getline.o

5HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

6HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

6 idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \

7 idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \

7 idris_utf8.h getline.h

8 idris_utf8.h getline.h

@@ -19,10 +20,10 @@ endif

19endif

20endif

20

21

21ifeq ($(OS), windows)

22ifeq ($(OS), windows)

22− OBJS += windows/idris_stdfgn.o windows/idris_net.o windows/win_utils.o

23+ OBJS += windows/idris_net.o windows/win_utils.o

23else

24else

24 CFLAGS += -fPIC

25 CFLAGS += -fPIC

25− OBJS += idris_stdfgn.o idris_net.o

26+ OBJS += idris_net.o

26endif

27endif

27

28

28LIBTARGET = libidris_rts.a

29LIBTARGET = libidris_rts.a

rts/idris_heap.c+12−12

@@ -7,11 +7,11 @@

7

8

9/* Used for initializing the heap. */

10−void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)

10+void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)

11{

12− char * mem = malloc(heap_size);

12+ char * mem = malloc(heap_size);

13 if (mem == NULL) {

14− fprintf(stderr,

14+ fprintf(stderr,

15 "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n",

16 heap_size);

17 exit(EXIT_FAILURE);

@@ -37,8 +37,8 @@ void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)

37void free_heap(Heap * h) {

38 free(h->heap);

39

40− if (h->old != NULL) {

40+ if (h->old != NULL) {

41− free(h->old);

41+ free(h->old);

42 }

43}

44

@@ -47,7 +47,7 @@ void free_heap(Heap * h) {

47/******************** Heap testing ********************************************/

48void heap_check_underflow(Heap * heap) {

49 if (!(heap->heap <= heap->next)) {

50− fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n",

50+ fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n",

51 heap->heap, heap->next);

52 exit(EXIT_FAILURE);

53 }

@@ -55,7 +55,7 @@ void heap_check_underflow(Heap * heap) {

55

56void heap_check_overflow(Heap * heap) {

57 if (!(heap->next <= heap->end)) {

58− fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n",

58+ fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n",

59 heap->next, heap->end);

60 exit(EXIT_FAILURE);

61 }

@@ -65,13 +65,13 @@ int is_valid_ref(VAL v) {

65 return (v != NULL) && !(ISINT(v));

66}

67

68−int ref_in_heap(Heap * heap, VAL v) {

68+int ref_in_heap(Heap * heap, VAL v) {

69 return ((VAL)heap->heap <= v) && (v < (VAL)heap->next);

70}

71

72// Checks three important properties:

73// 1. Closure.

74−// Check if all pointers in the _heap_ points only to heap.

74+// Check if all pointers in the _heap_ points only to heap.

75// 2. Unidirectionality. (if compact gc)

76// All references in the heap should be are unidirectional. In other words,

77// more recently allocated closure can point only to earlier allocated one.

@@ -79,7 +79,7 @@ int ref_in_heap(Heap * heap, VAL v) {

79//

80void heap_check_pointers(Heap * heap) {

81 char* scan = NULL;

82−

82+

83 size_t item_size = 0;

84 for(scan = heap->heap; scan < heap->next; scan += item_size) {

85 item_size = *((size_t*)scan);

@@ -96,7 +96,7 @@ void heap_check_pointers(Heap * heap) {

96 if (is_valid_ref(ptr)) {

97 // Check for closure.

98 if (!ref_in_heap(heap, ptr)) {

99− fprintf(stderr,

99+ fprintf(stderr,

100 "RTS ERROR: heap closure broken. "\

101 "<HEAP %p %p %p> <REF %p>\n",

102 heap->heap, heap->next, heap->end, ptr);

@@ -105,7 +105,7 @@ void heap_check_pointers(Heap * heap) {

105#if 0 // TODO macro

106 // Check for unidirectionality.

107 if (!(ptr < heap_item)) {

108− fprintf(stderr,

108+ fprintf(stderr,

109 "RTS ERROR: heap unidirectionality broken:" \

110 "<CON %p> <FIELD %p>\n",

111 heap_item, ptr);

rts/idris_heap.h+2−2

@@ -8,7 +8,7 @@ typedef struct {

8 char* heap; // Point to bottom of heap

9 char* end; // Point to top of heap

10 size_t size; // Size of _next_ heap. Size of current heap is /end - heap/.

11− size_t growth; // Quantity of heap growth in bytes.

11+ size_t growth; // Quantity of heap growth in bytes.

12

13 char* old;

14} Heap;

@@ -23,7 +23,7 @@ void heap_check_all(Heap * heap);

23// Should be used _between_ gc's.

24#define HEAP_CHECK(vm) heap_check_all(&(vm->heap));

25#else

26−#define HEAP_CHECK(vm)

26+#define HEAP_CHECK(vm)

27#endif // IDRIS_DEBUG

28

29#endif // _IDRIS_HEAP_H

rts/idris_main.c+1

@@ -21,6 +21,7 @@ int main(int argc, char* argv[]) {

21 init_gmpalloc();

22

23 init_nullaries();

24+ init_signals();

24

25

25 _idris__123_runMain0_125_(vm, NULL);

26 _idris__123_runMain0_125_(vm, NULL);

26

27

rts/idris_net.c+21−24

@@ -38,15 +38,15 @@ void idrnet_free(void* ptr) {

38}

39

40// We call this from quite a few functions. Given a textual host and an int port,

41−// populates a struct addrinfo.

41+// populates a struct addrinfo.

42−int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,

42+int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,

43 int family, int socket_type) {

44

45 struct addrinfo hints;

46 // Convert port into string

47 char str_port[8];

48 sprintf(str_port, "%d", port);

49−

49+

50 // Set up hints structure

51 memset(&hints, 0, sizeof(hints)); // zero out hints

52 hints.ai_family = family;

@@ -57,7 +57,7 @@ int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,

57 if (strlen(host) == 0) {

58 hints.ai_flags = AI_PASSIVE; // fill in IP automatically

59 return getaddrinfo(NULL, str_port, &hints, address_res);

60− }

60+ }

61 return getaddrinfo(host, str_port, &hints, address_res);

62

63}

@@ -75,7 +75,7 @@ int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {

75 //freeaddrinfo(address_res);

76 //printf("Lib err: bind\n");

77 return -1;

78− }

78+ }

79 return 0;

80}

81

@@ -111,7 +111,7 @@ char* idrnet_sockaddr_ipv4(void* sockaddr) {

111

112int idrnet_sockaddr_ipv4_port(void* sockaddr) {

113 struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;

114− return ((int) ntohs(addr->sin_port));

114+ return ((int) ntohs(addr->sin_port));

115}

116

117void* idrnet_create_sockaddr() {

@@ -141,13 +141,13 @@ int idrnet_send_buf(int sockfd, void* data, int len) {

141}

142

143void* idrnet_recv(int sockfd, int len) {

144− idrnet_recv_result* res_struct =

144+ idrnet_recv_result* res_struct =

145 (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));

146 char* buf = malloc(len + 1);

147 memset(buf, 0, len + 1);

148 int recv_res = recv(sockfd, buf, len, 0);

149 res_struct->result = recv_res;

150−

150+

151 if (recv_res > 0) { // Data was received

152 buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it

153 }

@@ -172,7 +172,7 @@ char* idrnet_get_recv_payload(void* res_struct) {

172}

173

174void idrnet_free_recv_struct(void* res_struct) {

175− idrnet_recv_result* i_res_struct =

175+ idrnet_recv_result* i_res_struct =

176 (idrnet_recv_result*) res_struct;

177 if (i_res_struct->payload != NULL) {

178 free(i_res_struct->payload);

@@ -191,9 +191,9 @@ int idrnet_sendto(int sockfd, char* data, char* host, int port, int family) {

191 int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);

192 if (addr_res == -1) {

193 return -1;

194− }

194+ }

195

196− int send_res = sendto(sockfd, data, strlen(data), 0,

196+ int send_res = sendto(sockfd, data, strlen(data), 0,

197 remote_host->ai_addr, remote_host->ai_addrlen);

198 freeaddrinfo(remote_host);

199 return send_res;

@@ -206,11 +206,11 @@ int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port,

206 if (addr_res == -1) {

207 //printf("lib err: sendto getaddrinfo \n");

208 return -1;

209− }

209+ }

210

211 buf_htonl(buf, buf_len);

212

213− int send_res = sendto(sockfd, buf, buf_len, 0,

213+ int send_res = sendto(sockfd, buf, buf_len, 0,

214 remote_host->ai_addr, remote_host->ai_addrlen);

215 if (send_res == -1) {

216 perror("lib err: sendto \n");

@@ -224,13 +224,13 @@ int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port,

224void* idrnet_recvfrom(int sockfd, int len) {

225/*

226 * int recvfrom(int sockfd, void *buf, int len, unsigned int flags,

227− struct sockaddr *from, int *fromlen);

227+ struct sockaddr *from, int *fromlen);

228*/

229 // Allocate the required structures, and nuke them

230− struct sockaddr_storage* remote_addr =

230+ struct sockaddr_storage* remote_addr =

231 (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));

232 char* buf = (char*) malloc(len + 1);

233− idrnet_recvfrom_result* ret =

233+ idrnet_recvfrom_result* ret =

234 (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));

235 memset(remote_addr, 0, sizeof(struct sockaddr_storage));

236 memset(buf, 0, len + 1);

@@ -240,7 +240,7 @@ void* idrnet_recvfrom(int sockfd, int len) {

240 int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);

241 ret->result = recv_res;

242 // Check for failure...

243− if (recv_res == -1) {

243+ if (recv_res == -1) {

244 free(buf);

245 free(remote_addr);

246 } else {

@@ -255,12 +255,11 @@ void* idrnet_recvfrom(int sockfd, int len) {

255 return ret;

256}

257

258−

259void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {

258void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {

260 // Allocate the required structures, and nuke them

259 // Allocate the required structures, and nuke them

261− struct sockaddr_storage* remote_addr =

260+ struct sockaddr_storage* remote_addr =

262 (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));

261 (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));

263− idrnet_recvfrom_result* ret =

262+ idrnet_recvfrom_result* ret =

264 (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));

263 (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));

265 memset(remote_addr, 0, sizeof(struct sockaddr_storage));

264 memset(remote_addr, 0, sizeof(struct sockaddr_storage));

266 memset(ret, 0, sizeof(idrnet_recvfrom_result));

265 memset(ret, 0, sizeof(idrnet_recvfrom_result));

@@ -269,7 +268,7 @@ void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {

269 int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);

268 int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);

270 // Check for failure... But don't free the buffer! Not our job.

269 // Check for failure... But don't free the buffer! Not our job.

271 ret->result = recv_res;

270 ret->result = recv_res;

272− if (recv_res == -1) {

271+ if (recv_res == -1) {

273 free(remote_addr);

272 free(remote_addr);

274 }

273 }

275 // Payload will be NULL -- since it's been put into the user-specified buffer. We

274 // Payload will be NULL -- since it's been put into the user-specified buffer. We

@@ -298,7 +297,7 @@ void* idrnet_get_recvfrom_sockaddr(void* res_struct) {

298int idrnet_get_recvfrom_port(void* res_struct) {

297int idrnet_get_recvfrom_port(void* res_struct) {

299 idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;

298 idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;

300 if (recv_struct->remote_addr != NULL) {

299 if (recv_struct->remote_addr != NULL) {

301− struct sockaddr_in* remote_addr_in =

300+ struct sockaddr_in* remote_addr_in =

302 (struct sockaddr_in*) recv_struct->remote_addr;

301 (struct sockaddr_in*) recv_struct->remote_addr;

303 return ((int) ntohs(remote_addr_in->sin_port));

302 return ((int) ntohs(remote_addr_in->sin_port));

304 }

303 }

@@ -316,5 +315,3 @@ void idrnet_free_recvfrom_struct(void* res_struct) {

316 }

315 }

317 }

316 }

318}

317}

319−

320−

rts/idris_rts.c+16

@@ -1,4 +1,5 @@

1#include <assert.h>

2+#include <errno.h>

2

3

3#include "idris_rts.h"

4#include "idris_rts.h"

4#include "idris_gc.h"

5#include "idris_gc.h"

@@ -72,6 +73,7 @@ VM* idris_vm() {

72 init_threaddata(vm);

73 init_threaddata(vm);

73 init_gmpalloc();

74 init_gmpalloc();

74 init_nullaries();

75 init_nullaries();

76+ init_signals();

75

77

76 return vm;

78 return vm;

77}

79}

@@ -92,6 +94,12 @@ void init_threaddata(VM *vm) {

92#endif

94#endif

93}

95}

94

96

97+void init_signals() {

98+#if (__linux__ || __APPLE__ || __FreeBSD__)

99+ signal(SIGPIPE, SIG_IGN);

100+#endif

101+}

102+

95Stats terminate(VM* vm) {

103Stats terminate(VM* vm) {

96 Stats stats = vm->stats;

104 Stats stats = vm->stats;

97 STATS_ENTER_EXIT(stats)

105 STATS_ENTER_EXIT(stats)

@@ -927,6 +935,14 @@ void idris_freeMsg(Msg* msg) {

927 free(msg);

935 free(msg);

928}

936}

929

937

938+int idris_errno() {

939+ return errno;

940+}

941+

942+char* idris_showerror(int err) {

943+ return strerror(err);

944+}

945+

930VAL* nullary_cons;

946VAL* nullary_cons;

931

947

932void init_nullaries() {

948void init_nullaries() {

rts/idris_rts.h+8

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

9#include <pthread.h>

10#endif

11#include <stdint.h>

12+#if (__linux__ || __APPLE__ || __FreeBSD__)

13+#include <signal.h>

14+#endif

12

15

13#include "idris_heap.h"

16#include "idris_heap.h"

14#include "idris_stats.h"

17#include "idris_stats.h"

@@ -252,10 +255,15 @@ void idris_free(void* ptr, size_t size);

252

255

253#define NULL_CON(x) nullary_cons[x]

256#define NULL_CON(x) nullary_cons[x]

254

257

258+int idris_errno();

259+char* idris_showerror(int err);

260+

255extern VAL* nullary_cons;

261extern VAL* nullary_cons;

256void init_nullaries();

262void init_nullaries();

257void free_nullaries();

263void free_nullaries();

258

264

265+void init_signals();

266+

259void* vmThread(VM* callvm, func f, VAL arg);

267void* vmThread(VM* callvm, func f, VAL arg);

260

268

261// Copy a structure to another vm's heap

269// Copy a structure to another vm's heap

rts/idris_stdfgn.c+36−6

@@ -2,11 +2,18 @@

2#include "idris_rts.h"

3#include "idris_gmp.h"

4#include "idris_gc.h"

5−#include <sys/select.h>

5+

6#include <fcntl.h>

7+#include <errno.h>

7#include <stdio.h>

8#include <stdio.h>

8#include <time.h>

9#include <time.h>

9

10

11+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)

12+int win_fpoll(void* h);

13+#else

14+#include <sys/select.h>

15+#endif

16+

10extern char** environ;

17extern char** environ;

11

18

12void putStr(char* str) {

19void putStr(char* str) {

@@ -24,13 +31,13 @@ void fileClose(void* h) {

24}

31}

25

32

26int fileEOF(void* h) {

33int fileEOF(void* h) {

27− FILE* f = (FILE*)h;

34+ FILE* f = (FILE*)h;

28− return feof(f);

35+ return feof(f);

29}

36}

30

37

31int fileError(void* h) {

38int fileError(void* h) {

32− FILE* f = (FILE*)h;

39+ FILE* f = (FILE*)h;

33− return ferror(f);

40+ return ferror(f);

34}

41}

35

42

36int idris_writeStr(void* h, char* str) {

43int idris_writeStr(void* h, char* str) {

@@ -44,6 +51,9 @@ int idris_writeStr(void* h, char* str) {

44

51

45int fpoll(void* h)

52int fpoll(void* h)

46{

53{

54+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)

55+ return win_fpoll(h);

56+#else

47 FILE* f = (FILE*)h;

57 FILE* f = (FILE*)h;

48 fd_set x;

58 fd_set x;

49 struct timeval timeout;

59 struct timeval timeout;

@@ -56,6 +66,7 @@ int fpoll(void* h)

56

66

57 int r = select(fd+1, &x, 0, 0, &timeout);

67 int r = select(fd+1, &x, 0, 0, &timeout);

58 return r;

68 return r;

69+#endif

59}

70}

60

71

61void* do_popen(const char* cmd, const char* mode) {

72void* do_popen(const char* cmd, const char* mode) {

@@ -86,6 +97,25 @@ VAL idris_time() {

86 return MKBIGI(t);

97 return MKBIGI(t);

87}

98}

88

99

100+VAL idris_mkFileError(VM* vm) {

101+ VAL result;

102+ switch(errno) {

103+ // Make sure this corresponds to the FileError structure in

104+ // Prelude.File

105+ case ENOENT:

106+ idris_constructor(result, vm, 2, 0, 0);

107+ break;

108+ case EACCES:

109+ idris_constructor(result, vm, 3, 0, 0);

110+ break;

111+ default:

112+ idris_constructor(result, vm, 4, 1, 0);

113+ idris_setConArg(result, 0, MKINT((intptr_t)errno));

114+ break;

115+ }

116+ return result;

117+}

118+

89void idris_forceGC(void* vm) {

119void idris_forceGC(void* vm) {

90− idris_gc((VM*)vm);

120+ idris_gc((VM*)vm);

91}

121}

rts/idris_stdfgn.h+2

@@ -14,6 +14,8 @@ int fileEOF(void* h);

14int fileError(void* h);

15// return 0 on success

16int idris_writeStr(void*h, char* str);

17+// construct a file error structure (see Prelude.File) from errno

18+VAL idris_mkFileError(VM* vm);

17

19

18void* do_popen(const char* cmd, const char* mode);

20void* do_popen(const char* cmd, const char* mode);

19int fpoll(void* h);

21int fpoll(void* h);

rts/windows/idris_net.c+6−7

@@ -12,7 +12,7 @@

12#include <Ws2tcpip.h>

13

14

15−// inet_ntop isn't defined in the old mingw delivered with GHC,

15+// inet_ntop isn't defined in the old mingw delivered with GHC,

16// so put the prototype here, cribbed from a newer version of it

17WINSOCK_API_LINKAGE LPCSTR WSAAPI InetNtopA(INT Family, PVOID pAddr,

18 LPSTR pStringBuf, size_t StringBufSize);

@@ -50,7 +50,7 @@ int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {

50 // Convert port into string

51 char str_port[8];

52 sprintf(str_port, "%d", port);

53−

53+

54 if (!check_init()) {

55 return -1;

56 }

@@ -73,7 +73,7 @@ int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {

73 int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);

74 if (bind_res == -1) {

75 return -1;

76− }

76+ }

77

78 return 0;

79}

@@ -152,13 +152,13 @@ void* idrnet_recv(int sockfd, int len) {

152 if (!check_init()) {

153 return NULL;

154 }

155− idrnet_recv_result* res_struct =

155+ idrnet_recv_result* res_struct =

156 (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));

157

158 char* buf = malloc(len + 1);

159 int recv_res = recv(sockfd, buf, len, 0);

160 res_struct->result = recv_res;

161−

161+

162 if (recv_res > 0) { // Data was received

163 buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it

164 }

@@ -182,7 +182,7 @@ char* idrnet_get_recv_payload(void* res_struct) {

182}

183

184void idrnet_free_recv_struct(void* res_struct) {

185− idrnet_recv_result* i_res_struct =

185+ idrnet_recv_result* i_res_struct =

186 (idrnet_recv_result*) res_struct;

187 if (i_res_struct->payload != NULL) {

188 free(i_res_struct->payload);

@@ -193,4 +193,3 @@ void idrnet_free_recv_struct(void* res_struct) {

193int idrnet_errno() {

194 return errno;

195}

196−

rts/windows/idris_stdfgn.cdeleted−82

@@ -1,82 +0,0 @@

1−#include "../idris_stdfgn.h"

2−#include "../idris_rts.h"

3−#include "../idris_gc.h"

4−

5−#include <fcntl.h>

6−#include <stdio.h>

7−#include <time.h>

8−#include <io.h>

9−

10−extern char** environ;

11−

12−int win_fpoll(void* h);

13−

14−void putStr(char* str) {

15− printf("%s", str);

16−}

17−

18−void* fileOpen(char* name, char* mode) {

19− FILE* f = fopen(name, mode);

20− return (void*)f;

21−}

22−

23−void fileClose(void* h) {

24− FILE* f = (FILE*)h;

25− fclose(f);

26−}

27−

28−int fileEOF(void* h) {

29− FILE* f = (FILE*)h;

30− return feof(f);

31−}

32−

33−int fileError(void* h) {

34− FILE* f = (FILE*)h;

35− return ferror(f);

36−}

37−

38−int idris_writeStr(void* h, char* str) {

39− FILE* f = (FILE*)h;

40− if (fputs(str, f)) {

41− return 0;

42− } else {

43− return -1;

44− }

45−}

46−

47−int fpoll(void* h)

48−{

49− return win_fpoll(h);

50−}

51−

52−void* do_popen(const char* cmd, const char* mode) {

53− FILE* f = _popen(cmd, mode);

54−// int d = fileno(f);

55−// fcntl(d, F_SETFL, O_NONBLOCK);

56− return f;

57−}

58−

59−int isNull(void* ptr) {

60− return ptr==NULL;

61−}

62−

63−int idris_eqPtr(void* x, void* y) {

64− return x==y;

65−}

66−

67−void* idris_stdin() {

68− return (void*)stdin;

69−}

70−

71−char* getEnvPair(int i) {

72− return *(environ + i);

73−}

74−

75−VAL idris_time() {

76− time_t t = time(NULL);

77− return MKBIGI(t);

78−}

79−

80−void idris_forceGC(void* vm) {

81− idris_gc((VM*)vm);

82−}

src/Idris/AbsSyntax.hs+7−3

@@ -1393,7 +1393,11 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1393 = (n, (p, t)) : collectImps sc

1394 collectImps _ = []

1395

1396+ scopedimpl (Just i) = not (toplevel_imp i)

1397+ scopedimpl _ = False

1398+

1396− getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps

1399+ getImps (Bind n (Pi i _ _) sc) imps

1400+ | scopedimpl i = getImps sc imps

1397 getImps (Bind n (Pi _ t _) sc) imps

1401 getImps (Bind n (Pi _ t _) sc) imps

1398 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1402 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1399 where

1403 where

@@ -1556,9 +1560,9 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1556 pibind using [] sc = sc

1560 pibind using [] sc = sc

1557 pibind using (n:ns) sc

1561 pibind using (n:ns) sc

1558 = case lookup n using of

1562 = case lookup n using of

1559− Just ty -> PPi (Imp [] Dynamic False Nothing)

1563+ Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))

1560 n NoFC ty (pibind using ns sc)

1564 n NoFC ty (pibind using ns sc)

1561− Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)

1565+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))

1562 n NoFC Placeholder (pibind using ns sc)

1566 n NoFC Placeholder (pibind using ns sc)

1563

1567

1564-- Add implicit arguments in function calls

1568-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+3−3

@@ -587,9 +587,9 @@ is_scoped :: Plicity -> Maybe ImplicitInfo

587is_scoped (Imp _ _ _ s) = s

588is_scoped _ = Nothing

589

590−impl = Imp [] Dynamic False Nothing

590+impl = Imp [] Dynamic False (Just (Impl False True))

591−forall_imp = Imp [] Dynamic False (Just (Impl False))

591+forall_imp = Imp [] Dynamic False (Just (Impl False False))

592−forall_constraint = Imp [] Dynamic False (Just (Impl True))

592+forall_constraint = Imp [] Dynamic False (Just (Impl True False))

593expl = Exp [] Dynamic False

594expl_param = Exp [] Dynamic True

595constraint = Constraint [] Static

src/Idris/CaseSplit.hs+47−27

@@ -50,8 +50,11 @@ names over '_', patterns over names, etc.

50-}

51

52-- Given a variable to split, and a term application, return a list of

53−-- variable updates

53+-- variable updates, paired with a flag to say whether the given update

54+-- typechecks (False = impossible)

55+-- if the flag is 'False' the splits should be output with the 'impossible'

56+-- flag, otherwise they should be output as normal

54−split :: Name -> PTerm -> Idris [[(Name, PTerm)]]

57+split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])

55split n t'

58split n t'

56 = do ist <- getIState

59 = do ist <- getIState

57 -- Make sure all the names in the term are accessible

60 -- Make sure all the names in the term are accessible

@@ -77,15 +80,26 @@ split n t'

77 logLvl 4 ("Working from " ++ show t)

80 logLvl 4 ("Working from " ++ show t)

78 logLvl 4 ("Trying " ++ showSep "\n"

81 logLvl 4 ("Trying " ++ showSep "\n"

79 (map (showTmImpls) newPats_in))

82 (map (showTmImpls) newPats_in))

80− newPats <- mapM elabNewPat newPats_in

83+ newPats_in <- mapM elabNewPat newPats_in

84+ case anyValid [] [] newPats_in of

85+ Left fails -> do

86+ let fails' = mergeAllPats ist n t fails

87+ return (False, (map snd fails'))

88+ Right newPats -> do

81− logLvl 3 ("Original:\n" ++ show t)

89+ logLvl 3 ("Original:\n" ++ show t)

82− logLvl 3 ("Split:\n" ++

90+ logLvl 3 ("Split:\n" ++

83− (showSep "\n" (map show (mapMaybe id newPats))))

91+ (showSep "\n" (map show newPats)))

84− logLvl 3 "----"

92+ logLvl 3 "----"

85− let newPats' = mergeAllPats ist n t (mapMaybe id newPats)

93+ let newPats' = mergeAllPats ist n t newPats

86− logLvl 1 ("Name updates " ++ showSep "\n"

94+ logLvl 1 ("Name updates " ++ showSep "\n"

87− (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))

95+ (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))

88− return (map snd newPats')

96+ return (True, (map snd newPats'))

97+ where

98+ anyValid ok bad [] = if null ok then Left (reverse bad)

99+ else Right (reverse ok)

100+ anyValid ok bad ((tc, p) : ps)

101+ | tc = anyValid (p : ok) bad ps

102+ | otherwise = anyValid ok (p : bad) ps

89

103

90data MergeState = MS { namemap :: [(Name, Name)],

104data MergeState = MS { namemap :: [(Name, Name)],

91 invented :: [(Name, Name)],

105 invented :: [(Name, Name)],

@@ -208,13 +222,13 @@ tidy ist tm ty = return tm

208-- where tidyVar (PRef _ _) = Placeholder

222-- where tidyVar (PRef _ _) = Placeholder

209-- tidyVar t = t

223-- tidyVar t = t

210

224

211−elabNewPat :: PTerm -> Idris (Maybe PTerm)

225+elabNewPat :: PTerm -> Idris (Bool, PTerm)

212elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

226elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

213 i <- getIState

227 i <- getIState

214− return (Just (delab i tm)))

228+ return (True, delab i tm))

215 (\e -> do i <- getIState

229 (\e -> do i <- getIState

216 logLvl 5 $ "Not a valid split:\n" ++ pshow i e

230 logLvl 5 $ "Not a valid split:\n" ++ pshow i e

217− return Nothing)

231+ return (False, t))

218

232

219findPats :: IState -> Type -> [PTerm]

233findPats :: IState -> Type -> [PTerm]

220findPats ist t | (P _ n _, _) <- unApply t

234findPats ist t | (P _ n _, _) <- unApply t

@@ -248,26 +262,27 @@ replaceVar ctxt n t pat = pat

248splitOnLine :: Int -- ^ line number

262splitOnLine :: Int -- ^ line number

249 -> Name -- ^ variable

263 -> Name -- ^ variable

250 -> FilePath -- ^ name of file

264 -> FilePath -- ^ name of file

251− -> Idris [[(Name, PTerm)]]

265+ -> Idris (Bool, [[(Name, PTerm)]])

252splitOnLine l n fn = do

266splitOnLine l n fn = do

253−-- let (before, later) = splitAt (l-1) (lines inp)

254−-- i <- getIState

255 cl <- getInternalApp fn l

267 cl <- getInternalApp fn l

256 logLvl 3 ("Working with " ++ showTmImpls cl)

268 logLvl 3 ("Working with " ++ showTmImpls cl)

257 tms <- split n cl

269 tms <- split n cl

258−-- iputStrLn (showSep "\n" (map show tms))

259− return tms -- "" -- not yet done...

270+ return tms

260

271

261−replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]

272+replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]

273+replaceSplits l ups impossible

262−replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

274+ = updateRHSs 1 (map (rep (expandBraces l)) ups)

263 where

275 where

264 rep str [] = str ++ "\n"

276 rep str [] = str ++ "\n"

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

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

266

278

267 updateRHSs i [] = return []

279 updateRHSs i [] = return []

280+ updateRHSs i (x : xs)

281+ | impossible = do xs' <- updateRHSs i xs

282+ return (setImpossible False x : xs')

268− updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x

283+ | otherwise = do (x', i') <- updateRHS (null xs) i x

269− xs' <- updateRHSs i' xs

284+ xs' <- updateRHSs i' xs

270− return (x' : xs')

285+ return (x' : xs')

271

286

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

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

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

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

@@ -283,6 +298,11 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

283 return (x : xs', i')

298 return (x : xs', i')

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

299 updateRHS last i [] = return ("", i)

285

300

301+ setImpossible brace ('}':xs) = '}' : setImpossible False xs

302+ setImpossible brace ('{':xs) = '{' : setImpossible True xs

303+ setImpossible False ('=':xs) = "impossible\n"

304+ setImpossible brace (x : xs) = x : setImpossible brace xs

305+ setImpossible brace [] = ""

286

306

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

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

288 -- this isn't supported in a pattern, so special case here

308 -- this isn't supported in a pattern, so special case here

@@ -342,7 +362,7 @@ getClause :: Int -- ^ line number that the type is declared on

342 -> Idris String

362 -> Idris String

343getClause l fn un fp

363getClause l fn un fp

344 = do i <- getIState

364 = do i <- getIState

345− case lookupCtxt fn (idris_classes i) of

365+ case lookupCtxt un (idris_classes i) of

346 [c] -> return (mkClassBodies i (class_methods c))

366 [c] -> return (mkClassBodies i (class_methods c))

347 _ -> do ty_in <- getInternalApp fp l

367 _ -> do ty_in <- getInternalApp fp l

348 let ty = case ty_in of

368 let ty = case ty_in of

@@ -434,8 +454,8 @@ nameMissing ps = do ist <- get

434

454

435 nm ptm = do mptm <- elabNewPat ptm

455 nm ptm = do mptm <- elabNewPat ptm

436 case mptm of

456 case mptm of

437− Nothing -> return ptm

457+ (False, _) -> return ptm

438− Just ptm' -> return ptm'

458+ (True, ptm') -> return ptm'

439

459

440

460

441

461

src/Idris/Completion.hs+2−8

@@ -12,7 +12,7 @@ import Idris.Colours

12import Idris.ParseHelpers(opChars)

13import qualified Idris.ParseExpr (constants, tactics)

14import Idris.ParseExpr (TacticArg (..))

15−import Idris.REPLParser (allHelp)

15+import Idris.REPLParser (allHelp, setOptions)

16import Control.Monad.State.Strict

17

18import Data.List

@@ -82,13 +82,7 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

82

83completeOption :: CompletionFunc Idris

84completeOption = completeWord Nothing " \t" completeOpt

85− where completeOpt = return . completeWith [ "errorcontext"

85+ where completeOpt = return . completeWith (map fst setOptions)

86− , "showimplicits"

87− , "originalerrors"

88− , "autosolve"

89− , "nobanner"

90− , "desugarnats"

91− ]

92

86

93completeConsoleWidth :: CompletionFunc Idris

87completeConsoleWidth :: CompletionFunc Idris

94completeConsoleWidth = completeWord Nothing " \t" completeW

88completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/Core/Binary.hs+3−2

@@ -484,10 +484,11 @@ instance Binary Raw where

484instance Binary ImplicitInfo where

485 put x

486 = case x of

487− Impl x1 -> put x1

487+ Impl x1 x2 -> do put x1; put x2

488 get

489 = do x1 <- get

490+ x2 <- get

490− return (Impl x1)

491+ return (Impl x1 x2)

491

492

492instance (Binary b) => Binary (Binder b) where

493instance (Binary b) => Binary (Binder b) where

493 put x

494 put x

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

@@ -167,7 +167,7 @@ instance NFData ErrorReportPart where

167 rnf (SubReport x1) = rnf x1 `seq` ()

168

169instance NFData ImplicitInfo where

170− rnf (Impl x1) = rnf x1 `seq` ()

170+ rnf (Impl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

171

172instance (NFData b) => NFData (Binder b) where

173 rnf (Lam x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+52−3

@@ -353,6 +353,9 @@ claimFn n bn t = processTactic' (ClaimFn n bn t)

353unifyGoal :: Raw -> Elab' aux ()

354unifyGoal t = processTactic' (UnifyGoal t)

355

356+unifyTerms :: Raw -> Raw -> Elab' aux ()

357+unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)

358+

356exact :: Raw -> Elab' aux ()

359exact :: Raw -> Elab' aux ()

357exact t = processTactic' (Exact t)

360exact t = processTactic' (Exact t)

358

361

@@ -724,7 +727,12 @@ checkPiGoal n

724 focus f

727 focus f

725

728

726simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

729simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

727−simple_app infer fun arg str =

730+simple_app infer fun arg str =

731+ try (dep_app fun arg str)

732+ (infer_app infer fun arg str)

733+

734+infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

735+infer_app infer fun arg str =

728 do a <- getNameFrom (sMN 0 "__argTy")

736 do a <- getNameFrom (sMN 0 "__argTy")

729 b <- getNameFrom (sMN 0 "__retTy")

737 b <- getNameFrom (sMN 0 "__retTy")

730 f <- getNameFrom (sMN 0 "f")

738 f <- getNameFrom (sMN 0 "f")

@@ -755,8 +763,49 @@ simple_app infer fun arg str =

755 when (a `elem` hs) $ do movelast a

763 when (a `elem` hs) $ do movelast a

756 when (b `elem` hs) $ do movelast b

764 when (b `elem` hs) $ do movelast b

757 end_unify

765 end_unify

758− where

766+

759− regretWith err = try regret (lift $ tfail err)

767+dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

768+dep_app fun arg str =

769+ do a <- getNameFrom (sMN 0 "__argTy")

770+ b <- getNameFrom (sMN 0 "__retTy")

771+ fty <- getNameFrom (sMN 0 "__fnTy")

772+ f <- getNameFrom (sMN 0 "f")

773+ s <- getNameFrom (sMN 0 "s")

774+ claim a RType

775+ claim fty RType

776+ claim f (Var fty)

777+ tm <- get_term

778+ g <- goal

779+ start_unify s

780+ claim s (Var a)

781+

782+ prep_fill f [s]

783+ focus f; attack; fun

784+ end_unify

785+ fty <- goal

786+ solve

787+ focus s; attack;

788+ ctxt <- get_context

789+ env <- get_env

790+ case normalise ctxt env fty of

791+ -- if f gives a function type, unify our argument type with

792+ -- f's expected argument type

793+ Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)

794+ -- Can't infer a type for 'f', so fail here (and drop back to

795+ -- simply typed application where we infer the type for f)

796+ _ -> fail "Can't make type"

797+ end_unify

798+ arg

799+ solve

800+ complete_fill

801+

802+ -- We don't need a and b in the hole queue any more since they were

803+ -- just for checking f, so move them to the end. If they never end up

804+ -- getting solved, we'll get an 'Incomplete term' error.

805+ hs <- get_holes

806+ when (a `elem` hs) $ do movelast a

807+ when (b `elem` hs) $ do movelast b

808+ end_unify

760

809

761-- Abstract over an argument of unknown type, giving a name for the hole

810-- Abstract over an argument of unknown type, giving a name for the hole

762-- which we'll fill with the argument type too.

811-- which we'll fill with the argument type too.

src/Idris/Core/Evaluate.hs+10−1

@@ -2,7 +2,8 @@

2 PatternGuards #-}

3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

4

5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,

5+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

6+ normaliseAll, normaliseBlocking, toValue, quoteTerm,

6 rt_simplify, simplify, specialise, hnf, convEq, convEq',

7 rt_simplify, simplify, specialise, hnf, convEq, convEq',

7 Def(..), CaseInfo(..), CaseDefs(..),

8 Def(..), CaseInfo(..), CaseDefs(..),

8 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

9 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

@@ -79,11 +80,19 @@ normaliseC ctxt env t

79 = evalState (do val <- eval False ctxt [] (map finalEntry env) t []

80 = evalState (do val <- eval False ctxt [] (map finalEntry env) t []

80 quote 0 val) initEval

81 quote 0 val) initEval

81

82

83+-- | Normalise everything, whether abstract, private or public

82normaliseAll :: Context -> Env -> TT Name -> TT Name

84normaliseAll :: Context -> Env -> TT Name -> TT Name

83normaliseAll ctxt env t

85normaliseAll ctxt env t

84 = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]

86 = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]

85 quote 0 val) initEval

87 quote 0 val) initEval

86

88

89+-- | As normaliseAll, but with an explicit list of names *not* to reduce

90+normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name

91+normaliseBlocking ctxt env blocked t

92+ = evalState (do val <- eval False ctxt (map (\n -> (n, 0)) blocked)

93+ (map finalEntry env) t [AtREPL]

94+ quote 0 val) initEval

95+

87normalise :: Context -> Env -> TT Name -> TT Name

96normalise :: Context -> Env -> TT Name -> TT Name

88normalise = normaliseTrace False

97normalise = normaliseTrace False

89

98

src/Idris/Core/Execute.hs+11

@@ -349,6 +349,17 @@ execForeign env ctxt arity ty fn xs onfail

349 "The argument to fileEOF should be a file handle, but it was " ++

350 show handle ++

351 ". Are all cases covered?"

352+ | Just (FFun "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs

353+ = case handle of

354+ -- errors handled differently in Haskell than in C, so if

355+ -- there's been an error we'll have had an exception already.

356+ -- Therefore, assume we're okay.

357+ EHandle h -> do let res = ioWrap (EConstant (I 0))

358+ execApp env ctxt res (drop arity xs)

359+ _ -> execFail . Msg $

360+ "The argument to fileError should be a file handle, but it was " ++

361+ show handle ++

362+ ". Are all cases covered?"

352 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs

363 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs

353 = case handle of

364 = case handle of

354 EHandle h -> do execIO $ hClose h

365 EHandle h -> do execIO $ hClose h

src/Idris/Core/ProofState.hs+10

@@ -91,6 +91,7 @@ data Tactic = Attack

91 | MatchProblems Bool

92 | UnifyProblems

93 | UnifyGoal Raw

94+ | UnifyTerms Raw Raw

94 | ProofState

95 | ProofState

95 | Undo

96 | Undo

96 | QED

97 | QED

@@ -477,6 +478,13 @@ unifyGoal tm ctxt env h@(Bind x b sc) =

477 return h

478 return h

478unifyGoal _ _ _ _ = fail "The focus is not a binder."

479unifyGoal _ _ _ _ = fail "The focus is not a binder."

479

480

481+unifyTerms :: Raw -> Raw -> RunTactic

482+unifyTerms tm1 tm2 ctxt env h =

483+ do (tm1v, _) <- lift $ check ctxt env tm1

484+ (tm2v, _) <- lift $ check ctxt env tm2

485+ ns' <- unify' ctxt env (tm1v, Nothing) (tm2v, Nothing)

486+ return h

487+

480exact :: Raw -> RunTactic

488exact :: Raw -> RunTactic

481exact guess ctxt env (Bind x (Hole ty) sc) =

489exact guess ctxt env (Bind x (Hole ty) sc) =

482 do (val, valty) <- lift $ check ctxt env guess

490 do (val, valty) <- lift $ check ctxt env guess

@@ -1113,3 +1121,5 @@ process t h = tactic (Just h) (mktac t)

1113 mktac (SetInjective n) = setinj n

1121 mktac (SetInjective n) = setinj n

1114 mktac (MoveLast n) = movelast n

1122 mktac (MoveLast n) = movelast n

1115 mktac (UnifyGoal r) = unifyGoal r

1123 mktac (UnifyGoal r) = unifyGoal r

1124+ mktac (UnifyTerms x y) = unifyTerms x y

1125+

src/Idris/Core/TT.hs+2−2

@@ -811,7 +811,7 @@ deriving instance Binary Raw

811deriving instance NFData Raw

812!-}

813

814−data ImplicitInfo = Impl { tcinstance :: Bool }

814+data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool }

815 deriving (Show, Eq, Ord, Data, Typeable)

816

817{-!

@@ -1612,7 +1612,7 @@ pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

1612 pureBinder (Let t v) = pureTerm t && pureTerm v

1613 pureBinder t = pureTerm (binderTy t)

1614

1615− notClassName (MN _ c) | c == txt "class" = False

1615+ notClassName (MN _ c) | c == txt "__class" = False

1616 notClassName _ = True

1617

1618pureTerm _ = True

src/Idris/DSL.hs+4−1

@@ -108,7 +108,10 @@ expandSugar dsl (PDoBlock ds)

108 block b (DoExp fc tm : rest)

109 = PApp fc b

110 [pexp tm,

111− pexp (PLam fc (sMN 0 "bindx") NoFC Placeholder (block b rest))]

111+ pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]

112+ where mkTy (PCase _ _ _) = PRef fc [] unitTy

113+ mkTy (PMetavar _ _) = PRef fc [] unitTy

114+ mkTy _ = Placeholder

112 block b _ = PElabError (Msg "Invalid statement in do block")

115 block b _ = PElabError (Msg "Invalid statement in do block")

113

116

114expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

117expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

src/Idris/Delaborate.hs+3

@@ -110,6 +110,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

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)

113+ de env (_ : is) (Bind n (Pi (Just impl) ty _) sc)

114+ | toplevel_imp impl -- information in 'imps' repeated

115+ = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)

113 de env is (Bind n (Pi (Just impl) ty _) sc)

116 de env is (Bind n (Pi (Just impl) ty _) sc)

114 | tcinstance impl

117 | tcinstance impl

115 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

118 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

src/Idris/Elab/Class.hs+1−1

@@ -258,7 +258,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

258 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

259 insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)

260 = PPi p n fc ty (insertConstraint c all sc)

261− insertConstraint c all sc = let dictN = sMN 0 "class"

261+ insertConstraint c all sc = let dictN = sMN 0 "__class"

262 in PPi (constraint { pstatic = Static })

263 dictN NoFC c

264 (constrainMeths (map basename all)

src/Idris/Elab/Clause.hs+10−22

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

551 -- pattern bindings

552 i <- getIState

553 inf <- isTyInferred fname

554+

555+ -- Check if we have "with" patterns outside of "with" block

556+ when (isOutsideWith lhs_in && (not $ null withs)) $

557+ ierror $ (At fc (Elaborating "left hand side of " fname Nothing

558+ (Msg "unexpected patterns outside of \"with\" block")))

559+

554 -- get the parameters first, to pass through to any where block

560 -- get the parameters first, to pass through to any where block

555 let fn_ty = case lookupTy fname (tt_ctxt i) of

561 let fn_ty = case lookupTy fname (tt_ctxt i) of

556 [t] -> t

562 [t] -> t

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

663 (erun fc (build i winfo ERHS opts fname rhs))

669 (erun fc (build i winfo ERHS opts fname rhs))

664 errAt "right hand side of " fname (Just clhsty)

670 errAt "right hand side of " fname (Just clhsty)

665 (erun fc $ psolve lhs_tm)

671 (erun fc $ psolve lhs_tm)

666− hs <- get_holes

667− mapM_ (elabCaseHole is) hs

668 tt <- get_term

672 tt <- get_term

669 aux <- getAux

673 aux <- getAux

670 let (tm, ds) = runState (collectDeferred (Just fname)

674 let (tm, ds) = runState (collectDeferred (Just fname)

@@ -782,26 +786,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

782 (b : bf, af)

786 (b : bf, af)

783 sepBlocks' ns [] = ([], [])

787 sepBlocks' ns [] = ([], [])

784

788

785−

789+ -- term is not within "with" block

786− -- if a hole is just an argument/result of a case block, treat it as

790+ isOutsideWith :: PTerm -> Bool

787− -- the unit type. Hack to help elaborate case in do blocks.

791+ isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False

788− elabCaseHole aux h = do

792+ isOutsideWith _ = True

789− focus h

790− g <- goal

791− case g of

792− TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve

793− _ -> return ()

794−

795− -- Is the name a pattern argument in the declaration

796− isArg :: Name -> PDecl -> Bool

797− isArg n (PClauses _ _ _ cs) = any isArg' cs

798− where

799− isArg' (PClause _ _ (PApp _ _ args) _ _ _)

800− = any (\x -> case x of

801− PRef _ _ n' -> n == n'

802− _ -> False) (map getTm args)

803− isArg' _ = False

804− isArg _ _ = False

805

793

806elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

794elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

807 = do let tcgen = Dictionary `elem` opts

795 = do let tcgen = Dictionary `elem` opts

src/Idris/Elab/Term.hs+46−34

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

363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

364 = do g <- goal; resolveTC' False False 5 g fn ist

365 elab' ina fc (PResolveTC fc')

366− = do c <- getNameFrom (sMN 0 "class")

366+ = do c <- getNameFrom (sMN 0 "__class")

367 instanceArg c

368 -- Elaborate the equality type first homogeneously, then

369 -- heterogeneously as a fallback

@@ -1028,12 +1028,22 @@ elab ist info emode opts fn tm

1028 solve

1029 elab' ina _ c@(PCase fc scr opts)

1030 = do attack

1031+

1031 tyn <- getNameFrom (sMN 0 "scty")

1032 tyn <- getNameFrom (sMN 0 "scty")

1032 claim tyn RType

1033 claim tyn RType

1033 valn <- getNameFrom (sMN 0 "scval")

1034 valn <- getNameFrom (sMN 0 "scval")

1034 scvn <- getNameFrom (sMN 0 "scvar")

1035 scvn <- getNameFrom (sMN 0 "scvar")

1035 claim valn (Var tyn)

1036 claim valn (Var tyn)

1036 letbind scvn (Var tyn) (Var valn)

1037 letbind scvn (Var tyn) (Var valn)

1038+

1039+ -- Start filling in the scrutinee type, if we can work one

1040+ -- out from the case options

1041+ let scrTy = getScrType (map fst opts)

1042+ case scrTy of

1043+ Nothing -> return ()

1044+ Just ty -> do focus tyn

1045+ elabE ina (Just fc) ty

1046+

1037 focus valn

1047 focus valn

1038 elabE (ina { e_inarg = True }) (Just fc) scr

1048 elabE (ina { e_inarg = True }) (Just fc) scr

1039 -- Solve any remaining implicits - we need to solve as many

1049 -- Solve any remaining implicits - we need to solve as many

@@ -1084,6 +1094,21 @@ elab ist info emode opts fn tm

1084 Just xs@(_:_) -> sNS n xs

1094 Just xs@(_:_) -> sNS n xs

1085 _ -> n

1095 _ -> n

1086

1096

1097+ getScrType [] = Nothing

1098+ getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

1099+

1100+ getAppType (PRef _ _ n) =

1101+ case lookupTyName n (tt_ctxt ist) of

1102+ [(n', ty)] | isDConName n' (tt_ctxt ist) ->

1103+ case unApply (getRetTy ty) of

1104+ (P _ tyn _, args) ->

1105+ Just (PApp fc (PRef fc [] tyn)

1106+ (map pexp (map (const Placeholder) args)))

1107+ _ -> Nothing

1108+ _ -> Nothing -- ambiguity is no help to us!

1109+ getAppType (PApp _ t as) = getAppType t

1110+ getAppType _ = Nothing

1111+

1087 inApp (P _ n _) = [n]

1112 inApp (P _ n _) = [n]

1088 inApp (App _ f a) = inApp f ++ inApp a

1113 inApp (App _ f a) = inApp f ++ inApp a

1089 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

1114 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

@@ -1415,9 +1440,9 @@ elab ist info emode opts fn tm

1415 notImplicitable _ = False

1440 notImplicitable _ = False

1416

1441

1417 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1442 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1418− | tcinstance i

1443+ | tcinstance i && not (toplevel_imp i)

1419 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1444 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1420− | otherwise

1445+ | not (toplevel_imp i)

1421 = pimp n Placeholder True : insertScopedImps fc sc xs

1446 = pimp n Placeholder True : insertScopedImps fc sc xs

1422 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

1447 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

1423 = x : insertScopedImps fc sc xs

1448 = x : insertScopedImps fc sc xs

@@ -1696,38 +1721,25 @@ resolveTC' di mv depth tm n ist

1696

1721

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

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

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

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

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

1724+collectDeferred top casenames ctxt tm = cd [] tm

1700− do ds <- get

1701− t' <- collectDeferred top casenames ctxt t

1702− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])

1703− collectDeferred top casenames ctxt app

1704 where

1725 where

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

1726+ cd env (Bind n (GHole i psns t) app) =

1706− -- not a name we're immediately going to define in a case block, so that

1727+ do ds <- get

1707− -- any immediate specialisation of the function applied to constructors

1728+ t' <- collectDeferred top casenames ctxt t

1708− -- can be done

1729+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])

1730+ cd env app

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

1731+ cd env (Bind n b t)

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

1732+ = do b' <- cdb b

1711− (tidyArg ((n, b) : env) sc)

1733+ t' <- cd ((n, b) : env) t

1712− tidyArg env t = tidy ctxt env t

1713−

1714− tidy ctxt env t = normalise ctxt env t

1715−

1716− getFn (Bind n (Lam _) t) = getFn t

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

1718−

1719−collectDeferred top ns ctxt (Bind n b t)

1720− = do b' <- cdb b

1721− t' <- collectDeferred top ns ctxt t

1722− return (Bind n b' t')

1734+ return (Bind n b' t')

1723− where

1735+ where

1724− cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)

1736+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)

1725− cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)

1737+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1726− cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)

1738+ cdb b = do ty' <- cd env (binderTy b)

1727− return (b { binderTy = ty' })

1739+ return (b { binderTy = ty' })

1728−collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)

1740+ cd env (App s f a) = liftM2 (App s) (cd env f)

1729− (collectDeferred top ns ctxt a)

1741+ (cd env a)

1730−collectDeferred top ns ctxt t = return t

1742+ cd env t = return t

1731

1743

1732case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1744case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1733case_ ind autoSolve ist fn tm = do

1745case_ ind autoSolve ist fn tm = do

src/Idris/Elab/Value.hs+2−1

@@ -127,7 +127,8 @@ elabExec fc tm = runtm (PAlternative [] FirstSuccess

127 printtm tm

128 ])

129 where

130− runtm t = PApp fc (PRef fc [] (sUN "run__IO")) [pexp t]

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO"))

131+ [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

131 printtm t = PApp fc (PRef fc [] (sUN "printLn"))

132 printtm t = PApp fc (PRef fc [] (sUN "printLn"))

132 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

133 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

133

134

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 126

43+ibcVersion = 127

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/Interactive.hs+2−2

@@ -34,10 +34,10 @@ import Debug.Trace

34caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

35caseSplitAt fn updatefile l n

36 = do src <- runIO $ readSource fn

37− res <- splitOnLine l n fn

37+ (ok, res) <- splitOnLine l n fn

38 logLvl 1 (showSep "\n" (map show res))

39 let (before, (ap : later)) = splitAt (l-1) (lines src)

40− res' <- replaceSplits ap res

40+ res' <- replaceSplits ap res (not ok)

41 let new = concat res'

42 if updatefile

43 then do let fb = fn ++ "~" -- make a backup!

src/Idris/ParseExpr.hs+3−3

@@ -1051,10 +1051,10 @@ normalImplicit opts st syn = do

1051 sc <- expr syn

1052 let (im,cl)

1053 = if implicitAllowed syn

1054− then (Imp opts st False Nothing,

1054+ then (Imp opts st False (Just (Impl False True)),

1055 constraint)

1056− else (Imp opts st False (Just (Impl False)),

1056+ else (Imp opts st False (Just (Impl False False)),

1057− Imp opts st False (Just (Impl True)))

1057+ Imp opts st False (Just (Impl True False)))

1058 return (bindList (PPi im) xt

1059 (bindList (PPi cl) cs sc))

1060

src/Idris/REPL.hs+11−3

@@ -805,7 +805,11 @@ process fn (Eval t)

805 getIState >>= flip warnDisamb t

806 (tm, ty) <- elabREPL recinfo ERHS t

807 ctxt <- getContext

808− let tm' = perhapsForce $ normaliseAll ctxt [] tm

808+ let tm' = perhapsForce $ normaliseBlocking ctxt []

809+ [sUN "foreign",

810+ sUN "prim_read",

811+ sUN "prim_write"]

812+ tm

809 let ty' = perhapsForce $ normaliseAll ctxt [] ty

813 let ty' = perhapsForce $ normaliseAll ctxt [] ty

810 -- Add value to context, call it "it"

814 -- Add value to context, call it "it"

811 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

815 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

@@ -813,7 +817,8 @@ process fn (Eval t)

813 logLvl 3 $ "Raw: " ++ show (tm', ty')

817 logLvl 3 $ "Raw: " ++ show (tm', ty')

814 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

818 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

815 let tmDoc = pprintDelab ist tm'

819 let tmDoc = pprintDelab ist tm'

820+ -- errReverse to make type more readable

816− tyDoc = pprintDelab ist ty'

821+ tyDoc = pprintDelab ist (errReverse ist ty')

817 iPrintTermWithType tmDoc tyDoc

822 iPrintTermWithType tmDoc tyDoc

818 where perhapsForce tm | termSmallerThan 100 tm = force tm

823 where perhapsForce tm | termSmallerThan 100 tm = force tm

819 | otherwise = tm

824 | otherwise = tm

@@ -938,7 +943,8 @@ process fn (Check (PRef _ _ n))

938 where

943 where

939 showMetavarInfo ppo ist n i

944 showMetavarInfo ppo ist n i

940 = case lookupTy n (tt_ctxt ist) of

945 = case lookupTy n (tt_ctxt ist) of

946+ (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

941− (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

947+ putTy ppo ist i [] (delab ist (errReverse ist ty'))

942 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

948 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

943 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

949 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

944 putTy ppo ist i bnd (PPi _ n _ t sc)

950 putTy ppo ist i bnd (PPi _ n _ t sc)

@@ -1059,6 +1065,8 @@ process fn (DebugInfo n)

1059 when (not (null si)) $ iputStrLn (show si)

1065 when (not (null si)) $ iputStrLn (show si)

1060 let di = lookupCtxt n (idris_datatypes i)

1066 let di = lookupCtxt n (idris_datatypes i)

1061 when (not (null di)) $ iputStrLn (show di)

1067 when (not (null di)) $ iputStrLn (show di)

1068+ let imps = lookupCtxt n (idris_implicits i)

1069+ when (not (null imps)) $ iputStrLn (show imps)

1062 let d = lookupDef n (tt_ctxt i)

1070 let d = lookupDef n (tt_ctxt i)

1063 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1071 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1064 let cg = lookupCtxtName n (idris_callgraph i)

1072 let cg = lookupCtxtName n (idris_callgraph i)

src/Idris/REPLParser.hs+26−13

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

1

2−module Idris.REPLParser (parseCmd, help, allHelp) where

2+module Idris.REPLParser (parseCmd, help, allHelp, setOptions) where

3

4import System.FilePath ((</>))

5import System.Console.ANSI (Color(..))

@@ -32,6 +32,16 @@ parseCmd i inputname = P.runparser pCmd i inputname . trim

32type CommandTable = [ ( [String], CmdArg, String

33 , String -> P.IdrisParser (Either String Command) ) ]

34

35+setOptions :: [(String, Opt)]

36+setOptions = [("errorcontext", ErrContext),

37+ ("showimplicits", ShowImpl),

38+ ("originalerrors", ShowOrigErr),

39+ ("autosolve", AutoSolve),

40+ ("nobanner", NoBanner),

41+ ("warnreach", WarnReach),

42+ ("evaltypes", EvalTypes),

43+ ("desugarnats", DesugarNats)]

44+

35help :: [([String], CmdArg, String)]

45help :: [([String], CmdArg, String)]

36help = (["<expr>"], NoArg, "Evaluate an expression") :

46help = (["<expr>"], NoArg, "Evaluate an expression") :

37 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

47 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

@@ -80,7 +90,7 @@ parserCommandsForHelp =

80 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

90 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

81 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

91 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

82 , noArgCmd ["?", "h", "help"] Help "Display this help text"

92 , noArgCmd ["?", "h", "help"] Help "Display this help text"

83− , optArgCmd ["set"] SetOpt "Set an option (errorcontext, showimplicits)"

93+ , optArgCmd ["set"] SetOpt $ "Set an option (" ++ optionsList ++ ")"

84 , optArgCmd ["unset"] UnsetOpt "Unset an option"

94 , optArgCmd ["unset"] UnsetOpt "Unset an option"

85 , (["color", "colour"], ColourArg

95 , (["color", "colour"], ColourArg

86 , "Turn REPL colours on or off; set a specific colour"

96 , "Turn REPL colours on or off; set a specific colour"

@@ -100,6 +110,7 @@ parserCommandsForHelp =

100 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

110 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

101 , cmd_pprint)

111 , cmd_pprint)

102 ]

112 ]

113+ where optionsList = intercalate ", " $ map fst setOptions

103

114

104parserCommands =

115parserCommands =

105 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

116 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

@@ -163,10 +174,9 @@ pCmd :: P.IdrisParser (Either String Command)

163pCmd = choice [ do c <- cmd names; parser c

174pCmd = choice [ do c <- cmd names; parser c

164 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

175 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

165 <|> unrecognized

176 <|> unrecognized

166− <|> nop

177+ <|> nop

167 <|> eval

178 <|> eval

168 where nop = do eof; return (Right NOP)

179 where nop = do eof; return (Right NOP)

169− eval = exprArg Eval ""

170 unrecognized = do

180 unrecognized = do

171 P.lchar ':'

181 P.lchar ':'

172 cmd <- many anyChar

182 cmd <- many anyChar

@@ -194,16 +204,26 @@ noArgs cmd name = do

194

204

195 emptyArgs <|> failure

205 emptyArgs <|> failure

196

206

207+eval :: P.IdrisParser (Either String Command)

208+eval = do

209+ t <- P.fullExpr defaultSyntax

210+ return $ Right (Eval t)

211+

197exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

212exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

198exprArg cmd name = do

213exprArg cmd name = do

199 let noArg = do

214 let noArg = do

200 eof

215 eof

201 return $ Left ("Usage is :" ++ name ++ " <expression>")

216 return $ Left ("Usage is :" ++ name ++ " <expression>")

202

217

218+ let justOperator = do

219+ (op, fc) <- P.operatorFC

220+ eof

221+ return $ Right $ cmd (PRef fc [] (sUN op))

222+

203 let properArg = do

223 let properArg = do

204 t <- P.fullExpr defaultSyntax

224 t <- P.fullExpr defaultSyntax

205 return $ Right (cmd t)

225 return $ Right (cmd t)

206− try noArg <|> properArg

226+ try noArg <|> try justOperator <|> properArg

207

227

208

228

209

229

@@ -253,14 +273,7 @@ optArg cmd name = do

253

273

254 where

274 where

255 pOption :: P.IdrisParser Opt

275 pOption :: P.IdrisParser Opt

256− pOption = do discard (P.symbol "errorcontext"); return ErrContext

257− <|> do discard (P.symbol "showimplicits"); return ShowImpl

258− <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

259− <|> do discard (P.symbol "autosolve"); return AutoSolve

260− <|> do discard (P.symbol "nobanner") ; return NoBanner

261− <|> do discard (P.symbol "warnreach"); return WarnReach

262− <|> do discard (P.symbol "evaltypes"); return EvalTypes

276+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

263− <|> do discard (P.symbol "desugarnats"); return DesugarNats

264

277

265proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

278proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

266proofArg cmd name = do

279proofArg cmd name = do

src/Idris/Reflection.hs+3−3

@@ -357,8 +357,8 @@ reifyTTConstApp f v@(P _ _ _) =

357reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

358

359reifyArithTy :: Term -> ElabD ArithTy

360−reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

360+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

361−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

361+reifyArithTy (P _ n _) | n == reflm "ATDouble" = return ATFloat

362reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

363

364reifyNativeTy :: Term -> ElabD NativeTy

@@ -768,7 +768,7 @@ reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

768reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

769reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]

770reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]

771−reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]

771+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATDouble")]

772reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]

773reflectConstant StrType = Var (reflm "StrType")

774reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]

src/Pkg/PParser.hs+24−9

@@ -15,6 +15,7 @@ import Idris.CmdOptions

15import Control.Monad.State.Strict

16import Control.Applicative

17import System.FilePath (takeFileName, isValid)

18+import Data.Maybe (isNothing, fromJust)

18

19

19import Util.System

20import Util.System

20

21

@@ -79,18 +80,32 @@ filename = (do

79 -- Through at least version 0.9.19.1, IPKG executable values were

80 -- Through at least version 0.9.19.1, IPKG executable values were

80 -- possibly namespaced identifiers, like foo.bar.baz.

81 -- possibly namespaced identifiers, like foo.bar.baz.

81 show <$> fst <$> iName []

82 show <$> fst <$> iName []

82− if isValidFilename filename

83+ case filenameErrorMessage filename of

83− then return filename

84+ Just errorMessage -> fail errorMessage

84− else fail "a filename must be non-empty and have no directory component")

85+ Nothing -> return filename)

85 <?> "filename"

86 <?> "filename"

86 where

87 where

87− isValidFilename :: FilePath -> Bool

88+ -- TODO: Report failing span better! We could lookAhead,

88− isValidFilename path =

89+ -- or do something with DeltaParsing?

89− and [isNonEmpty, isValidPath, hasNoDirectoryComponent]

90+ filenameErrorMessage :: FilePath -> Maybe String

91+ filenameErrorMessage path = either Just (const Nothing) $ do

92+ checkEmpty path

93+ checkValid path

94+ checkNoDirectoryComponent path

90 where

95 where

91− isNonEmpty = path /= ""

96+ checkThat ok message =

97+ if ok then Right () else Left message

98+

99+ checkEmpty path =

100+ checkThat (path /= "") "filename must not be empty"

101+

102+ checkValid path =

92− isValidPath = System.FilePath.isValid path

103+ checkThat (System.FilePath.isValid path)

104+ "filename must contain only valid characters"

105+

106+ checkNoDirectoryComponent path =

93− hasNoDirectoryComponent = path == takeFileName path

107+ checkThat (path == takeFileName path)

108+ "filename must contain no directory component"

94

109

95

110

96pClause :: PParser ()

111pClause :: PParser ()

src/Util/System.hs+11−7

@@ -16,9 +16,8 @@ import System.Directory (getTemporaryDirectory

16 , removeFile

17 , removeDirectoryRecursive

18 , createDirectoryIfMissing

19− , doesDirectoryExist

20 )

19 )

21−import System.FilePath ((</>), normalise, isAbsolute, dropFileName)

20+import System.FilePath ((</>), normalise)

22import System.IO

21import System.IO

23import System.Info

22import System.Info

24import System.IO.Error

23import System.IO.Error

@@ -66,7 +65,7 @@ isATTY = do

66withTempdir :: String -> (FilePath -> IO a) -> IO a

65withTempdir :: String -> (FilePath -> IO a) -> IO a

67withTempdir subdir callback

66withTempdir subdir callback

68 = do dir <- getTemporaryDirectory

67 = do dir <- getTemporaryDirectory

69− let tmpDir = (normalise dir) </> subdir

68+ let tmpDir = normalise dir </> subdir

70 removeLater <- catchIO (createDirectoryIfMissing True tmpDir >> return True)

69 removeLater <- catchIO (createDirectoryIfMissing True tmpDir >> return True)

71 (\ ioError -> if isAlreadyExistsError ioError then return False

70 (\ ioError -> if isAlreadyExistsError ioError then return False

72 else throw ioError

71 else throw ioError

@@ -76,10 +75,15 @@ withTempdir subdir callback

76 return result

75 return result

77

76

78rmFile :: FilePath -> IO ()

77rmFile :: FilePath -> IO ()

79−rmFile f = do putStrLn $ "Removing " ++ f

78+rmFile f = do

80− catchIO (removeFile f)

79+ result <- try (removeFile f)

80+ case result of

81+ Right _ -> putStrLn $ "Removed: " ++ f

82+ Left err -> handleExists err

83+ where handleExists e

84+ | isDoesNotExistError e = return ()

81− (\ioerr -> putStrLn $ "WARNING: Cannot remove file "

85+ | otherwise = putStrLn $ "WARNING: Cannot remove file "

82− ++ f ++ ", Error msg:" ++ show ioerr)

86+ ++ f ++ ", Error msg:" ++ show e

83

87

84setupBundledCC :: IO()

88setupBundledCC :: IO()

85#ifdef FREESTANDING

89#ifdef FREESTANDING

test/basic002/test006.idr+1−1

@@ -23,7 +23,7 @@ main = do printLn (natToBin 42)

23---------- Proofs ----------

24

25Main.parity_lemma_2 = proof {

26− intro;

26+ intro j;

27 intro;

28 rewrite sym (plusSuccRightSucc j j);

29 trivial;

test/dsl002/test014.idr+6−5

@@ -15,16 +15,17 @@ syntax "ifM" [test] "then" [t] "else" [e]

15 = test >>= (\b => if b then t else e)

16

17open : String -> (p:Purpose) -> Creator (Either () (FILE p))

18−open fn p = ioc (do h <- fopen fn (pstring p)

18+open fn p = ioc (do Right h <- fopen fn (pstring p)

19− ifM validFile h

19+ | Left err => return (Left ())

20− then return (Right (OpenH h))

20+ return (Right (OpenH h)))

21− else return (Left ()))

22

21

23close : FILE p -> Updater ()

22close : FILE p -> Updater ()

24close (OpenH h) = iou (closeFile h)

23close (OpenH h) = iou (closeFile h)

25

24

26readLine : FILE Reading -> Reader String

25readLine : FILE Reading -> Reader String

27−readLine (OpenH h) = ior (fread h)

26+readLine (OpenH h) = ior (do Right str <- fread h

27+ | return ""

28+ return str)

28

29

29eof : FILE Reading -> Reader Bool

30eof : FILE Reading -> Reader Bool

30eof (OpenH h) = ior (feof h)

31eof (OpenH h) = ior (feof h)

test/error006/WithPatsNoWith.idrnew file+6

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

1+module WithPatsNoWith

2+

3+foo : Int -> Bool

4+foo 1 | 2 | 3 = True

5+foo _ = False

6+

test/error006/expectednew file+2

@@ -0,0 +1,2 @@

1+WithPatsNoWith.idr:4:5:When checking left hand side of foo:

2+unexpected patterns outside of "with" block

test/error006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --consolewidth 80 $@ --check --nocolour WithPatsNoWith.idr

3+rm -f *.ibc

test/ffi001/test022.idr+2−2

@@ -2,8 +2,8 @@ module Main

2

3%dynamic "dummy", "libm", "msvcrt"

4

5−x : Float

5+x : Double

6−x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)

6+x = unsafePerformIO (foreign FFI_C "sin" (Double -> IO Double) 1.6)

7

8main : IO ()

9main = putStrLn (show x)

test/ffi004/test026.idr+2−1

@@ -10,7 +10,8 @@ strToType _ = Nat

10

11-- If the file contains "Int", provide Int as a type, otherwise provide Nat

12fromFile : String -> IO (Provider Type)

13−fromFile fname = do str <- readFile fname

13+fromFile fname = do Right str <- readFile fname

14+ | Left err => return (Provide Void)

14 return (Provide (strToType (trim str)))

15 return (Provide (strToType (trim str)))

15

16

16%provide (T1 : Type) with fromFile "theType"

17%provide (T1 : Type) with fromFile "theType"

test/interactive001/expected+6

@@ -11,3 +11,9 @@ isElem2 x (y :: ys) with (_)

11 [] => ?bar_1

12 (x :: ys) => ?bar_2

13

14+elemVoid1 Here impossible

15+elemVoid1 (There _) impossible

16+

17+ Here impossible

18+ (There _) impossible

19+

test/interactive001/input+2

@@ -4,3 +4,5 @@

4:mw 26 isElem2

5:cs 31 p

6:cs 36 xs'

7+:cs 39 x

8+:cs 43 case_val

test/interactive001/test032.idr+9

@@ -34,3 +34,12 @@ isElem3 x (y :: ys) with (decEq x y)

34foo : List a -> List a

35foo xs = case xs of

36 xs' => ?bar

37+

38+elemVoid1 : elem.Elem x [] -> Void

39+elemVoid1 x = ?elemVoid1_rhs

40+

41+elemVoid2 : elem.Elem x [] -> Void

42+elemVoid2 x = case x of

43+ case_val => ?elemVoid2_rhs

44+

45+

test/interactive010/expectednew file+22

@@ -0,0 +1,22 @@

1+Prelude.List.(++) : List a -> List a -> List a

2+Prelude.Strings.(++) : String -> String -> String

3+Prelude.Classes./ : (__pi_arg : Double) →

4+ (__pi_arg1 : Double) → Double

5+Usage is :doc <functionname>

6+Usage is :wc <functionname>

7+Usage is :printdef <functionname>

8+prim__divFloat

9+Prelude.Classes./

10+

11+ : Double -> Double -> Double

12+(input):1:1: error: expected: ":",

13+ dependent type signature,

14+ end of input

15+/<EOF>

16+^

17+(input):1:1: error: expected: ":",

18+ dependent type signature,

19+ end of input

20+++<EOF>

21+^

22+prim__divFloat

test/interactive010/inputnew file+10

@@ -0,0 +1,10 @@

1+:type ++

2+:core /

3+:doc +

4+:wc +

5+:printdef -

6+:spec /

7+:patt /

8+/

9+++

10+:whnf /

test/interactive010/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+idris --quiet --nobanner --nocolor --consolewidth 80 < input

test/interactive011/expectednew file+3

@@ -0,0 +1,3 @@

1+ show x = ?Show_rhs_1

2+ showPrec d x = ?Show_rhs_2

3+append [] _ = ?append_rhs_1

test/interactive011/inputnew file+2

@@ -0,0 +1,2 @@

1+:ac 5 Show

2+:ac 7 append

test/interactive011/interactive011.idrnew file+11

@@ -0,0 +1,11 @@

1+import Data.Vect

2+

3+data Foo = Bar | Baz

4+

5+instance Show Foo where

6+

7+append : Vect n a -> Vect m a -> Vect (n + m) a

8+append (x :: xs) ys = ?append_rhs_2

9+

10+

11+

test/interactive011/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet interactive011.idr < input

3+rm -f *.ibc

test/interactive012/expectednew file+33

@@ -0,0 +1,33 @@

1+ x : Int

2+--------------------------------------

3+mkString_rhs_1 : String

4+ x : String

5+--------------------------------------

6+mkString_rhs_2 : String

7+--------------------------------------

8+mkThing_rhs_1 : Int

9+--------------------------------------

10+mkThing_rhs_2 : String

11+ str : Bool

12+ x : IntString str

13+--------------------------------------

14+mkString2_rhs : String

15+ x : ?what

16+--------------------------------------

17+mkString3_rhs_1 : String

18+ x : ?what

19+--------------------------------------

20+mkString3_rhs_2 : String

21+ a : Type

22+ m : Nat

23+ ys : Vect m a

24+--------------------------------------

25+append_rhs_1 : Vect m a

26+ a : Type

27+ x : a

28+ k : Nat

29+ xs : Vect k a

30+ m : Nat

31+ ys : Vect m a

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

33+append_rhs_2 : Vect (S (plus k m)) a

test/interactive012/inputnew file+9

@@ -0,0 +1,9 @@

1+:t mkString_rhs_1

2+:t mkString_rhs_2

3+:t mkThing_rhs_1

4+:t mkThing_rhs_2

5+:t mkString2_rhs

6+:t mkString3_rhs_1

7+:t mkString3_rhs_2

8+:t append_rhs_1

9+:t append_rhs_2

test/interactive012/interactive012.idrnew file+26

@@ -0,0 +1,26 @@

1+IntString : Bool -> Type

2+IntString False = Int

3+IntString True = String

4+

5+mkString : (str : Bool) -> IntString str -> String

6+mkString False x = ?mkString_rhs_1

7+mkString True x = ?mkString_rhs_2

8+

9+mkThing : (str : Bool) -> IntString str

10+mkThing False = ?mkThing_rhs_1

11+mkThing True = ?mkThing_rhs_2

12+

13+mkString2 : (str : Bool) -> IntString str -> String

14+mkString2 str x = ?mkString2_rhs

15+

16+mkString3 : (str : Bool) -> ?what -> String

17+mkString3 False x = ?mkString3_rhs_1

18+mkString3 True x = ?mkString3_rhs_2

19+

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

21+ Nil : Vect Z a

22+ (::) : a -> Vect k a -> Vect (S k) a

23+

24+append : Vect n a -> Vect m a -> Vect (n + m) a

25+append [] ys = ?append_rhs_1

26+append (x :: xs) ys = ?append_rhs_2

test/interactive012/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --nocolour --consolewidth 70 --quiet interactive012.idr < input

3+rm -f *.ibc

test/io001/test004.idr+4−4

@@ -8,20 +8,20 @@ mwhile t b = do v <- t

8 False => return ()

9

10dumpFile : String -> IO ()

11−dumpFile fn = do { h <- openFile fn Read

11+dumpFile fn = do { Right h <- openFile fn Read

12 mwhile (do { -- putStrLn "TEST"

13 x <- feof h

14 return (not x) })

15− (do { l <- fread h

15+ (do { Right l <- fread h

16 putStr l })

17 closeFile h }

18

19main : IO ()

20−main = do { h <- openFile "testfile" Write

20+main = do { Right h <- openFile "testfile" Write

21 fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"

22 closeFile h

23 putStrLn "Reading testfile"

24− f <- readFile "testfile"

24+ Right f <- readFile "testfile"

25 putStrLn f

26 putStrLn "---"

27 dumpFile "testfile"

test/pkg001/expected−1

@@ -1 +0,0 @@

1−Type checking ./Main.idr

test/pkg001/test.ipkg+1−1

@@ -2,6 +2,6 @@ package test

2

3pkgs = effects

4

5−opts = "--warnpartial --warnreach"

5+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

6

7modules = Main

test/pkg002/expected−1

@@ -1 +0,0 @@

1−Type checking ./Main.idr

test/pkg002/test.ipkg+2

@@ -2,5 +2,7 @@ package test

2

3modules = Main

4

5+

6+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

5main = Main

7main = Main

6executable = some.namespaced.identifier

8executable = some.namespaced.identifier

test/pkg003/expected−1

@@ -1 +0,0 @@

1−Type checking ./Main.idr

test/pkg003/run+1−1

@@ -3,4 +3,4 @@

3### containing a valid filename.

4idris $@ --build test.ipkg

5rm -f *.ibc

6−rm -f 'quoting-allows-hyphens and spaces? and fun stuff!'

6+rm -f 'quoting-allows-hyphens and spaces and fun stuff!'

test/pkg003/test.ipkg+2−1

@@ -2,5 +2,6 @@ package test

2

3modules = Main

4

5+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

5main = Main

6main = Main

6−executable = "quoting-allows-hyphens and spaces? and fun stuff!"

7+executable = "quoting-allows-hyphens and spaces and fun stuff!"

test/pkg004/expected+2−3

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

1−Uncaught error: user error ([1mtest.ipkg[0m:[1m7[0m:[1m1[0m: [91merror[0m: a filename

1+Uncaught error: user error ([1mtest.ipkg[0m:[1m10[0m:[1m1[0m: [91merror[0m: filename

2− must be non-empty and have no

3− directory

2+ must contain no directory

4 component, expected: space

3 component, expected: space

5[1m[94m<EOF>[0;1m[0m

4[1m[94m<EOF>[0;1m[0m

6[92m^[0m )

5[92m^[0m )

test/pkg004/test.ipkg+3

@@ -2,5 +2,8 @@ package test

2

3modules = Main

4

5+

6+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

7+

5main = Main

8main = Main

6executable = "filenames/cannot include\a directory separator"

9executable = "filenames/cannot include\a directory separator"

test/reg001/reg001.idr+26

@@ -182,3 +182,29 @@ hVectEx1 = ["Hello",[1,2,3],42,(0,10)]

182

183vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]

184vecfoo = put (S (S Z)) hVectEx1

185+

186+foom : Monad m => Int -> m Int

187+foom = pure

188+

189+bar : IO ()

190+bar = case foom 5 of

191+ Nothing => print 42

192+ Just n => print n

193+

194+Max : (Nat -> Type) -> Type

195+Max p = (Nat , (k : Nat) -> p k -> Nat)

196+

197+maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat

198+maxEquiv a n1 pr1 = snd a n1 pr1

199+

200+data Rho = R

201+

202+rho : Rho -> Rho

203+rho r = case r of R => r

204+

205+data Kappa : (r : Rho) -> Type where K : Kappa r

206+

207+kappa : Kappa (rho r) -> Kappa (rho r)

208+kappa {r} k = k' where -- k' : Kappa (rho r)

209+ k' = k

210+

test/tutorial006/run+1

@@ -1,4 +1,5 @@

1#!/usr/bin/env bash

2idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check

3idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check

4+idris --nocolour --consolewidth 80 $@ tutorial006c.idr -p effects --check

4rm -f *.ibc

5rm -f *.ibc

test/tutorial006/tutorial006c.idrnew file+20

@@ -0,0 +1,20 @@

1+import Effects

2+import Effect.Exception

3+import Effect.StdIO

4+import Data.Vect

5+

6+read_vec : Eff (p ** Vect p Int) [STDIO]

7+read_vec = do putStr "Number (-1 when done): "

8+ case run (parseNumber (trim !getStr)) of

9+ Nothing => do putStrLn "Input error"

10+ read_vec

11+ Just v => if (v /= -1)

12+ then do (_ ** xs) <- read_vec

13+ pure (_ ** v :: xs)

14+ else pure (_ ** [])

15+ where

16+ parseNumber : String -> Eff Int [EXCEPTION String]

17+ parseNumber str

18+ = if all (\x => isDigit x || x == '-') (unpack str)

19+ then pure (cast str)

20+ else raise "Not a number"