git.iko.soy/Idris-dev
on ff0fbfa help sign in
Idris-dev/effects/Effect/File.idr
65 lines 2.3 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 () (OpenFile m) ()
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
17instance Handler FileIO IO where
18 handle () (Open fname m) k = do h <- openFile fname m
19 k (FH h) ()
20 handle (FH h) Close k = do closeFile h
21 k () ()
22 handle (FH h) ReadLine k = do str <- fread h
23 k (FH h) str
24 handle (FH h) (WriteLine str) k = do fwrite h str
25 k (FH h) ()
26 handle (FH h) EOF k = do e <- feof h
27 k (FH h) e
29instance Handler FileIO (IOExcept String) where
30 handle () (Open fname m) k
31 = do h <- ioe_lift (openFile fname m)
32 valid <- ioe_lift (validFile h)
33 if valid then k (FH h) ()
34 else ioe_fail "File open failed"
35 handle (FH h) Close k = do ioe_lift (closeFile h); k () ()
36 handle (FH h) ReadLine k = do str <- ioe_lift (fread h)
37 k (FH h) str
38 handle (FH h) (WriteLine str) k = do ioe_lift (fwrite h str)
39 k (FH h) ()
40 handle (FH h) EOF k = do e <- ioe_lift (feof h)
41 k (FH h) e
43FILE_IO : Type -> EFFECT
44FILE_IO t = MkEff t FileIO
46open : Handler FileIO e =>
47 String -> (m : Mode) -> EffM e [FILE_IO ()] [FILE_IO (OpenFile m)] ()
48open f m = Open f m
50close : Handler FileIO e =>
51 EffM e [FILE_IO (OpenFile m)] [FILE_IO ()] ()
52close = Close
54readLine : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] String
55readLine = ReadLine
57writeLine : Handler FileIO e => String -> Eff e [FILE_IO (OpenFile Write)] ()
58writeLine str = WriteLine str
60eof : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] Bool
61eof = EOF