git.iko.soy/Idris-dev
on f01873f help sign in
Idris-dev/libs/effects/Effect/File.idr
62 lines 1.9 kB history raw
1module Effect.File
3import Effects
4import Control.IOExcept
6data OpenFile : Mode -> Type where
7 FH : File -> OpenFile m
9openOK : Mode -> Bool -> Type
10openOK m True = OpenFile m
11openOK m False = ()
13data FileIO : Effect where
14 Open : String -> (m : Mode) ->
15 {() ==> {res} if res then OpenFile m else ()} FileIO Bool
16 Close : {OpenFile m ==> ()} FileIO ()
18 ReadLine : {OpenFile Read} FileIO String
19 WriteLine : String -> {OpenFile Write} FileIO ()
20 EOF : {OpenFile Read} FileIO Bool
22instance Handler FileIO IO where
23 handle () (Open fname m) k = do h <- openFile fname m
24 valid <- validFile h
25 if valid then k True (FH h)
26 else k False ()
27 handle (FH h) Close k = do closeFile h
28 k () ()
29 handle (FH h) ReadLine k = do str <- fread h
30 k str (FH h)
31 handle (FH h) (WriteLine str) k = do fwrite h str
32 k () (FH h)
33 handle (FH h) EOF k = do e <- feof h
34 k e (FH h)
36FILE_IO : Type -> EFFECT
37FILE_IO t = MkEff t FileIO
39open : Handler FileIO e =>
40 String -> (m : Mode) ->
41 { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool
42open f m = Open f m
44close : Handler FileIO e =>
45 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
46close = Close
48readLine : Handler FileIO e =>
49 { [FILE_IO (OpenFile Read)] } Eff e String
50readLine = ReadLine
52writeLine : Handler FileIO e =>
53 String -> { [FILE_IO (OpenFile Write)] } Eff e ()
54writeLine str = WriteLine str
56eof : Handler FileIO e =>
57 { [FILE_IO (OpenFile Read)] } Eff e Bool
58eof = EOF