git.iko.soy/Idris-dev
on master help sign in
Update Effect.File to use new failure handling
45378f1Edwin Brady
effects/Effect/File.idr+10−6
compare with master
unifiedsplit
@@ -7,16 +7,19 @@ data OpenFile : Mode -> Type where
7 FH : File -> OpenFile m
7 FH : File -> OpenFile m
8
8
9data FileIO : Effect where
9data FileIO : Effect where
10− Open : String -> (m : Mode) -> FileIO () (OpenFile m) ()
10+ Open : String -> (m : Mode) -> FileIO () (Either () (OpenFile m)) Bool
11 Close : FileIO (OpenFile m) () ()
11 Close : FileIO (OpenFile m) () ()
12−
12+
13 ReadLine : FileIO (OpenFile Read) (OpenFile Read) String
13 ReadLine : FileIO (OpenFile Read) (OpenFile Read) String
14 WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()
14 WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()
15 EOF : FileIO (OpenFile Read) (OpenFile Read) Bool
15 EOF : FileIO (OpenFile Read) (OpenFile Read) Bool
16+
16
17
17instance Handler FileIO IO where
18instance Handler FileIO IO where
18 handle () (Open fname m) k = do h <- openFile fname m
19 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
20 handle (FH h) Close k = do closeFile h
23 handle (FH h) Close k = do closeFile h
21 k () ()
24 k () ()
22 handle (FH h) ReadLine k = do str <- fread h
25 handle (FH h) ReadLine k = do str <- fread h
@@ -30,8 +33,8 @@ instance Handler FileIO (IOExcept String) where
30 handle () (Open fname m) k
33 handle () (Open fname m) k
31 = do h <- ioe_lift (openFile fname m)
34 = do h <- ioe_lift (openFile fname m)
32 valid <- ioe_lift (validFile h)
35 valid <- ioe_lift (validFile h)
33− if valid then k (FH h) ()
36+ if valid then k (Right (FH h)) True
34− else ioe_fail "File open failed"
37+ else k (Left ()) False
35 handle (FH h) Close k = do ioe_lift (closeFile h); k () ()
38 handle (FH h) Close k = do ioe_lift (closeFile h); k () ()
36 handle (FH h) ReadLine k = do str <- ioe_lift (fread h)
39 handle (FH h) ReadLine k = do str <- ioe_lift (fread h)
37 k (FH h) str
40 k (FH h) str
@@ -44,7 +47,8 @@ FILE_IO : Type -> EFFECT
44FILE_IO t = MkEff t FileIO
47FILE_IO t = MkEff t FileIO
45
48
46open : Handler FileIO e =>
49open : 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
48open f m = Open f m
52open f m = Open f m
49
53
50close : Handler FileIO e =>
54close : Handler FileIO e =>
test/test021/test021.idr+6−9
@@ -17,19 +17,16 @@ readFile = readAcc [] where
17 readAcc acc = do e <- eof
17 readAcc acc = do e <- eof
18 if (not e)
18 if (not e)
19 then do str <- readLine
19 then do str <- readLine
20− ls <- Count :- get
20+ Count :- put (!(Count :- get) + 1)
21− Count :- put (ls + 1)
22 readAcc (str :: acc)
21 readAcc (str :: acc)
23 else return (reverse acc)
22 else return (reverse acc)
24
23
25testFile : FileIO () ()
24testFile : FileIO () ()
26−testFile = catch (do open "testFile" Read
25+testFile = do open "testFile" Read
27− str <- readFile
26+ if_valid then do putStrLn (show !readFile)
27+ close
28− putStrLn (show str)
28+ putStrLn (show !(Count :- get))
29− ls <- Count :- get
29+ else putStrLn ("Error!")
30− close
31− putStrLn (show ls))
32− (\err => putStrLn ("Handled: " ++ show err))
33
30
34main : IO ()
31main : IO ()
35main = do ioe_run (run [(), (), Count := 0] testFile)
32main = do ioe_run (run [(), (), Count := 0] testFile)