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

(*
Enum Temperature
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Celsius";
        item := StructTuple [ Ty.path "i32" ];
        discriminant := None;
      };
      {
        name := "Fahrenheit";
        item := StructTuple [ Ty.path "i32" ];
        discriminant := None;
      }
    ];
}
*)

(*
fn main() {
    let temperature = Temperature::Celsius(35);
    // ^ TODO try different values for `temperature`

    match temperature {
        Temperature::Celsius(t) if t > 30 => println!("{}C is above 30 Celsius", t),
        // The `if condition` part ^ is a guard
        Temperature::Celsius(t) => println!("{}C is below 30 Celsius", t),

        Temperature::Fahrenheit(t) if t > 86 => println!("{}F is above 86 Fahrenheit", t),
        Temperature::Fahrenheit(t) => println!("{}F is below 86 Fahrenheit", t),
    }
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] =>
    ltac:(M.monadic
      (M.read (|
        let~ temperature :=
          M.alloc (|
            Value.StructTuple
              "match_guards::Temperature::Celsius"
              [ Value.Integer IntegerKind.I32 35 ]
          |) in
        M.match_operator (|
          temperature,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (|
                    γ,
                    "match_guards::Temperature::Celsius",
                    0
                  |) in
                let t := M.copy (| γ0_0 |) in
                let γ :=
                  M.alloc (| BinOp.gt (| M.read (| t |), Value.Integer IntegerKind.I32 30 |) |) in
                let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "" |);
                                  M.read (| Value.String "C is above 30 Celsius
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "i32" ]
                                    |),
                                    [ t ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (|
                    γ,
                    "match_guards::Temperature::Celsius",
                    0
                  |) in
                let t := M.copy (| γ0_0 |) 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_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "" |);
                                  M.read (| Value.String "C is below 30 Celsius
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "i32" ]
                                    |),
                                    [ t ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (|
                    γ,
                    "match_guards::Temperature::Fahrenheit",
                    0
                  |) in
                let t := M.copy (| γ0_0 |) in
                let γ :=
                  M.alloc (| BinOp.gt (| M.read (| t |), Value.Integer IntegerKind.I32 86 |) |) in
                let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "" |);
                                  M.read (| Value.String "F is above 86 Fahrenheit
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "i32" ]
                                    |),
                                    [ t ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)));
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.SubPointer.get_struct_tuple_field (|
                    γ,
                    "match_guards::Temperature::Fahrenheit",
                    0
                  |) in
                let t := M.copy (| γ0_0 |) 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_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "" |);
                                  M.read (| Value.String "F is below 86 Fahrenheit
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "i32" ]
                                    |),
                                    [ t ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)))
          ]
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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