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

CHANGELOG+9

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

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

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

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

2224

2325Library updates

2426---------------

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

3739 from Effectful programs.

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

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

4045

4146Tool updates

4247------------

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

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

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

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

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

4958 adds missing clauses if there is already a definition.

5059

CONTRIBUTORS+1

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

1515Guglielmo Fachini

1616Simon Fowler

1717Google

18+Zack Grannan

1819Cezar Ionescu

1920Heath Johns

2021Irene Knapp

Makefile+1−1

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

4343 $(CABAL) install $(CABALFLAGS)

4444

4545linecount:

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

4747

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

4949doc: dist/setup-config

docs/effects/depeff.rst+2−2

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

4848 readInt = do let x = trim !getStr

4949 putM (cast x :: !get)

5050

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

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

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

5454suffix 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:

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

9797 readInt = do let x = trim !getStr

9898 case all isDigit (unpack x) of

99− False => pure False

99+ False => pureM False

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

101101 pureM True

102102

docs/effects/hangman.rst+8−9

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

108108 Guess : (x : Char) ->

109109 sig MysteryRules Bool

110110 (Mystery (Running (S g) (S w)))

111− (\inword =>

112− Mystery (case inword of

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

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

111+ (\inword => if inword

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

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

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

116115 (Mystery NotRunning)

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

118117 (Mystery NotRunning)

119118 NewWord : (w : String) ->

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

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

121120 Get : sig MysteryRules String (Mystery h)

122121

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

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

243242.. code-block:: idris

244243

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

246− runGame = do srand (cast !time)

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

248− NewWord w

245+ runGame = do srand !time

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

247+ call $ NewWord w

249248 game

250− putStrLn !Get

249+ putStrLn !(call Get)

251250

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

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

docs/effects/simpleeff.rst+23−22

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

382382

383383 vadd : Vect n Int -> Vect n Int -> Vect n Int

384384 vadd [] [] = []

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

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

386386

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

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

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

410410

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

412412length, 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

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

416−within range.

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+

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

434+number to be within range.

417435

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

419437result 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

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

435453with gracefully.

436454

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"

454455

455456Example: An Expression Calculator

456457=================================

docs/faq/faq.rst+53

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

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

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

105105

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+

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

107160=============================================================================================

108161

docs/reference/repl.rst+2−1

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

128128+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

130130+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

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

132+| | | desugarnats) |

132133+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

134135+----------------+------------------------------+----------------------------------------------------------------------------------------------------------+

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

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

112112

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

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

116116

117117.. code:: idris

118118

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

126126 MyListType : Type

127127 MyListType = List Int

128128

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

130+arguments mean it is often a good idea.

131+

129132.. _syntax-data-types:

130133

131134Data 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

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

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

3838variables (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):

4042

4143.. code-block:: idris

4244

docs/tutorial/introduction.rst+1−1

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

1515Correspondingly, the following values are examples of inhabitants of

1616those types:

1717

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

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

1919

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

2121clear. 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

122122

123123 fact : Expr G (TyFun TyInt TyInt)

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

126126 (Var Stop)))

127127

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

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

162162

163163.. code-block:: idris

164164

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

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

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

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

167167

168168 pure : Expr G a -> Expr G a

169169 pure = id

docs/tutorial/typesfuns.rst+23−10

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

5656::

5757

5858 *prims> 6*6+6

59− 42 : Int

59+ 42 : Integer

6060 *prims> x == 6*6+6

6161 True : Bool

6262

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

792792

793793.. code-block:: idris

794794

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

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

796796

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

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

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

800−discarding it would be wasteful.

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

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

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

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

801801

802802Tuples

803803------

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

820820 jim : (String, Int, String)

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

822822

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+

823832Dependent Pairs

824833---------------

825834

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

10251034 className : String

10261035

10271036**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.

10291042

10301043.. code-block:: idris

10311044

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

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

11381151

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

1140− value of the same type.

1153+ value of the same type.

11411154

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

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

1144− itself.

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

1157+ itself.

idris.cabal+13−1

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

11Name: idris

2−Version: 0.9.19.1

2+Version: 0.9.20.1

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

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

538538 test/interactive009/input

539539 test/interactive009/*.idr

540540 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

541552

542553 test/io001/run

543554 test/io001/*.idr

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

9931004 cpp-options: -DIDRIS_FFI

9941005 if flag(GMP)

9951006 build-depends: libffi < 0.2

1007+ extra-libraries: gmp

9961008 cpp-options: -DIDRIS_GMP

9971009 if flag(curses)

9981010 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

1616 catch (Left err) h = h err

1717 catch (Right x) h = (Right x)

1818

19− throw x = Left x

19+ throw = Left

2020

2121instance Catchable (IOExcept err) err where

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

2323 case p' of

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

2525 Right val => return (Right val))

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

26+ throw = ioe_fail

2727

2828instance Catchable List () where

2929 catch [] h = h ()

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

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

22

33-- An IO monad with exception handling

44

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

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

5+record IOExcept err a where

6+ constructor IOM

7+ runIOExcept : IO (Either err a)

78

89instance Functor (IOExcept e) where

910 map f (IOM fn) = IOM (map (map f) fn)

1011

1112instance Applicative (IOExcept e) where

1213 pure x = IOM (pure (pure x))

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

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

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

1515

1616instance Monad (IOExcept e) where

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

18− case x' of

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

20− ka

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

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

2218

2319ioe_lift : IO a -> IOExcept err a

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

25− return (Right op'))

20+ioe_lift op = IOM $ map Right op

2621

2722ioe_fail : err -> IOExcept err a

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

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

2924

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

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

32− case act' of

33− Left e => err e

34− Right v => ok v

35−

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

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

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

2525 plus_i = User 6

2626

2727

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

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

2929-- we can do:

3030{-

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

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

4040

4141------------------------------ Polarform

4242

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

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

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

4545

46−cis : Float -> Complex Float

46+cis : Double -> Complex Double

4747cis angle = cos angle :+ sin angle

4848

49−magnitude : Complex Float -> Float

49+magnitude : Complex Double -> Double

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

5151

52−phase : Complex Float -> Float

52+phase : Complex Double -> Double

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

5454

5555

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

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

6363

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

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

66−instance Num (Complex Float) where

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

66+instance Num (Complex Double) where

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

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

6969 fromInteger x = (fromInteger x:+0)

7070

71−instance Neg (Complex Float) where

71+instance Neg (Complex Double) where

7272 negate = map negate

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

622622

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

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

129129

130130instance Show ArithTy where

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

132− showPrec d ATFloat = "ATFloat"

132+ showPrec d ATDouble = "ATDouble"

133133

134134instance Show Const where

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

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

162162

163163instance Eq ArithTy where

164164 (ATInt x) == (ATInt y) = x == y

165− ATFloat == ATFloat = True

165+ ATDouble == ATDouble = True

166166 _ == _ = False

167167

168168instance Eq Const where

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

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

4444 unity = 1

4545

4646

47−instance Semigroup Float where

47+instance Semigroup Double where

4848 (<+>) = (+)

4949

50−instance Monoid Float where

50+instance Monoid Double where

5151 neutral = 0

5252

53−instance Group Float where

53+instance Group Double where

5454 inverse = (* -1)

5555

56−instance AbelianGroup Float

56+instance AbelianGroup Double

5757

58−instance Ring Float where

58+instance Ring Double where

5959 (<.>) = (*)

6060

61−instance RingWithUnity Float where

61+instance RingWithUnity Double where

6262 unity = 1

6363

64−instance Field Float where

64+instance Field Double where

6565 inverseM f _ = 1 / f

6666

6767

libs/contrib/Network/Socket.idr−4

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

143143 socketType : SocketType

144144 protocalNumber : ProtocolNumber

145145

146−||| Get the C error number

147−getErrno : IO Int

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

149−

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

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

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

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

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

1111instance Default Integer where

1212 default = 0

1313

14−instance Default Float where

14+instance Default Double where

1515 default = 0

1616

1717instance Default Nat where

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

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

1818 believe_me (exit 1)

1919

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

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

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

2222

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

2424 handle _ (Raise e) k = Left e

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

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

7474

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

7676instance Handler FileIO IO where

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

78− valid <- validFile h

79− if valid then k True (FH h)

80− else k False ()

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

78+ | Left err => k False ()

79+ k True (FH h)

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

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

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

8688 k () (FH h)

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

8890 k e (FH h)

8991

9092instance Handler FileIO (IOExcept a) where

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

92− valid <- ioe_lift $ validFile h

93− if valid then k True (FH h)

94− else k False ()

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

94+ | Left err => k False ()

95+ k True (FH h)

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

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

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

100104 k () (FH h)

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

102106 k e (FH h)

libs/effects/Effects.idr+7−2

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

1212||| The Effect type describes effectful computations.

1313|||

1414||| This type is parameterised by:

15−||| + The input resource.

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

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

16+||| + The input resource.

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

1818Effect : Type

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

2020

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

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

246246 arg <- v

247247 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

248253

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

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

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

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

99instance Default Integer where

1010 default = 0

1111

12−instance Default Float where

12+instance Default Double where

1313 default = 0

1414

1515instance Default Nat where

libs/prelude/Builtins.idr+3−1

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

152152really_believe_me : a -> b

153153really_believe_me x = prim__believe_me _ _ x

154154

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.

156157Float : Type

157158Float = Double

159+%deprecate Float

158160

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

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

libs/prelude/IO.idr+10−6

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

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

3737||| it.

3838abstract

39−%error_reverse

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

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

4241

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

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

118117liftPrimIO = MkIO

119118

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

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

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

122121

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

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

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

125124run__IO f = call__IO f

126125

127126unsafePerformIO : IO' ffi a -> a

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

163162 ||| Supported C foreign types

164163 data C_Types : Type -> Type where

165164 C_Str : C_Types String

166− C_Float : C_Types Float

165+ C_Float : C_Types Double

167166 C_Ptr : C_Types Ptr

168167 C_MPtr : C_Types ManagedPtr

169168 C_Unit : C_Types ()

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

176175 FFI_C : FFI

177176 FFI_C = MkFFI C_Types String String

178177

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

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

179180%error_reverse

180−IO : Type -> Type

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

181182IO = IO' FFI_C

182183

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

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

198199 forceGC : IO ()

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

200201

202+ getErrno : IO Int

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

204+

201205--------- The Javascript/Node FFI

202206

203207

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

217221

218222 data JS_Types : Type -> Type where

219223 JS_Str : JS_Types String

220− JS_Float : JS_Types Float

224+ JS_Float : JS_Types Double

221225 JS_Ptr : JS_Types Ptr

222226 JS_Unit : JS_Types ()

223227 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

7070

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

7272

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

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

7474

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

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

7878 | AType ArithTy | StrType

7979 | VoidType | Forgot

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

8989instance ReflConst Integer where

9090 toConst = BI

9191

92−instance ReflConst Float where

92+instance ReflConst Double where

9393 toConst = Fl

9494

9595instance ReflConst Char where

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

366366 quotedTy = `(Int)

367367 quote x = RConstant (I x)

368368

369−instance Quotable Float TT where

370− quotedTy = `(Float)

369+instance Quotable Double TT where

370+ quotedTy = `(Double)

371371 quote x = TConst (Fl x)

372372

373−instance Quotable Float Raw where

374− quotedTy = `(Float)

373+instance Quotable Double Raw where

374+ quotedTy = `(Double)

375375 quote x = RConstant (Fl x)

376376

377377instance Quotable Char TT where

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

541541instance Quotable ArithTy TT where

542542 quotedTy = `(ArithTy)

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

544− quote ATFloat = `(ATFloat)

544+ quote ATDouble = `(ATDouble)

545545

546546instance Quotable ArithTy Raw where

547547 quotedTy = `(ArithTy)

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

549− quote ATFloat = `(ATFloat)

549+ quote ATDouble = `(ATDouble)

550550

551551instance Quotable Const TT where

552552 quotedTy = `(Const)

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

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

3737instance Eq Integer where

3838 (==) = boolOp prim__eqBigInt

3939

40−instance Eq Float where

40+instance Eq Double where

4141 (==) = boolOp prim__eqFloat

4242

4343instance Eq Char where

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

118118 GT

119119

120120

121−instance Ord Float where

121+instance Ord Double where

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

123123 if (boolOp prim__sltFloat x y) then LT else

124124 GT

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

170170 fromInteger = prim__truncBigInt_Int

171171

172172

173−instance Num Float where

173+instance Num Double where

174174 (+) = prim__addFloat

175175 (*) = prim__mulFloat

176176

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

215215 (-) = prim__subInt

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

217217

218−instance Neg Float where

218+instance Neg Double where

219219 negate x = prim__negFloat x

220220 (-) = prim__subFloat

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

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

306306

307307-- ------------------------------------------------------------- [ Fractionals ]

308308

309−||| Fractional division of two Floats.

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

309+||| Fractional division of two Doubles.

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

311311(/) = prim__divFloat

312312

313313

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

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

1010import Prelude.Bool

1111import Prelude.Basics

1212import Prelude.Classes

13−import Prelude.Monad

13+import Prelude.Either

14+import Prelude.Show

1415import IO

1516

1617%access public

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

1920abstract

2021data File = FHandle Ptr

2122

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+

2247||| Standard input

2348stdin : File

2449stdin = FHandle prim__stdin

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

3156stderr : File

3257stderr = FHandle prim__stderr

3358

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+

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

3567do_fopen : String -> String -> IO Ptr

3668do_fopen f m

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

3971||| Open a file

4072||| @ f the filename

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

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

44− return (FHandle h)

76+ if !(nullPtr h)

77+ then do err <- getFileError

78+ return (Left err)

79+ else return (Right (FHandle h))

4580

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

47−partial

4882validFile : File -> IO Bool

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

5084 return (not x)

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

5589||| Open a file

5690||| @ f the filename

5791||| @ m the mode

58−partial

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

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

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

6194 modeStr Read = "r"

6295 modeStr Write = "w"

6396 modeStr ReadWrite = "r+"

6497

65−partial

6698do_fclose : Ptr -> IO ()

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

68100

69−partial

70101closeFile : File -> IO ()

71102closeFile (FHandle h) = do_fclose h

72103

73−partial

74104do_fread : Ptr -> IO' l String

75105do_fread h = prim_fread h

76106

77−fgetc : File -> IO Char

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

79−

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

81−fgetc' (FHandle h)

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

83− if (x < 0) then return Nothing

84− else return (Just (cast x))

107+fgetc : File -> IO (Either FileError Char)

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

109+ if !(ferror (FHandle h))

110+ then return (Left FileReadError)

111+ else return (Right c)

85112

86113fflush : File -> IO ()

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

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

89116do_popen : String -> String -> IO Ptr

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

91118

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

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

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

94− return (FHandle ptr)

121+ if !(nullPtr ptr)

122+ then do err <- getFileError

123+ return (Left err)

124+ else return (Right (FHandle ptr))

95125 where

96126 modeStr Read = "r"

97127 modeStr Write = "w"

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

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

104134-- prim__vm h

105135

106−partial

107−fread : File -> IO' l String

108−fread (FHandle h) = do_fread h

109−

110−partial

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

112−do_fwrite h s = do prim_fwrite h s

113− return ()

114−

115−partial

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

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

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

138+ if !(ferror (FHandle h))

139+ then return (Left FileReadError)

140+ else return (Right str)

141+

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

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

144+ if (res /= 0)

145+ then do errno <- getErrno

146+ if errno == 0

147+ then return (Left FileWriteError)

148+ else do err <- getFileError

149+ return (Left err)

150+ else return (Right ())

151+

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

117153fwrite (FHandle h) s = do_fwrite h s

118154

119−partial

120155do_feof : Ptr -> IO Int

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

122157

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

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

126161 return (not (eof == 0))

127162

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−

136163fpoll : File -> IO Bool

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

138165 return (p > 0)

139166

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

141−partial -- no error checking!

142−readFile : String -> IO String

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

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

169+covering

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

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

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

144173 c <- readFile' h ""

145174 closeFile h

146175 return c

147176 where

148177 partial

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

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

150179 readFile' h contents =

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

153183 readFile' h (contents ++ l)

154− else return contents

155−

156−

184+ else return (Right contents)

185+

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

1717import Prelude.Cast

1818import Prelude.Maybe

1919import Prelude.Functor

20+import Prelude.Either

2021import Prelude.Monad

2122import IO

2223

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

2425

2526---- some basic io

2627

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+

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

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

29−putStr x = do prim_write x

30− return ()

35+putStr : String -> IO ()

36+putStr = putStr'

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

3142

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

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

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

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

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

3551

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

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

38−print x = putStr (show x)

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

54+print = print'

3955

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

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

42−printLn x = putStrLn (show x)

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

57+||| descriptor

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

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

4360

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

45−getLine : IO' ffi String

46−getLine = do x <- prim_read

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

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

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

63+printLn = printLn'

64+

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

66+||| descriptor

67+getLine' : IO' ffi String

68+getLine' = do x <- prim_read

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

4870 where trimNL : String -> String

4971 trimNL str with (strM str)

5072 trimNL "" | StrNil = ""

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

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

5375

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

77+getLine : IO String

78+getLine = getLine'

79+

5480||| Write a single character to stdout

5581putChar : Char -> IO ()

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

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

97123processHandle h acc onRead onEOF

98124 = if !(feof h)

99125 then putStr (onEOF acc)

100− else do x <- fread h

126+ else do Right x <- fread h

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

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

102129 putStr out

103130 processHandle h acc' onRead onEOF

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

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

1313infixl 5 >>=

1414

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

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

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

1717

1818||| Also called `join` or mu

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

libs/prelude/Prelude/Show.idr+5

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

1010import Prelude.Classes

1111import Prelude.List

1212import Prelude.Maybe

13+import Prelude.Either

1314import Prelude.Nat

1415import Prelude.Strings

1516

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

185186 showPrec d Nothing = "Nothing"

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

187188

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+

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

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

190195

rts/Makefile+4−3

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

11include ../config.mk

22

33OBJS = 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

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

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

78 idris_utf8.h getline.h

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

1920endif

2021

2122ifeq ($(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

2324else

2425 CFLAGS += -fPIC

25− OBJS += idris_stdfgn.o idris_net.o

26+ OBJS += idris_net.o

2627endif

2728

2829LIBTARGET = libidris_rts.a

rts/idris_heap.c+12−12

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

77

88

99/* 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)

1111{

12− char * mem = malloc(heap_size);

12+ char * mem = malloc(heap_size);

1313 if (mem == NULL) {

14− fprintf(stderr,

14+ fprintf(stderr,

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

1616 heap_size);

1717 exit(EXIT_FAILURE);

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

3737void free_heap(Heap * h) {

3838 free(h->heap);

3939

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

41− free(h->old);

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

41+ free(h->old);

4242 }

4343}

4444

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

4747/******************** Heap testing ********************************************/

4848void heap_check_underflow(Heap * heap) {

4949 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",

5151 heap->heap, heap->next);

5252 exit(EXIT_FAILURE);

5353 }

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

5555

5656void heap_check_overflow(Heap * heap) {

5757 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",

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

6060 exit(EXIT_FAILURE);

6161 }

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

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

6666}

6767

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

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

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

7070}

7171

7272// Checks three important properties:

7373// 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.

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

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

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

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

7979//

8080void heap_check_pointers(Heap * heap) {

8181 char* scan = NULL;

82−

82+

8383 size_t item_size = 0;

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

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

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

9696 if (is_valid_ref(ptr)) {

9797 // Check for closure.

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

99− fprintf(stderr,

99+ fprintf(stderr,

100100 "RTS ERROR: heap closure broken. "\

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

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

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

105105#if 0 // TODO macro

106106 // Check for unidirectionality.

107107 if (!(ptr < heap_item)) {

108− fprintf(stderr,

108+ fprintf(stderr,

109109 "RTS ERROR: heap unidirectionality broken:" \

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

111111 heap_item, ptr);

rts/idris_heap.h+2−2

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

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

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

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

1212

1313 char* old;

1414} Heap;

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

2323// Should be used _between_ gc's.

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

2525#else

26−#define HEAP_CHECK(vm)

26+#define HEAP_CHECK(vm)

2727#endif // IDRIS_DEBUG

2828

2929#endif // _IDRIS_HEAP_H

rts/idris_main.c+1

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

2121 init_gmpalloc();

2222

2323 init_nullaries();

24+ init_signals();

2425

2526 _idris__123_runMain0_125_(vm, NULL);

2627

rts/idris_net.c+21−24

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

3838}

3939

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

41−// populates a struct addrinfo.

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

41+// populates a struct addrinfo.

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

4343 int family, int socket_type) {

4444

4545 struct addrinfo hints;

4646 // Convert port into string

4747 char str_port[8];

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

49−

49+

5050 // Set up hints structure

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

5252 hints.ai_family = family;

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

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

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

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

60− }

60+ }

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

6262

6363}

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

7575 //freeaddrinfo(address_res);

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

7777 return -1;

78− }

78+ }

7979 return 0;

8080}

8181

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

111111

112112int idrnet_sockaddr_ipv4_port(void* sockaddr) {

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

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

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

115115}

116116

117117void* idrnet_create_sockaddr() {

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

141141}

142142

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

144− idrnet_recv_result* res_struct =

144+ idrnet_recv_result* res_struct =

145145 (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));

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

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

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

149149 res_struct->result = recv_res;

150−

150+

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

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

153153 }

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

172172}

173173

174174void idrnet_free_recv_struct(void* res_struct) {

175− idrnet_recv_result* i_res_struct =

175+ idrnet_recv_result* i_res_struct =

176176 (idrnet_recv_result*) res_struct;

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

178178 free(i_res_struct->payload);

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

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

192192 if (addr_res == -1) {

193193 return -1;

194− }

194+ }

195195

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

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

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

198198 freeaddrinfo(remote_host);

199199 return send_res;

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

206206 if (addr_res == -1) {

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

208208 return -1;

209− }

209+ }

210210

211211 buf_htonl(buf, buf_len);

212212

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

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

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

215215 if (send_res == -1) {

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

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

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

225225/*

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

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

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

228228*/

229229 // Allocate the required structures, and nuke them

230− struct sockaddr_storage* remote_addr =

230+ struct sockaddr_storage* remote_addr =

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

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

233− idrnet_recvfrom_result* ret =

233+ idrnet_recvfrom_result* ret =

234234 (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));

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

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

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

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

241241 ret->result = recv_res;

242242 // Check for failure...

243− if (recv_res == -1) {

243+ if (recv_res == -1) {

244244 free(buf);

245245 free(remote_addr);

246246 } else {

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

255255 return ret;

256256}

257257

258−

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

260259 // Allocate the required structures, and nuke them

261− struct sockaddr_storage* remote_addr =

260+ struct sockaddr_storage* remote_addr =

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

263− idrnet_recvfrom_result* ret =

262+ idrnet_recvfrom_result* ret =

264263 (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));

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

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

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

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

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

271270 ret->result = recv_res;

272− if (recv_res == -1) {

271+ if (recv_res == -1) {

273272 free(remote_addr);

274273 }

275274 // 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) {

298297int idrnet_get_recvfrom_port(void* res_struct) {

299298 idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;

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

301− struct sockaddr_in* remote_addr_in =

300+ struct sockaddr_in* remote_addr_in =

302301 (struct sockaddr_in*) recv_struct->remote_addr;

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

304303 }

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

316315 }

317316 }

318317}

319−

320−

rts/idris_rts.c+16

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

11#include <assert.h>

2+#include <errno.h>

23

34#include "idris_rts.h"

45#include "idris_gc.h"

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

7273 init_threaddata(vm);

7374 init_gmpalloc();

7475 init_nullaries();

76+ init_signals();

7577

7678 return vm;

7779}

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

9294#endif

9395}

9496

97+void init_signals() {

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

99+ signal(SIGPIPE, SIG_IGN);

100+#endif

101+}

102+

95103Stats terminate(VM* vm) {

96104 Stats stats = vm->stats;

97105 STATS_ENTER_EXIT(stats)

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

927935 free(msg);

928936}

929937

938+int idris_errno() {

939+ return errno;

940+}

941+

942+char* idris_showerror(int err) {

943+ return strerror(err);

944+}

945+

930946VAL* nullary_cons;

931947

932948void init_nullaries() {

rts/idris_rts.h+8

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

99#include <pthread.h>

1010#endif

1111#include <stdint.h>

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

13+#include <signal.h>

14+#endif

1215

1316#include "idris_heap.h"

1417#include "idris_stats.h"

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

252255

253256#define NULL_CON(x) nullary_cons[x]

254257

258+int idris_errno();

259+char* idris_showerror(int err);

260+

255261extern VAL* nullary_cons;

256262void init_nullaries();

257263void free_nullaries();

258264

265+void init_signals();

266+

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

260268

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

rts/idris_stdfgn.c+36−6

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

22#include "idris_rts.h"

33#include "idris_gmp.h"

44#include "idris_gc.h"

5−#include <sys/select.h>

5+

66#include <fcntl.h>

7+#include <errno.h>

78#include <stdio.h>

89#include <time.h>

910

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

12+int win_fpoll(void* h);

13+#else

14+#include <sys/select.h>

15+#endif

16+

1017extern char** environ;

1118

1219void putStr(char* str) {

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

2431}

2532

2633int fileEOF(void* h) {

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

28− return feof(f);

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

35+ return feof(f);

2936}

3037

3138int fileError(void* h) {

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

33− return ferror(f);

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

40+ return ferror(f);

3441}

3542

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

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

4451

4552int fpoll(void* h)

4653{

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

55+ return win_fpoll(h);

56+#else

4757 FILE* f = (FILE*)h;

4858 fd_set x;

4959 struct timeval timeout;

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

5666

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

5868 return r;

69+#endif

5970}

6071

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

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

8697 return MKBIGI(t);

8798}

8899

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+

89119void idris_forceGC(void* vm) {

90− idris_gc((VM*)vm);

120+ idris_gc((VM*)vm);

91121}

rts/idris_stdfgn.h+2

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

1414int fileError(void* h);

1515// return 0 on success

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

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

18+VAL idris_mkFileError(VM* vm);

1719

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

1921int fpoll(void* h);

rts/windows/idris_net.c+6−7

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

1212#include <Ws2tcpip.h>

1313

1414

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,

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

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

1818 LPSTR pStringBuf, size_t StringBufSize);

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

5050 // Convert port into string

5151 char str_port[8];

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

53−

53+

5454 if (!check_init()) {

5555 return -1;

5656 }

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

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

7474 if (bind_res == -1) {

7575 return -1;

76− }

76+ }

7777

7878 return 0;

7979}

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

152152 if (!check_init()) {

153153 return NULL;

154154 }

155− idrnet_recv_result* res_struct =

155+ idrnet_recv_result* res_struct =

156156 (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));

157157

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

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

160160 res_struct->result = recv_res;

161−

161+

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

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

164164 }

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

182182}

183183

184184void idrnet_free_recv_struct(void* res_struct) {

185− idrnet_recv_result* i_res_struct =

185+ idrnet_recv_result* i_res_struct =

186186 (idrnet_recv_result*) res_struct;

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

188188 free(i_res_struct->payload);

@@ -193,4 +193,3 @@ void idrnet_free_recv_struct(void* res_struct) {

193193int idrnet_errno() {

194194 return errno;

195195}

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)

13931393 = (n, (p, t)) : collectImps sc

13941394 collectImps _ = []

13951395

1396− getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps

1396+ scopedimpl (Just i) = not (toplevel_imp i)

1397+ scopedimpl _ = False

1398+

1399+ getImps (Bind n (Pi i _ _) sc) imps

1400+ | scopedimpl i = getImps sc imps

13971401 getImps (Bind n (Pi _ t _) sc) imps

13981402 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

13991403 where

@@ -1556,9 +1560,9 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

15561560 pibind using [] sc = sc

15571561 pibind using (n:ns) sc

15581562 = case lookup n using of

1559− Just ty -> PPi (Imp [] Dynamic False Nothing)

1563+ Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))

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

15621566 n NoFC Placeholder (pibind using ns sc)

15631567

15641568-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+3−3

@@ -587,9 +587,9 @@ is_scoped :: Plicity -> Maybe ImplicitInfo

587587is_scoped (Imp _ _ _ s) = s

588588is_scoped _ = Nothing

589589

590−impl = Imp [] Dynamic False Nothing

591−forall_imp = Imp [] Dynamic False (Just (Impl False))

592−forall_constraint = Imp [] Dynamic False (Just (Impl True))

590+impl = Imp [] Dynamic False (Just (Impl False True))

591+forall_imp = Imp [] Dynamic False (Just (Impl False False))

592+forall_constraint = Imp [] Dynamic False (Just (Impl True False))

593593expl = Exp [] Dynamic False

594594expl_param = Exp [] Dynamic True

595595constraint = Constraint [] Static

src/Idris/CaseSplit.hs+47−27

@@ -50,8 +50,11 @@ names over '_', patterns over names, etc.

5050-}

5151

5252-- Given a variable to split, and a term application, return a list of

53−-- variable updates

54−split :: Name -> PTerm -> Idris [[(Name, PTerm)]]

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

57+split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])

5558split n t'

5659 = do ist <- getIState

5760 -- Make sure all the names in the term are accessible

@@ -77,15 +80,26 @@ split n t'

7780 logLvl 4 ("Working from " ++ show t)

7881 logLvl 4 ("Trying " ++ showSep "\n"

7982 (map (showTmImpls) newPats_in))

80− newPats <- mapM elabNewPat newPats_in

81− logLvl 3 ("Original:\n" ++ show t)

82− logLvl 3 ("Split:\n" ++

83− (showSep "\n" (map show (mapMaybe id newPats))))

84− logLvl 3 "----"

85− let newPats' = mergeAllPats ist n t (mapMaybe id newPats)

86− logLvl 1 ("Name updates " ++ showSep "\n"

87− (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))

88− return (map snd newPats')

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

89+ logLvl 3 ("Original:\n" ++ show t)

90+ logLvl 3 ("Split:\n" ++

91+ (showSep "\n" (map show newPats)))

92+ logLvl 3 "----"

93+ let newPats' = mergeAllPats ist n t newPats

94+ logLvl 1 ("Name updates " ++ showSep "\n"

95+ (map (\ (p, u) -> show u ++ " " ++ show p) 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

89103

90104data MergeState = MS { namemap :: [(Name, Name)],

91105 invented :: [(Name, Name)],

@@ -208,13 +222,13 @@ tidy ist tm ty = return tm

208222-- where tidyVar (PRef _ _) = Placeholder

209223-- tidyVar t = t

210224

211−elabNewPat :: PTerm -> Idris (Maybe PTerm)

225+elabNewPat :: PTerm -> Idris (Bool, PTerm)

212226elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

213227 i <- getIState

214− return (Just (delab i tm)))

228+ return (True, delab i tm))

215229 (\e -> do i <- getIState

216230 logLvl 5 $ "Not a valid split:\n" ++ pshow i e

217− return Nothing)

231+ return (False, t))

218232

219233findPats :: IState -> Type -> [PTerm]

220234findPats ist t | (P _ n _, _) <- unApply t

@@ -248,26 +262,27 @@ replaceVar ctxt n t pat = pat

248262splitOnLine :: Int -- ^ line number

249263 -> Name -- ^ variable

250264 -> FilePath -- ^ name of file

251− -> Idris [[(Name, PTerm)]]

265+ -> Idris (Bool, [[(Name, PTerm)]])

252266splitOnLine l n fn = do

253−-- let (before, later) = splitAt (l-1) (lines inp)

254−-- i <- getIState

255267 cl <- getInternalApp fn l

256268 logLvl 3 ("Working with " ++ showTmImpls cl)

257269 tms <- split n cl

258−-- iputStrLn (showSep "\n" (map show tms))

259− return tms -- "" -- not yet done...

270+ return tms

260271

261−replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]

262−replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

272+replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]

273+replaceSplits l ups impossible

274+ = updateRHSs 1 (map (rep (expandBraces l)) ups)

263275 where

264276 rep str [] = str ++ "\n"

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

266278

267279 updateRHSs i [] = return []

268− updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x

269− xs' <- updateRHSs i' xs

270− return (x' : xs')

280+ updateRHSs i (x : xs)

281+ | impossible = do xs' <- updateRHSs i xs

282+ return (setImpossible False x : xs')

283+ | otherwise = do (x', i') <- updateRHS (null xs) i x

284+ xs' <- updateRHSs i' xs

285+ return (x' : xs')

271286

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

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

@@ -283,6 +298,11 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

283298 return (x : xs', i')

284299 updateRHS last i [] = return ("", i)

285300

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 [] = ""

286306

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

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

342362 -> Idris String

343363getClause l fn un fp

344364 = do i <- getIState

345− case lookupCtxt fn (idris_classes i) of

365+ case lookupCtxt un (idris_classes i) of

346366 [c] -> return (mkClassBodies i (class_methods c))

347367 _ -> do ty_in <- getInternalApp fp l

348368 let ty = case ty_in of

@@ -434,8 +454,8 @@ nameMissing ps = do ist <- get

434454

435455 nm ptm = do mptm <- elabNewPat ptm

436456 case mptm of

437− Nothing -> return ptm

438− Just ptm' -> return ptm'

457+ (False, _) -> return ptm

458+ (True, ptm') -> return ptm'

439459

440460

441461

src/Idris/Completion.hs+2−8

@@ -12,7 +12,7 @@ import Idris.Colours

1212import Idris.ParseHelpers(opChars)

1313import qualified Idris.ParseExpr (constants, tactics)

1414import Idris.ParseExpr (TacticArg (..))

15−import Idris.REPLParser (allHelp)

15+import Idris.REPLParser (allHelp, setOptions)

1616import Control.Monad.State.Strict

1717

1818import Data.List

@@ -82,13 +82,7 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

8282

8383completeOption :: CompletionFunc Idris

8484completeOption = completeWord Nothing " \t" completeOpt

85− where completeOpt = return . completeWith [ "errorcontext"

86− , "showimplicits"

87− , "originalerrors"

88− , "autosolve"

89− , "nobanner"

90− , "desugarnats"

91− ]

85+ where completeOpt = return . completeWith (map fst setOptions)

9286

9387completeConsoleWidth :: CompletionFunc Idris

9488completeConsoleWidth = completeWord Nothing " \t" completeW

src/Idris/Core/Binary.hs+3−2

@@ -484,10 +484,11 @@ instance Binary Raw where

484484instance Binary ImplicitInfo where

485485 put x

486486 = case x of

487− Impl x1 -> put x1

487+ Impl x1 x2 -> do put x1; put x2

488488 get

489489 = do x1 <- get

490− return (Impl x1)

490+ x2 <- get

491+ return (Impl x1 x2)

491492

492493instance (Binary b) => Binary (Binder b) where

493494 put x

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

@@ -167,7 +167,7 @@ instance NFData ErrorReportPart where

167167 rnf (SubReport x1) = rnf x1 `seq` ()

168168

169169instance NFData ImplicitInfo where

170− rnf (Impl x1) = rnf x1 `seq` ()

170+ rnf (Impl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

171171

172172instance (NFData b) => NFData (Binder b) where

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

353353unifyGoal :: Raw -> Elab' aux ()

354354unifyGoal t = processTactic' (UnifyGoal t)

355355

356+unifyTerms :: Raw -> Raw -> Elab' aux ()

357+unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)

358+

356359exact :: Raw -> Elab' aux ()

357360exact t = processTactic' (Exact t)

358361

@@ -724,7 +727,12 @@ checkPiGoal n

724727 focus f

725728

726729simple_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 =

728736 do a <- getNameFrom (sMN 0 "__argTy")

729737 b <- getNameFrom (sMN 0 "__retTy")

730738 f <- getNameFrom (sMN 0 "f")

@@ -755,8 +763,49 @@ simple_app infer fun arg str =

755763 when (a `elem` hs) $ do movelast a

756764 when (b `elem` hs) $ do movelast b

757765 end_unify

758− where

759− regretWith err = try regret (lift $ tfail err)

766+

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

760809

761810-- Abstract over an argument of unknown type, giving a name for the hole

762811-- which we'll fill with the argument type too.

src/Idris/Core/Evaluate.hs+10−1

@@ -2,7 +2,8 @@

22 PatternGuards #-}

33{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

44

5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,

5+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

6+ normaliseAll, normaliseBlocking, toValue, quoteTerm,

67 rt_simplify, simplify, specialise, hnf, convEq, convEq',

78 Def(..), CaseInfo(..), CaseDefs(..),

89 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

@@ -79,11 +80,19 @@ normaliseC ctxt env t

7980 = evalState (do val <- eval False ctxt [] (map finalEntry env) t []

8081 quote 0 val) initEval

8182

83+-- | Normalise everything, whether abstract, private or public

8284normaliseAll :: Context -> Env -> TT Name -> TT Name

8385normaliseAll ctxt env t

8486 = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]

8587 quote 0 val) initEval

8688

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+

8796normalise :: Context -> Env -> TT Name -> TT Name

8897normalise = normaliseTrace False

8998

src/Idris/Core/Execute.hs+11

@@ -349,6 +349,17 @@ execForeign env ctxt arity ty fn xs onfail

349349 "The argument to fileEOF should be a file handle, but it was " ++

350350 show handle ++

351351 ". 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?"

352363 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs

353364 = case handle of

354365 EHandle h -> do execIO $ hClose h

src/Idris/Core/ProofState.hs+10

@@ -91,6 +91,7 @@ data Tactic = Attack

9191 | MatchProblems Bool

9292 | UnifyProblems

9393 | UnifyGoal Raw

94+ | UnifyTerms Raw Raw

9495 | ProofState

9596 | Undo

9697 | QED

@@ -477,6 +478,13 @@ unifyGoal tm ctxt env h@(Bind x b sc) =

477478 return h

478479unifyGoal _ _ _ _ = fail "The focus is not a binder."

479480

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+

480488exact :: Raw -> RunTactic

481489exact guess ctxt env (Bind x (Hole ty) sc) =

482490 do (val, valty) <- lift $ check ctxt env guess

@@ -1113,3 +1121,5 @@ process t h = tactic (Just h) (mktac t)

11131121 mktac (SetInjective n) = setinj n

11141122 mktac (MoveLast n) = movelast n

11151123 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

811811deriving instance NFData Raw

812812!-}

813813

814−data ImplicitInfo = Impl { tcinstance :: Bool }

814+data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool }

815815 deriving (Show, Eq, Ord, Data, Typeable)

816816

817817{-!

@@ -1612,7 +1612,7 @@ pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

16121612 pureBinder (Let t v) = pureTerm t && pureTerm v

16131613 pureBinder t = pureTerm (binderTy t)

16141614

1615− notClassName (MN _ c) | c == txt "class" = False

1615+ notClassName (MN _ c) | c == txt "__class" = False

16161616 notClassName _ = True

16171617

16181618pureTerm _ = True

src/Idris/DSL.hs+4−1

@@ -108,7 +108,10 @@ expandSugar dsl (PDoBlock ds)

108108 block b (DoExp fc tm : rest)

109109 = PApp fc b

110110 [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

112115 block b _ = PElabError (Msg "Invalid statement in do block")

113116

114117expandSugar 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

110110 _ -> PRef un [] n

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

112112 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

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)

113116 de env is (Bind n (Pi (Just impl) ty _) sc)

114117 | tcinstance impl

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

258258 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

259259 insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)

260260 = 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"

262262 in PPi (constraint { pstatic = Static })

263263 dictN NoFC c

264264 (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

551551 -- pattern bindings

552552 i <- getIState

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

554560 -- get the parameters first, to pass through to any where block

555561 let fn_ty = case lookupTy fname (tt_ctxt i) of

556562 [t] -> t

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

663669 (erun fc (build i winfo ERHS opts fname rhs))

664670 errAt "right hand side of " fname (Just clhsty)

665671 (erun fc $ psolve lhs_tm)

666− hs <- get_holes

667− mapM_ (elabCaseHole is) hs

668672 tt <- get_term

669673 aux <- getAux

670674 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

782786 (b : bf, af)

783787 sepBlocks' ns [] = ([], [])

784788

785−

786− -- if a hole is just an argument/result of a case block, treat it as

787− -- the unit type. Hack to help elaborate case in do blocks.

788− elabCaseHole aux h = do

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

789+ -- term is not within "with" block

790+ isOutsideWith :: PTerm -> Bool

791+ isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False

792+ isOutsideWith _ = True

805793

806794elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

807795 = do let tcgen = Dictionary `elem` opts

src/Idris/Elab/Term.hs+46−34

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

363363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

364364 = do g <- goal; resolveTC' False False 5 g fn ist

365365 elab' ina fc (PResolveTC fc')

366− = do c <- getNameFrom (sMN 0 "class")

366+ = do c <- getNameFrom (sMN 0 "__class")

367367 instanceArg c

368368 -- Elaborate the equality type first homogeneously, then

369369 -- heterogeneously as a fallback

@@ -1028,12 +1028,22 @@ elab ist info emode opts fn tm

10281028 solve

10291029 elab' ina _ c@(PCase fc scr opts)

10301030 = do attack

1031+

10311032 tyn <- getNameFrom (sMN 0 "scty")

10321033 claim tyn RType

10331034 valn <- getNameFrom (sMN 0 "scval")

10341035 scvn <- getNameFrom (sMN 0 "scvar")

10351036 claim valn (Var tyn)

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

10371047 focus valn

10381048 elabE (ina { e_inarg = True }) (Just fc) scr

10391049 -- Solve any remaining implicits - we need to solve as many

@@ -1084,6 +1094,21 @@ elab ist info emode opts fn tm

10841094 Just xs@(_:_) -> sNS n xs

10851095 _ -> n

10861096

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+

10871112 inApp (P _ n _) = [n]

10881113 inApp (App _ f a) = inApp f ++ inApp a

10891114 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

@@ -1415,9 +1440,9 @@ elab ist info emode opts fn tm

14151440 notImplicitable _ = False

14161441

14171442 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1418− | tcinstance i

1443+ | tcinstance i && not (toplevel_imp i)

14191444 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1420− | otherwise

1445+ | not (toplevel_imp i)

14211446 = pimp n Placeholder True : insertScopedImps fc sc xs

14221447 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

14231448 = x : insertScopedImps fc sc xs

@@ -1696,38 +1721,25 @@ resolveTC' di mv depth tm n ist

16961721

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

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

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

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

1724+collectDeferred top casenames ctxt tm = cd [] tm

17041725 where

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

1706− -- not a name we're immediately going to define in a case block, so that

1707− -- any immediate specialisation of the function applied to constructors

1708− -- can be done

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

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

1711− (tidyArg ((n, b) : env) sc)

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

1723− where

1724− cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)

1725− cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)

1726− cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)

1727− return (b { binderTy = ty' })

1728−collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)

1729− (collectDeferred top ns ctxt a)

1730−collectDeferred top ns ctxt t = return t

1726+ cd env (Bind n (GHole i psns t) app) =

1727+ do ds <- get

1728+ t' <- collectDeferred top casenames ctxt t

1729+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])

1730+ cd env app

1731+ cd env (Bind n b t)

1732+ = do b' <- cdb b

1733+ t' <- cd ((n, b) : env) t

1734+ return (Bind n b' t')

1735+ where

1736+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)

1737+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1738+ cdb b = do ty' <- cd env (binderTy b)

1739+ return (b { binderTy = ty' })

1740+ cd env (App s f a) = liftM2 (App s) (cd env f)

1741+ (cd env a)

1742+ cd env t = return t

17311743

17321744case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

17331745case_ ind autoSolve ist fn tm = do

src/Idris/Elab/Value.hs+2−1

@@ -127,7 +127,8 @@ elabExec fc tm = runtm (PAlternative [] FirstSuccess

127127 printtm tm

128128 ])

129129 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]

131132 printtm t = PApp fc (PRef fc [] (sUN "printLn"))

132133 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

133134

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 126

43+ibcVersion = 127

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

src/Idris/Interactive.hs+2−2

@@ -34,10 +34,10 @@ import Debug.Trace

3434caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

3535caseSplitAt fn updatefile l n

3636 = do src <- runIO $ readSource fn

37− res <- splitOnLine l n fn

37+ (ok, res) <- splitOnLine l n fn

3838 logLvl 1 (showSep "\n" (map show res))

3939 let (before, (ap : later)) = splitAt (l-1) (lines src)

40− res' <- replaceSplits ap res

40+ res' <- replaceSplits ap res (not ok)

4141 let new = concat res'

4242 if updatefile

4343 then do let fb = fn ++ "~" -- make a backup!

src/Idris/ParseExpr.hs+3−3

@@ -1051,10 +1051,10 @@ normalImplicit opts st syn = do

10511051 sc <- expr syn

10521052 let (im,cl)

10531053 = if implicitAllowed syn

1054− then (Imp opts st False Nothing,

1054+ then (Imp opts st False (Just (Impl False True)),

10551055 constraint)

1056− else (Imp opts st False (Just (Impl False)),

1057− Imp opts st False (Just (Impl True)))

1056+ else (Imp opts st False (Just (Impl False False)),

1057+ Imp opts st False (Just (Impl True False)))

10581058 return (bindList (PPi im) xt

10591059 (bindList (PPi cl) cs sc))

10601060

src/Idris/REPL.hs+11−3

@@ -805,7 +805,11 @@ process fn (Eval t)

805805 getIState >>= flip warnDisamb t

806806 (tm, ty) <- elabREPL recinfo ERHS t

807807 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

809813 let ty' = perhapsForce $ normaliseAll ctxt [] ty

810814 -- Add value to context, call it "it"

811815 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

@@ -813,7 +817,8 @@ process fn (Eval t)

813817 logLvl 3 $ "Raw: " ++ show (tm', ty')

814818 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

815819 let tmDoc = pprintDelab ist tm'

816− tyDoc = pprintDelab ist ty'

820+ -- errReverse to make type more readable

821+ tyDoc = pprintDelab ist (errReverse ist ty')

817822 iPrintTermWithType tmDoc tyDoc

818823 where perhapsForce tm | termSmallerThan 100 tm = force tm

819824 | otherwise = tm

@@ -938,7 +943,8 @@ process fn (Check (PRef _ _ n))

938943 where

939944 showMetavarInfo ppo ist n i

940945 = case lookupTy n (tt_ctxt ist) of

941− (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

946+ (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

947+ putTy ppo ist i [] (delab ist (errReverse ist ty'))

942948 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

943949 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

944950 putTy ppo ist i bnd (PPi _ n _ t sc)

@@ -1059,6 +1065,8 @@ process fn (DebugInfo n)

10591065 when (not (null si)) $ iputStrLn (show si)

10601066 let di = lookupCtxt n (idris_datatypes i)

10611067 when (not (null di)) $ iputStrLn (show di)

1068+ let imps = lookupCtxt n (idris_implicits i)

1069+ when (not (null imps)) $ iputStrLn (show imps)

10621070 let d = lookupDef n (tt_ctxt i)

10631071 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

10641072 let cg = lookupCtxtName n (idris_callgraph i)

src/Idris/REPLParser.hs+26−13

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

11

2−module Idris.REPLParser (parseCmd, help, allHelp) where

2+module Idris.REPLParser (parseCmd, help, allHelp, setOptions) where

33

44import System.FilePath ((</>))

55import System.Console.ANSI (Color(..))

@@ -32,6 +32,16 @@ parseCmd i inputname = P.runparser pCmd i inputname . trim

3232type CommandTable = [ ( [String], CmdArg, String

3333 , String -> P.IdrisParser (Either String Command) ) ]

3434

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+

3545help :: [([String], CmdArg, String)]

3646help = (["<expr>"], NoArg, "Evaluate an expression") :

3747 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

@@ -80,7 +90,7 @@ parserCommandsForHelp =

8090 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

8191 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

8292 , 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 ++ ")"

8494 , optArgCmd ["unset"] UnsetOpt "Unset an option"

8595 , (["color", "colour"], ColourArg

8696 , "Turn REPL colours on or off; set a specific colour"

@@ -100,6 +110,7 @@ parserCommandsForHelp =

100110 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

101111 , cmd_pprint)

102112 ]

113+ where optionsList = intercalate ", " $ map fst setOptions

103114

104115parserCommands =

105116 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

@@ -163,10 +174,9 @@ pCmd :: P.IdrisParser (Either String Command)

163174pCmd = choice [ do c <- cmd names; parser c

164175 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

165176 <|> unrecognized

166− <|> nop

177+ <|> nop

167178 <|> eval

168179 where nop = do eof; return (Right NOP)

169− eval = exprArg Eval ""

170180 unrecognized = do

171181 P.lchar ':'

172182 cmd <- many anyChar

@@ -194,16 +204,26 @@ noArgs cmd name = do

194204

195205 emptyArgs <|> failure

196206

207+eval :: P.IdrisParser (Either String Command)

208+eval = do

209+ t <- P.fullExpr defaultSyntax

210+ return $ Right (Eval t)

211+

197212exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

198213exprArg cmd name = do

199214 let noArg = do

200215 eof

201216 return $ Left ("Usage is :" ++ name ++ " <expression>")

202217

218+ let justOperator = do

219+ (op, fc) <- P.operatorFC

220+ eof

221+ return $ Right $ cmd (PRef fc [] (sUN op))

222+

203223 let properArg = do

204224 t <- P.fullExpr defaultSyntax

205225 return $ Right (cmd t)

206− try noArg <|> properArg

226+ try noArg <|> try justOperator <|> properArg

207227

208228

209229

@@ -253,14 +273,7 @@ optArg cmd name = do

253273

254274 where

255275 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

263− <|> do discard (P.symbol "desugarnats"); return DesugarNats

276+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

264277

265278proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

266279proofArg cmd name = do

src/Idris/Reflection.hs+3−3

@@ -357,8 +357,8 @@ reifyTTConstApp f v@(P _ _ _) =

357357reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

358358

359359reifyArithTy :: Term -> ElabD ArithTy

360−reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

361−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

360+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

361+reifyArithTy (P _ n _) | n == reflm "ATDouble" = return ATFloat

362362reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

363363

364364reifyNativeTy :: Term -> ElabD NativeTy

@@ -768,7 +768,7 @@ reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

768768reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

769769reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]

770770reflectConstant (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")]

772772reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]

773773reflectConstant StrType = Var (reflm "StrType")

774774reflectConstant (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

1515import Control.Monad.State.Strict

1616import Control.Applicative

1717import System.FilePath (takeFileName, isValid)

18+import Data.Maybe (isNothing, fromJust)

1819

1920import Util.System

2021

@@ -79,18 +80,32 @@ filename = (do

7980 -- Through at least version 0.9.19.1, IPKG executable values were

8081 -- possibly namespaced identifiers, like foo.bar.baz.

8182 show <$> fst <$> iName []

82− if isValidFilename filename

83− then return filename

84− else fail "a filename must be non-empty and have no directory component")

83+ case filenameErrorMessage filename of

84+ Just errorMessage -> fail errorMessage

85+ Nothing -> return filename)

8586 <?> "filename"

8687 where

87− isValidFilename :: FilePath -> Bool

88− isValidFilename path =

89− and [isNonEmpty, isValidPath, hasNoDirectoryComponent]

88+ -- TODO: Report failing span better! We could lookAhead,

89+ -- or do something with DeltaParsing?

90+ filenameErrorMessage :: FilePath -> Maybe String

91+ filenameErrorMessage path = either Just (const Nothing) $ do

92+ checkEmpty path

93+ checkValid path

94+ checkNoDirectoryComponent path

9095 where

91− isNonEmpty = path /= ""

92− isValidPath = System.FilePath.isValid path

93− hasNoDirectoryComponent = path == takeFileName 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 =

103+ checkThat (System.FilePath.isValid path)

104+ "filename must contain only valid characters"

105+

106+ checkNoDirectoryComponent path =

107+ checkThat (path == takeFileName path)

108+ "filename must contain no directory component"

94109

95110

96111pClause :: PParser ()

src/Util/System.hs+11−7

@@ -16,9 +16,8 @@ import System.Directory (getTemporaryDirectory

1616 , removeFile

1717 , removeDirectoryRecursive

1818 , createDirectoryIfMissing

19− , doesDirectoryExist

2019 )

21−import System.FilePath ((</>), normalise, isAbsolute, dropFileName)

20+import System.FilePath ((</>), normalise)

2221import System.IO

2322import System.Info

2423import System.IO.Error

@@ -66,7 +65,7 @@ isATTY = do

6665withTempdir :: String -> (FilePath -> IO a) -> IO a

6766withTempdir subdir callback

6867 = do dir <- getTemporaryDirectory

69− let tmpDir = (normalise dir) </> subdir

68+ let tmpDir = normalise dir </> subdir

7069 removeLater <- catchIO (createDirectoryIfMissing True tmpDir >> return True)

7170 (\ ioError -> if isAlreadyExistsError ioError then return False

7271 else throw ioError

@@ -76,10 +75,15 @@ withTempdir subdir callback

7675 return result

7776

7877rmFile :: FilePath -> IO ()

79−rmFile f = do putStrLn $ "Removing " ++ f

80− catchIO (removeFile f)

81− (\ioerr -> putStrLn $ "WARNING: Cannot remove file "

82− ++ f ++ ", Error msg:" ++ show ioerr)

78+rmFile f = do

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

85+ | otherwise = putStrLn $ "WARNING: Cannot remove file "

86+ ++ f ++ ", Error msg:" ++ show e

8387

8488setupBundledCC :: IO()

8589#ifdef FREESTANDING

test/basic002/test006.idr+1−1

@@ -23,7 +23,7 @@ main = do printLn (natToBin 42)

2323---------- Proofs ----------

2424

2525Main.parity_lemma_2 = proof {

26− intro;

26+ intro j;

2727 intro;

2828 rewrite sym (plusSuccRightSucc j j);

2929 trivial;

test/dsl002/test014.idr+6−5

@@ -15,16 +15,17 @@ syntax "ifM" [test] "then" [t] "else" [e]

1515 = test >>= (\b => if b then t else e)

1616

1717open : String -> (p:Purpose) -> Creator (Either () (FILE p))

18−open fn p = ioc (do h <- fopen fn (pstring p)

19− ifM validFile h

20− then return (Right (OpenH h))

21− else return (Left ()))

18+open fn p = ioc (do Right h <- fopen fn (pstring p)

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

20+ return (Right (OpenH h)))

2221

2322close : FILE p -> Updater ()

2423close (OpenH h) = iou (closeFile h)

2524

2625readLine : 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)

2829

2930eof : FILE Reading -> Reader Bool

3031eof (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

22

33%dynamic "dummy", "libm", "msvcrt"

44

5−x : Float

6−x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)

5+x : Double

6+x = unsafePerformIO (foreign FFI_C "sin" (Double -> IO Double) 1.6)

77

88main : IO ()

99main = putStrLn (show x)

test/ffi004/test026.idr+2−1

@@ -10,7 +10,8 @@ strToType _ = Nat

1010

1111-- If the file contains "Int", provide Int as a type, otherwise provide Nat

1212fromFile : 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)

1415 return (Provide (strToType (trim str)))

1516

1617%provide (T1 : Type) with fromFile "theType"

test/interactive001/expected+6

@@ -11,3 +11,9 @@ isElem2 x (y :: ys) with (_)

1111 [] => ?bar_1

1212 (x :: ys) => ?bar_2

1313

14+elemVoid1 Here impossible

15+elemVoid1 (There _) impossible

16+

17+ Here impossible

18+ (There _) impossible

19+

test/interactive001/input+2

@@ -4,3 +4,5 @@

44:mw 26 isElem2

55:cs 31 p

66: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)

3434foo : List a -> List a

3535foo xs = case xs of

3636 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

88 False => return ()

99

1010dumpFile : String -> IO ()

11−dumpFile fn = do { h <- openFile fn Read

11+dumpFile fn = do { Right h <- openFile fn Read

1212 mwhile (do { -- putStrLn "TEST"

1313 x <- feof h

1414 return (not x) })

15− (do { l <- fread h

15+ (do { Right l <- fread h

1616 putStr l })

1717 closeFile h }

1818

1919main : IO ()

20−main = do { h <- openFile "testfile" Write

20+main = do { Right h <- openFile "testfile" Write

2121 fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"

2222 closeFile h

2323 putStrLn "Reading testfile"

24− f <- readFile "testfile"

24+ Right f <- readFile "testfile"

2525 putStrLn f

2626 putStrLn "---"

2727 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

22

33pkgs = effects

44

5−opts = "--warnpartial --warnreach"

5+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

66

77modules = Main

test/pkg002/expected−1

@@ -1 +0,0 @@

1−Type checking ./Main.idr

test/pkg002/test.ipkg+2

@@ -2,5 +2,7 @@ package test

22

33modules = Main

44

5+

6+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

57main = Main

68executable = some.namespaced.identifier

test/pkg003/expected−1

@@ -1 +0,0 @@

1−Type checking ./Main.idr

test/pkg003/run+1−1

@@ -3,4 +3,4 @@

33### containing a valid filename.

44idris $@ --build test.ipkg

55rm -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

22

33modules = Main

44

5+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

56main = 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

2− must be non-empty and have no

3− directory

1+Uncaught error: user error ([1mtest.ipkg[0m:[1m10[0m:[1m1[0m: [91merror[0m: filename

2+ must contain no directory

43 component, expected: space

54[1m[94m<EOF>[0;1m[0m

65[92m^[0m )

test/pkg004/test.ipkg+3

@@ -2,5 +2,8 @@ package test

22

33modules = Main

44

5+

6+opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

7+

58main = Main

69executable = "filenames/cannot include\a directory separator"

test/reg001/reg001.idr+26

@@ -182,3 +182,29 @@ hVectEx1 = ["Hello",[1,2,3],42,(0,10)]

182182

183183vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]

184184vecfoo = 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 @@

11#!/usr/bin/env bash

22idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check

33idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check

4+idris --nocolour --consolewidth 80 $@ tutorial006c.idr -p effects --check

45rm -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"