0 | module Control.RIO.Console
  1 |
  2 | import Data.IORef
  3 | import System.File
  4 |
  5 | %default total
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --          ConsoleOut
  9 | --------------------------------------------------------------------------------
 10 |
 11 | ||| Record representing a console with
 12 | ||| standard output and error output
 13 | public export
 14 | record ConsoleOut where
 15 |   constructor MkConsoleOut
 16 |   putStr_   : String -> IO ()
 17 |   putErr_   : String -> IO ()
 18 |
 19 | ||| The default console, printing to standard out and standard err.
 20 | export
 21 | stdOut : ConsoleOut
 22 | stdOut = MkConsoleOut putStr (\s => ignore $ fPutStr stderr s)
 23 |
 24 | ||| Put a string to the console's standard output.
 25 | export %inline
 26 | cputStr : ConsoleOut => HasIO io => String -> io ()
 27 | cputStr s = liftIO $ putStr_ %search s
 28 |
 29 | ||| Put a string plus trailing line break
 30 | ||| to the console's standard output.
 31 | export %inline
 32 | cputStrLn : ConsoleOut => HasIO io => String -> io ()
 33 | cputStrLn s = cputStr $ s ++ "\n"
 34 |
 35 | ||| Print a value to the console's standard output.
 36 | export %inline
 37 | cprint : ConsoleOut => Show a => HasIO io => a -> io ()
 38 | cprint = cputStr . show
 39 |
 40 | ||| Print a value plus trailing lne break
 41 | ||| to the console's standard output.
 42 | export
 43 | cprintLn : ConsoleOut => Show a => HasIO io => a -> io ()
 44 | cprintLn = cputStrLn . show
 45 |
 46 | ||| Put a string to the console's error output.
 47 | export
 48 | cputErr : ConsoleOut => HasIO io => String -> io ()
 49 | cputErr s = liftIO $ putErr_ %search s
 50 |
 51 | ||| Put a string plus trailing line break
 52 | ||| to the console's error output.
 53 | export
 54 | cputErrLn : ConsoleOut => HasIO io => String -> io ()
 55 | cputErrLn s = cputErr $ s ++ "\n"
 56 |
 57 | ||| Print a value to the console's error output.
 58 | export
 59 | cprintErr : ConsoleOut => Show a => HasIO io => a -> io ()
 60 | cprintErr = cputErr . show
 61 |
 62 | ||| Print a value plus trailing lne break
 63 | ||| to the console's error output.
 64 | export
 65 | cprintErrLn : ConsoleOut => Show a => HasIO io => a -> io ()
 66 | cprintErrLn = cputErrLn . show
 67 |
 68 | --------------------------------------------------------------------------------
 69 | --          ConsoleIn
 70 | --------------------------------------------------------------------------------
 71 |
 72 | ||| Record representing a console with standard input.
 73 | public export
 74 | record ConsoleIn where
 75 |   constructor MkConsoleIn
 76 |   getChar_  : IO Char
 77 |   getLine_  : IO String
 78 |
 79 | ||| The default console, reading from standard input.
 80 | export
 81 | stdIn : ConsoleIn
 82 | stdIn = MkConsoleIn getChar getLine
 83 |
 84 | ||| Read a line from the console's standard input.
 85 | export
 86 | cgetLine : ConsoleIn => HasIO io => io String
 87 | cgetLine = liftIO $ getLine_ %search
 88 |
 89 | ||| Read a single character from the console's standard input.
 90 | export
 91 | cgetChar : ConsoleIn => HasIO io => io Char
 92 | cgetChar = liftIO $ getChar_ %search
 93 |
 94 | --------------------------------------------------------------------------------
 95 | --          Console
 96 | --------------------------------------------------------------------------------
 97 |
 98 | public export
 99 | record Console where
100 |   constructor MkConsole
101 |   cin : ConsoleIn
102 |   out : ConsoleOut
103 |
104 | export
105 | stdIO : Console
106 | stdIO = MkConsole stdIn stdOut
107 |
108 | export %hint %inline
109 | consoleOut : Console -> ConsoleOut
110 | consoleOut = out
111 |
112 | export %hint %inline
113 | consoleIn : Console -> ConsoleIn
114 | consoleIn = cin
115 |