从文件读取🔗

从文件读取需要在 IO 单子中完成。要把整个文件作为字符串读取，可以使用 IO.FS.readFile：

def readWholeFile (path : System.FilePath) : IO String :=
  IO.FS.readFile path

如果你想把文件文本放到一个变量里使用，可以取得 IO.FS.readFile 的结果并把它当作字符串来操作：

def readAndUse (path : System.FilePath) : IO String := do
  let content ← IO.FS.readFile path
  -- Do something with content, like convert it to uppercase
  return content.toUpper

如果你想逐行读取文件，可以使用 IO.FS.withFile 获取文件的句柄，然后从中读取行。IO.FS.Handle.getLine 方法从文件读取一行：

def readFirstLine (path : System.FilePath) : IO String :=
  IO.FS.withFile path .read fun handle => do
    handle.getLine

如果你想把所有行读入一个数组，可以使用 IO.FS.lines：

def readAllLines (path : System.FilePath) :
    IO (Array String) :=
  IO.FS.lines path

现在假设你想通过去掉读到的行两端的空白来修剪它。你可以用 String.trimAscii 方法来做，这也会去掉行末的 \n 字符：

def readTrimmedLines (path : System.FilePath) :
    IO String := do
  let line ← readFirstLine path
  return line.trimAscii.toString