mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-01 14:27:19 +03:00
e6121e0935
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
36 lines
1.0 KiB
Idris
36 lines
1.0 KiB
Idris
module System.REPL
|
|
|
|
import System.File
|
|
|
|
||| A basic read-eval-print loop, maintaining a state
|
|
||| @ state the input state
|
|
||| @ prompt the prompt to show
|
|
||| @ onInput the function to run on reading input, returning a String to
|
|
||| output and a new state. Returns Nothing if the repl should exit
|
|
export
|
|
replWith : (state : a) -> (prompt : String) ->
|
|
(onInput : a -> String -> Maybe (String, a)) -> IO ()
|
|
replWith acc prompt fn
|
|
= do putStr prompt
|
|
eof <- fEOF stdin
|
|
if eof
|
|
then pure ()
|
|
else do x <- getLine
|
|
case fn acc x of
|
|
Just (out, acc') =>
|
|
do putStr out
|
|
replWith acc' prompt fn
|
|
Nothing => pure ()
|
|
|
|
||| A basic read-eval-print loop
|
|
||| @ prompt the prompt to show
|
|
||| @ onInput the function to run on reading input, returning a String to
|
|
||| output
|
|
export
|
|
repl : (prompt : String) ->
|
|
(onInput : String -> String) -> IO ()
|
|
repl prompt fn
|
|
= replWith () prompt (\x, s => Just (fn s, ()))
|
|
|
|
|