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

Module iter.
  Module sources.
    Module repeat_with.
      (*
      pub fn repeat_with<A, F: FnMut() -> A>(repeater: F) -> RepeatWith<F> {
          RepeatWith { repeater }
      }
      *)
      Definition repeat_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ A; F ], [ repeater ] =>
          ltac:(M.monadic
            (let repeater := M.alloc (| repeater |) in
            Value.StructRecord
              "core::iter::sources::repeat_with::RepeatWith"
              [ ("repeater", M.read (| repeater |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_repeat_with :
        M.IsFunction "core::iter::sources::repeat_with::repeat_with" repeat_with.
      
      (* StructRecord
        {
          name := "RepeatWith";
          const_params := [];
          ty_params := [ "F" ];
          fields := [ ("repeater", F) ];
        } *)
      
      Module Impl_core_marker_Copy_where_core_marker_Copy_F_for_core_iter_sources_repeat_with_RepeatWith_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_with::RepeatWith") [] [ F ].
        
        Axiom Implements :
          forall (F : Ty.t),
          M.IsTraitInstance
            "core::marker::Copy"
            (Self F)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_where_core_marker_Copy_F_for_core_iter_sources_repeat_with_RepeatWith_F.
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_F_for_core_iter_sources_repeat_with_RepeatWith_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_with::RepeatWith") [] [ 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.StructRecord
                "core::iter::sources::repeat_with::RepeatWith"
                [
                  ("repeater",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", F, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::sources::repeat_with::RepeatWith",
                          "repeater"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_repeat_with_RepeatWith_F.
      
      Module Impl_core_fmt_Debug_for_core_iter_sources_repeat_with_RepeatWith_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_with::RepeatWith") [] [ F ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_struct("RepeatWith").finish_non_exhaustive()
            }
        *)
        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_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 "RepeatWith" |) ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_repeat_with_RepeatWith_F.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_repeat_with_RepeatWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_with::RepeatWith") [] [ F ].
        
        (*     type Item = A; *)
        Definition _Item (A F : Ty.t) : Ty.t := A.
        
        (*
            fn next(&mut self) -> Option<A> {
                Some((self.repeater)())
            }
        *)
        Definition next (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructTuple
                "core::option::Option::Some"
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::function::FnMut",
                      F,
                      [ Ty.tuple [] ],
                      "call_mut",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::sources::repeat_with::RepeatWith",
                        "repeater"
                      |);
                      Value.Tuple []
                    ]
                  |)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                (usize::MAX, None)
            }
        *)
        Definition size_hint
            (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.Tuple
                [
                  M.read (| M.get_constant (| "core::num::MAX" |) |);
                  Value.StructTuple "core::option::Option::None" []
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<Acc, Fold, R>(&mut self, mut init: Acc, mut fold: Fold) -> R
            where
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                // This override isn't strictly needed, but avoids the need to optimize
                // away the `next`-always-returns-`Some` and emphasizes that the `?`
                // is the only way to exit the loop.
        
                loop {
                    let item = (self.repeater)();
                    init = fold(init, item)?;
                }
            }
        *)
        Definition try_fold
            (A F : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A F in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; init; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let fold := M.alloc (| fold |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      M.loop (|
                        ltac:(M.monadic
                          (let~ item :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnMut",
                                  F,
                                  [ Ty.tuple [] ],
                                  "call_mut",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_with::RepeatWith",
                                    "repeater"
                                  |);
                                  Value.Tuple []
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              init,
                              M.read (|
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::Try",
                                        R,
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            Fold,
                                            [ Ty.tuple [ Acc; A ] ],
                                            "call_mut",
                                            []
                                          |),
                                          [
                                            fold;
                                            Value.Tuple [ M.read (| init |); M.read (| item |) ]
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::ops::control_flow::ControlFlow::Break",
                                            0
                                          |) in
                                        let residual := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::FromResidual",
                                                    R,
                                                    [ Ty.associated ],
                                                    "from_residual",
                                                    []
                                                  |),
                                                  [ M.read (| residual |) ]
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::ops::control_flow::ControlFlow::Continue",
                                            0
                                          |) in
                                        let val := M.copy (| γ0_0 |) in
                                        val))
                                  ]
                                |)
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self A F)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item A F));
              ("next", InstanceField.Method (next A F));
              ("size_hint", InstanceField.Method (size_hint A F));
              ("try_fold", InstanceField.Method (try_fold A F))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_repeat_with_RepeatWith_F.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_repeat_with_RepeatWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_with::RepeatWith") [] [ F ].
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self A F)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_repeat_with_RepeatWith_F.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_repeat_with_RepeatWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_with::RepeatWith") [] [ F ].
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self A F)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_where_core_ops_function_FnMut_F_Tuple__for_core_iter_sources_repeat_with_RepeatWith_F.
    End repeat_with.
  End sources.
End iter.
