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

(*
fn multiply(first_number_str: &str, second_number_str: &str) -> Result<i32, ParseIntError> {
    first_number_str.parse::<i32>().and_then(|first_number| {
        second_number_str
            .parse::<i32>()
            .map(|second_number| first_number * second_number)
    })
}
*)
Definition multiply (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ first_number_str; second_number_str ] =>
    ltac:(M.monadic
      (let first_number_str := M.alloc (| first_number_str |) in
      let second_number_str := M.alloc (| second_number_str |) in
      M.call_closure (|
        M.get_associated_function (|
          Ty.apply
            (Ty.path "core::result::Result")
            []
            [ Ty.path "i32"; Ty.path "core::num::error::ParseIntError" ],
          "and_then",
          [
            Ty.path "i32";
            Ty.function
              [ Ty.tuple [ Ty.path "i32" ] ]
              (Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.path "i32"; Ty.path "core::num::error::ParseIntError" ])
          ]
        |),
        [
          M.call_closure (|
            M.get_associated_function (| Ty.path "str", "parse", [ Ty.path "i32" ] |),
            [ M.read (| first_number_str |) ]
          |);
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let first_number := M.copy (| γ |) in
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.path "i32"; Ty.path "core::num::error::ParseIntError" ],
                                "map",
                                [
                                  Ty.path "i32";
                                  Ty.function [ Ty.tuple [ Ty.path "i32" ] ] (Ty.path "i32")
                                ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "parse",
                                    [ Ty.path "i32" ]
                                  |),
                                  [ M.read (| second_number_str |) ]
                                |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let second_number := M.copy (| γ |) in
                                                  BinOp.Wrap.mul (|
                                                    M.read (| first_number |),
                                                    M.read (| second_number |)
                                                  |)))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))
        ]
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_multiply : M.IsFunction "map_in_result_via_combinators::multiply" multiply.

(*
fn print(result: Result<i32, ParseIntError>) {
    match result {
        Ok(n) => println!("n is {}", n),
        Err(e) => println!("Error: {}", e),
    }
}
*)
Definition print (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ result ] =>
    ltac:(M.monadic
      (let result := M.alloc (| result |) in
      M.read (|
        M.match_operator (|
          result,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                let n := 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 "n is " |); 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 "i32" ]
                                    |),
                                    [ n ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| 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
                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 "Error: " |); 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 "core::num::error::ParseIntError" ]
                                    |),
                                    [ e ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_print : M.IsFunction "map_in_result_via_combinators::print" print.

(*
fn main() {
    // This still presents a reasonable answer.
    let twenty = multiply("10", "2");
    print(twenty);

    // The following now provides a much more helpful error message.
    let tt = multiply("t", "2");
    print(tt);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ twenty :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "map_in_result_via_combinators::multiply", [] |),
              [ M.read (| Value.String "10" |); M.read (| Value.String "2" |) ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "map_in_result_via_combinators::print", [] |),
              [ M.read (| twenty |) ]
            |)
          |) in
        let~ tt_ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "map_in_result_via_combinators::multiply", [] |),
              [ M.read (| Value.String "t" |); M.read (| Value.String "2" |) ]
            |)
          |) in
        let~ _ :=
          M.alloc (|
            M.call_closure (|
              M.get_function (| "map_in_result_via_combinators::print", [] |),
              [ M.read (| tt_ |) ]
            |)
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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