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

Module iter.
  Module adapters.
    (* Trait *)
    (* Empty module 'SourceIter' *)
    
    (* StructRecord
      {
        name := "GenericShunt";
        const_params := [];
        ty_params := [ "I"; "R" ];
        fields :=
          [
            ("iter", I);
            ("residual",
              Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "core::option::Option") [] [ R ] ])
          ];
      } *)
    
    (*
    pub(crate) fn try_process<I, T, R, F, U>(iter: I, mut f: F) -> ChangeOutputType<I::Item, U>
    where
        I: Iterator<Item: Try<Output = T, Residual = R>>,
        for<'a> F: FnMut(GenericShunt<'a, I, R>) -> U,
        R: Residual<U>,
    {
        let mut residual = None;
        let shunt = GenericShunt { iter, residual: &mut residual };
        let value = f(shunt);
        match residual {
            Some(r) => FromResidual::from_residual(r),
            None => Try::from_output(value),
        }
    }
    *)
    Definition try_process (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I; T; R; F; U ], [ iter; f ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ residual := M.alloc (| Value.StructTuple "core::option::Option::None" [] |) in
            let~ shunt :=
              M.alloc (|
                Value.StructRecord
                  "core::iter::adapters::GenericShunt"
                  [ ("iter", M.read (| iter |)); ("residual", residual) ]
              |) in
            let~ value :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnMut",
                    F,
                    [
                      Ty.tuple
                        [ Ty.apply (Ty.path "core::iter::adapters::GenericShunt") [] [ I; R ] ]
                    ],
                    "call_mut",
                    []
                  |),
                  [ f; Value.Tuple [ M.read (| shunt |) ] ]
                |)
              |) in
            M.match_operator (|
              residual,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let r := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::FromResidual",
                          Ty.associated,
                          [ R ],
                          "from_residual",
                          []
                        |),
                        [ M.read (| r |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.associated,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| value |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_try_process : M.IsFunction "core::iter::adapters::try_process" try_process.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_GenericShunt_I_R.
      Definition Self (I R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::iter::adapters::GenericShunt") [] [ I; R ].
      
      (*     type Item = <I::Item as Try>::Output; *)
      Definition _Item (I R : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn next(&mut self) -> Option<Self::Item> {
              self.try_for_each(ControlFlow::Break).break_value()
          }
      *)
      Definition next (I R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I R 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::ops::control_flow::ControlFlow")
                  []
                  [ Ty.associated; Ty.tuple [] ],
                "break_value",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply (Ty.path "core::iter::adapters::GenericShunt") [] [ I; R ],
                    [],
                    "try_for_each",
                    [
                      Ty.function
                        [ Ty.associated ]
                        (Ty.apply
                          (Ty.path "core::ops::control_flow::ControlFlow")
                          []
                          [ Ty.associated; Ty.tuple [] ]);
                      Ty.apply
                        (Ty.path "core::ops::control_flow::ControlFlow")
                        []
                        [ Ty.associated; Ty.tuple [] ]
                    ]
                  |),
                  [
                    M.read (| self |);
                    M.constructor_as_closure "core::ops::control_flow::ControlFlow::Break"
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              if self.residual.is_some() {
                  (0, Some(0))
              } else {
                  let (_, upper) = self.iter.size_hint();
                  (0, upper)
              }
          }
      *)
      Definition size_hint (I R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I R in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) 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") [] [ R ],
                                "is_some",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::adapters::GenericShunt",
                                    "residual"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.Tuple
                          [
                            Value.Integer IntegerKind.Usize 0;
                            Value.StructTuple
                              "core::option::Option::Some"
                              [ Value.Integer IntegerKind.Usize 0 ]
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              I,
                              [],
                              "size_hint",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::iter::adapters::GenericShunt",
                                "iter"
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let upper := M.copy (| γ0_1 |) in
                              M.alloc (|
                                Value.Tuple
                                  [ Value.Integer IntegerKind.Usize 0; M.read (| upper |) ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn try_fold<B, F, T>(&mut self, init: B, mut f: F) -> T
          where
              F: FnMut(B, Self::Item) -> T,
              T: Try<Output = B>,
          {
              self.iter
                  .try_fold(init, |acc, x| match Try::branch(x) {
                      ControlFlow::Continue(x) => ControlFlow::from_try(f(acc, x)),
                      ControlFlow::Break(r) => {
                          *self.residual = Some(r);
                          ControlFlow::Break(try { acc })
                      }
                  })
                  .into_try()
          }
      *)
      Definition try_fold (I R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I R in
        match ε, τ, α with
        | [], [ B; F; T ], [ self; init; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ T; Ty.associated ],
                "into_try",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    I,
                    [],
                    "try_fold",
                    [
                      B;
                      Ty.function
                        [ Ty.tuple [ B; Ty.associated ] ]
                        (Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ T; B ]);
                      Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ T; B ]
                    ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::GenericShunt",
                      "iter"
                    |);
                    M.read (| init |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let acc := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let x := M.copy (| γ |) in
                                              M.read (|
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::try_trait::Try",
                                                        Ty.associated,
                                                        [],
                                                        "branch",
                                                        []
                                                      |),
                                                      [ M.read (| x |) ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::ops::control_flow::ControlFlow::Continue",
                                                            0
                                                          |) in
                                                        let x := M.copy (| γ0_0 |) in
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::ops::control_flow::ControlFlow")
                                                                []
                                                                [ T; Ty.associated ],
                                                              "from_try",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::function::FnMut",
                                                                  F,
                                                                  [ Ty.tuple [ B; Ty.associated ] ],
                                                                  "call_mut",
                                                                  []
                                                                |),
                                                                [
                                                                  f;
                                                                  Value.Tuple
                                                                    [
                                                                      M.read (| acc |);
                                                                      M.read (| x |)
                                                                    ]
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::ops::control_flow::ControlFlow::Break",
                                                            0
                                                          |) in
                                                        let r := M.copy (| γ0_0 |) in
                                                        let~ _ :=
                                                          M.write (|
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "core::iter::adapters::GenericShunt",
                                                                "residual"
                                                              |)
                                                            |),
                                                            Value.StructTuple
                                                              "core::option::Option::Some"
                                                              [ M.read (| r |) ]
                                                          |) in
                                                        M.alloc (|
                                                          Value.StructTuple
                                                            "core::ops::control_flow::ControlFlow::Break"
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::Try",
                                                                  T,
                                                                  [],
                                                                  "from_output",
                                                                  []
                                                                |),
                                                                [ M.read (| acc |) ]
                                                              |)
                                                            ]
                                                        |)))
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn $fold<AAA, FFF>(mut self, init: AAA, fold: FFF) -> AAA
              where
                  FFF: FnMut(AAA, Self::Item) -> AAA,
              {
                  use crate::ops::NeverShortCircuit;
      
                  self.$try_fold(init, NeverShortCircuit::wrap_mut_2(fold)).0
              }
      *)
      Definition fold (I R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I R in
        match ε, τ, α with
        | [], [ AAA; FFF ], [ 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.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply (Ty.path "core::iter::adapters::GenericShunt") [] [ I; R ],
                      [],
                      "try_fold",
                      [
                        AAA;
                        Ty.associated;
                        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ AAA ]
                      ]
                    |),
                    [
                      self;
                      M.read (| init |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ AAA ],
                          "wrap_mut_2",
                          [ AAA; Ty.associated; FFF ]
                        |),
                        [ M.read (| fold |) ]
                      |)
                    ]
                  |)
                |),
                "core::ops::try_trait::NeverShortCircuit",
                0
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I R : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self I R)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item I R));
            ("next", InstanceField.Method (next I R));
            ("size_hint", InstanceField.Method (size_hint I R));
            ("try_fold", InstanceField.Method (try_fold I R));
            ("fold", InstanceField.Method (fold I R))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_GenericShunt_I_R.
    
    Module Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_GenericShunt_I_R.
      Definition Self (I R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::iter::adapters::GenericShunt") [] [ I; R ].
      
      (*     type Source = I::Source; *)
      Definition _Source (I R : Ty.t) : Ty.t := Ty.associated.
      
      (*
          unsafe fn as_inner(&mut self) -> &mut Self::Source {
              // SAFETY: unsafe function forwarding to unsafe function with the same requirements
              unsafe { SourceIter::as_inner(&mut self.iter) }
          }
      *)
      Definition as_inner (I R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I R in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (| "core::iter::adapters::SourceIter", I, [], "as_inner", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::iter::adapters::GenericShunt",
                  "iter"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I R : Ty.t),
        M.IsTraitInstance
          "core::iter::adapters::SourceIter"
          (Self I R)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Source", InstanceField.Ty (_Source I R));
            ("as_inner", InstanceField.Method (as_inner I R))
          ].
    End Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_GenericShunt_I_R.
    
    Module Impl_core_iter_traits_marker_InPlaceIterable_where_core_iter_traits_marker_InPlaceIterable_I_for_core_iter_adapters_GenericShunt_I_R.
      Definition Self (I R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::iter::adapters::GenericShunt") [] [ I; R ].
      
      (*     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY; *)
      (* Ty.apply
        (Ty.path "core::option::Option")
        []
        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
      Definition value_EXPAND_BY (I R : Ty.t) : Value.t :=
        let Self : Ty.t := Self I R in
        M.run
          ltac:(M.monadic
            (M.get_constant (| "core::iter::traits::marker::InPlaceIterable::EXPAND_BY" |))).
      
      (*     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY; *)
      (* Ty.apply
        (Ty.path "core::option::Option")
        []
        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
      Definition value_MERGE_BY (I R : Ty.t) : Value.t :=
        let Self : Ty.t := Self I R in
        M.run
          ltac:(M.monadic
            (M.get_constant (| "core::iter::traits::marker::InPlaceIterable::MERGE_BY" |))).
      
      Axiom Implements :
        forall (I R : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::InPlaceIterable"
          (Self I R)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("value_EXPAND_BY", InstanceField.Constant (value_EXPAND_BY I R));
            ("value_MERGE_BY", InstanceField.Constant (value_MERGE_BY I R))
          ].
    End Impl_core_iter_traits_marker_InPlaceIterable_where_core_iter_traits_marker_InPlaceIterable_I_for_core_iter_adapters_GenericShunt_I_R.
  End adapters.
End iter.
