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

Module vec.
  Module spec_from_iter.
    (* Trait *)
    (* Empty module 'SpecFromIter' *)
    
    Module Impl_alloc_vec_spec_from_iter_SpecFromIter_where_core_iter_traits_iterator_Iterator_I_T_I_for_alloc_vec_Vec_T_alloc_alloc_Global.
      Definition Self (T I : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ].
      
      (*
          default fn from_iter(iterator: I) -> Self {
              SpecFromIterNested::from_iter(iterator)
          }
      *)
      Definition 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 (|
                "alloc::vec::spec_from_iter_nested::SpecFromIterNested",
                Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                [ T; I ],
                "from_iter",
                []
              |),
              [ M.read (| iterator |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T I : Ty.t),
        M.IsTraitInstance
          "alloc::vec::spec_from_iter::SpecFromIter"
          (Self T I)
          (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
          (* Instance *) [ ("from_iter", InstanceField.Method (from_iter T I)) ].
    End Impl_alloc_vec_spec_from_iter_SpecFromIter_where_core_iter_traits_iterator_Iterator_I_T_I_for_alloc_vec_Vec_T_alloc_alloc_Global.
    
    Module Impl_alloc_vec_spec_from_iter_SpecFromIter_T_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_vec_Vec_T_alloc_alloc_Global.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ].
      
      (*
          fn from_iter(iterator: IntoIter<T>) -> Self {
              // A common case is passing a vector into a function which immediately
              // re-collects into a vector. We can short circuit this if the IntoIter
              // has not been advanced at all.
              // When it has been advanced We can also reuse the memory and move the data to the front.
              // But we only do so when the resulting Vec wouldn't have more unused capacity
              // than creating it through the generic FromIterator implementation would. That limitation
              // is not strictly necessary as Vec's allocation behavior is intentionally unspecified.
              // But it is a conservative choice.
              let has_advanced = iterator.buf != iterator.ptr;
              if !has_advanced || iterator.len() >= iterator.cap / 2 {
                  unsafe {
                      let it = ManuallyDrop::new(iterator);
                      if has_advanced {
                          ptr::copy(it.ptr.as_ptr(), it.buf.as_ptr(), it.len());
                      }
                      return Vec::from_parts(it.buf, it.len(), it.cap);
                  }
              }
      
              let mut vec = Vec::new();
              // must delegate to spec_extend() since extend() itself delegates
              // to spec_from for empty Vecs
              vec.spec_extend(iterator);
              vec
          }
      *)
      Definition 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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ has_advanced :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                          [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ],
                          "ne",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            iterator,
                            "alloc::vec::into_iter::IntoIter",
                            "buf"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            iterator,
                            "alloc::vec::into_iter::IntoIter",
                            "ptr"
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.or (|
                                    UnOp.not (| M.read (| has_advanced |) |),
                                    ltac:(M.monadic
                                      (BinOp.ge (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::exact_size::ExactSizeIterator",
                                            Ty.apply
                                              (Ty.path "alloc::vec::into_iter::IntoIter")
                                              []
                                              [ T; Ty.path "alloc::alloc::Global" ],
                                            [],
                                            "len",
                                            []
                                          |),
                                          [ iterator ]
                                        |),
                                        BinOp.Wrap.div (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              iterator,
                                              "alloc::vec::into_iter::IntoIter",
                                              "cap"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.Usize 2
                                        |)
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ it :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::vec::into_iter::IntoIter")
                                                []
                                                [ T; Ty.path "alloc::alloc::Global" ]
                                            ],
                                          "new",
                                          []
                                        |),
                                        [ M.read (| iterator |) ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ := M.use has_advanced in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::intrinsics::copy",
                                                    [ T ]
                                                  |),
                                                  [
                                                    (* MutToConstPointer *)
                                                    M.pointer_coercion
                                                      (M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::ptr::non_null::NonNull")
                                                            []
                                                            [ T ],
                                                          "as_ptr",
                                                          []
                                                        |),
                                                        [
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::deref::Deref",
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::mem::manually_drop::ManuallyDrop")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "alloc::vec::into_iter::IntoIter")
                                                                        []
                                                                        [
                                                                          T;
                                                                          Ty.path
                                                                            "alloc::alloc::Global"
                                                                        ]
                                                                    ],
                                                                  [],
                                                                  "deref",
                                                                  []
                                                                |),
                                                                [ it ]
                                                              |),
                                                              "alloc::vec::into_iter::IntoIter",
                                                              "ptr"
                                                            |)
                                                          |)
                                                        ]
                                                      |));
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "core::ptr::non_null::NonNull")
                                                          []
                                                          [ T ],
                                                        "as_ptr",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::deref::Deref",
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "core::mem::manually_drop::ManuallyDrop")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "alloc::vec::into_iter::IntoIter")
                                                                      []
                                                                      [
                                                                        T;
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ]
                                                                  ],
                                                                [],
                                                                "deref",
                                                                []
                                                              |),
                                                              [ it ]
                                                            |),
                                                            "alloc::vec::into_iter::IntoIter",
                                                            "buf"
                                                          |)
                                                        |)
                                                      ]
                                                    |);
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::iter::traits::exact_size::ExactSizeIterator",
                                                        Ty.apply
                                                          (Ty.path
                                                            "alloc::vec::into_iter::IntoIter")
                                                          []
                                                          [ T; Ty.path "alloc::alloc::Global" ],
                                                        [],
                                                        "len",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::deref::Deref",
                                                            Ty.apply
                                                              (Ty.path
                                                                "core::mem::manually_drop::ManuallyDrop")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "alloc::vec::into_iter::IntoIter")
                                                                  []
                                                                  [
                                                                    T;
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ]
                                                              ],
                                                            [],
                                                            "deref",
                                                            []
                                                          |),
                                                          [ it ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.alloc (| Value.Tuple [] |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [ T; Ty.path "alloc::alloc::Global" ],
                                        "from_parts",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.apply
                                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::into_iter::IntoIter")
                                                      []
                                                      [ T; Ty.path "alloc::alloc::Global" ]
                                                  ],
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [ it ]
                                            |),
                                            "alloc::vec::into_iter::IntoIter",
                                            "buf"
                                          |)
                                        |);
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::exact_size::ExactSizeIterator",
                                            Ty.apply
                                              (Ty.path "alloc::vec::into_iter::IntoIter")
                                              []
                                              [ T; Ty.path "alloc::alloc::Global" ],
                                            [],
                                            "len",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.apply
                                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::into_iter::IntoIter")
                                                      []
                                                      [ T; Ty.path "alloc::alloc::Global" ]
                                                  ],
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [ it ]
                                            |)
                                          ]
                                        |);
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.apply
                                                  (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::into_iter::IntoIter")
                                                      []
                                                      [ T; Ty.path "alloc::alloc::Global" ]
                                                  ],
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [ it ]
                                            |),
                                            "alloc::vec::into_iter::IntoIter",
                                            "cap"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ vec :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ T; Ty.path "alloc::alloc::Global" ],
                          "new",
                          []
                        |),
                        []
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "alloc::vec::spec_extend::SpecExtend",
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ T; Ty.path "alloc::alloc::Global" ],
                          [
                            T;
                            Ty.apply
                              (Ty.path "alloc::vec::into_iter::IntoIter")
                              []
                              [ T; Ty.path "alloc::alloc::Global" ]
                          ],
                          "spec_extend",
                          []
                        |),
                        [ vec; M.read (| iterator |) ]
                      |)
                    |) in
                  vec
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "alloc::vec::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 *) [ ("from_iter", InstanceField.Method (from_iter T)) ].
    End Impl_alloc_vec_spec_from_iter_SpecFromIter_T_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_vec_Vec_T_alloc_alloc_Global.
  End spec_from_iter.
End vec.
