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

Module collections.
  Module vec_deque.
    Module spec_extend.
      (* Trait *)
      (* Empty module 'SpecExtend' *)
      
      Module Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_iter_traits_iterator_Iterator_I_T_I_for_alloc_collections_vec_deque_VecDeque_T_A.
        Definition Self (T I A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
        
        (*
            default fn spec_extend(&mut self, mut iter: I) {
                // This function should be the moral equivalent of:
                //
                // for item in iter {
                //     self.push_back(item);
                // }
        
                while let Some(element) = iter.next() {
                    let (lower, _) = iter.size_hint();
                    self.reserve(lower.saturating_add(1));
        
                    // SAFETY: We just reserved space for at least one element.
                    unsafe { self.push_unchecked(element) };
        
                    // Inner loop to avoid repeatedly calling `reserve`.
                    while self.len < self.capacity() {
                        let Some(element) = iter.next() else {
                            return;
                        };
                        // SAFETY: The loop condition guarantees that `self.len() < self.capacity()`.
                        unsafe { self.push_unchecked(element) };
                    }
                }
            }
        *)
        Definition spec_extend
            (T I A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T I A in
          match ε, τ, α with
          | [], [], [ self; iter ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let iter := M.alloc (| iter |) in
              M.read (|
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    I,
                                    [],
                                    "next",
                                    []
                                  |),
                                  [ iter ]
                                |)
                              |) in
                            let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let element := M.copy (| γ0_0 |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    I,
                                    [],
                                    "size_hint",
                                    []
                                  |),
                                  [ 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 lower := M.copy (| γ0_0 |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                                              []
                                              [ T; A ],
                                            "reserve",
                                            []
                                          |),
                                          [
                                            M.read (| self |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "usize",
                                                "saturating_add",
                                                []
                                              |),
                                              [
                                                M.read (| lower |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                                              []
                                              [ T; A ],
                                            "push_unchecked",
                                            []
                                          |),
                                          [ M.read (| self |); M.read (| element |) ]
                                        |)
                                      |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      BinOp.lt (|
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "alloc::collections::vec_deque::VecDeque",
                                                            "len"
                                                          |)
                                                        |),
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "alloc::collections::vec_deque::VecDeque")
                                                              []
                                                              [ T; A ],
                                                            "capacity",
                                                            []
                                                          |),
                                                          [ M.read (| self |) ]
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::iter::traits::iterator::Iterator",
                                                        I,
                                                        [],
                                                        "next",
                                                        []
                                                      |),
                                                      [ iter ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::option::Option::Some",
                                                            0
                                                          |) in
                                                        let element := M.copy (| γ0_0 |) in
                                                        let~ _ :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "alloc::collections::vec_deque::VecDeque")
                                                                  []
                                                                  [ T; A ],
                                                                "push_unchecked",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (| element |)
                                                              ]
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.alloc (|
                                                  M.never_to_any (|
                                                    M.read (|
                                                      let~ _ :=
                                                        M.alloc (|
                                                          M.never_to_any (|
                                                            M.read (| M.break (||) |)
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)
                                                    |)
                                                  |)
                                                |)))
                                          ]
                                        |)))
                                    |)))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T I A : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_extend::SpecExtend"
            (Self T I A)
            (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
            (* Instance *) [ ("spec_extend", InstanceField.Method (spec_extend T I A)) ].
      End Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_iter_traits_iterator_Iterator_I_T_I_for_alloc_collections_vec_deque_VecDeque_T_A.
      
      Module Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_iter_traits_marker_TrustedLen_I_T_I_for_alloc_collections_vec_deque_VecDeque_T_A.
        Definition Self (T I A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
        
        (*
            default fn spec_extend(&mut self, iter: I) {
                // This is the case for a TrustedLen iterator.
                let (low, high) = iter.size_hint();
                if let Some(additional) = high {
                    debug_assert_eq!(
                        low,
                        additional,
                        "TrustedLen iterator's size hint is not exact: {:?}",
                        (low, high)
                    );
                    self.reserve(additional);
        
                    let written = unsafe {
                        self.write_iter_wrapping(self.to_physical_idx(self.len), iter, additional)
                    };
        
                    debug_assert_eq!(
                        additional, written,
                        "The number of items written to VecDeque doesn't match the TrustedLen size hint"
                    );
                } else {
                    // Per TrustedLen contract a `None` upper bound means that the iterator length
                    // truly exceeds usize::MAX, which would eventually lead to a capacity overflow anyway.
                    // Since the other branch already panics eagerly (via `reserve()`) we do the same here.
                    // This avoids additional codegen for a fallback code path which would eventually
                    // panic anyway.
                    panic!("capacity overflow");
                }
            }
        *)
        Definition spec_extend
            (T I A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T I A in
          match ε, τ, α with
          | [], [], [ self; iter ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let iter := M.alloc (| iter |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        I,
                        [],
                        "size_hint",
                        []
                      |),
                      [ 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 low := M.copy (| γ0_0 |) in
                        let high := M.copy (| γ0_1 |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := high in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let additional := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [ low; additional ] |),
                                              [
                                                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 left_val := M.copy (| γ0_0 |) in
                                                    let right_val := M.copy (| γ0_1 |) in
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  UnOp.not (|
                                                                    BinOp.eq (|
                                                                      M.read (|
                                                                        M.read (| left_val |)
                                                                      |),
                                                                      M.read (|
                                                                        M.read (| right_val |)
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  let~ kind :=
                                                                    M.alloc (|
                                                                      Value.StructTuple
                                                                        "core::panicking::AssertKind::Eq"
                                                                        []
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_function (|
                                                                        "core::panicking::assert_failed",
                                                                        [
                                                                          Ty.path "usize";
                                                                          Ty.path "usize"
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.read (| kind |);
                                                                        M.read (| left_val |);
                                                                        M.read (| right_val |);
                                                                        Value.StructTuple
                                                                          "core::option::Option::Some"
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::Arguments",
                                                                                "new_v1",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.alloc (|
                                                                                  Value.Array
                                                                                    [
                                                                                      M.read (|
                                                                                        Value.String
                                                                                          "TrustedLen iterator's size hint is not exact: "
                                                                                      |)
                                                                                    ]
                                                                                |);
                                                                                M.alloc (|
                                                                                  Value.Array
                                                                                    [
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.path
                                                                                            "core::fmt::rt::Argument",
                                                                                          "new_debug",
                                                                                          [
                                                                                            Ty.tuple
                                                                                              [
                                                                                                Ty.path
                                                                                                  "usize";
                                                                                                Ty.apply
                                                                                                  (Ty.path
                                                                                                    "core::option::Option")
                                                                                                  []
                                                                                                  [
                                                                                                    Ty.path
                                                                                                      "usize"
                                                                                                  ]
                                                                                              ]
                                                                                          ]
                                                                                        |),
                                                                                        [
                                                                                          M.alloc (|
                                                                                            Value.Tuple
                                                                                              [
                                                                                                M.read (|
                                                                                                  low
                                                                                                |);
                                                                                                M.read (|
                                                                                                  high
                                                                                                |)
                                                                                              ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                      ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "reserve",
                                        []
                                      |),
                                      [ M.read (| self |); M.read (| additional |) ]
                                    |)
                                  |) in
                                let~ written :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "write_iter_wrapping",
                                        [ I ]
                                      |),
                                      [
                                        M.read (| self |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                                              []
                                              [ T; A ],
                                            "to_physical_idx",
                                            []
                                          |),
                                          [
                                            M.read (| self |);
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "alloc::collections::vec_deque::VecDeque",
                                                "len"
                                              |)
                                            |)
                                          ]
                                        |);
                                        M.read (| iter |);
                                        M.read (| additional |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [ additional; written ] |),
                                              [
                                                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 left_val := M.copy (| γ0_0 |) in
                                                    let right_val := M.copy (| γ0_1 |) in
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  UnOp.not (|
                                                                    BinOp.eq (|
                                                                      M.read (|
                                                                        M.read (| left_val |)
                                                                      |),
                                                                      M.read (|
                                                                        M.read (| right_val |)
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (|
                                                                  let~ kind :=
                                                                    M.alloc (|
                                                                      Value.StructTuple
                                                                        "core::panicking::AssertKind::Eq"
                                                                        []
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_function (|
                                                                        "core::panicking::assert_failed",
                                                                        [
                                                                          Ty.path "usize";
                                                                          Ty.path "usize"
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.read (| kind |);
                                                                        M.read (| left_val |);
                                                                        M.read (| right_val |);
                                                                        Value.StructTuple
                                                                          "core::option::Option::Some"
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::Arguments",
                                                                                "new_const",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.alloc (|
                                                                                  Value.Array
                                                                                    [
                                                                                      M.read (|
                                                                                        Value.String
                                                                                          "The number of items written to VecDeque doesn't match the TrustedLen size hint"
                                                                                      |)
                                                                                    ]
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                      ]
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic_fmt", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::Arguments",
                                            "new_const",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array
                                                [ M.read (| Value.String "capacity overflow" |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T I A : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_extend::SpecExtend"
            (Self T I A)
            (* Trait polymorphic types *) [ (* T *) T; (* I *) I ]
            (* Instance *) [ ("spec_extend", InstanceField.Method (spec_extend T I A)) ].
      End Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_iter_traits_marker_TrustedLen_I_T_I_for_alloc_collections_vec_deque_VecDeque_T_A.
      
      Module Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_T_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_collections_vec_deque_VecDeque_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
        
        (*
            fn spec_extend(&mut self, mut iterator: vec::IntoIter<T>) {
                let slice = iterator.as_slice();
                self.reserve(slice.len());
        
                unsafe {
                    self.copy_slice(self.to_physical_idx(self.len), slice);
                    self.len += slice.len();
                }
                iterator.forget_remaining_elements();
            }
        *)
        Definition spec_extend
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self; iterator ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let iterator := M.alloc (| iterator |) in
              M.read (|
                let~ slice :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::into_iter::IntoIter")
                          []
                          [ T; Ty.path "alloc::alloc::Global" ],
                        "as_slice",
                        []
                      |),
                      [ iterator ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                        "reserve",
                        []
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "len",
                            []
                          |),
                          [ M.read (| slice |) ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "copy_slice",
                          []
                        |),
                        [
                          M.read (| self |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::vec_deque::VecDeque")
                                []
                                [ T; A ],
                              "to_physical_idx",
                              []
                            |),
                            [
                              M.read (| self |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::VecDeque",
                                  "len"
                                |)
                              |)
                            ]
                          |);
                          M.read (| slice |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    let β :=
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::vec_deque::VecDeque",
                        "len"
                      |) in
                    M.write (|
                      β,
                      BinOp.Wrap.add (|
                        M.read (| β |),
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "len",
                            []
                          |),
                          [ M.read (| slice |) ]
                        |)
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::into_iter::IntoIter")
                          []
                          [ T; Ty.path "alloc::alloc::Global" ],
                        "forget_remaining_elements",
                        []
                      |),
                      [ iterator ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_extend::SpecExtend"
            (Self T A)
            (* Trait polymorphic types *)
            [
              (* T *) T;
              (* I *)
              Ty.apply
                (Ty.path "alloc::vec::into_iter::IntoIter")
                []
                [ T; Ty.path "alloc::alloc::Global" ]
            ]
            (* Instance *) [ ("spec_extend", InstanceField.Method (spec_extend T A)) ].
      End Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_T_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global_for_alloc_collections_vec_deque_VecDeque_T_A.
      
      Module Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Copy_T_ref__T_I_for_alloc_collections_vec_deque_VecDeque_T_A.
        Definition Self (T I A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
        
        (*
            default fn spec_extend(&mut self, iterator: I) {
                self.spec_extend(iterator.copied())
            }
        *)
        Definition spec_extend
            (T I A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T I A in
          match ε, τ, α with
          | [], [], [ self; iterator ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let iterator := M.alloc (| iterator |) in
              M.call_closure (|
                M.get_trait_method (|
                  "alloc::collections::vec_deque::spec_extend::SpecExtend",
                  Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                  [ T; Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ] ],
                  "spec_extend",
                  []
                |),
                [
                  M.read (| self |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "copied",
                      [ T ]
                    |),
                    [ M.read (| iterator |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T I A : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_extend::SpecExtend"
            (Self T I A)
            (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "&") [] [ T ]; (* I *) I ]
            (* Instance *) [ ("spec_extend", InstanceField.Method (spec_extend T I A)) ].
      End Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Copy_T_ref__T_I_for_alloc_collections_vec_deque_VecDeque_T_A.
      
      Module Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_marker_Copy_T_ref__T_core_slice_iter_Iter_T_for_alloc_collections_vec_deque_VecDeque_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
        
        (*
            fn spec_extend(&mut self, iterator: slice::Iter<'a, T>) {
                let slice = iterator.as_slice();
                self.reserve(slice.len());
        
                unsafe {
                    self.copy_slice(self.to_physical_idx(self.len), slice);
                    self.len += slice.len();
                }
            }
        *)
        Definition spec_extend
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self; iterator ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let iterator := M.alloc (| iterator |) in
              M.read (|
                let~ slice :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                        "as_slice",
                        []
                      |),
                      [ iterator ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                        "reserve",
                        []
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ T ],
                            "len",
                            []
                          |),
                          [ M.read (| slice |) ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                        "copy_slice",
                        []
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                              []
                              [ T; A ],
                            "to_physical_idx",
                            []
                          |),
                          [
                            M.read (| self |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::VecDeque",
                                "len"
                              |)
                            |)
                          ]
                        |);
                        M.read (| slice |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  let β :=
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::collections::vec_deque::VecDeque",
                      "len"
                    |) in
                  M.write (|
                    β,
                    BinOp.Wrap.add (|
                      M.read (| β |),
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ T ],
                          "len",
                          []
                        |),
                        [ M.read (| slice |) ]
                      |)
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "alloc::collections::vec_deque::spec_extend::SpecExtend"
            (Self T A)
            (* Trait polymorphic types *)
            [
              (* T *) Ty.apply (Ty.path "&") [] [ T ];
              (* I *) Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ]
            ]
            (* Instance *) [ ("spec_extend", InstanceField.Method (spec_extend T A)) ].
      End Impl_alloc_collections_vec_deque_spec_extend_SpecExtend_where_core_alloc_Allocator_A_where_core_marker_Copy_T_ref__T_core_slice_iter_Iter_T_for_alloc_collections_vec_deque_VecDeque_T_A.
    End spec_extend.
  End vec_deque.
End collections.
