git.iko.soy/Idris-dev
on master help sign in
File IO type indicates possibility of failure
b1872fbEdwin Brady
CHANGELOG+3
compare with master
unifiedsplit
@@ -37,6 +37,9 @@ Library updates
37 from Effectful programs.
37 from Effectful programs.
38* Some constructors that never actually occurred have been removed from
38* Some constructors that never actually occurred have been removed from
39 the TT and Raw reflection datatypes in Language.Reflection.
39 the TT and Raw reflection datatypes in Language.Reflection.
40+* File IO operations (for example openFile/fread/fwrite) now return
41+ 'Either FileError ty' where the return type was previously 'ty' to indicate
42+ that they may fail.
40
43
41Tool updates
44Tool updates
42------------
45------------
libs/contrib/Network/Socket.idr−4
@@ -143,10 +143,6 @@ record Socket where
143 socketType : SocketType
143 socketType : SocketType
144 protocalNumber : ProtocolNumber
144 protocalNumber : ProtocolNumber
145
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
74
75--- An implementation of the resource access protocol for the IO Context.
75--- An implementation of the resource access protocol for the IO Context.
76instance Handler FileIO IO where
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+3
@@ -198,6 +198,9 @@ namespace IO
198 forceGC : IO ()
198 forceGC : IO ()
199 forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
199 forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
200
200
201+ getErrno : IO Int
202+ getErrno = foreign FFI_C "idris_errno" (IO Int)
203+
201--------- The Javascript/Node FFI
204--------- The Javascript/Node FFI
202
205
203
206
libs/prelude/Prelude/File.idr+76−45
@@ -10,7 +10,8 @@ import Prelude.Cast
10import Prelude.Bool
10import Prelude.Bool
11import Prelude.Basics
11import Prelude.Basics
12import Prelude.Classes
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,31 @@ 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 Success = "Success"
44+ show FileNotFound = "File Not Found"
45+ show PermissionDenied = "Permission Denied"
46+ show (GenericFileError errno) = strError errno
47+
22||| Standard input
48||| Standard input
23stdin : File
49stdin : File
24stdin = FHandle prim__stdin
50stdin = FHandle prim__stdin
@@ -31,6 +57,13 @@ stdout = FHandle prim__stdout
31stderr : File
57stderr : File
32stderr = FHandle prim__stderr
58stderr = FHandle prim__stderr
33
59
60+do_ferror : Ptr -> IO Int
61+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h
62+
63+ferror : File -> IO Bool
64+ferror (FHandle h) = do err <- do_ferror h
65+ return (not (err == 0))
66+
34||| Call the RTS's file opening function
67||| Call the RTS's file opening function
35do_fopen : String -> String -> IO Ptr
68do_fopen : String -> String -> IO Ptr
36do_fopen f m
69do_fopen f m
@@ -39,12 +72,14 @@ do_fopen f m
39||| Open a file
72||| Open a file
40||| @ f the filename
73||| @ f the filename
41||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
74||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
42−fopen : (f : String) -> (m : String) -> IO File
75+fopen : (f : String) -> (m : String) -> IO (Either FileError File)
43fopen f m = do h <- do_fopen f m
76fopen f m = do h <- do_fopen f m
77+ if !(nullPtr h)
78+ then do err <- getFileError
44− return (FHandle h)
79+ return (Left err)
80+ else return (Right (FHandle h))
45
81
46||| Check whether a file handle is actually a null pointer
82||| Check whether a file handle is actually a null pointer
47−partial
48validFile : File -> IO Bool
83validFile : File -> IO Bool
49validFile (FHandle h) = do x <- nullPtr h
84validFile (FHandle h) = do x <- nullPtr h
50 return (not x)
85 return (not x)
@@ -55,33 +90,26 @@ data Mode = Read | Write | ReadWrite
55||| Open a file
90||| Open a file
56||| @ f the filename
91||| @ f the filename
57||| @ m the mode
92||| @ m the mode
58−partial
59−openFile : (f : String) -> (m : Mode) -> IO File
93+openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
60openFile f m = fopen f (modeStr m) where
94openFile f m = fopen f (modeStr m) where
61 modeStr Read = "r"
95 modeStr Read = "r"
62 modeStr Write = "w"
96 modeStr Write = "w"
63 modeStr ReadWrite = "r+"
97 modeStr ReadWrite = "r+"
64
98
65−partial
66do_fclose : Ptr -> IO ()
99do_fclose : Ptr -> IO ()
67do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
100do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h
68
101
69−partial
70closeFile : File -> IO ()
102closeFile : File -> IO ()
71closeFile (FHandle h) = do_fclose h
103closeFile (FHandle h) = do_fclose h
72
104
73−partial
74do_fread : Ptr -> IO' l String
105do_fread : Ptr -> IO' l String
75do_fread h = prim_fread h
106do_fread h = prim_fread h
76
107
77−fgetc : File -> IO Char
108+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
109+fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)
110+ if !(ferror (FHandle h))
83− if (x < 0) then return Nothing
111+ then return (Left FileReadError)
84− else return (Just (cast x))
112+ else return (Right c)
85
113
86fflush : File -> IO ()
114fflush : File -> IO ()
87fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
115fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
@@ -89,9 +117,12 @@ fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h
89do_popen : String -> String -> IO Ptr
117do_popen : String -> String -> IO Ptr
90do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
118do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m
91
119
92−popen : String -> Mode -> IO File
120+popen : String -> Mode -> IO (Either FileError File)
93popen f m = do ptr <- do_popen f (modeStr m)
121popen f m = do ptr <- do_popen f (modeStr m)
122+ if !(nullPtr ptr)
123+ then do err <- getFileError
124+ return (Left err)
94− return (FHandle ptr)
125+ else return (Right (FHandle ptr))
95 where
126 where
96 modeStr Read = "r"
127 modeStr Read = "r"
97 modeStr Write = "w"
128 modeStr Write = "w"
@@ -103,20 +134,25 @@ pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
103-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
134-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
104-- prim__vm h
135-- prim__vm h
105
136
106−partial
107−fread : File -> IO' l String
137+fread : File -> IO (Either FileError String)
108−fread (FHandle h) = do_fread h
138+fread (FHandle h) = do str <- do_fread h
109−
139+ if !(ferror (FHandle h))
110−partial
140+ then return (Left FileReadError)
141+ else return (Right str)
142+
111−do_fwrite : Ptr -> String -> IO ()
143+do_fwrite : Ptr -> String -> IO (Either FileError ())
112−do_fwrite h s = do prim_fwrite h s
144+do_fwrite h s = do res <- prim_fwrite h s
113− return ()
145+ if (res /= 0)
114−
146+ then do errno <- getErrno
115−partial
147+ if errno == 0
148+ then return (Left FileWriteError)
149+ else do err <- getFileError
150+ return (Left err)
151+ else return (Right ())
152+
116−fwrite : File -> String -> IO ()
153+fwrite : File -> String -> IO (Either FileError ())
117fwrite (FHandle h) s = do_fwrite h s
154fwrite (FHandle h) s = do_fwrite h s
118
155
119−partial
120do_feof : Ptr -> IO Int
156do_feof : Ptr -> IO Int
121do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
157do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
122
158
@@ -125,32 +161,27 @@ feof : File -> IO Bool
125feof (FHandle h) = do eof <- do_feof h
161feof (FHandle h) = do eof <- do_feof h
126 return (not (eof == 0))
162 return (not (eof == 0))
127
163
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
164fpoll : File -> IO Bool
137fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
165fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
138 return (p > 0)
166 return (p > 0)
139
167
140||| Read the contents of a file into a string
168||| Read the contents of a file into a string
141−partial -- no error checking!
169+partial -- might be reading something infinitely long like /dev/null ...
170+covering
142−readFile : String -> IO String
171+readFile : String -> IO (Either FileError String)
143−readFile fn = do h <- openFile fn Read
172+readFile fn = do Right h <- openFile fn Read
173+ | Left err => return (Left err)
144 c <- readFile' h ""
174 c <- readFile' h ""
145 closeFile h
175 closeFile h
146 return c
176 return c
147 where
177 where
148 partial
178 partial
149− readFile' : File -> String -> IO String
179+ readFile' : File -> String -> IO (Either FileError String)
150 readFile' h contents =
180 readFile' h contents =
151 do x <- feof h
181 do x <- feof h
152− if not x then do l <- fread h
182+ if not x then do Right l <- fread h
183+ | Left err => return (Left err)
153 readFile' h (contents ++ l)
184 readFile' h (contents ++ l)
154− else return contents
185+ else return (Right contents)
155
186
156
187
libs/prelude/Prelude/Interactive.idr+3−1
@@ -17,6 +17,7 @@ import Prelude.Show
17import Prelude.Cast
17import Prelude.Cast
18import Prelude.Maybe
18import Prelude.Maybe
19import Prelude.Functor
19import Prelude.Functor
20+import Prelude.Either
20import Prelude.Monad
21import Prelude.Monad
21import IO
22import IO
22
23
@@ -97,7 +98,8 @@ processHandle : File ->
97processHandle h acc onRead onEOF
98processHandle h acc onRead onEOF
98 = if !(feof h)
99 = if !(feof h)
99 then putStr (onEOF acc)
100 then putStr (onEOF acc)
100− else do x <- fread h
101+ else do Right x <- fread h
102+ | Left err => putStr (onEOF acc)
101 let (out, acc') = onRead acc x
103 let (out, acc') = onRead acc x
102 putStr out
104 putStr out
103 processHandle h acc' onRead onEOF
105 processHandle h acc' onRead onEOF
libs/prelude/Prelude/Show.idr+5
@@ -10,6 +10,7 @@ import Prelude.Chars
10import Prelude.Classes
10import Prelude.Classes
11import Prelude.List
11import Prelude.List
12import Prelude.Maybe
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>
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
255
256#define NULL_CON(x) nullary_cons[x]
256#define NULL_CON(x) nullary_cons[x]
257
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"
4#include "idris_gc.h"
5#include <sys/select.h>
5#include <sys/select.h>
6#include <fcntl.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);
14int fileError(void* h);
15// return 0 on success
15// return 0 on success
16int idris_writeStr(void*h, char* str);
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 #-}
2 PatternGuards #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4
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 " ++
349 "The argument to fileEOF should be a file handle, but it was " ++
350 show handle ++
350 show handle ++
351 ". Are all cases covered?"
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/REPL.hs+7−2
@@ -805,7 +805,11 @@ process fn (Eval t)
805 getIState >>= flip warnDisamb t
805 getIState >>= flip warnDisamb t
806 (tm, ty) <- elabREPL recinfo ERHS t
806 (tm, ty) <- elabREPL recinfo ERHS t
807 ctxt <- getContext
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)
15 = test >>= (\b => if b then t else e)
16
16
17open : String -> (p:Purpose) -> Creator (Either () (FILE p))
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
10
11-- If the file contains "Int", provide Int as a type, otherwise provide Nat
11-- If the file contains "Int", provide Int as a type, otherwise provide Nat
12fromFile : String -> IO (Provider Type)
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 ()
8 False => return ()
9
9
10dumpFile : String -> IO ()
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"
12 mwhile (do { -- putStrLn "TEST"
13 x <- feof h
13 x <- feof h
14 return (not x) })
14 return (not x) })
15− (do { l <- fread h
15+ (do { Right l <- fread h
16 putStr l })
16 putStr l })
17 closeFile h }
17 closeFile h }
18
18
19main : IO ()
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"
21 fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
22 closeFile h
22 closeFile h
23 putStrLn "Reading testfile"
23 putStrLn "Reading testfile"
24− f <- readFile "testfile"
24+ Right f <- readFile "testfile"
25 putStrLn f
25 putStrLn f
26 putStrLn "---"
26 putStrLn "---"
27 dumpFile "testfile"
27 dumpFile "testfile"