如何在Idris2中读取全部标准输入？

当编译时无法确定输入行数，且需要区分输入中的空行与输入结束时，Idris2有两种常用解决方案：

方案一：一次性读取全部输入 #

使用Prelude提供的getContents : HasIO io => io String，它会直接读取整个标准输入流直到EOF，返回完整的字符串。之后可以用lines : String -> List String将其分割为行列表，自然保留输入中的空行，且不会产生多余的空字符串。

示例代码：

module Solve

import Data.List

main : IO ()
main = do
  content <- getContents
  let linesList = lines content
  traverse_ (\line => putStrLn ("'" ++ line ++ "'")) linesList

方案二：逐行读取并检测EOF #

借助isEOF : HasIO io => io Bool检测输入流是否结束，以此作为递归终止条件，逐行读取所有内容。这种方式可以在读取过程中实时处理每行数据，无需一次性加载全部输入。

示例代码：

module Solve

readAllLines : IO (List String)
readAllLines = do
  eof <- isEOF
  if eof
    then pure []
    else do
      line <- getLine
      rest <- readAllLines
      pure (line :: rest)

main : IO ()
main = do
  allLines <- readAllLines
  traverse_ (\line => putStrLn ("'" ++ line ++ "'")) allLines

测试验证 #

用包含三行（中间有空行）的输入测试上述程序，输出结果如下：

'foo'
''
'bar'

完美区分了输入中的空行与输入结束，不会产生多余的空行输出。

内容的提问来源于stack exchange，提问作者Tomas Aschan