module SortedList
  [@java:package:fr.parcoursup.whyml.ordreappel.algo]

  use ref.Ref
  use int.Int
  use seq.Seq
  use seq.Permut

  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.lang.Integer
  use mach.java.util.List as L
  use mach.java.util.UnmodifiableList as UL

  type elt
  val function key elt : integer

  predicate le_keys[@rewrite] (e1 e2 : elt) = key e1 <= key e2

  clone seq.Sorted as SortedSeq with type t=elt, predicate le=le_keys

  predicate sorted (l1 : seq elt) (l2 : seq elt) =
    SortedSeq.sorted l2 && Permut.permut_all l1 l2

  let lemma sort_inner_loop_lemma (l : seq elt) (i : int)
    requires { SortedSeq.sorted_sub l 0 i }
    ensures { forall p q. 0 <= p <= q < i -> key l[p] <= key l[q] }
  =
    assert { forall x y. le_keys x y -> key x <= key y }

  val sort [@java:ignore] (l1 : L.list elt) : unit
    writes { l1 }
    ensures { sorted (old l1) l1 }

  let sort_list (l1 : L.list elt) : (l2 : UL.ulist elt)
    requires { L.size l1 < Integer.max_integer }
    ensures { sorted l1 l2 }
  =
    try
      let l1p = L.empty () in
      for i = 0 to L.size l1 -1 do
        invariant { L.size l1p = i }
        invariant { forall j. 0 <= j < i -> l1[j] = l1p[j] }
        let _ = L.add l1p (L.get l1 i) in ()
      done;
      assert { l1p == l1 };
      sort l1p;
      L.copy_of l1p
    with
      IndexOutOfBoundsException.E _ -> absurd
    end

  let sort_ulist (l1 : UL.ulist elt) : (l2 : UL.ulist elt)
    requires { UL.size l1 < Integer.max_integer }
    ensures { sorted l1 l2 }
  =
    try
      let l1p = L.empty () in
      for i = 0 to UL.size l1 -1 do
        invariant { L.size l1p = i }
        invariant { forall j. 0 <= j < i -> l1[j] = l1p[j] }
        let _ = L.add l1p (UL.get l1 i) in ()
      done;
      assert { l1p == l1 };
      sort l1p;
      L.copy_of l1p
    with
      IndexOutOfBoundsException.E _ -> absurd
    end

  let is_sorted (l : UL.ulist elt) : bool
    requires { UL.size l < Integer.max_integer }
    ensures { result = SortedSeq.sorted l }
  =
    if UL.size l <= 1 then
      return true;
    try
      for i = 1 to UL.size l - 1 do
        invariant { forall j k. 0 <= j < k < i -> le_keys l[j] l[k] }
        if key (UL.get l (i-1)) > key (UL.get l i) then
          return false;
        assert { le_keys l[i-1] l[i] };
      done;
      return true;
    with
      IndexOutOfBoundsException.E _ -> absurd
    end
end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)