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

(*
fn main() {
    let number = 13;
    // TODO ^ Try different values for `number`

    println!("Tell me about {}", number);
    match number {
        // Match a single value
        1 => println!("One!"),
        // Match several values
        2 | 3 | 5 | 7 | 11 => println!("This is a prime"),
        // TODO ^ Try adding 13 to the list of prime values
        // Match an inclusive range
        13..=19 => println!("A teen"),
        // Handle the rest of cases
        _ => println!("Ain't special"),
        // TODO ^ Try commenting out this catch-all arm
    }

    let boolean = true;
    // Match is an expression too
    let binary = match boolean {
        // The arms of a match must cover all the possible values
        false => 0,
        true => 1,
        // TODO ^ Try commenting out one of these arms
    };

    println!("{} -> {}", boolean, binary);
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ number := M.alloc (| Value.Integer IntegerKind.I32 13 |) 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 "Tell me about " |);
                            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" ]
                              |),
                              [ number ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        let~ _ :=
          M.match_operator (|
            number,
            [
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.I32 1
                    |) 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_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "One!
" |) ] |) ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.I32 2
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.I32 3
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.I32 5
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.I32 7
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.I32 11
                            |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] =>
                            ltac:(M.monadic
                              (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 "This is a prime
" |) ]
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (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 "A teen
" |) ] |) ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ =>
                ltac:(M.monadic
                  (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 "Ain't special
" |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        let~ boolean := M.alloc (| Value.Bool true |) in
        let~ binary :=
          M.copy (|
            M.match_operator (|
              boolean,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool false |) in
                    M.alloc (| Value.Integer IntegerKind.I32 0 |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (| Value.Integer IntegerKind.I32 1 |)))
              ]
            |)
          |) 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 "" |);
                            M.read (| Value.String " -> " |);
                            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" ]
                              |),
                              [ boolean ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "i32" ]
                              |),
                              [ binary ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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