git.iko.soy/Idris-dev
on 307efbb help sign in
Idris-dev/libs/effects/Effect/File.idr
69 lines 2.5 kB history raw
1module Effect.File
3import Effects
4import Control.IOExcept
6data OpenFile : Mode -> Type where
7 FH : File -> OpenFile m
9data FileIO : Effect where
10 Open : String -> (m : Mode) -> FileIO () (Either () (OpenFile m)) Bool
11 Close : FileIO (OpenFile m) () ()
13 ReadLine : FileIO (OpenFile Read) (OpenFile Read) String
14 WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()
15 EOF : FileIO (OpenFile Read) (OpenFile Read) Bool
18instance Handler FileIO IO where
19 handle () (Open fname m) k = do h <- openFile fname m
20 valid <- validFile h
21 if valid then k (Right (FH h)) True
22 else k (Left ()) False
23 handle (FH h) Close k = do closeFile h
24 k () ()
25 handle (FH h) ReadLine k = do str <- fread h
26 k (FH h) str
27 handle (FH h) (WriteLine str) k = do fwrite h str
28 k (FH h) ()
29 handle (FH h) EOF k = do e <- feof h
30 k (FH h) e
32instance Handler FileIO (IOExcept String) where
33 handle () (Open fname m) k
34 = do h <- ioe_lift (openFile fname m)
35 valid <- ioe_lift (validFile h)
36 if valid then k (Right (FH h)) True
37 else k (Left ()) False
38 handle (FH h) Close k = do ioe_lift (closeFile h); k () ()
39 handle (FH h) ReadLine k = do str <- ioe_lift (fread h)
40 k (FH h) str
41 handle (FH h) (WriteLine str) k = do ioe_lift (fwrite h str)
42 k (FH h) ()
43 handle (FH h) EOF k = do e <- ioe_lift (feof h)
44 k (FH h) e
46FILE_IO : Type -> EFFECT
47FILE_IO t = MkEff t FileIO
49open : Handler FileIO e =>
50 String -> (m : Mode) -> EffM e [FILE_IO ()]
51 [FILE_IO (Either () (OpenFile m))] Bool
52open f m = Open f m
54close : Handler FileIO e =>
55 EffM e [FILE_IO (OpenFile m)] [FILE_IO ()] ()
56close = Close
58readLine : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] String
59readLine = ReadLine
61writeLine : Handler FileIO e => String -> Eff e [FILE_IO (OpenFile Write)] ()
62writeLine str = WriteLine str
64eof : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] Bool
65eof = EOF