Reading—and using—lines from a file

Stream: new members

[drone]

I'm just starting to learn Lean 4 and was attempting to write a program that would read lines from a file and perform some action for each line.

In Haskell, I would use something like whileM, but I have not seen a similar function in Lean 4.

Here is a minimal example:

def readLines (handle : IO.FS.Handle) : IO Unit := do
  match ← handle.getLine with
  | "" =>
    return -- End of file, terminate
  | line =>
    IO.println line
    readLines handle -- Recursive call for the next line

which produces the error:

well-founded recursion cannot be used, 'readLines' does not take any (non-fixed) arguments

While I think I understand that error in general (no inductive type/no base case), I'm not sure how I can define a function which will exhaustively read and process lines from the file. Any suggestions or links to relevant references appreciated!

[Michael Rothgang]

Does docs#IO.FS.lines do what you want?

[drone]

Thanks! That should work for this case where the file isn't too large. But I'm curious if there is a way to process individual lines at a time without reading all lines from the file into memory first.

[Matt Diamond]

Could this be a good use case for using partial def? That's the escape hatch that lets you write potentially non-terminating functions

[drone]

Marking readLines as partial does remove the error and the code does run as expected. Thank you!

[Eric Wieser]

Indeed this has to partial, because the handle might be an infinite file like dev/urandom