git.iko.soy/Idris-dev
on master help sign in
File handling in prelude
commite2d0099fbd4c330ce4788ae1b84a6bd074d6c7a8 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 16 Dec 2011, 17:20 (15 years ago) parente06c1c1
3 files changed+35−27
compare with master
unifiedsplit
lib/prelude.idr+31−4 src/Main.hs+2 test/test004/test004.idr+2−23
lib/prelude.idr+31−4
@@ -152,11 +152,21 @@ fopen : String -> String -> IO File;
152152fopen f m = do { h <- do_fopen f m;
153153 return (FHandle h); };
154154
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+
155165do_fclose : Ptr -> IO ();
156166do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;
157167
158−fclose : File -> IO ();
159−fclose (FHandle h) = do_fclose h;
168+closeFile : File -> IO ();
169+closeFile (FHandle h) = do_fclose h;
160170
161171do_fread : Ptr -> IO String;
162172do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;
@@ -177,6 +187,23 @@ feof : File -> IO Bool;
177187feof (FHandle h) = do { eof <- do_feof h;
178188 return (not (eof == 0)); };
179189
180−
181−
190+while : |(test : IO Bool) -> |(body : IO ()) -> IO ();
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+ }
182209
src/Main.hs+2
@@ -61,6 +61,8 @@ runIdris opts =
6161 [] -> return ()
6262 (o:_) -> process (Compile o)
6363 when runrepl $ repl ist inputs
64+ ok <- noErrors
65+ when (not ok) $ lift (exitWith (ExitFailure 1))
6466 where
6567 makeOption (OLogging i) = setLogLevel i
6668 makeOption TypeCase = setTypeCase True
test/test004/test004.idr+2−23
@@ -1,33 +1,12 @@
11module main;
22
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−
243dumpFile : String -> IO ();
25−dumpFile fn = do { h <- fopen fn "r";
4+dumpFile fn = do { h <- openFile fn Read;
265 while (do { x <- feof h;
276 return (not x); })
287 (do { l <- fread h;
298 putStr l; });
30− fclose h; };
9+ closeFile h; };
3110
3211main : IO ();
3312main = do { h <- fopen "testfile" "w";