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

Module collections.
  Module vec_deque.
    Module spec_from_iter.
      (* Trait *)
      (* Empty module 'SpecFromIter' *)
      
      Module Impl_alloc_collections_vec_deque_spec_from_iter_SpecFromIter_where_core_iter_traits_iterator_Iterator_I_T_I_for_alloc_collections_vec_deque_VecDeque_T_alloc_alloc_Global.
        Definition Self (T I : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::vec_deque::VecDeque")
            []
            [ T; Ty.path "alloc::alloc::Global" ].
        
        (*
            default fn spec_from_iter(iterator: I) -> Self {
                // Since converting is O(1) now, just re-use the `Vec` logic for
                // anything where we can't do something extra-special for `VecDeque`,
                // especially as that could save us some monomorphization work
                // if one uses the same iterators (like slice ones) with both.
                crate::vec::Vec::from_iter(iterator).into()
            }
        *)
        Definition spec_from_iter
            (T I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T I in
          match ε, τ, α with
          | [], [], [ iterator ] =>
            ltac:(M.monadic
              (let iterator := M.alloc (| iterator |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::Into",
                  Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                  [
                    Ty.apply
                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                      []
                      [ T; Ty.path "alloc::alloc::Global" ]
                  ],
                  "into",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::FromIterator",
                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                      [ T ],
                      "from_iter",
                      [ I ]
                    |),
                    [ M.read (| iterator |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T I : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_from_iter::SpecFromIter"
            (Self T I)
            (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
            (* Instance *) [ ("spec_from_iter", InstanceField.Method (spec_from_iter T I)) ].
      End Impl_alloc_collections_vec_deque_spec_from_iter_SpecFromIter_where_core_iter_traits_iterator_Iterator_I_T_I_for_alloc_collections_vec_deque_VecDeque_T_alloc_alloc_Global.
      
      Module Impl_alloc_collections_vec_deque_spec_from_iter_SpecFromIter_T_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_collections_vec_deque_VecDeque_T_alloc_alloc_Global.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::vec_deque::VecDeque")
            []
            [ T; Ty.path "alloc::alloc::Global" ].
        
        (*
            fn spec_from_iter(iterator: crate::vec::IntoIter<T>) -> Self {
                iterator.into_vecdeque()
            }
        *)
        Definition spec_from_iter
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ iterator ] =>
            ltac:(M.monadic
              (let iterator := M.alloc (| iterator |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::into_iter::IntoIter")
                    []
                    [ T; Ty.path "alloc::alloc::Global" ],
                  "into_vecdeque",
                  []
                |),
                [ M.read (| iterator |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_from_iter::SpecFromIter"
            (Self T)
            (* Trait polymorphic types *)
            [
              (* T *) T;
              (* I *)
              Ty.apply
                (Ty.path "alloc::vec::into_iter::IntoIter")
                []
                [ T; Ty.path "alloc::alloc::Global" ]
            ]
            (* Instance *) [ ("spec_from_iter", InstanceField.Method (spec_from_iter T)) ].
      End Impl_alloc_collections_vec_deque_spec_from_iter_SpecFromIter_T_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_collections_vec_deque_VecDeque_T_alloc_alloc_Global.
      
      Module Impl_alloc_collections_vec_deque_spec_from_iter_SpecFromIter_T_alloc_collections_vec_deque_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_collections_vec_deque_VecDeque_T_alloc_alloc_Global.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "alloc::collections::vec_deque::VecDeque")
            []
            [ T; Ty.path "alloc::alloc::Global" ].
        
        (*
            fn spec_from_iter(iterator: IntoIter<T>) -> Self {
                iterator.into_vecdeque()
            }
        *)
        Definition spec_from_iter
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ iterator ] =>
            ltac:(M.monadic
              (let iterator := M.alloc (| iterator |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter")
                    []
                    [ T; Ty.path "alloc::alloc::Global" ],
                  "into_vecdeque",
                  []
                |),
                [ M.read (| iterator |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_from_iter::SpecFromIter"
            (Self T)
            (* Trait polymorphic types *)
            [
              (* T *) T;
              (* I *)
              Ty.apply
                (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter")
                []
                [ T; Ty.path "alloc::alloc::Global" ]
            ]
            (* Instance *) [ ("spec_from_iter", InstanceField.Method (spec_from_iter T)) ].
      End Impl_alloc_collections_vec_deque_spec_from_iter_SpecFromIter_T_alloc_collections_vec_deque_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_collections_vec_deque_VecDeque_T_alloc_alloc_Global.
    End spec_from_iter.
  End vec_deque.
End collections.
