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

Module collections.
  Module btree.
    Module dedup_sorted_iter.
      (* StructRecord
        {
          name := "DedupSortedIter";
          const_params := [];
          ty_params := [ "K"; "V"; "I" ];
          fields :=
            [ ("iter", Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ]) ];
        } *)
      
      Module Impl_alloc_collections_btree_dedup_sorted_iter_DedupSortedIter_K_V_I.
        Definition Self (K V I : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::dedup_sorted_iter::DedupSortedIter")
            []
            [ K; V; I ].
        
        (*
            pub fn new(iter: I) -> Self {
                Self { iter: iter.peekable() }
            }
        *)
        Definition new (K V I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self K V I in
          match ε, τ, α with
          | [], [], [ iter ] =>
            ltac:(M.monadic
              (let iter := M.alloc (| iter |) in
              Value.StructRecord
                "alloc::collections::btree::dedup_sorted_iter::DedupSortedIter"
                [
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        I,
                        [],
                        "peekable",
                        []
                      |),
                      [ M.read (| iter |) ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (K V I : Ty.t),
          M.IsAssociatedFunction (Self K V I) "new" (new K V I).
      End Impl_alloc_collections_btree_dedup_sorted_iter_DedupSortedIter_K_V_I.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_cmp_Eq_K_where_core_iter_traits_iterator_Iterator_I_for_alloc_collections_btree_dedup_sorted_iter_DedupSortedIter_K_V_I.
        Definition Self (K V I : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::btree::dedup_sorted_iter::DedupSortedIter")
            []
            [ K; V; I ].
        
        (*     type Item = (K, V); *)
        Definition _Item (K V I : Ty.t) : Ty.t := Ty.tuple [ K; V ].
        
        (*
            fn next(&mut self) -> Option<(K, V)> {
                loop {
                    let next = match self.iter.next() {
                        Some(next) => next,
                        None => return None,
                    };
        
                    let peeked = match self.iter.peek() {
                        Some(peeked) => peeked,
                        None => return Some(next),
                    };
        
                    if next.0 != peeked.0 {
                        return Some(next);
                    }
                }
            }
        *)
        Definition next (K V I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self K V I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.never_to_any (|
                    M.read (|
                      M.loop (|
                        ltac:(M.monadic
                          (let~ next :=
                            M.copy (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::iter::adapters::peekable::Peekable")
                                        []
                                        [ I ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "alloc::collections::btree::dedup_sorted_iter::DedupSortedIter",
                                        "iter"
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let next := M.copy (| γ0_0 |) in
                                      next));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.StructTuple "core::option::Option::None" []
                                            |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)
                            |) in
                          let~ peeked :=
                            M.copy (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::iter::adapters::peekable::Peekable")
                                        []
                                        [ I ],
                                      "peek",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "alloc::collections::btree::dedup_sorted_iter::DedupSortedIter",
                                        "iter"
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let peeked := M.copy (| γ0_0 |) in
                                      peeked));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.StructTuple
                                                "core::option::Option::Some"
                                                [ M.read (| next |) ]
                                            |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            K,
                                            [ K ],
                                            "ne",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_tuple_field (| next, 0 |);
                                            M.SubPointer.get_tuple_field (|
                                              M.read (| peeked |),
                                              0
                                            |)
                                          ]
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [ M.read (| next |) ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)))
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (K V I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self K V I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("Item", InstanceField.Ty (_Item K V I)); ("next", InstanceField.Method (next K V I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_cmp_Eq_K_where_core_iter_traits_iterator_Iterator_I_for_alloc_collections_btree_dedup_sorted_iter_DedupSortedIter_K_V_I.
    End dedup_sorted_iter.
  End btree.
End collections.
