b24a685 · Idris-dev · git.iko.soy

CHANGELOG+5

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

docs/effects/depeff.rst+1−1

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

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

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/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/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/prelude/IO.idr+9−4

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

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

176175 FFI_C : FFI

177176 FFI_C = MkFFI C_Types String String

178177

178+||| The type of interactive programs, performing some I/O side effects

179+||| and returning a value.

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

179181%error_reverse

180−IO : Type -> Type

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

181183IO = IO' FFI_C

182184

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

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

198200 forceGC : IO ()

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

200202

203+ getErrno : IO Int

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

205+

201206--------- The Javascript/Node FFI

202207

203208

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/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/idris_rts.c+9

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

11#include <assert.h>

2+#include <errno.h>

23

34#include "idris_rts.h"

45#include "idris_gc.h"

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

934935 free(msg);

935936}

936937

938+int idris_errno() {

939+ return errno;

940+}

941+

942+char* idris_showerror(int err) {

943+ return strerror(err);

944+}

945+

937946VAL* nullary_cons;

938947

939948void init_nullaries() {

rts/idris_rts.h+3

@@ -255,6 +255,9 @@ void idris_free(void* ptr, size_t size);

255255

256256#define NULL_CON(x) nullary_cons[x]

257257

258+int idris_errno();

259+char* idris_showerror(int err);

260+

258261extern VAL* nullary_cons;

259262void init_nullaries();

260263void free_nullaries();

rts/idris_stdfgn.c+20

@@ -4,6 +4,7 @@

44#include "idris_gc.h"

55#include <sys/select.h>

66#include <fcntl.h>

7+#include <errno.h>

78#include <stdio.h>

89#include <time.h>

910

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

8687 return MKBIGI(t);

8788}

8889

90+VAL idris_mkFileError(VM* vm) {

91+ VAL result;

92+ switch(errno) {

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

94+ // Prelude.File

95+ case ENOENT:

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

97+ break;

98+ case EACCES:

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

100+ break;

101+ default:

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

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

104+ break;

105+ }

106+ return result;

107+}

108+

89109void idris_forceGC(void* vm) {

90110 idris_gc((VM*)vm);

91111}

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

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/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/REPL.hs+7−2

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

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