#line 13 "/home/travis/build/felix-lang/felix/src/packages/trees.fdoc"
  class MinHeap[T with Tord[T]]
  {
    fun left_child (p:int)  => 2*p + 1;
    fun right_child (p:int) => 2*p + 2;
    fun parent (c:int) => if c == 0 then 0 else (c - 1)/2;
  
    axiom family (i:int): i == i.left_child.parent and i == i.right_child.parent;
    typedef minheap_t = darray[T];
    ctor minheap_t () => darray[T] ();
    axiom left_heap (m:minheap_t, i:int):
      i.left_child < m.len.int or m.i < m.(i.left_child)
    ;
  
    proc heap_swap (h:minheap_t,i:int,j:int) {
      var tmp = h.i;
      set(h,i,h.j);
      set(h,j,tmp);
    }
  
    proc bubble_up(h:minheap_t, j:int)
    {
       var p = parent j; // parent of root is itself
       if h.p > h.j do // and so can't satisfy this condition
          heap_swap(h,p,j);
          bubble_up(h,p);
       done
    }
    proc heap_insert (h:minheap_t) (elt:T) {
      push_back (h,elt);
      bubble_up (h,h.len.int - 1);
    }
  
    // this procedure does nothing if the index p
    // is greater than or equal to the limit - 2,
    // since the last used slot is lim - 1,
    // and that node cannot have any children.
    proc bubble_down_lim (h:minheap_t, p:int, lim:int) {
      var min_index = p;
      var left = p.left_child;
      if left < lim do
        if h.min_index > h.left perform min_index = left;
        var right = left + 1;
        if right < lim
          if h.min_index > h.right perform min_index = right;
      done
      if min_index != p do
        heap_swap (h, p, min_index);
        bubble_down_lim (h, min_index, lim);
      done
    }
  
    proc bubble_down (h:minheap_t,p:int) =>
      bubble_down_lim (h, p, h.len.int)
    ;
  
    gen extract_min (h:minheap_t) : opt[T] =  {
      if h.len.int == 0 return None[T];
        var min = h.0;
        set(h,0,h.(h.len.int - 1));
        h.pop;
        bubble_down (h,0);
        return Some min;
    }
  
    // sorts largest to smallest!!
    // based on extract_min, except the minimum element
    // is moved to the position at the end of the heap
    // which would otherwise be deleted.
    proc heap_sort (h:minheap_t) {
      var tosort = h.len.int;
      while tosort > 1 do
        --tosort;
        heap_swap(h,0,tosort);
        bubble_down_lim (h,0, tosort);
      done
    }
  
    proc heapify (h:minheap_t) {
      var index = h.len.int - 2;
      while index >= 0 do
        bubble_down (h, index); --index;
      done
    }
  
  }