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 = (<=)
  use map.Occ as O

  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

  lemma permut_append: forall a1 a2: array int. forall l mid u: int.
    l <= mid <= u -> permut a1 a2 l mid -> permut a1 a2 mid u -> permut a1 a2 l u

  lemma occ_left_no_add: forall v: int, m: M.map int int, l u: int.
    l < u -> M.get m l <> v -> O.occ v m l u = O.occ v m (l+1) u

  lemma occ_left_add: forall v: int, m: M.map int int, l u: int.
    l < u -> M.get m l = v -> O.occ v m l u = 1 + O.occ v m (l+1) u

  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 { permut_sub (old a) a lo hi }
  if lo + 1 < hi then
  let m = div (lo+hi) 2 in
    assert{ lo < m < hi };
'L1: mergesort1 a b lo m;
     assert{ permut_sub (at a 'L1) a lo hi };
'L2: mergesort1 a b m hi;
'L3: assert { permut_sub (at a 'L1) a lo hi };
    for i = lo to m-1 do
      invariant { array_eq_sub b a lo i}
      b[i] <- a[i]
      done;
    for j = m to hi-1 do
      invariant { array_eq_sub_rev_offset b a m j (hi - j) }
      invariant { array_eq_sub b a lo m }
      invariant { forall v: int. O.occ v b.elts m j = O.occ v a.elts (m + hi - j) hi }
      b[j] <- a[m + hi - 1 - j]
      done;
    assert{ permut a b lo m /\ permut a b m hi };
    assert{ permut a b lo hi };
    assert{ array_eq (at a 'L3) a } ;
'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{ forall v: int. O.occ v a.elts lo k = O.occ v b.elts lo !i + O.occ v b.elts !j hi }
      invariant{ array_eq_sub (at a 'L4) a 0 lo /\ array_eq_sub (at a 'L4) a hi (length a) }
      assert { !i < !j };
    'L: if b[!i] < b[!j - 1] then
        begin a[k] <- b[!i]; i := !i + 1 ;
        assert{ O.occ b[!i-1] a.elts lo (k+1) = 1 + O.occ b[!i-1] (at a.elts 'L) lo k };
        assert{ forall v: int. v <> b[!i-1] -> O.occ v a.elts lo (k+1) = O.occ v (at a.elts 'L) lo k }
        end
      else
        begin j := !j - 1; a[k] <- b[!j] ;
        assert{ O.occ b[!j] a.elts lo (k+1) = 1 + O.occ b[!j] (at a.elts 'L) lo k };
        assert{ forall v: int. v <> b[!j] -> O.occ v a.elts lo (k+1) = O.occ v (at a.elts 'L) lo k }
      end
    done;
    assert{ i = j };
    assert{ permut a b lo hi };
    assert{ permut_sub (at a 'L4) a lo hi}

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

end