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