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

(*
fn main() {
    // Integer addition
    println!("1 + 2 = {}", 1u32 + 2);

    // Integer subtraction
    println!("1 - 2 = {}", 1i32 - 2);
    // TODO ^ Try changing `1i32` to `1u32` to see why the type is important

    // Short-circuiting boolean logic
    println!("true AND false is {}", true && false);
    println!("true OR false is {}", true || false);
    println!("NOT true is {}", !true);

    // Bitwise operations
    println!("0011 AND 0101 is {:04b}", 0b0011u32 & 0b0101);
    println!("0011 OR 0101 is {:04b}", 0b0011u32 | 0b0101);
    println!("0011 XOR 0101 is {:04b}", 0b0011u32 ^ 0b0101);
    println!("1 << 5 is {}", 1u32 << 5);
    println!("0x80 >> 2 is 0x{:x}", 0x80u32 >> 2);

    // Use underscores to improve readability!
    println!("One million is written as {}", 1_000_000u32);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        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 "1 + 2 = " |); 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" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.Wrap.add (|
                                    Value.Integer IntegerKind.U32 1,
                                    Value.Integer IntegerKind.U32 2
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "1 - 2 = " |); 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" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.Wrap.sub (|
                                    Value.Integer IntegerKind.I32 1,
                                    Value.Integer IntegerKind.I32 2
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "true AND false 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 "bool" ]
                              |),
                              [
                                M.alloc (|
                                  LogicalOp.and (|
                                    Value.Bool true,
                                    ltac:(M.monadic (Value.Bool false))
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "true OR false 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 "bool" ]
                              |),
                              [
                                M.alloc (|
                                  LogicalOp.or (|
                                    Value.Bool true,
                                    ltac:(M.monadic (Value.Bool false))
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "NOT true 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 "bool" ]
                              |),
                              [ M.alloc (| UnOp.not (| Value.Bool true |) |) ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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_formatted",
                      []
                    |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "0011 AND 0101 is " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_binary",
                                [ Ty.path "u32" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.bit_and
                                    (Value.Integer IntegerKind.U32 3)
                                    (Value.Integer IntegerKind.U32 5)
                                |)
                              ]
                            |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 0;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 8;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple
                                  "core::fmt::rt::Count::Is"
                                  [ Value.Integer IntegerKind.Usize 4 ]
                              ]
                            |)
                          ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::UnsafeArg",
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |) 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_formatted",
                      []
                    |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "0011 OR 0101 is " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_binary",
                                [ Ty.path "u32" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.bit_or
                                    (Value.Integer IntegerKind.U32 3)
                                    (Value.Integer IntegerKind.U32 5)
                                |)
                              ]
                            |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 0;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 8;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple
                                  "core::fmt::rt::Count::Is"
                                  [ Value.Integer IntegerKind.Usize 4 ]
                              ]
                            |)
                          ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::UnsafeArg",
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |) 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_formatted",
                      []
                    |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "0011 XOR 0101 is " |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_binary",
                                [ Ty.path "u32" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.bit_xor
                                    (Value.Integer IntegerKind.U32 3)
                                    (Value.Integer IntegerKind.U32 5)
                                |)
                              ]
                            |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 0;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 8;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple
                                  "core::fmt::rt::Count::Is"
                                  [ Value.Integer IntegerKind.Usize 4 ]
                              ]
                            |)
                          ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::UnsafeArg",
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "1 << 5 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 "u32" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.Wrap.shl (|
                                    Value.Integer IntegerKind.U32 1,
                                    Value.Integer IntegerKind.I32 5
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "0x80 >> 2 is 0x" |);
                            M.read (| Value.String "
" |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_lower_hex",
                                [ Ty.path "u32" ]
                              |),
                              [
                                M.alloc (|
                                  BinOp.Wrap.shr (|
                                    Value.Integer IntegerKind.U32 128,
                                    Value.Integer IntegerKind.I32 2
                                  |)
                                |)
                              ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) 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 "One million is written as 1000000
" |) ]
                      |);
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "none",
                            []
                          |),
                          []
                        |)
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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