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

(*
fn main() {
    // Make `optional` of type `Option<i32>`
    let mut optional = Some(0);

    // This reads: "while `let` destructures `optional` into
    // `Some(i)`, evaluate the block (`{}`). Else `break`".
    while let Some(i) = optional {
        if i > 9 {
            println!("Greater than 9, quit!");
            optional = None;
        } else {
            println!("`i` is `{:?}`. Try again.", i);
            optional = Some(i + 1);
        }
        // ^ Less rightward drift and doesn't require
        // explicitly handling the failing case.
    }
    // ^ `if let` had additional optional `else`/`else if`
    // clauses. `while let` does not have these.
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ optional :=
          M.alloc (|
            Value.StructTuple "core::option::Option::Some" [ Value.Integer IntegerKind.I32 0 ]
          |) in
        M.loop (|
          ltac:(M.monadic
            (M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := optional in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let i := M.copy (| γ0_0 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (| M.read (| i |), Value.Integer IntegerKind.I32 9 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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 "Greater than 9, quit!
" |) ]
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |) in
                            let~ _ :=
                              M.write (|
                                optional,
                                Value.StructTuple "core::option::Option::None" []
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (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 "`i` is `" |);
                                                M.read (| Value.String "`. Try again.
" |)
                                              ]
                                          |);
                                          M.alloc (|
                                            Value.Array
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::rt::Argument",
                                                    "new_debug",
                                                    [ Ty.path "i32" ]
                                                  |),
                                                  [ i ]
                                                |)
                                              ]
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |) in
                            let~ _ :=
                              M.write (|
                                optional,
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [
                                    BinOp.Wrap.add (|
                                      M.read (| i |),
                                      Value.Integer IntegerKind.I32 1
                                    |)
                                  ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.never_to_any (|
                        M.read (|
                          let~ _ := M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                          M.alloc (| Value.Tuple [] |)
                        |)
                      |)
                    |)))
              ]
            |)))
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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