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

Module iter.
  Module sources.
    Module from_fn.
      (*
      pub fn from_fn<T, F>(f: F) -> FromFn<F>
      where
          F: FnMut() -> Option<T>,
      {
          FromFn(f)
      }
      *)
      Definition from_fn (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; F ], [ f ] =>
          ltac:(M.monadic
            (let f := M.alloc (| f |) in
            Value.StructTuple "core::iter::sources::from_fn::FromFn" [ M.read (| f |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_from_fn : M.IsFunction "core::iter::sources::from_fn::from_fn" from_fn.
      
      (* StructTuple
        {
          name := "FromFn";
          const_params := [];
          ty_params := [ "F" ];
          fields := [ F ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_F_for_core_iter_sources_from_fn_FromFn_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::from_fn::FromFn") [] [ F ].
        
        (* Clone *)
        Definition clone (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
              Value.StructTuple
                "core::iter::sources::from_fn::FromFn"
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", F, [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_tuple_field (|
                        M.read (| self |),
                        "core::iter::sources::from_fn::FromFn",
                        0
                      |)
                    ]
                  |)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (F : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self F)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone F)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_F_for_core_iter_sources_from_fn_FromFn_F.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_from_fn_FromFn_F.
        Definition Self (T F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::from_fn::FromFn") [] [ F ].
        
        (*     type Item = T; *)
        Definition _Item (T F : Ty.t) : Ty.t := T.
        
        (*
            fn next(&mut self) -> Option<Self::Item> {
                (self.0)()
            }
        *)
        Definition next (T F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T F in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnMut",
                  F,
                  [ Ty.tuple [] ],
                  "call_mut",
                  []
                |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::iter::sources::from_fn::FromFn",
                    0
                  |);
                  Value.Tuple []
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T F : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self T F)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("Item", InstanceField.Ty (_Item T F)); ("next", InstanceField.Method (next T F)) ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_from_fn_FromFn_F.
      
      Module Impl_core_fmt_Debug_for_core_iter_sources_from_fn_FromFn_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::from_fn::FromFn") [] [ F ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_struct("FromFn").finish()
            }
        *)
        Definition fmt (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self F 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",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "debug_struct",
                        []
                      |),
                      [ M.read (| f |); M.read (| Value.String "FromFn" |) ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (F : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self F)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt F)) ].
      End Impl_core_fmt_Debug_for_core_iter_sources_from_fn_FromFn_F.
    End from_fn.
  End sources.
End iter.
