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

Module future.
  Module future.
    (* Trait *)
    (* Empty module 'Future' *)
    
    Module Impl_core_future_future_Future_where_core_marker_Sized_F_where_core_future_future_Future_F_where_core_marker_Unpin_F_for_ref_mut_F.
      Definition Self (F : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ F ].
      
      (*     type Output = F::Output; *)
      Definition _Output (F : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              F::poll(Pin::new(&mut **self), cx)
          }
      *)
      Definition poll (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self F in
        match ε, τ, α with
        | [], [], [ self; cx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let cx := M.alloc (| cx |) in
            M.call_closure (|
              M.get_trait_method (| "core::future::future::Future", F, [], "poll", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ F ] ],
                    "new",
                    []
                  |),
                  [
                    M.read (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::DerefMut",
                          Ty.apply
                            (Ty.path "core::pin::Pin")
                            []
                            [ Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "&mut") [] [ F ] ] ],
                          [],
                          "deref_mut",
                          []
                        |),
                        [ self ]
                      |)
                    |)
                  ]
                |);
                M.read (| cx |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (F : Ty.t),
        M.IsTraitInstance
          "core::future::future::Future"
          (Self F)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output F)); ("poll", InstanceField.Method (poll F)) ].
    End Impl_core_future_future_Future_where_core_marker_Sized_F_where_core_future_future_Future_F_where_core_marker_Unpin_F_for_ref_mut_F.
    
    Module Impl_core_future_future_Future_where_core_ops_deref_DerefMut_P_for_core_pin_Pin_P.
      Definition Self (P : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ P ].
      
      (*     type Output = <<P as ops::Deref>::Target as Future>::Output; *)
      Definition _Output (P : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              <P::Target as Future>::poll(self.as_deref_mut(), cx)
          }
      *)
      Definition poll (P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self P in
        match ε, τ, α with
        | [], [], [ self; cx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let cx := M.alloc (| cx |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::future::future::Future",
                Ty.associated,
                [],
                "poll",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::pin::Pin") [] [ P ],
                    "as_deref_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| cx |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (P : Ty.t),
        M.IsTraitInstance
          "core::future::future::Future"
          (Self P)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output P)); ("poll", InstanceField.Method (poll P)) ].
    End Impl_core_future_future_Future_where_core_ops_deref_DerefMut_P_for_core_pin_Pin_P.
  End future.
End future.
