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

Module future.
  Module join.
    (*
    Enum MaybeDone
    {
      const_params := [];
      ty_params := [ "F" ];
      variants :=
        [
          {
            name := "Future";
            item := StructTuple [ F ];
            discriminant := None;
          };
          {
            name := "Done";
            item := StructTuple [ Ty.associated ];
            discriminant := None;
          };
          {
            name := "Taken";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_future_join_MaybeDone_F.
      Definition Self (F : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::join::MaybeDone") [] [ F ].
      
      (*
          pub fn take_output(&mut self) -> Option<F::Output> {
              match *self {
                  MaybeDone::Done(_) => match mem::replace(self, Self::Taken) {
                      MaybeDone::Done(val) => Some(val),
                      _ => unreachable!(),
                  },
                  _ => None,
              }
          }
      *)
      Definition take_output (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self F in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::future::join::MaybeDone::Done",
                          0
                        |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::mem::replace",
                              [ Ty.apply (Ty.path "core::future::join::MaybeDone") [] [ F ] ]
                            |),
                            [
                              M.read (| self |);
                              Value.StructTuple "core::future::join::MaybeDone::Taken" []
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::future::join::MaybeDone::Done",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              M.alloc (|
                                Value.StructTuple "core::option::Option::Some" [ M.read (| val |) ]
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::panicking::panic", [] |),
                                    [
                                      M.read (|
                                        Value.String "internal error: entered unreachable code"
                                      |)
                                    ]
                                  |)
                                |)
                              |)))
                        ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_take_output :
        forall (F : Ty.t),
        M.IsAssociatedFunction (Self F) "take_output" (take_output F).
    End Impl_core_future_join_MaybeDone_F.
    
    Module Impl_core_future_future_Future_where_core_future_future_Future_F_for_core_future_join_MaybeDone_F.
      Definition Self (F : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::future::join::MaybeDone") [] [ F ].
      
      (*     type Output = (); *)
      Definition _Output (F : Ty.t) : Ty.t := Ty.tuple [].
      
      (*
          fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              // SAFETY: pinning in structural for `f`
              unsafe {
                  // Do not mix match ergonomics with unsafe.
                  match *self.as_mut().get_unchecked_mut() {
                      MaybeDone::Future(ref mut f) => {
                          let val = ready!(Pin::new_unchecked(f).poll(cx));
                          self.set(Self::Done(val));
                      }
                      MaybeDone::Done(_) => {}
                      MaybeDone::Taken => unreachable!(),
                  }
              }
      
              Poll::Ready(())
          }
      *)
      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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::pin::Pin")
                            []
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [ Ty.apply (Ty.path "core::future::join::MaybeDone") [] [ F ] ]
                            ],
                          "get_unchecked_mut",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::pin::Pin")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "&mut")
                                    []
                                    [ Ty.apply (Ty.path "core::future::join::MaybeDone") [] [ F ] ]
                                ],
                              "as_mut",
                              []
                            |),
                            [ self ]
                          |)
                        ]
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::future::join::MaybeDone::Future",
                                0
                              |) in
                            let f := M.alloc (| γ0_0 |) in
                            let~ val :=
                              M.copy (|
                                M.match_operator (|
                                  M.alloc (|
                                    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_unchecked",
                                            []
                                          |),
                                          [ M.read (| f |) ]
                                        |);
                                        M.read (| cx |)
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::task::poll::Poll::Ready",
                                            0
                                          |) in
                                        let t := M.copy (| γ0_0 |) in
                                        t));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (|
                                            γ,
                                            "core::task::poll::Poll::Pending"
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::task::poll::Poll::Pending"
                                                  []
                                              |)
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::pin::Pin")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "&mut")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::future::join::MaybeDone")
                                              []
                                              [ F ]
                                          ]
                                      ],
                                    "set",
                                    []
                                  |),
                                  [
                                    self;
                                    Value.StructTuple
                                      "core::future::join::MaybeDone::Done"
                                      [ M.read (| val |) ]
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::future::join::MaybeDone::Done",
                                0
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (| γ, "core::future::join::MaybeDone::Taken" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.call_closure (|
                                  M.get_function (| "core::panicking::panic", [] |),
                                  [
                                    M.read (|
                                      Value.String "internal error: entered unreachable code"
                                    |)
                                  ]
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  M.alloc (| Value.StructTuple "core::task::poll::Poll::Ready" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => 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_future_future_Future_F_for_core_future_join_MaybeDone_F.
  End join.
End future.
