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

Module async_iter.
  Module async_iter.
    (* Trait *)
    Module AsyncIterator.
      Definition size_hint
          (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
            Value.Tuple
              [ Value.Integer IntegerKind.Usize 0; Value.StructTuple "core::option::Option::None" []
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom ProvidedMethod_size_hint :
        M.IsProvidedMethod "core::async_iter::async_iter::AsyncIterator" "size_hint" size_hint.
    End AsyncIterator.
    
    Module Impl_core_async_iter_async_iter_AsyncIterator_where_core_marker_Sized_S_where_core_async_iter_async_iter_AsyncIterator_S_where_core_marker_Unpin_S_for_ref_mut_S.
      Definition Self (S : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ S ].
      
      (*     type Item = S::Item; *)
      Definition _Item (S : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn poll_next(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Option<Self::Item>> {
              S::poll_next(Pin::new(&mut **self), cx)
          }
      *)
      Definition poll_next (S : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self S 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::async_iter::async_iter::AsyncIterator",
                S,
                [],
                "poll_next",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ S ] ],
                    "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") [] [ S ] ] ],
                          [],
                          "deref_mut",
                          []
                        |),
                        [ self ]
                      |)
                    |)
                  ]
                |);
                M.read (| cx |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              ( **self).size_hint()
          }
      *)
      Definition size_hint (S : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self S in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::async_iter::async_iter::AsyncIterator",
                S,
                [],
                "size_hint",
                []
              |),
              [ M.read (| M.read (| self |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (S : Ty.t),
        M.IsTraitInstance
          "core::async_iter::async_iter::AsyncIterator"
          (Self S)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item S));
            ("poll_next", InstanceField.Method (poll_next S));
            ("size_hint", InstanceField.Method (size_hint S))
          ].
    End Impl_core_async_iter_async_iter_AsyncIterator_where_core_marker_Sized_S_where_core_async_iter_async_iter_AsyncIterator_S_where_core_marker_Unpin_S_for_ref_mut_S.
    
    Module Impl_core_async_iter_async_iter_AsyncIterator_where_core_ops_deref_DerefMut_P_where_core_async_iter_async_iter_AsyncIterator_associated_type_for_core_pin_Pin_P.
      Definition Self (P : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ P ].
      
      (*     type Item = <P::Target as AsyncIterator>::Item; *)
      Definition _Item (P : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn poll_next(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Option<Self::Item>> {
              <P::Target as AsyncIterator>::poll_next(self.as_deref_mut(), cx)
          }
      *)
      Definition poll_next (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::async_iter::async_iter::AsyncIterator",
                Ty.associated,
                [],
                "poll_next",
                []
              |),
              [
                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.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              ( **self).size_hint()
          }
      *)
      Definition size_hint (P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::async_iter::async_iter::AsyncIterator",
                Ty.associated,
                [],
                "size_hint",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::deref::Deref",
                    Ty.apply (Ty.path "core::pin::Pin") [] [ P ],
                    [],
                    "deref",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (P : Ty.t),
        M.IsTraitInstance
          "core::async_iter::async_iter::AsyncIterator"
          (Self P)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item P));
            ("poll_next", InstanceField.Method (poll_next P));
            ("size_hint", InstanceField.Method (size_hint P))
          ].
    End Impl_core_async_iter_async_iter_AsyncIterator_where_core_ops_deref_DerefMut_P_where_core_async_iter_async_iter_AsyncIterator_associated_type_for_core_pin_Pin_P.
    
    Module Impl_core_task_poll_Poll_core_option_Option_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "core::task::poll::Poll")
          []
          [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ].
      
      (*
          pub fn async_gen_ready(t: T) -> Self {
              Poll::Ready(Some(t))
          }
      *)
      Definition async_gen_ready
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ t ] =>
          ltac:(M.monadic
            (let t := M.alloc (| t |) in
            Value.StructTuple
              "core::task::poll::Poll::Ready"
              [ Value.StructTuple "core::option::Option::Some" [ M.read (| t |) ] ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_async_gen_ready :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "async_gen_ready" (async_gen_ready T).
      
      (*     pub const PENDING: Self = Poll::Pending; *)
      (* Ty.apply
        (Ty.path "core::task::poll::Poll")
        []
        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ] *)
      Definition value_PENDING (T : Ty.t) : Value.t :=
        let Self : Ty.t := Self T in
        M.run
          ltac:(M.monadic (M.alloc (| Value.StructTuple "core::task::poll::Poll::Pending" [] |))).
      
      Axiom AssociatedConstant_value_PENDING :
        forall (T : Ty.t),
        M.IsAssociatedConstant (Self T) "value_PENDING" (value_PENDING T).
      
      (*     pub const FINISHED: Self = Poll::Ready(None); *)
      (* Ty.apply
        (Ty.path "core::task::poll::Poll")
        []
        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ] *)
      Definition value_FINISHED (T : Ty.t) : Value.t :=
        let Self : Ty.t := Self T in
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.StructTuple
                "core::task::poll::Poll::Ready"
                [ Value.StructTuple "core::option::Option::None" [] ]
            |))).
      
      Axiom AssociatedConstant_value_FINISHED :
        forall (T : Ty.t),
        M.IsAssociatedConstant (Self T) "value_FINISHED" (value_FINISHED T).
    End Impl_core_task_poll_Poll_core_option_Option_T.
    
    (* Trait *)
    (* Empty module 'IntoAsyncIterator' *)
    
    Module Impl_core_async_iter_async_iter_IntoAsyncIterator_where_core_async_iter_async_iter_AsyncIterator_I_for_I.
      Definition Self (I : Ty.t) : Ty.t := I.
      
      (*     type Item = I::Item; *)
      Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
      
      (*     type IntoAsyncIter = I; *)
      Definition _IntoAsyncIter (I : Ty.t) : Ty.t := I.
      
      (*
          fn into_async_iter(self) -> Self::IntoAsyncIter {
              self
          }
      *)
      Definition into_async_iter
          (I : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self I in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::async_iter::async_iter::IntoAsyncIterator"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item I));
            ("IntoAsyncIter", InstanceField.Ty (_IntoAsyncIter I));
            ("into_async_iter", InstanceField.Method (into_async_iter I))
          ].
    End Impl_core_async_iter_async_iter_IntoAsyncIterator_where_core_async_iter_async_iter_AsyncIterator_I_for_I.
  End async_iter.
End async_iter.
