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

Module future.
  Module pending.
    (* StructRecord
      {
        name := "Pending";
        const_params := [];
        ty_params := [ "T" ];
        fields :=
          [ ("_data", Ty.apply (Ty.path "core::marker::PhantomData") [] [ Ty.function [] T ]) ];
      } *)
    
    (*
    pub fn pending<T>() -> Pending<T> {
        Pending { _data: marker::PhantomData }
    }
    *)
    Definition pending (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::future::pending::Pending"
            [ ("_data", Value.StructTuple "core::marker::PhantomData" []) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_pending : M.IsFunction "core::future::pending::pending" pending.
    
    Module Impl_core_future_future_Future_for_core_future_pending_Pending_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::pending::Pending") [] [ T ].
      
      (*     type Output = T; *)
      Definition _Output (T : Ty.t) : Ty.t := T.
      
      (*
          fn poll(self: Pin<&mut Self>, _: &mut Context<'_>) -> Poll<T> {
              Poll::Pending
          }
      *)
      Definition poll (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; β1 ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let β1 := M.alloc (| β1 |) in
            M.match_operator (|
              β1,
              [ fun γ => ltac:(M.monadic (Value.StructTuple "core::task::poll::Poll::Pending" [])) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::future::future::Future"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output T)); ("poll", InstanceField.Method (poll T)) ].
    End Impl_core_future_future_Future_for_core_future_pending_Pending_T.
    
    Module Impl_core_fmt_Debug_for_core_future_pending_Pending_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::pending::Pending") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_struct("Pending").finish()
          }
      *)
      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::builders::DebugStruct",
                "finish",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct",
                      []
                    |),
                    [ M.read (| f |); M.read (| Value.String "Pending" |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_for_core_future_pending_Pending_T.
    
    Module Impl_core_clone_Clone_for_core_future_pending_Pending_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::pending::Pending") [] [ T ].
      
      (*
          fn clone(&self) -> Self {
              pending()
          }
      *)
      Definition clone (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
            M.call_closure (| M.get_function (| "core::future::pending::pending", [ T ] |), [] |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
    End Impl_core_clone_Clone_for_core_future_pending_Pending_T.
  End pending.
End future.
