
(* Insertion sort. *)

module InsertionSort

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

  let insertion_sort (a: array int)
    ensures { sorted a /\ permut_all (old a) a }
  = for i = 1 to length a - 1 do
      (* a[0..i[ is sorted; now insert a[i] *)
      invariant { sorted_sub a 0 i /\ permut_all (old a) a }
      let v = a[i] in
      let j = ref i in
      while !j > 0 && a[!j - 1] > v do
        invariant { 0 <= !j <= i }
        invariant { permut_all (old a) a[!j <- v] }
        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 -> v < a[k] }
        variant { !j }
        label L in
        a[!j] <- a[!j - 1];
        assert { exchange (a at L)[!j <- v] a[!j-1 <- v] (!j - 1) !j };
        j := !j - 1
      done;
      assert { forall k: int. 0 <= k < !j -> a[k] <= v };
      a[!j] <- v
    done

  let test1 () =
    let a = make 3 0 in
    a[0] <- 7; a[1] <- 3; a[2] <- 1;
    insertion_sort a;
    a

  let test2 () ensures { result.length = 8 } =
    let a = make 8 0 in
    a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
    a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
    insertion_sort a;
    a

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let a = test2 () in
    if a[0] <> -5 then raise BenchFailure;
    if a[1] <> 6 then raise BenchFailure;
    if a[2] <> 17 then raise BenchFailure;
    if a[3] <> 42 then raise BenchFailure;
    if a[4] <> 53 then raise BenchFailure;
    if a[5] <> 69 then raise BenchFailure;
    if a[6] <> 91 then raise BenchFailure;
    if a[7] <> 413 then raise BenchFailure;
    a

end

module InsertionSortGen

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

  type elt

  val predicate le elt elt

  clone map.MapSorted as M with type elt = elt, predicate le = le

  axiom le_refl: forall x:elt. le x x

  axiom le_asym: forall x y:elt. not (le x y) -> le y x

  axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z

  predicate sorted_sub (a : array elt) (l u : int) =
    M.sorted_sub a.elts l u

  predicate sorted (a : array elt) =
    M.sorted_sub a.elts 0 a.length

  let insertion_sort (a: array elt)
    ensures { sorted a /\ permut_all (old a) a }
  = for i = 1 to length a - 1 do
      (* a[0..i[ is sorted; now insert a[i] *)
      invariant { sorted_sub a 0 i /\ permut_all (old a) a }
      let v = a[i] in
      let j = ref i in
      while !j > 0 && not (le a[!j - 1] v) do
        invariant { 0 <= !j <= i }
        invariant { permut_all (old a) a[!j <- v] }
        invariant { forall k1 k2: int.
             0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> le a[k1] a[k2] }
        invariant { forall k: int. !j+1 <= k <= i -> le v a[k] }
        variant { !j }
        label L in
        a[!j] <- a[!j - 1];
        assert { exchange (a at L)[!j <- v] a[!j-1 <- v] (!j - 1) !j };
        j := !j - 1
      done;
      assert { forall k: int. 0 <= k < !j -> le a[k] v };
      a[!j] <- v
    done

end
