
  0 | module LeftistHeap
  1 | 
  2 | import Heap
  3 | 
  4 | %default total
  5 | 
  6 | export
  7 | data LeftistHeap a = E | T Int a (LeftistHeap a) (LeftistHeap a)
  8 | 
  9 | rank : LeftistHeap a -> Int
 10 | rank E           = 0
 11 | rank (T r _ _ _) = r
 12 | 
 13 | makeT : a -> LeftistHeap a -> LeftistHeap a -> LeftistHeap a
 14 | makeT x a b = if rank a >= rank b then T (rank b + 1) x a b
 15 |               else T (rank a + 1) x b a
 16 | 
 17 | export
 18 | Heap LeftistHeap where
 19 |   empty = E
 20 |   isEmpty E = True
 21 |   isEmpty _ = False
 22 | 
 23 |   insert x h = merge (T 1 x E E) h
 24 | 
 25 |   merge h  E  = h
 26 |   merge E  h  = h
 27 |   merge h1@(T _ x a1 b1) h2@(T _ y a2 b2) =
 28 |     if x <= y then makeT x a1 (assert_total $ merge b1 h2)
 29 |     else makeT y a2 (assert_total $ merge h1 b2)
 30 | 
 31 |   findMin E = assert_total $ idris_crash "empty heap"
 32 |   findMin (T _ x a b) = x
 33 | 
 34 |   deleteMin E = assert_total $ idris_crash "empty heap"
 35 |   deleteMin (T _ x a b) = merge a b
 36 |