on master help sign in
Standard IO effect docstrings
8741859David Raymond Christiansen
libs/effects/Effect/StdIO.idr+17
@@ -3,12 +3,22 @@ module Effect.StdIO
3import Effects
3import Effects
4import Control.IOExcept
4import Control.IOExcept
5
5
6+-------------------------------------------------------------
7+-- IO effects internals
8+-------------------------------------------------------------
9+
10+||| The internal representation of StdIO effects
6data StdIO : Effect where
11data StdIO : Effect where
7 PutStr : String -> { () } StdIO ()
12 PutStr : String -> { () } StdIO ()
8 GetStr : { () } StdIO String
13 GetStr : { () } StdIO String
9 PutCh : Char -> { () } StdIO ()
14 PutCh : Char -> { () } StdIO ()
10 GetCh : { () } StdIO Char
15 GetCh : { () } StdIO Char
11
16
17+
18+-------------------------------------------------------------
19+-- IO effects handlers
20+-------------------------------------------------------------
21+
12instance Handler StdIO IO where
22instance Handler StdIO IO where
13 handle () (PutStr s) k = do putStr s; k () ()
23 handle () (PutStr s) k = do putStr s; k () ()
14 handle () GetStr k = do x <- getLine; k x ()
24 handle () GetStr k = do x <- getLine; k x ()
@@ -21,23 +31,30 @@ instance Handler StdIO (IOExcept a) where
21 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
31 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
22 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
23
33
34+-------------------------------------------------------------
24--- The Effect and associated functions
35--- The Effect and associated functions
36+-------------------------------------------------------------
25
37
26STDIO : EFFECT
38STDIO : EFFECT
27STDIO = MkEff () StdIO
39STDIO = MkEff () StdIO
28
40
41+||| Write a string to standard output.
29putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
42putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
30putStr s = PutStr s
43putStr s = PutStr s
31
44
45+||| Write a character to standard output.
32putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
46putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
33putChar c = PutCh c
47putChar c = PutCh c
34
48
49+||| Write a string to standard output, terminating with a newline.
35putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
50putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
36putStrLn s = putStr (s ++ "\n")
51putStrLn s = putStr (s ++ "\n")
37
52
53+||| Read a string from standard input.
38getStr : Handler StdIO e => { [STDIO] } Eff e String
54getStr : Handler StdIO e => { [STDIO] } Eff e String
39getStr = GetStr
55getStr = GetStr
40
56
57+||| Read a character from standard input.
41getChar : Handler StdIO e => { [STDIO] } Eff e Char
58getChar : Handler StdIO e => { [STDIO] } Eff e Char
42getChar = GetCh
59getChar = GetCh
43
60