io-monad.lean

import system.io

instance : monad_except io.error io :=
{ throw := λ α s, monad_io.fail io_core io.error α s,
  catch := λ α x f, monad_io.catch io.error io.error α x f }

def process_error : io.error → io unit
| (io.error.other s) := io.put_str_ln s
| (io.error.sys n) := io.put_str_ln $ sformat! "System error #{n}"

def print_file : io unit :=
catch (io.put_str "> " >> io.get_line >>=
        io.fs.read_file >>=
          io.put_str_ln ∘ buffer.to_string) process_error

def main : io unit := io.forever print_file
/-
  $ cat test.txt
  cat: test.txt: No such file or directory
  $ lean --run io-monad.lean
  > test.txt
  failed to open file 'test.txt'
  >
-/