Merge sort as in Sedgewick

module MergeSort

  use import int.Int
  use import int.EuclideanDivision
  use import int.Div2
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq
  use map.Map as M
  clone map.MapSorted as N with type elt = int, predicate le = (<=)

  predicate map_eq_sub_rev_offset (a1 a2: M.map int int) (l u: int) (offset: int) =
    forall i: int. l <= i < u -> M.get a1 i = M.get a2 (offset + l + u - 1 - i)

  predicate array_eq_sub_rev_offset (a1 a2: array int) (l u: int) (offset: int) =
     map_eq_sub_rev_offset a1.elts a2.elts l u offset

  predicate map_dsorted_sub (a: M.map int int) (l u: int) =
    forall i1 i2 : int. l <= i1 <= i2 < u -> M.get a i2 <= M.get a i1

  predicate dsorted_sub (a: array int) (l u: int) =
    map_dsorted_sub a.elts l u

  predicate map_bitonic_sub (a: M.map int int) (l u: int) =  l < u ->
    exists i: int. l <= i <= u /\ N.sorted_sub a l i /\ map_dsorted_sub a i u

  predicate bitonic (a: array int) (l u: int) =
    map_bitonic_sub a.elts l u

  lemma map_bitonic_incr : forall a: M.map int int, l u: int.
     map_bitonic_sub a l u -> map_bitonic_sub a (l+1) u

  lemma map_bitonic_decr : forall a: M.map int int, l u: int.
     map_bitonic_sub a l u -> map_bitonic_sub a l (u-1)

  predicate modified_inside (a1 a2: array int) (l u: int) =
    (Array.length a1 = Array.length a2) /\
    array_eq_sub a1 a2 0 l /\ array_eq_sub a1 a2 u (Array.length a1)

  let rec mergesort1 (a b: array int) (lo hi: int) =
    requires {Array.length a = Array.length b /\
              0 <= lo <= (Array.length a) /\ 0 <= hi <= (Array.length a) }
    ensures { sorted_sub a lo hi /\ modified_inside (old a) a lo hi }
  if lo + 1 < hi then
  let m = div (lo+hi) 2 in
    assert{ lo < m < hi};
    mergesort1 a b lo m;
'L2: mergesort1 a b m hi;
    assert { array_eq_sub (at a 'L2) a lo m};
    for i = lo to m-1 do
      invariant { array_eq_sub b a lo i}
      b[i] <- a[i]
      done;
    assert{ array_eq_sub a b lo m};
    assert{ sorted_sub b lo m};
    for j = m to hi-1 do
      invariant { array_eq_sub_rev_offset b a m j (hi - j)}
      invariant { array_eq_sub a b lo m}
      b[j] <- a[m + hi - 1 - j]
      done;
    assert{ array_eq_sub a b lo m};
    assert{ sorted_sub b lo m};
    assert{ array_eq_sub_rev_offset b a m hi 0};
    assert{ dsorted_sub b m hi};
'L4: let i = ref lo in
    let j = ref hi in
    for k = lo to hi-1 do
      invariant{ lo <= !i < hi /\ lo <= !j <= hi}
      invariant{ k = !i + hi - !j}
      invariant{ sorted_sub a lo k }
      invariant{ forall k1 k2: int. lo <= k1 < k -> !i <= k2 < !j -> a[k1] <= b[k2] }
      invariant{ bitonic b !i !j }
      invariant{ modified_inside a (at a 'L4) lo hi }
      assert { !i < !j };
      if b[!i] < b[!j - 1] then
        begin a[k] <- b[!i]; i := !i + 1 end
      else
        begin j := !j - 1; a[k] <- b[!j] end
    done

  let mergesort (a: array int) =
    ensures { sorted a }
  let n = Array.length a in
  let b = Array.make n 0 in
    mergesort1 a b 0 n

end