Insertion sort -- with swap

module InsertionSort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq

  let swap (a: array int) (i: int) (j: int) =
    requires { 0 <= i < length a /\ 0 <= j < length a }
    ensures { exchange (old a) a i j }
   let v = a[i] in
    a[i] <- a[j];
    a[j] <- v

  let insertion_sort (a: array int) =
    ensures { sorted a /\ permut_all (old a) a }
'L:
    for i = 1 to length a - 1 do
      invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a }
      let j = ref i in
'L1:
      while !j > 0 && a[!j - 1] > a[!j] do
        invariant { 0 <= !j <= i }
        invariant { permut_all (at a 'L) a}
        invariant { forall k1 k2: int. 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2] }
        invariant { forall k: int. !j+1 <= k <= i -> a[!j] < a[k] }
        variant { !j }
        swap a (!j-1) !j;
        assert { permut_all (at a 'L1) a } ;
        j := !j - 1
      done
    done

end