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

Module slice.
  Module sort.
    Module unstable.
      Module heapsort.
        (*
        pub(crate) fn heapsort<T, F>(v: &mut [T], is_less: &mut F)
        where
            F: FnMut(&T, &T) -> bool,
        {
            let len = v.len();
        
            for i in (0..len + len / 2).rev() {
                let sift_idx = if i >= len {
                    i - len
                } else {
                    v.swap(0, i);
                    0
                };
        
                // SAFETY: The above calculation ensures that `sift_idx` is either 0 or
                // `(len..(len + (len / 2))) - len`, which simplifies to `0..(len / 2)`.
                // This guarantees the required `sift_idx <= len`.
                unsafe {
                    sift_down(&mut v[..cmp::min(i, len)], sift_idx, is_less);
                }
            }
        }
        *)
        Definition heapsort (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "len",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "core::iter::adapters::rev::Rev")
                            []
                            [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                              [],
                              "rev",
                              []
                            |),
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [
                                  ("start", Value.Integer IntegerKind.Usize 0);
                                  ("end_",
                                    BinOp.Wrap.add (|
                                      M.read (| len |),
                                      BinOp.Wrap.div (|
                                        M.read (| len |),
                                        Value.Integer IntegerKind.Usize 2
                                      |)
                                    |))
                                ]
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::rev::Rev")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::ops::range::Range")
                                              []
                                              [ Ty.path "usize" ]
                                          ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let i := M.copy (| γ0_0 |) in
                                        let~ sift_idx :=
                                          M.copy (|
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          BinOp.ge (|
                                                            M.read (| i |),
                                                            M.read (| len |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      BinOp.Wrap.sub (|
                                                        M.read (| i |),
                                                        M.read (| len |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let~ _ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply (Ty.path "slice") [] [ T ],
                                                            "swap",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| v |);
                                                            Value.Integer IntegerKind.Usize 0;
                                                            M.read (| i |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (|
                                                      Value.Integer IntegerKind.Usize 0
                                                    |)))
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_function (|
                                                "core::slice::sort::unstable::heapsort::sift_down",
                                                [ T; F ]
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::index::IndexMut",
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ops::range::RangeTo")
                                                        []
                                                        [ Ty.path "usize" ]
                                                    ],
                                                    "index_mut",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| v |);
                                                    Value.StructRecord
                                                      "core::ops::range::RangeTo"
                                                      [
                                                        ("end_",
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "core::cmp::min",
                                                              [ Ty.path "usize" ]
                                                            |),
                                                            [ M.read (| i |); M.read (| len |) ]
                                                          |))
                                                      ]
                                                  ]
                                                |);
                                                M.read (| sift_idx |);
                                                M.read (| is_less |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_heapsort :
          M.IsFunction "core::slice::sort::unstable::heapsort::heapsort" heapsort.
        
        (*
        unsafe fn sift_down<T, F>(v: &mut [T], mut node: usize, is_less: &mut F)
        where
            F: FnMut(&T, &T) -> bool,
        {
            // SAFETY: See function safety.
            unsafe {
                intrinsics::assume(node <= v.len());
            }
        
            let len = v.len();
        
            let v_base = v.as_mut_ptr();
        
            loop {
                // Children of `node`.
                let mut child = 2 * node + 1;
                if child >= len {
                    break;
                }
        
                // SAFETY: The invariants and checks guarantee that both node and child are in-bounds.
                unsafe {
                    // Choose the greater child.
                    if child + 1 < len {
                        // We need a branch to be sure not to out-of-bounds index,
                        // but it's highly predictable.  The comparison, however,
                        // is better done branchless, especially for primitives.
                        child += is_less(&*v_base.add(child), &*v_base.add(child + 1)) as usize;
                    }
        
                    // Stop if the invariant holds at `node`.
                    if !is_less(&*v_base.add(node), &*v_base.add(child)) {
                        break;
                    }
        
                    ptr::swap_nonoverlapping(v_base.add(node), v_base.add(child), 1);
                }
        
                node = child;
            }
        }
        *)
        Definition sift_down (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ v; node; is_less ] =>
            ltac:(M.monadic
              (let v := M.alloc (| v |) in
              let node := M.alloc (| node |) in
              let is_less := M.alloc (| is_less |) in
              M.read (|
                let~ _ :=
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::assume", [] |),
                        [
                          BinOp.le (|
                            M.read (| node |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ T ],
                                "len",
                                []
                              |),
                              [ M.read (| v |) ]
                            |)
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |) in
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "len",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                let~ v_base :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ T ],
                        "as_mut_ptr",
                        []
                      |),
                      [ M.read (| v |) ]
                    |)
                  |) in
                M.loop (|
                  ltac:(M.monadic
                    (let~ child :=
                      M.alloc (|
                        BinOp.Wrap.add (|
                          BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 2, M.read (| node |) |),
                          Value.Integer IntegerKind.Usize 1
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.ge (| M.read (| child |), M.read (| len |) |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.lt (|
                                        BinOp.Wrap.add (|
                                          M.read (| child |),
                                          Value.Integer IntegerKind.Usize 1
                                        |),
                                        M.read (| len |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  let β := child in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      M.rust_cast
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            F,
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply (Ty.path "&") [] [ T ];
                                                  Ty.apply (Ty.path "&") [] [ T ]
                                                ]
                                            ],
                                            "call_mut",
                                            []
                                          |),
                                          [
                                            M.read (| is_less |);
                                            Value.Tuple
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [ M.read (| v_base |); M.read (| child |) ]
                                                |);
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| v_base |);
                                                    BinOp.Wrap.add (|
                                                      M.read (| child |),
                                                      Value.Integer IntegerKind.Usize 1
                                                    |)
                                                  ]
                                                |)
                                              ]
                                          ]
                                        |))
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            F,
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply (Ty.path "&") [] [ T ];
                                                  Ty.apply (Ty.path "&") [] [ T ]
                                                ]
                                            ],
                                            "call_mut",
                                            []
                                          |),
                                          [
                                            M.read (| is_less |);
                                            Value.Tuple
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [ M.read (| v_base |); M.read (| node |) ]
                                                |);
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                                    "add",
                                                    []
                                                  |),
                                                  [ M.read (| v_base |); M.read (| child |) ]
                                                |)
                                              ]
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "core::ptr::swap_nonoverlapping", [ T ] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| v_base |); M.read (| node |) ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "add",
                                  []
                                |),
                                [ M.read (| v_base |); M.read (| child |) ]
                              |);
                              Value.Integer IntegerKind.Usize 1
                            ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |) in
                    let~ _ := M.write (| node, M.read (| child |) |) in
                    M.alloc (| Value.Tuple [] |)))
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Function_sift_down :
          M.IsFunction "core::slice::sort::unstable::heapsort::sift_down" sift_down.
      End heapsort.
    End unstable.
  End sort.
End slice.
