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

(*
fn main() {
    let x = 5u32;

    let y = {
        let x_squared = x * x;
        let x_cube = x_squared * x;

        // This expression will be assigned to `y`
        x_cube + x_squared + x
    };

    let z = {
        // The semicolon suppresses this expression and `()` is assigned to `z`
        2 * x;
    };

    println!("x is {:?}", x);
    println!("y is {:?}", y);
    println!("z is {:?}", z);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ x := M.alloc (| Value.Integer IntegerKind.U32 5 |) in
        let~ y :=
          M.copy (|
            let~ x_squared := M.alloc (| BinOp.Wrap.mul (| M.read (| x |), M.read (| x |) |) |) in
            let~ x_cube :=
              M.alloc (| BinOp.Wrap.mul (| M.read (| x_squared |), M.read (| x |) |) |) in
            M.alloc (|
              BinOp.Wrap.add (|
                BinOp.Wrap.add (| M.read (| x_cube |), M.read (| x_squared |) |),
                M.read (| x |)
              |)
            |)
          |) in
        let~ z :=
          M.copy (|
            let~ _ :=
              M.alloc (| BinOp.Wrap.mul (| Value.Integer IntegerKind.U32 2, M.read (| x |) |) |) 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_v1", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [ M.read (| Value.String "x is " |); 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 "u32" ]
                              |),
                              [ x ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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_v1", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [ M.read (| Value.String "y is " |); 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 "u32" ]
                              |),
                              [ y ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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_v1", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [ M.read (| Value.String "z is " |); M.read (| Value.String "
" |) ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_debug",
                                [ Ty.tuple [] ]
                              |),
                              [ z ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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