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

Module iter.
  Module sources.
    Module once_with.
      (*
      pub fn once_with<A, F: FnOnce() -> A>(gen: F) -> OnceWith<F> {
          OnceWith { gen: Some(gen) }
      }
      *)
      Definition once_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ A; F ], [ gen ] =>
          ltac:(M.monadic
            (let gen := M.alloc (| gen |) in
            Value.StructRecord
              "core::iter::sources::once_with::OnceWith"
              [ ("gen", Value.StructTuple "core::option::Option::Some" [ M.read (| gen |) ]) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_once_with : M.IsFunction "core::iter::sources::once_with::once_with" once_with.
      
      (* StructRecord
        {
          name := "OnceWith";
          const_params := [];
          ty_params := [ "F" ];
          fields := [ ("gen", Ty.apply (Ty.path "core::option::Option") [] [ F ]) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_F_for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ 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::once_with::OnceWith"
                [
                  ("gen",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::option::Option") [] [ F ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::sources::once_with::OnceWith",
                          "gen"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_once_with_OnceWith_F.
      
      Module Impl_core_fmt_Debug_for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ F ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                if self.gen.is_some() {
                    f.write_str("OnceWith(Some(_))")
                } else {
                    f.write_str("OnceWith(None)")
                }
            }
        *)
        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.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::option::Option") [] [ F ],
                                  "is_some",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::once_with::OnceWith",
                                    "gen"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_str",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "OnceWith(Some(_))" |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_str",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "OnceWith(None)" |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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_once_with_OnceWith_F.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ F ].
        
        (*     type Item = A; *)
        Definition _Item (A F : Ty.t) : Ty.t := A.
        
        (*
            fn next(&mut self) -> Option<A> {
                let f = self.gen.take()?;
                Some(f())
            }
        *)
        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
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ f :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply (Ty.path "core::option::Option") [] [ F ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ F ],
                                    "take",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::sources::once_with::OnceWith",
                                      "gen"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply (Ty.path "core::option::Option") [] [ A ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [] ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                self.gen.iter().size_hint()
            }
        *)
        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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::option::Iter") [] [ F ],
                  [],
                  "size_hint",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::option::Option") [] [ F ],
                        "iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::sources::once_with::OnceWith",
                          "gen"
                        |)
                      ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ F ].
        
        (*
            fn next_back(&mut self) -> Option<A> {
                self.next()
            }
        *)
        Definition next_back
            (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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ F ],
                  [],
                  "next",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self A F)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("next_back", InstanceField.Method (next_back A F)) ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ F ].
        
        (*
            fn len(&self) -> usize {
                self.gen.iter().len()
            }
        *)
        Definition len (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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  Ty.apply (Ty.path "core::option::Iter") [] [ F ],
                  [],
                  "len",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::option::Option") [] [ F ],
                        "iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::sources::once_with::OnceWith",
                          "gen"
                        |)
                      ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A F : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self A F)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("len", InstanceField.Method (len A F)) ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ 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_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_ops_function_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
        Definition Self (A F : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once_with::OnceWith") [] [ 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_FnOnce_F_Tuple__for_core_iter_sources_once_with_OnceWith_F.
    End once_with.
  End sources.
End iter.
