git.iko.soy/Idris-dev
on master help sign in
No need for Handler constraints on effectful ops
34d6f39Edwin Brady
libs/effects/Effect/File.idr+5−10
compare with master
unifiedsplit
@@ -101,8 +101,7 @@ FILE_IO t = MkEff t FileIO
101|||
101|||
102||| @ fname The file name to be opened.
102||| @ fname The file name to be opened.
103||| @ m The file mode.
103||| @ m The file mode.
104−open : Handler FileIO e =>
105− (fname : String)
104+open : (fname : String)
106 -> (m : Mode)
105 -> (m : Mode)
107 -> { [FILE_IO ()] ==> [FILE_IO (if result
106 -> { [FILE_IO ()] ==> [FILE_IO (if result
108 then OpenFile m
107 then OpenFile m
@@ -111,23 +110,19 @@ open f m = call $ Open f m
111
110
112
111
113||| Close a file.
112||| Close a file.
114−close : Handler FileIO e =>
115− { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
113+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
116close = call $ Close
114close = call $ Close
117
115
118||| Read a line from the file.
116||| Read a line from the file.
119−readLine : Handler FileIO e =>
120− { [FILE_IO (OpenFile Read)] } Eff e String
117+readLine : { [FILE_IO (OpenFile Read)] } Eff e String
121readLine = call $ ReadLine
118readLine = call $ ReadLine
122
119
123||| Write a line to a file.
120||| Write a line to a file.
124−writeLine : Handler FileIO e =>
125− String -> { [FILE_IO (OpenFile Write)] } Eff e ()
121+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e ()
126writeLine str = call $ WriteLine str
122writeLine str = call $ WriteLine str
127
123
128||| End of file?
124||| End of file?
129−eof : Handler FileIO e =>
130− { [FILE_IO (OpenFile Read)] } Eff e Bool
125+eof : { [FILE_IO (OpenFile Read)] } Eff e Bool
131eof = call $ EOF
126eof = call $ EOF
132
127
133-- --------------------------------------------------------------------- [ EOF ]
128-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/StdIO.idr+5−5
@@ -39,22 +39,22 @@ STDIO : EFFECT
39STDIO = MkEff () StdIO
39STDIO = MkEff () StdIO
40
40
41||| Write a string to standard output.
41||| Write a string to standard output.
42−putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
42+putStr : String -> { [STDIO] } Eff e ()
43putStr s = call $ PutStr s
43putStr s = call $ PutStr s
44
44
45||| Write a character to standard output.
45||| Write a character to standard output.
46−putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
46+putChar : Char -> { [STDIO] } Eff e ()
47putChar c = call $ PutCh c
47putChar c = call $ PutCh c
48
48
49||| Write a string to standard output, terminating with a newline.
49||| Write a string to standard output, terminating with a newline.
50−putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
50+putStrLn : String -> { [STDIO] } Eff e ()
51putStrLn s = putStr (s ++ "\n")
51putStrLn s = putStr (s ++ "\n")
52
52
53||| Read a string from standard input.
53||| Read a string from standard input.
54−getStr : Handler StdIO e => { [STDIO] } Eff e String
54+getStr : { [STDIO] } Eff e String
55getStr = call $ GetStr
55getStr = call $ GetStr
56
56
57||| Read a character from standard input.
57||| Read a character from standard input.
58−getChar : Handler StdIO e => { [STDIO] } Eff e Char
58+getChar : { [STDIO] } Eff e Char
59getChar = call $ GetCh
59getChar = call $ GetCh
60
60