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

(*
fn main() {
    match 1 {
        0 => false,
        _ => true,
    };
    if true {
        0
    } else {
        1
    };
    if false {
        2
    } else if false {
        3
    } else if false {
        4
    } else {
        5
    };
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Integer IntegerKind.I32 1 |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_constant_or_break_match (|
                      M.read (| γ |),
                      Value.Integer IntegerKind.I32 0
                    |) in
                  M.alloc (| Value.Bool false |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
            ]
          |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (| Value.Integer IntegerKind.I32 0 |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 1 |)))
            ]
          |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use (M.alloc (| Value.Bool false |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (| Value.Integer IntegerKind.I32 2 |)));
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use (M.alloc (| Value.Bool false |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (| Value.Integer IntegerKind.I32 3 |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use (M.alloc (| Value.Bool false |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (| Value.Integer IntegerKind.I32 4 |)));
                              fun γ =>
                                ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I32 5 |)))
                            ]
                          |)))
                    ]
                  |)))
            ]
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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