grep written in Lean 4

gistfile1.txt

partial def grep (stream : IO.FS.Stream) (expected : String) : IO Unit := do
  let line ← stream.getLine
  if line.isEmpty then
    pure ()
  else
    let words := line.splitOn " "
    if words.contains expected then
      IO.print line
    grep stream expected

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

def processFiles (expected : String) (files : List String) : IO UInt32 := do
  match files with
  | [] =>
    pure 0
  | filename :: rest =>
    let streamOpt ← fileStream filename
    match streamOpt with
    | none =>
      let code ← processFiles expected rest
      pure (code+1)
    | some stream =>
      grep stream expected
      processFiles expected rest

def process (expected : String) (files : List String) : IO UInt32 := do
  match files with
  | [] =>
    let stdin ← IO.getStdin
    grep stdin expected
    pure 0
  | _ =>
    processFiles expected files

def printUsage : IO UInt32 := do
  let stdout ← IO.getStdout
  stdout.putStrLn "grep [--help] expected_word [files]"
  pure (1)

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => printUsage
  | [x] => process x []
  | x :: xs => process x xs