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

Module slice.
  Module sort.
    Module unstable.
      (*
      pub fn sort<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
          // Arrays of zero-sized types are always all-equal, and thus sorted.
          if T::IS_ZST {
              return;
          }
      
          // Instrumenting the standard library showed that 90+% of the calls to sort
          // by rustc are either of size 0 or 1.
          let len = v.len();
          if intrinsics::likely(len < 2) {
              return;
          }
      
          cfg_if! {
              if #[cfg(any(feature = "optimize_for_size", target_pointer_width = "16"))] {
                  heapsort::heapsort(v, is_less);
              } else {
                  // More advanced sorting methods than insertion sort are faster if called in
                  // a hot loop for small inputs, but for general-purpose code the small
                  // binary size of insertion sort is more important. The instruction cache in
                  // modern processors is very valuable, and for a single sort call in general
                  // purpose code any gains from an advanced method are cancelled by i-cache
                  // misses during the sort, and thrashing the i-cache for surrounding code.
                  const MAX_LEN_ALWAYS_INSERTION_SORT: usize = 20;
                  if intrinsics::likely(len <= MAX_LEN_ALWAYS_INSERTION_SORT) {
                      insertion_sort_shift_left(v, 1, is_less);
                      return;
                  }
      
                  ipnsort(v, is_less);
              }
          }
      }
      *)
      Definition sort (ε : 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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) 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.Tuple [] |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (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~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::likely", [] |),
                                    [
                                      BinOp.lt (|
                                        M.read (| len |),
                                        Value.Integer IntegerKind.Usize 2
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| 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 (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::likely", [] |),
                                    [
                                      BinOp.le (|
                                        M.read (| len |),
                                        M.read (|
                                          M.get_constant (|
                                            "core::slice::sort::unstable::sort::MAX_LEN_ALWAYS_INSERTION_SORT"
                                          |)
                                        |)
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "core::slice::sort::shared::smallsort::insertion_sort_shift_left",
                                          [ T; F ]
                                        |),
                                        [
                                          M.read (| v |);
                                          Value.Integer IntegerKind.Usize 1;
                                          M.read (| is_less |)
                                        ]
                                      |)
                                    |) in
                                  M.return_ (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::slice::sort::unstable::ipnsort", [ T; F ] |),
                        [ M.read (| v |); M.read (| is_less |) ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_sort : M.IsFunction "core::slice::sort::unstable::sort" sort.
      
      Module sort.
        Definition value_MAX_LEN_ALWAYS_INSERTION_SORT : Value.t :=
          M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 20 |))).
      End sort.
      
      (*
      fn ipnsort<T, F>(v: &mut [T], is_less: &mut F)
      where
          F: FnMut(&T, &T) -> bool,
      {
          let len = v.len();
          let (run_len, was_reversed) = find_existing_run(v, is_less);
      
          // SAFETY: find_existing_run promises to return a valid run_len.
          unsafe { intrinsics::assume(run_len <= len) };
      
          if run_len == len {
              if was_reversed {
                  v.reverse();
              }
      
              // It would be possible to a do in-place merging here for a long existing streak. But that
              // makes the implementation a lot bigger, users can use `slice::sort` for that use-case.
              return;
          }
      
          // Limit the number of imbalanced partitions to `2 * floor(log2(len))`.
          // The binary OR by one is used to eliminate the zero-check in the logarithm.
          let limit = 2 * (len | 1).ilog2();
          crate::slice::sort::unstable::quicksort::quicksort(v, None, limit, is_less);
      }
      *)
      Definition ipnsort (ε : 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.catch_return (|
              ltac:(M.monadic
                (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.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::slice::sort::shared::find_existing_run",
                          [ T; F ]
                        |),
                        [ M.read (| v |); M.read (| is_less |) ]
                      |)
                    |),
                    [
                      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 run_len := M.copy (| γ0_0 |) in
                          let was_reversed := M.copy (| γ0_1 |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::assume", [] |),
                                [ BinOp.le (| M.read (| run_len |), M.read (| len |) |) ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (| M.read (| run_len |), 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 (|
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ := M.use was_reversed in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    let~ _ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply (Ty.path "slice") [] [ T ],
                                                            "reverse",
                                                            []
                                                          |),
                                                          [ M.read (| v |) ]
                                                        |)
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.return_ (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ limit :=
                            M.alloc (|
                              BinOp.Wrap.mul (|
                                Value.Integer IntegerKind.U32 2,
                                M.call_closure (|
                                  M.get_associated_function (| Ty.path "usize", "ilog2", [] |),
                                  [
                                    BinOp.bit_or
                                      (M.read (| len |))
                                      (Value.Integer IntegerKind.Usize 1)
                                  ]
                                |)
                              |)
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::slice::sort::unstable::quicksort::quicksort",
                                  [ T; F ]
                                |),
                                [
                                  M.read (| v |);
                                  Value.StructTuple "core::option::Option::None" [];
                                  M.read (| limit |);
                                  M.read (| is_less |)
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_ipnsort : M.IsFunction "core::slice::sort::unstable::ipnsort" ipnsort.
    End unstable.
  End sort.
End slice.
