/*
 * This is an example in Xanadu showing that array bounds checking
 * is not needed for doing quicksort on an array. The code is written
 * by Hongwei Xi (December 1999)
 */

{size:nat, i:nat, j:nat, k:nat | i < size, j < size, k < size}
[n:nat | n < size] int(n)
median(i:int(i), j:int(j), k:int(k), vec[size]: int) {
  var: int x, y, z;;

  x = vec[i]; y = vec[j]; z = vec[k];

  if (x > y) {
     if (y > z) return j; else { if (x > z) return k; else return i; }
  } else {
    if (y > z) { if (x > z) return i; else return k; } else return j;
  }
}

{size:nat, start:nat, end:nat | start < end <= size}
[n:nat | n < size] int(n)
get_pivot (start: int(start), end: int(end), vec[size]: int) {
  var: int d, diff; int i, j, k;;

  diff = end - start;
  
  if (diff < 7) return start + (diff / 2);
  else {
    i = start; j = start + diff / 2; k = end - 1;
    if (diff < 40) return median(i, j, k, vec);
    else {
      d = diff / 8;
      i = median(i, i + d, i + 2 * d, vec);
      j = median(j - d, j, j + d, vec);
      k = median(k - 2 * d, k - d, k, vec);
      return median(i, j, k, vec);
    }
  }
}

{size:nat, start: nat, end: nat | start < end <= size}
[n:nat | start <= n < end] int(n)
split(start: int(start), end: int(end), vec[size]: int) {
  var: int pivot; int x, temp;
       l: [i:int | start <= i <= end] int(i);
       h: [j:int | start <= j < end] int(j);;

  pivot = get_pivot(start, end, vec);
  l = start; h = end - 1; x = vec[pivot];

  while (true) {
    while (l < end) { if (vec[l] <= x) l = l + 1; else break; }
    while (start < h) { if (vec[h] > x) h = h - 1; else break; }
    if (l < h) {
      temp = vec[l]; vec[l] = vec[h]; vec[h] = temp;
      l = l + 1; h = h - 1;
    } else return h;
  }
  exit;
}

{size:nat, start: nat, end: nat | start < end <= size}
unit
sort_range (start: int(start), end: int(end), vec[size]: int) {
  var: int diff, sp;;

  diff = end - start;
  if (diff <= 1) return;

  sp = split(start, end, vec);

  sort_range (start, sp, vec);
  sort_range (sp, end, vec);
  return;
}

unit
main () {
  var: int i, n, x, vec[];;

    n = 10;
    vec = alloc(n, 0);
    for (i = 0; i < n; i = i + 1) { vec[i] = (n - i) * ( n + i); }
    sort_range(0, 10, vec);
    return;
}