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

(* Trait *)
Module ProvidedAndRequired.
  Definition provided (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        BinOp.Wrap.add (|
          Value.Integer IntegerKind.I32 42,
          M.call_closure (|
            M.get_trait_method (|
              "provided_method::ProvidedAndRequired",
              Self,
              [],
              "required",
              []
            |),
            [ M.read (| self |) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom ProvidedMethod_provided :
    M.IsProvidedMethod "provided_method::ProvidedAndRequired" "provided" provided.
End ProvidedAndRequired.

Module Impl_provided_method_ProvidedAndRequired_for_i32.
  Definition Self : Ty.t := Ty.path "i32".
  
  (*
      fn required(&self) -> i32 {
          *self
      }
  *)
  Definition required (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (| M.read (| self |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "provided_method::ProvidedAndRequired"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("required", InstanceField.Method required) ].
End Impl_provided_method_ProvidedAndRequired_for_i32.

Module Impl_provided_method_ProvidedAndRequired_for_u32.
  Definition Self : Ty.t := Ty.path "u32".
  
  (*
      fn required(&self) -> i32 {
          *self as i32
      }
  *)
  Definition required (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.rust_cast (M.read (| M.read (| self |) |))))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  (*
      fn provided(&self) -> i32 {
          0
      }
  *)
  Definition provided (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        Value.Integer IntegerKind.I32 0))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "provided_method::ProvidedAndRequired"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("required", InstanceField.Method required); ("provided", InstanceField.Method provided) ].
End Impl_provided_method_ProvidedAndRequired_for_u32.

(*
fn main() {
    let x = 5;
    assert_eq!(x.provided(), 47);
    let y = 5u32;
    assert_eq!(y.provided(), 0);
}
*)
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.I32 5 |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              Value.Tuple
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "provided_method::ProvidedAndRequired",
                        Ty.path "i32",
                        [],
                        "provided",
                        []
                      |),
                      [ x ]
                    |)
                  |);
                  M.alloc (| Value.Integer IntegerKind.I32 47 |)
                ]
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                  let left_val := M.copy (| γ0_0 |) in
                  let right_val := M.copy (| γ0_1 |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  BinOp.eq (|
                                    M.read (| M.read (| left_val |) |),
                                    M.read (| M.read (| right_val |) |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ kind :=
                                  M.alloc (|
                                    Value.StructTuple "core::panicking::AssertKind::Eq" []
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::panicking::assert_failed",
                                      [ Ty.path "i32"; Ty.path "i32" ]
                                    |),
                                    [
                                      M.read (| kind |);
                                      M.read (| left_val |);
                                      M.read (| right_val |);
                                      Value.StructTuple "core::option::Option::None" []
                                    ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |)))
            ]
          |) in
        let~ y := M.alloc (| Value.Integer IntegerKind.U32 5 |) in
        let~ _ :=
          M.match_operator (|
            M.alloc (|
              Value.Tuple
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "provided_method::ProvidedAndRequired",
                        Ty.path "u32",
                        [],
                        "provided",
                        []
                      |),
                      [ y ]
                    |)
                  |);
                  M.alloc (| Value.Integer IntegerKind.I32 0 |)
                ]
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                  let left_val := M.copy (| γ0_0 |) in
                  let right_val := M.copy (| γ0_1 |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  BinOp.eq (|
                                    M.read (| M.read (| left_val |) |),
                                    M.read (| M.read (| right_val |) |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ kind :=
                                  M.alloc (|
                                    Value.StructTuple "core::panicking::AssertKind::Eq" []
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (|
                                      "core::panicking::assert_failed",
                                      [ Ty.path "i32"; Ty.path "i32" ]
                                    |),
                                    [
                                      M.read (| kind |);
                                      M.read (| left_val |);
                                      M.read (| right_val |);
                                      Value.StructTuple "core::option::Option::None" []
                                    ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |)))
            ]
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

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