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

(*
fn foo<A>(o: Option<A>) {
    match o {
        Some(_a) => println!("some"),
        None => println!("nothing"),
    }
}
*)
Definition foo (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [ A ], [ o ] =>
    ltac:(M.monadic
      (let o := M.alloc (| o |) in
      M.read (|
        M.match_operator (|
          o,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                let _a := 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_const",
                            []
                          |),
                          [ M.alloc (| Value.Array [ M.read (| Value.String "some
" |) ] |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ =>
              ltac:(M.monadic
                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) 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_const",
                            []
                          |),
                          [ M.alloc (| Value.Array [ M.read (| Value.String "nothing
" |) ] |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_foo : M.IsFunction "concurrent_tests::foo" foo.

Module tests.
  (*
      fn test_file() {
          // Opens the file ferris.txt or creates one if it doesn't exist.
          let mut file = OpenOptions::new()
              .append(true)
              .create(true)
              .open("ferris.txt")
              .expect("Failed to open ferris.txt");
  
          // Print "Ferris" 5 times.
          for _ in 0..5 {
              file.write_all("Ferris\n".as_bytes())
                  .expect("Could not write to ferris.txt");
          }
      }
  *)
  Definition test_file (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ file :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.path "std::fs::File"; Ty.path "std::io::error::Error" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "std::fs::OpenOptions",
                      "open",
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "std::fs::OpenOptions",
                          "create",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "std::fs::OpenOptions",
                              "append",
                              []
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "std::fs::OpenOptions",
                                    "new",
                                    []
                                  |),
                                  []
                                |)
                              |);
                              Value.Bool true
                            ]
                          |);
                          Value.Bool true
                        ]
                      |);
                      M.read (| Value.String "ferris.txt" |)
                    ]
                  |);
                  M.read (| Value.String "Failed to open ferris.txt" |)
                ]
              |)
            |) in
          M.use
            (M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "i32" ],
                    [],
                    "into_iter",
                    []
                  |),
                  [
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start", Value.Integer IntegerKind.I32 0);
                        ("end_", Value.Integer IntegerKind.I32 5)
                      ]
                  ]
                |)
              |),
              [
                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.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "i32" ],
                                  [],
                                  "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~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                                          "expect",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "std::io::Write",
                                              Ty.path "std::fs::File",
                                              [],
                                              "write_all",
                                              []
                                            |),
                                            [
                                              file;
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "str",
                                                  "as_bytes",
                                                  []
                                                |),
                                                [ M.read (| Value.String "Ferris
" |) ]
                                              |)
                                            ]
                                          |);
                                          M.read (| Value.String "Could not write to ferris.txt" |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                    |)))
              ]
            |))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_test_file : M.IsFunction "concurrent_tests::tests::test_file'1" test_file.
  
  (*
      fn test_file_also() {
          // Opens the file ferris.txt or creates one if it doesn't exist.
          let mut file = OpenOptions::new()
              .append(true)
              .create(true)
              .open("ferris.txt")
              .expect("Failed to open ferris.txt");
  
          // Print "Corro" 5 times.
          for _ in 0..5 {
              file.write_all("Corro\n".as_bytes())
                  .expect("Could not write to ferris.txt");
          }
      }
  *)
  Definition test_file_also (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ file :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.path "std::fs::File"; Ty.path "std::io::error::Error" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "std::fs::OpenOptions",
                      "open",
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "std::fs::OpenOptions",
                          "create",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "std::fs::OpenOptions",
                              "append",
                              []
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "std::fs::OpenOptions",
                                    "new",
                                    []
                                  |),
                                  []
                                |)
                              |);
                              Value.Bool true
                            ]
                          |);
                          Value.Bool true
                        ]
                      |);
                      M.read (| Value.String "ferris.txt" |)
                    ]
                  |);
                  M.read (| Value.String "Failed to open ferris.txt" |)
                ]
              |)
            |) in
          M.use
            (M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "i32" ],
                    [],
                    "into_iter",
                    []
                  |),
                  [
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start", Value.Integer IntegerKind.I32 0);
                        ("end_", Value.Integer IntegerKind.I32 5)
                      ]
                  ]
                |)
              |),
              [
                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.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "i32" ],
                                  [],
                                  "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~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                                          "expect",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "std::io::Write",
                                              Ty.path "std::fs::File",
                                              [],
                                              "write_all",
                                              []
                                            |),
                                            [
                                              file;
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "str",
                                                  "as_bytes",
                                                  []
                                                |),
                                                [ M.read (| Value.String "Corro
" |) ]
                                              |)
                                            ]
                                          |);
                                          M.read (| Value.String "Could not write to ferris.txt" |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                    |)))
              ]
            |))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_test_file_also :
    M.IsFunction "concurrent_tests::tests::test_file_also'1" test_file_also.
End tests.
