{max:nat}
record <'a> heap(max) {
  max: int(max);
  size: int[0,max];
  data[max]: 'a
}

{max:nat, i:nat | i < max}
unit heapify (heap: <float> heap(max), i: int(i)) {
  var: int size, left, right;
       float temp;
       largest: int[0, max);;

  left = 2 * i + 1; right = 2 * i + 2;

  size = heap.size; largest = i;

  if (left < size) {
    if (heap.data[left] >. heap.data[i]) { largest = left; }
  }

  if (right < size) {
    if (heap.data[right] >. heap.data[largest]) { largest = right; }
  }

  if (largest <> i) {
    temp = heap.data[i];
    heap.data[i] = heap.data[largest];
    heap.data[largest] = temp;
    heapify (heap, largest);
  }
}

{max:nat}
unit buildheap (heap: <float> heap(max)) {
  var: int i, size;;
 
  size = heap.size;

  invariant: [i:int | i < max] (i: int(i))
  for (i =  size / 2 - 1; i >= 0; i = i - 1) {
    heapify (heap, i);
  }
}

{max:nat}
unit heapsort (heap: <float> heap(max)) {
  var: int size, i; float temp;;

  buildheap (heap);
  invariant: [i:int | i < max] (i: int(i))
  for (i = heap.max - 1; i >= 1; i = i - 1) {
    temp = heap.data[i];
    heap.data[i] = heap.data[0];
    heap.data[0] = temp;
    heap.size = i;
    heapify(heap, 0);
  }
}

unit main () {
  var: nat i; data[]: float; heap: <float> heap;;

  data = alloc(16, 0.0);
  for (i = 0; i < 16; i = i + 1) {
    data[i] = float_of_int ((16 - i) * i);
  }

  heap = heap { max = 16; size = 16; data = data };
  heapsort(heap);
}