(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

(*
fn cat(path: &Path) -> io::Result<String> {
    let mut f = File::open(path)?;
    let mut s = String::new();
    match f.read_to_string(&mut s) {
        Ok(_) => Ok(s),
        Err(e) => Err(e),
    }
}
*)
Definition cat (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ path ] =>
    ltac:(M.monadic
      (let path := M.alloc (| path |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let~ f :=
              M.copy (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.path "std::fs::File"; Ty.path "std::io::error::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "std::fs::File",
                            "open",
                            [ Ty.apply (Ty.path "&") [] [ Ty.path "std::path::Path" ] ]
                          |),
                          [ M.read (| path |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [
                                        Ty.path "alloc::string::String";
                                        Ty.path "std::io::error::Error"
                                      ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "std::io::error::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |)
              |) in
            let~ s :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "alloc::string::String", "new", [] |),
                  []
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "std::io::Read",
                    Ty.path "std::fs::File",
                    [],
                    "read_to_string",
                    []
                  |),
                  [ f; s ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| s |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_cat : M.IsFunction "filesystem_operations::cat" cat.

(*
fn echo(s: &str, path: &Path) -> io::Result<()> {
    let mut f = File::create(path)?;

    f.write_all(s.as_bytes())
}
*)
Definition echo (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ s; path ] =>
    ltac:(M.monadic
      (let s := M.alloc (| s |) in
      let path := M.alloc (| path |) in
      M.catch_return (|
        ltac:(M.monadic
          (M.read (|
            let~ f :=
              M.copy (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.path "std::fs::File"; Ty.path "std::io::error::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "std::fs::File",
                            "create",
                            [ Ty.apply (Ty.path "&") [] [ Ty.path "std::path::Path" ] ]
                          |),
                          [ M.read (| path |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "std::io::error::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "std::io::Write",
                  Ty.path "std::fs::File",
                  [],
                  "write_all",
                  []
                |),
                [
                  f;
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| s |) ]
                  |)
                ]
              |)
            |)
          |)))
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_echo : M.IsFunction "filesystem_operations::echo" echo.

(*
fn touch(path: &Path) -> io::Result<()> {
    match OpenOptions::new().create(true).write(true).open(path) {
        Ok(_) => Ok(()),
        Err(e) => Err(e),
    }
}
*)
Definition touch (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ path ] =>
    ltac:(M.monadic
      (let path := M.alloc (| path |) in
      M.read (|
        M.match_operator (|
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "std::fs::OpenOptions",
                "open",
                [ Ty.apply (Ty.path "&") [] [ Ty.path "std::path::Path" ] ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "std::fs::OpenOptions", "write", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "std::fs::OpenOptions", "create", [] |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "std::fs::OpenOptions",
                              "new",
                              []
                            |),
                            []
                          |)
                        |);
                        Value.Bool true
                      ]
                    |);
                    Value.Bool true
                  ]
                |);
                M.read (| path |)
              ]
            |)
          |),
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)));
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                let e := M.copy (| γ0_0 |) in
                M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_touch : M.IsFunction "filesystem_operations::touch" touch.

(*
fn main() {
    println!("`mkdir a`");
    // Create a directory, returns `io::Result<()>`
    match fs::create_dir("a") {
        Err(why) => println!("! {:?}", why.kind()),
        Ok(_) => {}
    }

    println!("`echo hello > a/b.txt`");
    // The previous match can be simplified using the `unwrap_or_else` method
    echo("hello", &Path::new("a/b.txt")).unwrap_or_else(|why| {
        println!("! {:?}", why.kind());
    });

    println!("`mkdir -p a/c/d`");
    // Recursively create a directory, returns `io::Result<()>`
    fs::create_dir_all("a/c/d").unwrap_or_else(|why| {
        println!("! {:?}", why.kind());
    });

    println!("`touch a/c/e.txt`");
    touch(&Path::new("a/c/e.txt")).unwrap_or_else(|why| {
        println!("! {:?}", why.kind());
    });

    println!("`ln -s ../b.txt a/c/b.txt`");
    // Create a symbolic link, returns `io::Result<()>`
    if cfg!(target_family = "unix") {
        unix::fs::symlink("../b.txt", "a/c/b.txt").unwrap_or_else(|why| {
            println!("! {:?}", why.kind());
        });
    }

    println!("`cat a/c/b.txt`");
    match cat(&Path::new("a/c/b.txt")) {
        Err(why) => println!("! {:?}", why.kind()),
        Ok(s) => println!("> {}", s),
    }

    println!("`ls a`");
    // Read the contents of a directory, returns `io::Result<Vec<Path>>`
    match fs::read_dir("a") {
        Err(why) => println!("! {:?}", why.kind()),
        Ok(paths) => {
            for path in paths {
                println!("> {:?}", path.unwrap().path());
            }
        }
    }

    println!("`rm a/c/e.txt`");
    // Remove a file, returns `io::Result<()>`
    fs::remove_file("a/c/e.txt").unwrap_or_else(|why| {
        println!("! {:?}", why.kind());
    });

    println!("`rmdir a/c/d`");
    // Remove an empty directory, returns `io::Result<()>`
    fs::remove_dir("a/c/d").unwrap_or_else(|why| {
        println!("! {:?}", why.kind());
    });
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`mkdir a`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "std::fs::create_dir",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                |),
                [ M.read (| Value.String "a" |) ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                  let why := M.copy (| γ0_0 |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "std::io::stdio::_print", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "! " |); M.read (| Value.String "
" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_debug",
                                        [ Ty.path "std::io::error::ErrorKind" ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "std::io::error::Error",
                                              "kind",
                                              []
                                            |),
                                            [ why ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                  M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [
                      M.alloc (|
                        Value.Array [ M.read (| Value.String "`echo hello > a/b.txt`
" |) ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                "unwrap_or_else",
                [ Ty.function [ Ty.tuple [ Ty.path "std::io::error::Error" ] ] (Ty.tuple []) ]
              |),
              [
                M.call_closure (|
                  M.get_function (| "filesystem_operations::echo", [] |),
                  [
                    M.read (| Value.String "hello" |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "std::path::Path",
                        "new",
                        [ Ty.path "str" ]
                      |),
                      [ M.read (| Value.String "a/b.txt" |) ]
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let why := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "std::io::stdio::_print", [] |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::Arguments",
                                                  "new_v1",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.read (| Value.String "! " |);
                                                        M.read (| Value.String "
" |)
                                                      ]
                                                  |);
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "new_debug",
                                                            [ Ty.path "std::io::error::ErrorKind" ]
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "std::io::error::Error",
                                                                  "kind",
                                                                  []
                                                                |),
                                                                [ why ]
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`mkdir -p a/c/d`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                "unwrap_or_else",
                [ Ty.function [ Ty.tuple [ Ty.path "std::io::error::Error" ] ] (Ty.tuple []) ]
              |),
              [
                M.call_closure (|
                  M.get_function (|
                    "std::fs::create_dir_all",
                    [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                  |),
                  [ M.read (| Value.String "a/c/d" |) ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let why := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "std::io::stdio::_print", [] |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::Arguments",
                                                  "new_v1",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.read (| Value.String "! " |);
                                                        M.read (| Value.String "
" |)
                                                      ]
                                                  |);
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "new_debug",
                                                            [ Ty.path "std::io::error::ErrorKind" ]
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "std::io::error::Error",
                                                                  "kind",
                                                                  []
                                                                |),
                                                                [ why ]
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`touch a/c/e.txt`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                "unwrap_or_else",
                [ Ty.function [ Ty.tuple [ Ty.path "std::io::error::Error" ] ] (Ty.tuple []) ]
              |),
              [
                M.call_closure (|
                  M.get_function (| "filesystem_operations::touch", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "std::path::Path",
                        "new",
                        [ Ty.path "str" ]
                      |),
                      [ M.read (| Value.String "a/c/e.txt" |) ]
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let why := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "std::io::stdio::_print", [] |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::Arguments",
                                                  "new_v1",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.read (| Value.String "! " |);
                                                        M.read (| Value.String "
" |)
                                                      ]
                                                  |);
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "new_debug",
                                                            [ Ty.path "std::io::error::ErrorKind" ]
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "std::io::error::Error",
                                                                  "kind",
                                                                  []
                                                                |),
                                                                [ why ]
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [
                      M.alloc (|
                        Value.Array [ M.read (| Value.String "`ln -s ../b.txt a/c/b.txt`
" |) ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                          "unwrap_or_else",
                          [
                            Ty.function
                              [ Ty.tuple [ Ty.path "std::io::error::Error" ] ]
                              (Ty.tuple [])
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_function (|
                              "std::os::unix::fs::symlink",
                              [
                                Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                                Ty.apply (Ty.path "&") [] [ Ty.path "str" ]
                              ]
                            |),
                            [
                              M.read (| Value.String "../b.txt" |);
                              M.read (| Value.String "a/c/b.txt" |)
                            ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α0 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let why := M.copy (| γ |) in
                                            M.read (|
                                              let~ _ :=
                                                let~ _ :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "std::io::stdio::_print",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (| Value.String "! " |);
                                                                  M.read (| Value.String "
" |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_debug",
                                                                      [
                                                                        Ty.path
                                                                          "std::io::error::ErrorKind"
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "std::io::error::Error",
                                                                            "kind",
                                                                            []
                                                                          |),
                                                                          [ why ]
                                                                        |)
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                M.alloc (| Value.Tuple [] |) in
                                              M.alloc (| Value.Tuple [] |)
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`cat a/c/b.txt`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_function (| "filesystem_operations::cat", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "std::path::Path",
                      "new",
                      [ Ty.path "str" ]
                    |),
                    [ M.read (| Value.String "a/c/b.txt" |) ]
                  |)
                ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                  let why := M.copy (| γ0_0 |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "std::io::stdio::_print", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "! " |); M.read (| Value.String "
" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_debug",
                                        [ Ty.path "std::io::error::ErrorKind" ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "std::io::error::Error",
                                              "kind",
                                              []
                                            |),
                                            [ why ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                  let s := M.copy (| γ0_0 |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "std::io::stdio::_print", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "> " |); M.read (| Value.String "
" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.path "alloc::string::String" ]
                                      |),
                                      [ s ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`ls a`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "std::fs::read_dir",
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                |),
                [ M.read (| Value.String "a" |) ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                  let why := M.copy (| γ0_0 |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "std::io::stdio::_print", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "! " |); M.read (| Value.String "
" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_debug",
                                        [ Ty.path "std::io::error::ErrorKind" ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "std::io::error::Error",
                                              "kind",
                                              []
                                            |),
                                            [ why ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                  let paths := M.copy (| γ0_0 |) in
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.path "std::fs::ReadDir",
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| paths |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.path "std::fs::ReadDir",
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let path := M.copy (| γ0_0 |) in
                                          let~ _ :=
                                            let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (| "std::io::stdio::_print", [] |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::Arguments",
                                                        "new_v1",
                                                        []
                                                      |),
                                                      [
                                                        M.alloc (|
                                                          Value.Array
                                                            [
                                                              M.read (| Value.String "> " |);
                                                              M.read (| Value.String "
" |)
                                                            ]
                                                        |);
                                                        M.alloc (|
                                                          Value.Array
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "core::fmt::rt::Argument",
                                                                  "new_debug",
                                                                  [ Ty.path "std::path::PathBuf" ]
                                                                |),
                                                                [
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path "std::fs::DirEntry",
                                                                        "path",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::result::Result")
                                                                                []
                                                                                [
                                                                                  Ty.path
                                                                                    "std::fs::DirEntry";
                                                                                  Ty.path
                                                                                    "std::io::error::Error"
                                                                                ],
                                                                              "unwrap",
                                                                              []
                                                                            |),
                                                                            [ M.read (| path |) ]
                                                                          |)
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |))))
            ]
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`rm a/c/e.txt`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                "unwrap_or_else",
                [ Ty.function [ Ty.tuple [ Ty.path "std::io::error::Error" ] ] (Ty.tuple []) ]
              |),
              [
                M.call_closure (|
                  M.get_function (|
                    "std::fs::remove_file",
                    [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                  |),
                  [ M.read (| Value.String "a/c/e.txt" |) ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let why := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "std::io::stdio::_print", [] |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::Arguments",
                                                  "new_v1",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.read (| Value.String "! " |);
                                                        M.read (| Value.String "
" |)
                                                      ]
                                                  |);
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "new_debug",
                                                            [ Ty.path "std::io::error::ErrorKind" ]
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "std::io::error::Error",
                                                                  "kind",
                                                                  []
                                                                |),
                                                                [ why ]
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)
          |) in
        let~ _ :=
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "std::io::stdio::_print", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [ M.alloc (| Value.Array [ M.read (| Value.String "`rmdir a/c/d`
" |) ] |) ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                "unwrap_or_else",
                [ Ty.function [ Ty.tuple [ Ty.path "std::io::error::Error" ] ] (Ty.tuple []) ]
              |),
              [
                M.call_closure (|
                  M.get_function (|
                    "std::fs::remove_dir",
                    [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                  |),
                  [ M.read (| Value.String "a/c/d" |) ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let why := M.copy (| γ |) in
                                  M.read (|
                                    let~ _ :=
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (| "std::io::stdio::_print", [] |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::Arguments",
                                                  "new_v1",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.read (| Value.String "! " |);
                                                        M.read (| Value.String "
" |)
                                                      ]
                                                  |);
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "new_debug",
                                                            [ Ty.path "std::io::error::ErrorKind" ]
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "std::io::error::Error",
                                                                  "kind",
                                                                  []
                                                                |),
                                                                [ why ]
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_main : M.IsFunction "filesystem_operations::main" main.
