How do I read all of standard input in Idris2?

Question

I'm trying to figure out how to do something very simple: read all of standard input into a string (or a list of strings would be fine too).

Prelude has getLine : HasIO io => io String, which can give me one line, but it doesn't give me a way to know that I've read it all. If there is no more input, it just gives me an empty string, which means if the input contains empty lines, I can't tell that apart from the end of the input.

Consider the following program:

module Example

main : IO ()
module Solve

main : IO ()
main = do
  putStrLn ("'" ++ !getLine ++ "'")
  putStrLn ("'" ++ !getLine ++ "'")
  putStrLn ("'" ++ !getLine ++ "'")
  putStrLn ("'" ++ !getLine ++ "'")
  putStrLn ("'" ++ !getLine ++ "'")
  putStrLn ("'" ++ !getLine ++ "'")

This program will print six lines, each wrapped in single quotes, taking contents from standard input. If I compile it to ./example and run with three lines of input, and a blank line in the middle, here's the output:

$ ./example <<EOF
foo

bar
EOF
'foo'
''
'bar'
''
''
''

Note that it keeps printing out lines after the standard input stream is exhausted. This means if I put this in some recursive function to get me all of the input, I don't have a reasonable stop condition.

What is the idiomatic way to read all of standard input in Idris2, without knowing at build-time how many lines of input there will be?

Answer 1

You can use fEOF.

You can see an example here.