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

(*
fn some_number() -> Option<u32> {
    Some(42)
}
*)
Definition some_number (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (Value.StructTuple "core::option::Option::Some" [ Value.Integer IntegerKind.U32 42 ]))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_some_number :
  M.IsFunction "match_binding_destructure_enum_variants::some_number" some_number.

(*
fn main() {
    match some_number() {
        // Got `Some` variant, match if its value, bound to `n`,
        // is equal to 42.
        Some(n @ 42) => println!("The Answer: {}!", n),
        // Match any other number.
        Some(n) => println!("Not interesting... {}", n),
        // Match anything else (`None` variant).
        _ => (),
    }
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        M.match_operator (|
          M.alloc (|
            M.call_closure (|
              M.get_function (| "match_binding_destructure_enum_variants::some_number", [] |),
              []
            |)
          |),
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                let n := M.copy (| γ0_0 |) in
                let _ :=
                  M.is_constant_or_break_match (|
                    M.read (| γ0_0 |),
                    Value.Integer IntegerKind.U32 42
                  |) 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 "The Answer: " |);
                                  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 "u32" ]
                                    |),
                                    [ n ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 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 "Not interesting... " |);
                                  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 "u32" ]
                                    |),
                                    [ n ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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