git.iko.soy/Idris-dev
on master help sign in
Update Effect.File to use new failure handling

i.e. using if_valid to test for failure, and update resource accordingly, rather than using exceptions.

commit45378f1e244c19e67d7f60fa55bd76603ff98c6a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Oct 2013, 16:27 (13 years ago) parentfafe598
2 files changed+16−15
compare with master
unifiedsplit
effects/Effect/File.idr+10−6 test/test021/test021.idr+6−9
effects/Effect/File.idr+10−6
@@ -7,16 +7,19 @@ data OpenFile : Mode -> Type where
77 FH : File -> OpenFile m
88
99data FileIO : Effect where
10− Open : String -> (m : Mode) -> FileIO () (OpenFile m) ()
10+ Open : String -> (m : Mode) -> FileIO () (Either () (OpenFile m)) Bool
1111 Close : FileIO (OpenFile m) () ()
12−
12+
1313 ReadLine : FileIO (OpenFile Read) (OpenFile Read) String
1414 WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()
1515 EOF : FileIO (OpenFile Read) (OpenFile Read) Bool
16+
1617
1718instance Handler FileIO IO where
1819 handle () (Open fname m) k = do h <- openFile fname m
19− k (FH h) ()
20+ valid <- validFile h
21+ if valid then k (Right (FH h)) True
22+ else k (Left ()) False
2023 handle (FH h) Close k = do closeFile h
2124 k () ()
2225 handle (FH h) ReadLine k = do str <- fread h
@@ -30,8 +33,8 @@ instance Handler FileIO (IOExcept String) where
3033 handle () (Open fname m) k
3134 = do h <- ioe_lift (openFile fname m)
3235 valid <- ioe_lift (validFile h)
33− if valid then k (FH h) ()
34− else ioe_fail "File open failed"
36+ if valid then k (Right (FH h)) True
37+ else k (Left ()) False
3538 handle (FH h) Close k = do ioe_lift (closeFile h); k () ()
3639 handle (FH h) ReadLine k = do str <- ioe_lift (fread h)
3740 k (FH h) str
@@ -44,7 +47,8 @@ FILE_IO : Type -> EFFECT
4447FILE_IO t = MkEff t FileIO
4548
4649open : Handler FileIO e =>
47− String -> (m : Mode) -> EffM e [FILE_IO ()] [FILE_IO (OpenFile m)] ()
50+ String -> (m : Mode) -> EffM e [FILE_IO ()]
51+ [FILE_IO (Either () (OpenFile m))] Bool
4852open f m = Open f m
4953
5054close : Handler FileIO e =>
test/test021/test021.idr+6−9
@@ -17,19 +17,16 @@ readFile = readAcc [] where
1717 readAcc acc = do e <- eof
1818 if (not e)
1919 then do str <- readLine
20− ls <- Count :- get
21− Count :- put (ls + 1)
20+ Count :- put (!(Count :- get) + 1)
2221 readAcc (str :: acc)
2322 else return (reverse acc)
2423
2524testFile : FileIO () ()
26−testFile = catch (do open "testFile" Read
27− str <- readFile
28− putStrLn (show str)
29− ls <- Count :- get
30− close
31− putStrLn (show ls))
32− (\err => putStrLn ("Handled: " ++ show err))
25+testFile = do open "testFile" Read
26+ if_valid then do putStrLn (show !readFile)
27+ close
28+ putStrLn (show !(Count :- get))
29+ else putStrLn ("Error!")
3330
3431main : IO ()
3532main = do ioe_run (run [(), (), Count := 0] testFile)