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

Module sync.
  Module exclusive.
    (* StructRecord
      {
        name := "Exclusive";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ ("inner", T) ];
      } *)
    
    Module Impl_core_default_Default_where_core_default_Default_T_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ].
      
      (* Default *)
      Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "core::sync::exclusive::Exclusive"
              [
                ("inner",
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::default::Default"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    End Impl_core_default_Default_where_core_default_Default_T_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
    
    Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::Sync"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
    
    Module Impl_core_fmt_Debug_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
              f.debug_struct("Exclusive").finish_non_exhaustive()
          }
      *)
      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_non_exhaustive",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct",
                      []
                    |),
                    [ M.read (| f |); M.read (| Value.String "Exclusive" |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
    
    Module Impl_core_sync_exclusive_Exclusive_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ].
      
      (*
          pub const fn new(t: T) -> Self {
              Self { inner: t }
          }
      *)
      Definition new (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.StructRecord "core::sync::exclusive::Exclusive" [ ("inner", M.read (| t |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "new" (new T).
      
      (*
          pub const fn into_inner(self) -> T {
              self.inner
          }
      *)
      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.read (|
              M.SubPointer.get_struct_record_field (|
                self,
                "core::sync::exclusive::Exclusive",
                "inner"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_inner :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
      (*
          pub const fn get_mut(&mut self) -> &mut T {
              &mut self.inner
          }
      *)
      Definition get_mut (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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "core::sync::exclusive::Exclusive",
              "inner"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
      
      (*
          pub const fn get_pin_mut(self: Pin<&mut Self>) -> Pin<&mut T> {
              // SAFETY: `Exclusive` can only produce `&mut T` if itself is unpinned
              // `Pin::map_unchecked_mut` is not const, so we do this conversion manually
              unsafe { Pin::new_unchecked(&mut self.get_unchecked_mut().inner) }
          }
      *)
      Definition get_pin_mut (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::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                "new_unchecked",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::pin::Pin")
                        []
                        [
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [ Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ] ]
                        ],
                      "get_unchecked_mut",
                      []
                    |),
                    [ M.read (| self |) ]
                  |),
                  "core::sync::exclusive::Exclusive",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get_pin_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "get_pin_mut" (get_pin_mut T).
      
      (*
          pub const fn from_mut(r: &'_ mut T) -> &'_ mut Exclusive<T> {
              // SAFETY: repr is ≥ C, so refs have the same layout; and `Exclusive` properties are `&mut`-agnostic
              unsafe { &mut *(r as *mut T as *mut Exclusive<T>) }
          }
      *)
      Definition from_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ r ] =>
          ltac:(M.monadic
            (let r := M.alloc (| r |) in
            M.rust_cast (M.read (| M.use (M.alloc (| M.read (| r |) |)) |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "from_mut" (from_mut T).
      
      (*
          pub const fn from_pin_mut(r: Pin<&'_ mut T>) -> Pin<&'_ mut Exclusive<T>> {
              // SAFETY: `Exclusive` can only produce `&mut T` if itself is unpinned
              // `Pin::map_unchecked_mut` is not const, so we do this conversion manually
              unsafe { Pin::new_unchecked(Self::from_mut(r.get_unchecked_mut())) }
          }
      *)
      Definition from_pin_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ r ] =>
          ltac:(M.monadic
            (let r := M.alloc (| r |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::pin::Pin")
                  []
                  [
                    Ty.apply
                      (Ty.path "&mut")
                      []
                      [ Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ] ]
                  ],
                "new_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ],
                    "from_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::pin::Pin")
                          []
                          [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                        "get_unchecked_mut",
                        []
                      |),
                      [ M.read (| r |) ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_pin_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "from_pin_mut" (from_pin_mut T).
    End Impl_core_sync_exclusive_Exclusive_T.
    
    
    Module Impl_core_convert_From_T_for_core_sync_exclusive_Exclusive_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ].
      
      (*
          fn from(t: T) -> Self {
              Self::new(t)
          }
      *)
      Definition from (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
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ],
                "new",
                []
              |),
              [ M.read (| t |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_T_for_core_sync_exclusive_Exclusive_T.
    
    Module Impl_core_ops_function_FnOnce_where_core_ops_function_FnOnce_F_Args_where_core_marker_Tuple_Args_Args_for_core_sync_exclusive_Exclusive_F.
      Definition Self (F Args : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ F ].
      
      (*     type Output = F::Output; *)
      Definition _Output (F Args : Ty.t) : Ty.t := Ty.associated.
      
      (*
          extern "rust-call" fn call_once(self, args: Args) -> Self::Output {
              self.into_inner().call_once(args)
          }
      *)
      Definition call_once
          (F Args : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self F Args in
        match ε, τ, α with
        | [], [], [ self; args ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let args := M.alloc (| args |) in
            M.call_closure (|
              M.get_trait_method (| "core::ops::function::FnOnce", F, [ Args ], "call_once", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ F ],
                    "into_inner",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| args |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (F Args : Ty.t),
        M.IsTraitInstance
          "core::ops::function::FnOnce"
          (Self F Args)
          (* Trait polymorphic types *) [ (* Args *) Args ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output F Args));
            ("call_once", InstanceField.Method (call_once F Args))
          ].
    End Impl_core_ops_function_FnOnce_where_core_ops_function_FnOnce_F_Args_where_core_marker_Tuple_Args_Args_for_core_sync_exclusive_Exclusive_F.
    
    Module Impl_core_ops_function_FnMut_where_core_ops_function_FnMut_F_Args_where_core_marker_Tuple_Args_Args_for_core_sync_exclusive_Exclusive_F.
      Definition Self (F Args : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ F ].
      
      (*
          extern "rust-call" fn call_mut(&mut self, args: Args) -> Self::Output {
              self.get_mut().call_mut(args)
          }
      *)
      Definition call_mut
          (F Args : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self F Args in
        match ε, τ, α with
        | [], [], [ self; args ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let args := M.alloc (| args |) in
            M.call_closure (|
              M.get_trait_method (| "core::ops::function::FnMut", F, [ Args ], "call_mut", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ F ],
                    "get_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| args |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (F Args : Ty.t),
        M.IsTraitInstance
          "core::ops::function::FnMut"
          (Self F Args)
          (* Trait polymorphic types *) [ (* Args *) Args ]
          (* Instance *) [ ("call_mut", InstanceField.Method (call_mut F Args)) ].
    End Impl_core_ops_function_FnMut_where_core_ops_function_FnMut_F_Args_where_core_marker_Tuple_Args_Args_for_core_sync_exclusive_Exclusive_F.
    
    Module Impl_core_future_future_Future_where_core_future_future_Future_T_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ].
      
      (*     type Output = T::Output; *)
      Definition _Output (T : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
              self.get_pin_mut().poll(cx)
          }
      *)
      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
            M.call_closure (|
              M.get_trait_method (| "core::future::future::Future", T, [], "poll", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ T ],
                    "get_pin_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| cx |)
              ]
            |)))
        | _, _, _ => 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_where_core_future_future_Future_T_where_core_marker_Sized_T_for_core_sync_exclusive_Exclusive_T.
    
    Module Impl_core_ops_coroutine_Coroutine_where_core_ops_coroutine_Coroutine_G_R_where_core_marker_Sized_G_R_for_core_sync_exclusive_Exclusive_G.
      Definition Self (R G : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ G ].
      
      (*     type Yield = G::Yield; *)
      Definition _Yield (R G : Ty.t) : Ty.t := Ty.associated.
      
      (*     type Return = G::Return; *)
      Definition _Return (R G : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn resume(self: Pin<&mut Self>, arg: R) -> CoroutineState<Self::Yield, Self::Return> {
              G::resume(self.get_pin_mut(), arg)
          }
      *)
      Definition resume (R G : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self R G in
        match ε, τ, α with
        | [], [], [ self; arg ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let arg := M.alloc (| arg |) in
            M.call_closure (|
              M.get_trait_method (| "core::ops::coroutine::Coroutine", G, [ R ], "resume", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::sync::exclusive::Exclusive") [] [ G ],
                    "get_pin_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| arg |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (R G : Ty.t),
        M.IsTraitInstance
          "core::ops::coroutine::Coroutine"
          (Self R G)
          (* Trait polymorphic types *) [ (* R *) R ]
          (* Instance *)
          [
            ("Yield", InstanceField.Ty (_Yield R G));
            ("Return", InstanceField.Ty (_Return R G));
            ("resume", InstanceField.Method (resume R G))
          ].
    End Impl_core_ops_coroutine_Coroutine_where_core_ops_coroutine_Coroutine_G_R_where_core_marker_Sized_G_R_for_core_sync_exclusive_Exclusive_G.
  End exclusive.
End sync.
