e2d0099 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

File handling in prelude

e2d0099Edwin Brady15 years ago

lib/prelude.idr+31−4

compare with master

unifiedsplit

@@ -152,11 +152,21 @@ fopen : String -> String -> IO File;

152fopen f m = do { h <- do_fopen f m;

153 return (FHandle h); };

154

155+data Mode = Read | Write | ReadWrite;

156+

157+openFile : String -> Mode -> IO File;

158+openFile f m = fopen f (modeStr m) where {

159+ modeStr : Mode -> String;

160+ modeStr Read = "r";

161+ modeStr Write = "w";

162+ modeStr ReadWrite = "r+";

163+}

164+

155do_fclose : Ptr -> IO ();

165do_fclose : Ptr -> IO ();

156do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;

166do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;

157

167

158−fclose : File -> IO ();

168+closeFile : File -> IO ();

159−fclose (FHandle h) = do_fclose h;

169+closeFile (FHandle h) = do_fclose h;

160

170

161do_fread : Ptr -> IO String;

171do_fread : Ptr -> IO String;

162do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;

172do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;

@@ -177,6 +187,23 @@ feof : File -> IO Bool;

177feof (FHandle h) = do { eof <- do_feof h;

187feof (FHandle h) = do { eof <- do_feof h;

178 return (not (eof == 0)); };

188 return (not (eof == 0)); };

179

189

180−

190+while : |(test : IO Bool) -> |(body : IO ()) -> IO ();

181−

191+while t b = do { v <- t;

192+ if v then (do { b; while t b; }) else return (); };

193+

194+readFile : String -> IO String;

195+readFile fn = do { h <- openFile fn Read;

196+ c <- readFile' h "";

197+ closeFile h;

198+ return c;

199+ }

200+ where {

201+ readFile' : File -> String -> IO String;

202+ readFile' h contents =

203+ do { x <- feof h;

204+ if (not x) then (do { l <- fread h;

205+ readFile' h (contents ++ l);

206+ })

207+ else (return contents); };

208+ }

182

209

src/Main.hs+2

@@ -61,6 +61,8 @@ runIdris opts =

61 [] -> return ()

62 (o:_) -> process (Compile o)

63 when runrepl $ repl ist inputs

64+ ok <- noErrors

65+ when (not ok) $ lift (exitWith (ExitFailure 1))

64 where

66 where

65 makeOption (OLogging i) = setLogLevel i

67 makeOption (OLogging i) = setLogLevel i

66 makeOption TypeCase = setTypeCase True

68 makeOption TypeCase = setTypeCase True

test/test004/test004.idr+2−23

@@ -1,33 +1,12 @@

1module main;

3−while : |(test : IO Bool) -> |(body : IO ()) -> IO ();

4−while t b = do { v <- t;

5− if v then (do { b; while t b; }) else return (); };

6−

7−

8−readFile : String -> IO String;

9−readFile fn = do { h <- fopen fn "r";

10− c <- readFile' h "";

11− fclose h;

12− return c;

13− }

14− where {

15− readFile' : File -> String -> IO String;

16− readFile' h contents =

17− do { x <- feof h;

18− if (not x) then (do { l <- fread h;

19− readFile' h (contents ++ l);

20− })

21− else (return contents); };

22− }

23−

24dumpFile : String -> IO ();

3dumpFile : String -> IO ();

25−dumpFile fn = do { h <- fopen fn "r";

4+dumpFile fn = do { h <- openFile fn Read;

26 while (do { x <- feof h;

5 while (do { x <- feof h;

27 return (not x); })

6 return (not x); })

28 (do { l <- fread h;

7 (do { l <- fread h;

29 putStr l; });

8 putStr l; });

30− fclose h; };

9+ closeFile h; };

32main : IO ();

11main : IO ();

33main = do { h <- fopen "testfile" "w";

12main = do { h <- fopen "testfile" "w";