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

Module ops.
  Module async_function.
    (* Trait *)
    (* Empty module 'AsyncFn' *)
    
    (* Trait *)
    (* Empty module 'AsyncFnMut' *)
    
    (* Trait *)
    (* Empty module 'AsyncFnOnce' *)
    
    Module impls.
      Module Impl_core_ops_async_function_AsyncFn_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFn_F_A_A_for_ref__F.
        Definition Self (A F : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ F ].
        
        (*
                extern "rust-call" fn async_call(&self, args: A) -> Self::CallRefFuture<'_> {
                    F::async_call( *self, args)
                }
        *)
        Definition async_call
            (A F : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A F 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::async_function::AsyncFn",
                  F,
                  [ A ],
                  "async_call",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| args |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::ops::async_function::AsyncFn"
            (Self A F)
            (* Trait polymorphic types *) [ (* Args *) A ]
            (* Instance *) [ ("async_call", InstanceField.Method (async_call A F)) ].
      End Impl_core_ops_async_function_AsyncFn_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFn_F_A_A_for_ref__F.
      
      Module Impl_core_ops_async_function_AsyncFnMut_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFn_F_A_A_for_ref__F.
        Definition Self (A F : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ F ].
        
        (*
                type CallRefFuture<'a>
                    = F::CallRefFuture<'a>
                where
                    Self: 'a;
        *)
        Definition _CallRefFuture (A F : Ty.t) : Ty.t := Ty.associated.
        
        (*
                extern "rust-call" fn async_call_mut(&mut self, args: A) -> Self::CallRefFuture<'_> {
                    F::async_call( *self, args)
                }
        *)
        Definition async_call_mut
            (A F : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A F 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::async_function::AsyncFn",
                  F,
                  [ A ],
                  "async_call",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| args |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::ops::async_function::AsyncFnMut"
            (Self A F)
            (* Trait polymorphic types *) [ (* Args *) A ]
            (* Instance *)
            [
              ("CallRefFuture", InstanceField.Ty (_CallRefFuture A F));
              ("async_call_mut", InstanceField.Method (async_call_mut A F))
            ].
      End Impl_core_ops_async_function_AsyncFnMut_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFn_F_A_A_for_ref__F.
      
      Module Impl_core_ops_async_function_AsyncFnOnce_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFn_F_A_A_for_ref__F.
        Definition Self (A F : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ F ].
        
        (*         type Output = F::Output; *)
        Definition _Output (A F : Ty.t) : Ty.t := Ty.associated.
        
        (*         type CallOnceFuture = F::CallRefFuture<'a>; *)
        Definition _CallOnceFuture (A F : Ty.t) : Ty.t := Ty.associated.
        
        (*
                extern "rust-call" fn async_call_once(self, args: A) -> Self::CallOnceFuture {
                    F::async_call(self, args)
                }
        *)
        Definition async_call_once
            (A F : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A F 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::async_function::AsyncFn",
                  F,
                  [ A ],
                  "async_call",
                  []
                |),
                [ M.read (| self |); M.read (| args |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::ops::async_function::AsyncFnOnce"
            (Self A F)
            (* Trait polymorphic types *) [ (* Args *) A ]
            (* Instance *)
            [
              ("Output", InstanceField.Ty (_Output A F));
              ("CallOnceFuture", InstanceField.Ty (_CallOnceFuture A F));
              ("async_call_once", InstanceField.Method (async_call_once A F))
            ].
      End Impl_core_ops_async_function_AsyncFnOnce_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFn_F_A_A_for_ref__F.
      
      Module Impl_core_ops_async_function_AsyncFnMut_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFnMut_F_A_A_for_ref_mut_F.
        Definition Self (A F : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ F ].
        
        (*
                type CallRefFuture<'a>
                    = F::CallRefFuture<'a>
                where
                    Self: 'a;
        *)
        Definition _CallRefFuture (A F : Ty.t) : Ty.t := Ty.associated.
        
        (*
                extern "rust-call" fn async_call_mut(&mut self, args: A) -> Self::CallRefFuture<'_> {
                    F::async_call_mut( *self, args)
                }
        *)
        Definition async_call_mut
            (A F : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A F 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::async_function::AsyncFnMut",
                  F,
                  [ A ],
                  "async_call_mut",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| args |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::ops::async_function::AsyncFnMut"
            (Self A F)
            (* Trait polymorphic types *) [ (* Args *) A ]
            (* Instance *)
            [
              ("CallRefFuture", InstanceField.Ty (_CallRefFuture A F));
              ("async_call_mut", InstanceField.Method (async_call_mut A F))
            ].
      End Impl_core_ops_async_function_AsyncFnMut_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFnMut_F_A_A_for_ref_mut_F.
      
      Module Impl_core_ops_async_function_AsyncFnOnce_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFnMut_F_A_A_for_ref_mut_F.
        Definition Self (A F : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ F ].
        
        (*         type Output = F::Output; *)
        Definition _Output (A F : Ty.t) : Ty.t := Ty.associated.
        
        (*         type CallOnceFuture = F::CallRefFuture<'a>; *)
        Definition _CallOnceFuture (A F : Ty.t) : Ty.t := Ty.associated.
        
        (*
                extern "rust-call" fn async_call_once(self, args: A) -> Self::CallOnceFuture {
                    F::async_call_mut(self, args)
                }
        *)
        Definition async_call_once
            (A F : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A F 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::async_function::AsyncFnMut",
                  F,
                  [ A ],
                  "async_call_mut",
                  []
                |),
                [ M.read (| self |); M.read (| args |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::ops::async_function::AsyncFnOnce"
            (Self A F)
            (* Trait polymorphic types *) [ (* Args *) A ]
            (* Instance *)
            [
              ("Output", InstanceField.Ty (_Output A F));
              ("CallOnceFuture", InstanceField.Ty (_CallOnceFuture A F));
              ("async_call_once", InstanceField.Method (async_call_once A F))
            ].
      End Impl_core_ops_async_function_AsyncFnOnce_where_core_marker_Tuple_A_where_core_marker_Sized_F_where_core_ops_async_function_AsyncFnMut_F_A_A_for_ref_mut_F.
    End impls.
    
    Module internal_implementation_detail.
      (* Trait *)
      (* Empty module 'AsyncFnKindHelper' *)
    End internal_implementation_detail.
  End async_function.
End ops.
