git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/libs/base/System/Interactive.idr
73 lines 2.6 kB history raw
1||| Various helper functions for creating simple interactive systems.
2|||
3||| These are mostly intended for helping with teaching, in that they will allow
4||| the easy creation of interactive programs without needing to teach IO
5||| or Effects first, but they also capture some common patterns of interactive
6||| programming.
7module System.Interactive
9{-
10When the interfaces and names are stable, these are intended for the Prelude.
11-}
13import System
15||| Process input from an open file handle, while maintaining a state.
16||| @ state the input state
17||| @ onRead the function to run on reading a line, returning a String to
18||| output and a new state
19||| @ onEOF the function to run on reaching end of file, returning a String
20||| to output
21public partial
22processHandle : File ->
23 (state : a) ->
24 (onRead : a -> String -> (String, a)) ->
25 (onEOF : a -> String) ->
26 IO ()
27processHandle h acc onRead onEOF
28 = if !(feof h)
29 then putStr (onEOF acc)
30 else do x <- fread h
31 let (out, acc') = onRead acc x
32 putStr out
33 processHandle h acc' onRead onEOF
35||| Process input from the standard input stream, while maintaining a state.
36||| @ state the input state
37||| @ onRead the function to run on reading a line, returning a String to
38||| output and a new state
39||| @ onEOI the function to run on reaching end of input, returning a String
40||| to output
41public partial
42processStdin : (state : a) ->
43 (onRead : a -> String -> (String, a)) ->
44 (onEOI : a -> String) -> IO ()
45processStdin = processHandle stdin
47||| A basic read-eval-print loop, maintaining a state
48||| @ state the input state
49||| @ prompt the prompt to show
50||| @ onInput the function to run on reading input, returning a String to
51||| output and a new state. Returns Nothing if the repl should exit
52public partial
53replWith : (state : a) -> (prompt : String) ->
54 (onInput : a -> String -> Maybe (String, a)) -> IO a
55replWith acc prompt fn
56 = do putStr prompt
57 x <- getLine
58 case fn acc x of
59 Just (out, acc') => do putStr out
60 replWith acc' prompt fn
61 Nothing => return acc
63||| A basic read-eval-print loop
64||| @ prompt the prompt to show
65||| @ onInput the function to run on reading input, returning a String to
66||| output
67public partial
68repl : (prompt : String) ->
69 (onInput : String -> String) -> IO ()
70repl prompt fn
71 = do replWith () prompt (\x, s => Just (fn s, ()))
72 return ()