b24a685 · Idris-dev · git.iko.soy

CHANGELOG+5

compare with master

unifiedsplit

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

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

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

21 arguments, are treated as bound pattern variables.

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

23+ deprecated name is referenced.

22

24

23Library updates

25Library updates

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

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

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

37 from Effectful programs.

39 from Effectful programs.

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

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

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

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

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

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

44+ that they may fail.

40

45

41Tool updates

46Tool updates

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

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

docs/effects/depeff.rst+1−1

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

48 readInt = do let x = trim !getStr

49 putM (cast x :: !get)

50

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

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

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

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

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

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

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

112

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

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

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

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

116

117.. code:: idris

118

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

126 MyListType : Type

127 MyListType = List Int

128

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

130+arguments mean it is often a good idea.

131+

129.. _syntax-data-types:

132.. _syntax-data-types:

130

133

131Data types

134Data types

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

622

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

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

libs/contrib/Network/Socket.idr−4

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

143 socketType : SocketType

144 protocalNumber : ProtocolNumber

145

146−||| Get the C error number

147−getErrno : IO Int

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

149−

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

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

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

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

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

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

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

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

74

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

76instance Handler FileIO IO where

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

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

78− valid <- validFile h

78+ | Left err => k False ()

79− if valid then k True (FH h)

79+ k True (FH h)

80− else k False ()

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

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

82 k () ()

81 k () ()

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

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

83+ -- Need proper error handling!

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

84 k str (FH h)

85 k str (FH h)

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

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

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

86 k () (FH h)

88 k () (FH h)

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

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

88 k e (FH h)

90 k e (FH h)

89

91

90instance Handler FileIO (IOExcept a) where

92instance Handler FileIO (IOExcept a) where

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

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

92− valid <- ioe_lift $ validFile h

94+ | Left err => k False ()

93− if valid then k True (FH h)

95+ k True (FH h)

94− else k False ()

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

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

96 k () ()

97 k () ()

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

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

99+ -- Need proper error handling!

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

98 k str (FH h)

101 k str (FH h)

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

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

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

100 k () (FH h)

104 k () (FH h)

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

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

102 k e (FH h)

106 k e (FH h)

libs/prelude/IO.idr+9−4

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

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

37||| it.

38abstract

39−%error_reverse

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

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

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

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

42

41

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

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

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

118liftPrimIO = MkIO

117liftPrimIO = MkIO

119

118

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

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

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

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

122

121

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

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

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

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

125run__IO f = call__IO f

124run__IO f = call__IO f

126

125

127unsafePerformIO : IO' ffi a -> a

126unsafePerformIO : IO' ffi a -> a

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

176 FFI_C : FFI

175 FFI_C : FFI

177 FFI_C = MkFFI C_Types String String

176 FFI_C = MkFFI C_Types String String

178

177

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

179+||| and returning a value.

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

179%error_reverse

181%error_reverse

180−IO : Type -> Type

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

181IO = IO' FFI_C

183IO = IO' FFI_C

182

184

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

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

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

198 forceGC : IO ()

200 forceGC : IO ()

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

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

200

202

203+ getErrno : IO Int

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

205+

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

206--------- The Javascript/Node FFI

202

207

203

208

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

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

10import Prelude.Bool

11import Prelude.Basics

12import Prelude.Classes

13−import Prelude.Monad

13+import Prelude.Either

14+import Prelude.Show

14import IO

15import IO

15

16

16%access public

17%access public

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

19abstract

20abstract

20data File = FHandle Ptr

21data File = FHandle Ptr

21

22

23+||| An error from a file operation

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

25+-- the values correspond!

26+data FileError = FileReadError

27+ | FileWriteError

28+ | FileNotFound

29+ | PermissionDenied

30+ | GenericFileError Int -- errno

31+

32+private

33+strError : Int -> String

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

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

36+

37+getFileError : IO FileError

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

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

40+ return err

41+

42+instance Show FileError where

43+ show FileNotFound = "File Not Found"

44+ show PermissionDenied = "Permission Denied"

45+ show (GenericFileError errno) = strError errno

46+

22||| Standard input

47||| Standard input

23stdin : File

48stdin : File

24stdin = FHandle prim__stdin

49stdin = FHandle prim__stdin

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

31stderr : File

56stderr : File

32stderr = FHandle prim__stderr

57stderr = FHandle prim__stderr

33

58

59+do_ferror : Ptr -> IO Int

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

61+

62+ferror : File -> IO Bool

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

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

65+

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

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

35do_fopen : String -> String -> IO Ptr

67do_fopen : String -> String -> IO Ptr

36do_fopen f m

68do_fopen f m

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

39||| Open a file

71||| Open a file

40||| @ f the filename

72||| @ f the filename

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

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

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

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

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

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

76+ if !(nullPtr h)

77+ then do err <- getFileError

44− return (FHandle h)

78+ return (Left err)

79+ else return (Right (FHandle h))

45

80

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

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

47−partial

48validFile : File -> IO Bool

82validFile : File -> IO Bool

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

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

50 return (not x)

84 return (not x)

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

55||| Open a file

89||| Open a file

56||| @ f the filename

90||| @ f the filename

57||| @ m the mode

91||| @ m the mode

58−partial

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

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

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

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

61 modeStr Read = "r"

94 modeStr Read = "r"

62 modeStr Write = "w"

95 modeStr Write = "w"

63 modeStr ReadWrite = "r+"

96 modeStr ReadWrite = "r+"

64

97

65−partial

66do_fclose : Ptr -> IO ()

98do_fclose : Ptr -> IO ()

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

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

68

100

69−partial

70closeFile : File -> IO ()

101closeFile : File -> IO ()

71closeFile (FHandle h) = do_fclose h

102closeFile (FHandle h) = do_fclose h

72

103

73−partial

74do_fread : Ptr -> IO' l String

104do_fread : Ptr -> IO' l String

75do_fread h = prim_fread h

105do_fread h = prim_fread h

76

106

77−fgetc : File -> IO Char

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

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

79−

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

81−fgetc' (FHandle h)

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

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

109+ if !(ferror (FHandle h))

83− if (x < 0) then return Nothing

110+ then return (Left FileReadError)

84− else return (Just (cast x))

111+ else return (Right c)

85

112

86fflush : File -> IO ()

113fflush : File -> IO ()

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

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

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

89do_popen : String -> String -> IO Ptr

116do_popen : String -> String -> IO Ptr

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

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

91

118

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

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

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

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

121+ if !(nullPtr ptr)

122+ then do err <- getFileError

123+ return (Left err)

94− return (FHandle ptr)

124+ else return (Right (FHandle ptr))

95 where

125 where

96 modeStr Read = "r"

126 modeStr Read = "r"

97 modeStr Write = "w"

127 modeStr Write = "w"

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

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

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

104-- prim__vm h

134-- prim__vm h

105

135

106−partial

107−fread : File -> IO' l String

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

108−fread (FHandle h) = do_fread h

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

109−

138+ if !(ferror (FHandle h))

110−partial

139+ then return (Left FileReadError)

140+ else return (Right str)

141+

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

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

112−do_fwrite h s = do prim_fwrite h s

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

113− return ()

144+ if (res /= 0)

114−

145+ then do errno <- getErrno

115−partial

146+ if errno == 0

147+ then return (Left FileWriteError)

148+ else do err <- getFileError

149+ return (Left err)

150+ else return (Right ())

151+

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

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

117fwrite (FHandle h) s = do_fwrite h s

153fwrite (FHandle h) s = do_fwrite h s

118

154

119−partial

120do_feof : Ptr -> IO Int

155do_feof : Ptr -> IO Int

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

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

122

157

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

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

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

126 return (not (eof == 0))

161 return (not (eof == 0))

127

162

128−partial

129−do_ferror : Ptr -> IO Int

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

131−

132−ferror : File -> IO Bool

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

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

135−

136fpoll : File -> IO Bool

163fpoll : File -> IO Bool

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

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

138 return (p > 0)

165 return (p > 0)

139

166

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

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

141−partial -- no error checking!

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

169+covering

142−readFile : String -> IO String

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

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

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

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

144 c <- readFile' h ""

173 c <- readFile' h ""

145 closeFile h

174 closeFile h

146 return c

175 return c

147 where

176 where

148 partial

177 partial

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

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

150 readFile' h contents =

179 readFile' h contents =

151 do x <- feof h

180 do x <- feof h

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

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

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

153 readFile' h (contents ++ l)

183 readFile' h (contents ++ l)

154− else return contents

184+ else return (Right contents)

155−

185+

156−

186+||| Write a string to a file

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

188+ IO (Either FileError ())

189+writeFile fn contents = do

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

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

192+ closeFile h

193+ return (Right ())

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

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

17import Prelude.Cast

18import Prelude.Maybe

19import Prelude.Functor

20+import Prelude.Either

20import Prelude.Monad

21import Prelude.Monad

21import IO

22import IO

22

23

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

24

25

25---- some basic io

26---- some basic io

26

27

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

29+||| descriptor

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

31+putStr' x = do prim_write x

32+ return ()

33+

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

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

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

35+putStr : String -> IO ()

29−putStr x = do prim_write x

36+putStr = putStr'

30− return ()

37+

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

39+||| descriptor

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

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

31

42

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

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

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

44+putStrLn : String -> IO ()

45+putStrLn = putStrLn'

46+

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

48+||| descriptor

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

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

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

35

51

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

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

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

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

38−print x = putStr (show x)

54+print = print'

39

55

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

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

57+||| descriptor

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

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

42−printLn x = putStrLn (show x)

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

43

60

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

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

63+printLn = printLn'

64+

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

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

66+||| descriptor

45−getLine : IO' ffi String

67+getLine' : IO' ffi String

46−getLine = do x <- prim_read

68+getLine' = do x <- prim_read

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

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

48 where trimNL : String -> String

70 where trimNL : String -> String

49 trimNL str with (strM str)

71 trimNL str with (strM str)

50 trimNL "" | StrNil = ""

72 trimNL "" | StrNil = ""

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

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

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

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

53

75

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

77+getLine : IO String

78+getLine = getLine'

79+

54||| Write a single character to stdout

80||| Write a single character to stdout

55putChar : Char -> IO ()

81putChar : Char -> IO ()

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

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

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

97processHandle h acc onRead onEOF

123processHandle h acc onRead onEOF

98 = if !(feof h)

124 = if !(feof h)

99 then putStr (onEOF acc)

125 then putStr (onEOF acc)

100− else do x <- fread h

126+ else do Right x <- fread h

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

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

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

102 putStr out

129 putStr out

103 processHandle h acc' onRead onEOF

130 processHandle h acc' onRead onEOF

libs/prelude/Prelude/Show.idr+5

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

10import Prelude.Classes

11import Prelude.List

12import Prelude.Maybe

13+import Prelude.Either

13import Prelude.Nat

14import Prelude.Nat

14import Prelude.Strings

15import Prelude.Strings

15

16

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

185 showPrec d Nothing = "Nothing"

186 showPrec d Nothing = "Nothing"

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

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

187

188

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

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

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

192+

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

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

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

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

190

195

rts/idris_rts.c+9

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

1#include <assert.h>

2+#include <errno.h>

2

3

3#include "idris_rts.h"

4#include "idris_rts.h"

4#include "idris_gc.h"

5#include "idris_gc.h"

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

934 free(msg);

935 free(msg);

935}

936}

936

937

938+int idris_errno() {

939+ return errno;

940+}

941+

942+char* idris_showerror(int err) {

943+ return strerror(err);

944+}

945+

937VAL* nullary_cons;

946VAL* nullary_cons;

938

947

939void init_nullaries() {

948void init_nullaries() {

rts/idris_rts.h+3

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

255

256#define NULL_CON(x) nullary_cons[x]

257

258+int idris_errno();

259+char* idris_showerror(int err);

260+

258extern VAL* nullary_cons;

261extern VAL* nullary_cons;

259void init_nullaries();

262void init_nullaries();

260void free_nullaries();

263void free_nullaries();

rts/idris_stdfgn.c+20

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

4#include "idris_gc.h"

5#include <sys/select.h>

6#include <fcntl.h>

7+#include <errno.h>

7#include <stdio.h>

8#include <stdio.h>

8#include <time.h>

9#include <time.h>

9

10

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

86 return MKBIGI(t);

87 return MKBIGI(t);

87}

88}

88

89

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+

89void idris_forceGC(void* vm) {

109void idris_forceGC(void* vm) {

90 idris_gc((VM*)vm);

110 idris_gc((VM*)vm);

91}

111}

rts/idris_stdfgn.h+2

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

14int fileError(void* h);

15// return 0 on success

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

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

18+VAL idris_mkFileError(VM* vm);

17

19

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

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

19int fpoll(void* h);

21int fpoll(void* h);

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

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

2 PatternGuards #-}

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

4

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

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

6+ normaliseAll, normaliseBlocking, toValue, quoteTerm,

6 rt_simplify, simplify, specialise, hnf, convEq, convEq',

7 rt_simplify, simplify, specialise, hnf, convEq, convEq',

7 Def(..), CaseInfo(..), CaseDefs(..),

8 Def(..), CaseInfo(..), CaseDefs(..),

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

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

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

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

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

80 quote 0 val) initEval

81 quote 0 val) initEval

81

82

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

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

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

83normaliseAll ctxt env t

85normaliseAll ctxt env t

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

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

85 quote 0 val) initEval

87 quote 0 val) initEval

86

88

89+-- | As normaliseAll, but with an explicit list of names *not* to reduce

90+normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name

91+normaliseBlocking ctxt env blocked t

92+ = evalState (do val <- eval False ctxt (map (\n -> (n, 0)) blocked)

93+ (map finalEntry env) t [AtREPL]

94+ quote 0 val) initEval

95+

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

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

88normalise = normaliseTrace False

97normalise = normaliseTrace False

89

98

src/Idris/Core/Execute.hs+11

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

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

350 show handle ++

351 ". Are all cases covered?"

352+ | Just (FFun "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs

353+ = case handle of

354+ -- errors handled differently in Haskell than in C, so if

355+ -- there's been an error we'll have had an exception already.

356+ -- Therefore, assume we're okay.

357+ EHandle h -> do let res = ioWrap (EConstant (I 0))

358+ execApp env ctxt res (drop arity xs)

359+ _ -> execFail . Msg $

360+ "The argument to fileError should be a file handle, but it was " ++

361+ show handle ++

362+ ". Are all cases covered?"

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

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

353 = case handle of

364 = case handle of

354 EHandle h -> do execIO $ hClose h

365 EHandle h -> do execIO $ hClose h

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

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

127 printtm tm

128 ])

129 where

130− runtm t = PApp fc (PRef fc [] (sUN "run__IO")) [pexp t]

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO"))

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

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

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

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

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

133

134

src/Idris/REPL.hs+7−2

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

805 getIState >>= flip warnDisamb t

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

807 ctxt <- getContext

808− let tm' = perhapsForce $ normaliseAll ctxt [] tm

808+ let tm' = perhapsForce $ normaliseBlocking ctxt []

809+ [sUN "foreign",

810+ sUN "prim_read",

811+ sUN "prim_write"]

812+ tm

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

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

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

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

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

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

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

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

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

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

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

815 let tmDoc = pprintDelab ist tm'

819 let tmDoc = pprintDelab ist tm'

820+ -- errReverse to make type more readable

816− tyDoc = pprintDelab ist ty'

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

817 iPrintTermWithType tmDoc tyDoc

822 iPrintTermWithType tmDoc tyDoc

818 where perhapsForce tm | termSmallerThan 100 tm = force tm

823 where perhapsForce tm | termSmallerThan 100 tm = force tm

819 | otherwise = tm

824 | otherwise = tm

test/dsl002/test014.idr+6−5

@@ -15,16 +15,17 @@ syntax "ifM" [test] "then" [t] "else" [e]

15 = test >>= (\b => if b then t else e)

16

17open : String -> (p:Purpose) -> Creator (Either () (FILE p))

18−open fn p = ioc (do h <- fopen fn (pstring p)

18+open fn p = ioc (do Right h <- fopen fn (pstring p)

19− ifM validFile h

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

20− then return (Right (OpenH h))

20+ return (Right (OpenH h)))

21− else return (Left ()))

22

21

23close : FILE p -> Updater ()

22close : FILE p -> Updater ()

24close (OpenH h) = iou (closeFile h)

23close (OpenH h) = iou (closeFile h)

25

24

26readLine : FILE Reading -> Reader String

25readLine : FILE Reading -> Reader String

27−readLine (OpenH h) = ior (fread h)

26+readLine (OpenH h) = ior (do Right str <- fread h

27+ | return ""

28+ return str)

28

29

29eof : FILE Reading -> Reader Bool

30eof : FILE Reading -> Reader Bool

30eof (OpenH h) = ior (feof h)

31eof (OpenH h) = ior (feof h)

test/ffi004/test026.idr+2−1

@@ -10,7 +10,8 @@ strToType _ = Nat

10

11-- If the file contains "Int", provide Int as a type, otherwise provide Nat

12fromFile : String -> IO (Provider Type)

13−fromFile fname = do str <- readFile fname

13+fromFile fname = do Right str <- readFile fname

14+ | Left err => return (Provide Void)

14 return (Provide (strToType (trim str)))

15 return (Provide (strToType (trim str)))

15

16

16%provide (T1 : Type) with fromFile "theType"

17%provide (T1 : Type) with fromFile "theType"

test/io001/test004.idr+4−4

@@ -8,20 +8,20 @@ mwhile t b = do v <- t

8 False => return ()

9

10dumpFile : String -> IO ()

11−dumpFile fn = do { h <- openFile fn Read

11+dumpFile fn = do { Right h <- openFile fn Read

12 mwhile (do { -- putStrLn "TEST"

13 x <- feof h

14 return (not x) })

15− (do { l <- fread h

15+ (do { Right l <- fread h

16 putStr l })

17 closeFile h }

18

19main : IO ()

20−main = do { h <- openFile "testfile" Write

20+main = do { Right h <- openFile "testfile" Write

21 fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"

22 closeFile h

23 putStrLn "Reading testfile"

24− f <- readFile "testfile"

24+ Right f <- readFile "testfile"

25 putStrLn f

26 putStrLn "---"

27 dumpFile "testfile"