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

Module collections.
  Module vec_deque.
    Module drain.
      (* StructRecord
        {
          name := "Drain";
          const_params := [];
          ty_params := [ "T"; "A" ];
          fields :=
            [
              ("deque",
                Ty.apply
                  (Ty.path "core::ptr::non_null::NonNull")
                  []
                  [ Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ] ]);
              ("drain_len", Ty.path "usize");
              ("idx", Ty.path "usize");
              ("new_len", Ty.path "usize");
              ("remaining", Ty.path "usize");
              ("_marker",
                Ty.apply
                  (Ty.path "core::marker::PhantomData")
                  []
                  [ Ty.apply (Ty.path "&") [] [ T ] ])
            ];
        } *)
      
      Module Impl_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        (*
            pub(super) unsafe fn new(
                deque: &'a mut VecDeque<T, A>,
                drain_start: usize,
                drain_len: usize,
            ) -> Self {
                let orig_len = mem::replace(&mut deque.len, drain_start);
                let new_len = orig_len - drain_len;
                Drain {
                    deque: NonNull::from(deque),
                    drain_len,
                    idx: drain_start,
                    new_len,
                    remaining: drain_len,
                    _marker: PhantomData,
                }
            }
        *)
        Definition new (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ deque; drain_start; drain_len ] =>
            ltac:(M.monadic
              (let deque := M.alloc (| deque |) in
              let drain_start := M.alloc (| drain_start |) in
              let drain_len := M.alloc (| drain_len |) in
              M.read (|
                let~ orig_len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::mem::replace", [ Ty.path "usize" ] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| deque |),
                          "alloc::collections::vec_deque::VecDeque",
                          "len"
                        |);
                        M.read (| drain_start |)
                      ]
                    |)
                  |) in
                let~ new_len :=
                  M.alloc (|
                    BinOp.Wrap.sub (| M.read (| orig_len |), M.read (| drain_len |) |)
                  |) in
                M.alloc (|
                  Value.StructRecord
                    "alloc::collections::vec_deque::drain::Drain"
                    [
                      ("deque",
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.apply
                              (Ty.path "core::ptr::non_null::NonNull")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::vec_deque::VecDeque")
                                  []
                                  [ T; A ]
                              ],
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloc::collections::vec_deque::VecDeque")
                                    []
                                    [ T; A ]
                                ]
                            ],
                            "from",
                            []
                          |),
                          [ M.read (| deque |) ]
                        |));
                      ("drain_len", M.read (| drain_len |));
                      ("idx", M.read (| drain_start |));
                      ("new_len", M.read (| new_len |));
                      ("remaining", M.read (| drain_len |));
                      ("_marker", Value.StructTuple "core::marker::PhantomData" [])
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (T A : Ty.t),
          M.IsAssociatedFunction (Self T A) "new" (new T A).
        
        (*
            unsafe fn as_slices(&self) -> ( *mut [T], *mut [T]) {
                unsafe {
                    let deque = self.deque.as_ref();
        
                    // We know that `self.idx + self.remaining <= deque.len <= usize::MAX`, so this won't overflow.
                    let logical_remaining_range = self.idx..self.idx + self.remaining;
        
                    // SAFETY: `logical_remaining_range` represents the
                    // range into the logical buffer of elements that
                    // haven't been drained yet, so they're all initialized,
                    // and `slice::range(start..end, end) == start..end`,
                    // so the preconditions for `slice_ranges` are met.
                    let (a_range, b_range) =
                        deque.slice_ranges(logical_remaining_range.clone(), logical_remaining_range.end);
                    (deque.buffer_range(a_range), deque.buffer_range(b_range))
                }
            }
        *)
        Definition as_slices
            (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ deque :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ptr::non_null::NonNull")
                          []
                          [ Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ]
                          ],
                        "as_ref",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::drain::Drain",
                          "deque"
                        |)
                      ]
                    |)
                  |) in
                let~ logical_remaining_range :=
                  M.alloc (|
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::collections::vec_deque::drain::Drain",
                              "idx"
                            |)
                          |));
                        ("end_",
                          BinOp.Wrap.add (|
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::drain::Drain",
                                "idx"
                              |)
                            |),
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::drain::Drain",
                                "remaining"
                              |)
                            |)
                          |))
                      ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                        "slice_ranges",
                        [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ]
                      |),
                      [
                        M.read (| deque |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::clone::Clone",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [],
                            "clone",
                            []
                          |),
                          [ logical_remaining_range ]
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            logical_remaining_range,
                            "core::ops::range::Range",
                            "end"
                          |)
                        |)
                      ]
                    |)
                  |),
                  [
                    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 a_range := M.copy (| γ0_0 |) in
                        let b_range := M.copy (| γ0_1 |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::vec_deque::VecDeque")
                                    []
                                    [ T; A ],
                                  "buffer_range",
                                  []
                                |),
                                [ M.read (| deque |); M.read (| a_range |) ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::vec_deque::VecDeque")
                                    []
                                    [ T; A ],
                                  "buffer_range",
                                  []
                                |),
                                [ M.read (| deque |); M.read (| b_range |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_as_slices :
          forall (T A : Ty.t),
          M.IsAssociatedFunction (Self T A) "as_slices" (as_slices T A).
      End Impl_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_tuple("Drain")
                    .field(&self.drain_len)
                    .field(&self.idx)
                    .field(&self.new_len)
                    .field(&self.remaining)
                    .finish()
            }
        *)
        Definition fmt (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; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::builders::DebugTuple",
                  "finish",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::builders::DebugTuple",
                      "field",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::builders::DebugTuple",
                          "field",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::builders::DebugTuple",
                              "field",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::builders::DebugTuple",
                                  "field",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::Formatter",
                                        "debug_tuple",
                                        []
                                      |),
                                      [ M.read (| f |); M.read (| Value.String "Drain" |) ]
                                    |)
                                  |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::collections::vec_deque::drain::Drain",
                                    "drain_len"
                                  |)
                                ]
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::drain::Drain",
                                "idx"
                              |)
                            ]
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::collections::vec_deque::drain::Drain",
                            "new_len"
                          |)
                        ]
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::vec_deque::drain::Drain",
                        "remaining"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt T A)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_marker_Sync_where_core_marker_Sync_T_where_core_alloc_Allocator_A_where_core_marker_Sync_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::marker::Sync"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Sync_where_core_marker_Sync_T_where_core_alloc_Allocator_A_where_core_marker_Sync_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_marker_Send_where_core_marker_Send_T_where_core_alloc_Allocator_A_where_core_marker_Send_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::marker::Send"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Send_where_core_marker_Send_T_where_core_alloc_Allocator_A_where_core_marker_Send_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_ops_drop_Drop_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        (*
            fn drop(&mut self) {
                struct DropGuard<'r, 'a, T, A: Allocator>(&'r mut Drain<'a, T, A>);
        
                let guard = DropGuard(self);
        
                if mem::needs_drop::<T>() && guard.0.remaining != 0 {
                    unsafe {
                        // SAFETY: We just checked that `self.remaining != 0`.
                        let (front, back) = guard.0.as_slices();
                        // since idx is a logical index, we don't need to worry about wrapping.
                        guard.0.idx += front.len();
                        guard.0.remaining -= front.len();
                        ptr::drop_in_place(front);
                        guard.0.remaining = 0;
                        ptr::drop_in_place(back);
                    }
                }
        
                // Dropping `guard` handles moving the remaining elements into place.
                impl<'r, 'a, T, A: Allocator> Drop for DropGuard<'r, 'a, T, A> {
                    #[inline]
                    fn drop(&mut self) {
                        if mem::needs_drop::<T>() && self.0.remaining != 0 {
                            unsafe {
                                // SAFETY: We just checked that `self.remaining != 0`.
                                let (front, back) = self.0.as_slices();
                                ptr::drop_in_place(front);
                                ptr::drop_in_place(back);
                            }
                        }
        
                        let source_deque = unsafe { self.0.deque.as_mut() };
        
                        let drain_len = self.0.drain_len;
                        let new_len = self.0.new_len;
        
                        if T::IS_ZST {
                            // no need to copy around any memory if T is a ZST
                            source_deque.len = new_len;
                            return;
                        }
        
                        let head_len = source_deque.len; // #elements in front of the drain
                        let tail_len = new_len - head_len; // #elements behind the drain
        
                        // Next, we will fill the hole left by the drain with as few writes as possible.
                        // The code below handles the following control flow and reduces the amount of
                        // branches under the assumption that `head_len == 0 || tail_len == 0`, i.e.
                        // draining at the front or at the back of the dequeue is especially common.
                        //
                        // H = "head index" = `deque.head`
                        // h = elements in front of the drain
                        // d = elements in the drain
                        // t = elements behind the drain
                        //
                        // Note that the buffer may wrap at any point and the wrapping is handled by
                        // `wrap_copy` and `to_physical_idx`.
                        //
                        // Case 1: if `head_len == 0 && tail_len == 0`
                        // Everything was drained, reset the head index back to 0.
                        //             H
                        // [ . . . . . d d d d . . . . . ]
                        //   H
                        // [ . . . . . . . . . . . . . . ]
                        //
                        // Case 2: else if `tail_len == 0`
                        // Don't move data or the head index.
                        //         H
                        // [ . . . h h h h d d d d . . . ]
                        //         H
                        // [ . . . h h h h . . . . . . . ]
                        //
                        // Case 3: else if `head_len == 0`
                        // Don't move data, but move the head index.
                        //         H
                        // [ . . . d d d d t t t t . . . ]
                        //                 H
                        // [ . . . . . . . t t t t . . . ]
                        //
                        // Case 4: else if `tail_len <= head_len`
                        // Move data, but not the head index.
                        //       H
                        // [ . . h h h h d d d d t t . . ]
                        //       H
                        // [ . . h h h h t t . . . . . . ]
                        //
                        // Case 5: else
                        // Move data and the head index.
                        //       H
                        // [ . . h h d d d d t t t t . . ]
                        //               H
                        // [ . . . . . . h h t t t t . . ]
        
                        // When draining at the front (`.drain(..n)`) or at the back (`.drain(n..)`),
                        // we don't need to copy any data. The number of elements copied would be 0.
                        if head_len != 0 && tail_len != 0 {
                            join_head_and_tail_wrapping(source_deque, drain_len, head_len, tail_len);
                            // Marking this function as cold helps LLVM to eliminate it entirely if
                            // this branch is never taken.
                            // We use `#[cold]` instead of `#[inline(never)]`, because inlining this
                            // function into the general case (`.drain(n..m)`) is fine.
                            // See `tests/codegen/vecdeque-drain.rs` for a test.
                            #[cold]
                            fn join_head_and_tail_wrapping<T, A: Allocator>(
                                source_deque: &mut VecDeque<T, A>,
                                drain_len: usize,
                                head_len: usize,
                                tail_len: usize,
                            ) {
                                // Pick whether to move the head or the tail here.
                                let (src, dst, len);
                                if head_len < tail_len {
                                    src = source_deque.head;
                                    dst = source_deque.to_physical_idx(drain_len);
                                    len = head_len;
                                } else {
                                    src = source_deque.to_physical_idx(head_len + drain_len);
                                    dst = source_deque.to_physical_idx(head_len);
                                    len = tail_len;
                                };
        
                                unsafe {
                                    source_deque.wrap_copy(src, dst, len);
                                }
                            }
                        }
        
                        if new_len == 0 {
                            // Special case: If the entire dequeue was drained, reset the head back to 0,
                            // like `.clear()` does.
                            source_deque.head = 0;
                        } else if head_len < tail_len {
                            // If we moved the head above, then we need to adjust the head index here.
                            source_deque.head = source_deque.to_physical_idx(drain_len);
                        }
                        source_deque.len = new_len;
                    }
                }
            }
        *)
        Definition drop (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ guard :=
                  M.alloc (|
                    Value.StructTuple
                      "alloc::collections::vec_deque::drain::drop::DropGuard"
                      [ M.read (| self |) ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_function (| "core::mem::needs_drop", [ T ] |),
                                    []
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.ne (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (|
                                            M.SubPointer.get_struct_tuple_field (|
                                              guard,
                                              "alloc::collections::vec_deque::drain::drop::DropGuard",
                                              0
                                            |)
                                          |),
                                          "alloc::collections::vec_deque::drain::Drain",
                                          "remaining"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::vec_deque::drain::Drain")
                                    []
                                    [ T; A ],
                                  "as_slices",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_tuple_field (|
                                      guard,
                                      "alloc::collections::vec_deque::drain::drop::DropGuard",
                                      0
                                    |)
                                  |)
                                ]
                              |)
                            |),
                            [
                              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 front := M.copy (| γ0_0 |) in
                                  let back := M.copy (| γ0_1 |) in
                                  let~ _ :=
                                    let β :=
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (|
                                          M.SubPointer.get_struct_tuple_field (|
                                            guard,
                                            "alloc::collections::vec_deque::drain::drop::DropGuard",
                                            0
                                          |)
                                        |),
                                        "alloc::collections::vec_deque::drain::Drain",
                                        "idx"
                                      |) in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "*mut")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| front |) ]
                                        |)
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β :=
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (|
                                          M.SubPointer.get_struct_tuple_field (|
                                            guard,
                                            "alloc::collections::vec_deque::drain::drop::DropGuard",
                                            0
                                          |)
                                        |),
                                        "alloc::collections::vec_deque::drain::Drain",
                                        "remaining"
                                      |) in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.sub (|
                                        M.read (| β |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "*mut")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            "len",
                                            []
                                          |),
                                          [ M.read (| front |) ]
                                        |)
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::ptr::drop_in_place",
                                          [ Ty.apply (Ty.path "slice") [] [ T ] ]
                                        |),
                                        [ M.read (| front |) ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (|
                                          M.SubPointer.get_struct_tuple_field (|
                                            guard,
                                            "alloc::collections::vec_deque::drain::drop::DropGuard",
                                            0
                                          |)
                                        |),
                                        "alloc::collections::vec_deque::drain::Drain",
                                        "remaining"
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::ptr::drop_in_place",
                                          [ Ty.apply (Ty.path "slice") [] [ T ] ]
                                        |),
                                        [ M.read (| back |) ]
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::ops::drop::Drop"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("drop", InstanceField.Method (drop T A)) ].
      End Impl_core_ops_drop_Drop_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        (*     type Item = T; *)
        Definition _Item (T A : Ty.t) : Ty.t := T.
        
        (*
            fn next(&mut self) -> Option<T> {
                if self.remaining == 0 {
                    return None;
                }
                let wrapped_idx = unsafe { self.deque.as_ref().to_physical_idx(self.idx) };
                self.idx += 1;
                self.remaining -= 1;
                Some(unsafe { self.deque.as_mut().buffer_read(wrapped_idx) })
            }
        *)
        Definition next (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.eq (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "alloc::collections::vec_deque::drain::Drain",
                                          "remaining"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple "core::option::Option::None" []
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ wrapped_idx :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                              []
                              [ T; A ],
                            "to_physical_idx",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                                      []
                                      [ T; A ]
                                  ],
                                "as_ref",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::drain::Drain",
                                  "deque"
                                |)
                              ]
                            |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::drain::Drain",
                                "idx"
                              |)
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::drain::Drain",
                          "idx"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::drain::Drain",
                          "remaining"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::vec_deque::VecDeque")
                                []
                                [ T; A ],
                              "buffer_read",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::collections::vec_deque::VecDeque")
                                        []
                                        [ T; A ]
                                    ],
                                  "as_mut",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::collections::vec_deque::drain::Drain",
                                    "deque"
                                  |)
                                ]
                              |);
                              M.read (| wrapped_idx |)
                            ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                let len = self.remaining;
                (len, Some(len))
            }
        *)
        Definition size_hint
            (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ len :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::collections::vec_deque::drain::Drain",
                      "remaining"
                    |)
                  |) in
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (| len |);
                      Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item T A));
              ("next", InstanceField.Method (next T A));
              ("size_hint", InstanceField.Method (size_hint T A))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        (*
            fn next_back(&mut self) -> Option<T> {
                if self.remaining == 0 {
                    return None;
                }
                self.remaining -= 1;
                let wrapped_idx = unsafe { self.deque.as_ref().to_physical_idx(self.idx + self.remaining) };
                Some(unsafe { self.deque.as_mut().buffer_read(wrapped_idx) })
            }
        *)
        Definition next_back
            (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 ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.eq (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "alloc::collections::vec_deque::drain::Drain",
                                          "remaining"
                                        |)
                                      |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple "core::option::Option::None" []
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::drain::Drain",
                          "remaining"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                      |) in
                    let~ wrapped_idx :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                              []
                              [ T; A ],
                            "to_physical_idx",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ptr::non_null::NonNull")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                                      []
                                      [ T; A ]
                                  ],
                                "as_ref",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::drain::Drain",
                                  "deque"
                                |)
                              ]
                            |);
                            BinOp.Wrap.add (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::drain::Drain",
                                  "idx"
                                |)
                              |),
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::vec_deque::drain::Drain",
                                  "remaining"
                                |)
                              |)
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::vec_deque::VecDeque")
                                []
                                [ T; A ],
                              "buffer_read",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::collections::vec_deque::VecDeque")
                                        []
                                        [ T; A ]
                                    ],
                                  "as_mut",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::collections::vec_deque::drain::Drain",
                                    "deque"
                                  |)
                                ]
                              |);
                              M.read (| wrapped_idx |)
                            ]
                          |)
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("next_back", InstanceField.Method (next_back T A)) ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::drain::Drain") [] [ T; A ].
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_drain_Drain_T_A.
    End drain.
  End vec_deque.
End collections.
