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

Module future.
  Module ready.
    (* StructTuple
      {
        name := "Ready";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_future_ready_Ready_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::future::ready::Ready") [] [ 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 "Ready" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::future::ready::Ready",
                    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_future_ready_Ready_T.
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_future_ready_Ready_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::future::ready::Ready") [] [ T ].
      
      (* Clone *)
      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
            Value.StructTuple
              "core::future::ready::Ready"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ T ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "core::future::ready::Ready",
                      0
                    |)
                  ]
                |)
              ]))
        | _, _, _ => 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_where_core_clone_Clone_T_for_core_future_ready_Ready_T.
    
    Module Impl_core_marker_Unpin_for_core_future_ready_Ready_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::future::ready::Ready") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::Unpin"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Unpin_for_core_future_ready_Ready_T.
    
    Module Impl_core_future_future_Future_for_core_future_ready_Ready_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::future::ready::Ready") [] [ T ].
      
      (*     type Output = T; *)
      Definition _Output (T : Ty.t) : Ty.t := T.
      
      (*
          fn poll(mut self: Pin<&mut Self>, _cx: &mut Context<'_>) -> Poll<T> {
              Poll::Ready(self.0.take().expect("`Ready` polled after completion"))
          }
      *)
      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; _cx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _cx := M.alloc (| _cx |) in
            Value.StructTuple
              "core::task::poll::Poll::Ready"
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ T ],
                    "expect",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::option::Option") [] [ T ],
                        "take",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_tuple_field (|
                          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 "core::future::ready::Ready") [] [ T ] ]
                                ],
                              [],
                              "deref_mut",
                              []
                            |),
                            [ self ]
                          |),
                          "core::future::ready::Ready",
                          0
                        |)
                      ]
                    |);
                    M.read (| Value.String "`Ready` polled after completion" |)
                  ]
                |)
              ]))
        | _, _, _ => 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_ready_Ready_T.
    
    Module Impl_core_future_ready_Ready_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::future::ready::Ready") [] [ T ].
      
      (*
          pub fn into_inner(self) -> T {
              self.0.expect("Called `into_inner()` on `Ready` after completion")
          }
      *)
      Definition into_inner (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_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ T ],
                "expect",
                []
              |),
              [
                M.read (|
                  M.SubPointer.get_struct_tuple_field (| self, "core::future::ready::Ready", 0 |)
                |);
                M.read (| Value.String "Called `into_inner()` on `Ready` after completion" |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_inner :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
    End Impl_core_future_ready_Ready_T.
    
    (*
    pub fn ready<T>(t: T) -> Ready<T> {
        Ready(Some(t))
    }
    *)
    Definition ready (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ t ] =>
        ltac:(M.monadic
          (let t := M.alloc (| t |) in
          Value.StructTuple
            "core::future::ready::Ready"
            [ Value.StructTuple "core::option::Option::Some" [ M.read (| t |) ] ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_ready : M.IsFunction "core::future::ready::ready" ready.
  End ready.
End future.
