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

Module ops.
  Module try_trait.
    (* Trait *)
    (* Empty module 'Try' *)
    
    (* Trait *)
    (* Empty module 'FromResidual' *)
    
    (*
    pub fn from_yeet<T, Y>(yeeted: Y) -> T
    where
        T: FromResidual<Yeet<Y>>,
    {
        FromResidual::from_residual(Yeet(yeeted))
    }
    *)
    Definition from_yeet (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; Y ], [ yeeted ] =>
        ltac:(M.monadic
          (let yeeted := M.alloc (| yeeted |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::try_trait::FromResidual",
              T,
              [ Ty.apply (Ty.path "core::ops::try_trait::Yeet") [] [ Y ] ],
              "from_residual",
              []
            |),
            [ Value.StructTuple "core::ops::try_trait::Yeet" [ M.read (| yeeted |) ] ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_yeet : M.IsFunction "core::ops::try_trait::from_yeet" from_yeet.
    
    (* Trait *)
    (* Empty module 'Residual' *)
    
    Axiom ChangeOutputType :
      forall (T V : Ty.t),
      (Ty.apply (Ty.path "core::ops::try_trait::ChangeOutputType") [] [ T; V ]) = Ty.associated.
    
    (* StructTuple
      {
        name := "NeverShortCircuit";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ T ];
      } *)
    
    Module Impl_core_ops_try_trait_NeverShortCircuit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ].
      
      (*
          pub fn wrap_mut_1<A>(mut f: impl FnMut(A) -> T) -> impl FnMut(A) -> NeverShortCircuit<T> {
              move |a| NeverShortCircuit(f(a))
          }
      *)
      Definition wrap_mut_1 (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ A; impl_FnMut_A__arrow_T ], [ f ] =>
          ltac:(M.monadic
            (let f := M.alloc (| f |) in
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let a := M.copy (| γ |) in
                              Value.StructTuple
                                "core::ops::try_trait::NeverShortCircuit"
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      impl_FnMut_A__arrow_T,
                                      [ Ty.tuple [ A ] ],
                                      "call_mut",
                                      []
                                    |),
                                    [ f; Value.Tuple [ M.read (| a |) ] ]
                                  |)
                                ]))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrap_mut_1 :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrap_mut_1" (wrap_mut_1 T).
      
      (*
          pub fn wrap_mut_2<A, B>(mut f: impl FnMut(A, B) -> T) -> impl FnMut(A, B) -> Self {
              move |a, b| NeverShortCircuit(f(a, b))
          }
      *)
      Definition wrap_mut_2 (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ A; B; impl_FnMut_A__B__arrow_T ], [ f ] =>
          ltac:(M.monadic
            (let f := M.alloc (| f |) in
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let a := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let b := M.copy (| γ |) in
                                      Value.StructTuple
                                        "core::ops::try_trait::NeverShortCircuit"
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::function::FnMut",
                                              impl_FnMut_A__B__arrow_T,
                                              [ Ty.tuple [ A; B ] ],
                                              "call_mut",
                                              []
                                            |),
                                            [ f; Value.Tuple [ M.read (| a |); M.read (| b |) ] ]
                                          |)
                                        ]))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_wrap_mut_2 :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "wrap_mut_2" (wrap_mut_2 T).
    End Impl_core_ops_try_trait_NeverShortCircuit_T.
    
    (*
    Enum NeverShortCircuitResidual
    {
      const_params := [];
      ty_params := [];
      variants := [];
    }
    *)
    
    Module Impl_core_ops_try_trait_Try_for_core_ops_try_trait_NeverShortCircuit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ].
      
      (*     type Output = T; *)
      Definition _Output (T : Ty.t) : Ty.t := T.
      
      (*     type Residual = NeverShortCircuitResidual; *)
      Definition _Residual (T : Ty.t) : Ty.t :=
        Ty.path "core::ops::try_trait::NeverShortCircuitResidual".
      
      (*
          fn branch(self) -> ControlFlow<NeverShortCircuitResidual, T> {
              ControlFlow::Continue(self.0)
          }
      *)
      Definition branch (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructTuple
              "core::ops::control_flow::ControlFlow::Continue"
              [
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    self,
                    "core::ops::try_trait::NeverShortCircuit",
                    0
                  |)
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn from_output(x: T) -> Self {
              NeverShortCircuit(x)
          }
      *)
      Definition from_output (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            Value.StructTuple "core::ops::try_trait::NeverShortCircuit" [ M.read (| x |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::try_trait::Try"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output T));
            ("Residual", InstanceField.Ty (_Residual T));
            ("branch", InstanceField.Method (branch T));
            ("from_output", InstanceField.Method (from_output T))
          ].
    End Impl_core_ops_try_trait_Try_for_core_ops_try_trait_NeverShortCircuit_T.
    
    Module Impl_core_ops_try_trait_FromResidual_for_core_ops_try_trait_NeverShortCircuit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ].
      
      (*
          fn from_residual(never: NeverShortCircuitResidual) -> Self {
              match never {}
          }
      *)
      Definition from_residual
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ never ] =>
          ltac:(M.monadic
            (let never := M.alloc (| never |) in
            M.never_to_any (| M.read (| M.match_operator (| never, [] |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::try_trait::FromResidual"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("from_residual", InstanceField.Method (from_residual T)) ].
    End Impl_core_ops_try_trait_FromResidual_for_core_ops_try_trait_NeverShortCircuit_T.
    
    Module Impl_core_ops_try_trait_Residual_T_for_core_ops_try_trait_NeverShortCircuitResidual.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.path "core::ops::try_trait::NeverShortCircuitResidual".
      
      (*     type TryType = NeverShortCircuit<T>; *)
      Definition _TryType (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::try_trait::Residual"
          (Self T)
          (* Trait polymorphic types *) [ (* O *) T ]
          (* Instance *) [ ("TryType", InstanceField.Ty (_TryType T)) ].
    End Impl_core_ops_try_trait_Residual_T_for_core_ops_try_trait_NeverShortCircuitResidual.
    
    (* StructTuple
      {
        name := "Yeet";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ T ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_ops_try_trait_Yeet_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::ops::try_trait::Yeet") [] [ T ].
      
      (* Debug *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_tuple_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Yeet" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::ops::try_trait::Yeet",
                    0
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_ops_try_trait_Yeet_T.
  End try_trait.
End ops.
