
  0 | module LazyPairingHeap
  1 | 
  2 | import Heap
  3 | 
  4 | %default total
  5 | 
  6 | export
  7 | data PairingHeap a = E | T a (PairingHeap a) (Lazy (PairingHeap a))
  8 | 
  9 | mutual
 10 |   link : Ord a => PairingHeap a -> PairingHeap a -> PairingHeap a
 11 |   link (T x E m) a = T x a m
 12 |   link (T x b m) a = T x E (assert_total $ merge (merge a b) m)
 13 |   link E         _ = assert_total $ idris_crash "assert_unreachable"
 14 | 
 15 |   export
 16 |   Heap PairingHeap where
 17 |     empty = E
 18 |     isEmpty E = True
 19 |     isEmpty _ = False
 20 | 
 21 |     insert x a = merge (T x E E) a
 22 | 
 23 |     merge a E = a
 24 |     merge E b = b
 25 |     merge a@(T x _ _) b@(T y _ _) = if x <= y then link a b else link b a
 26 | 
 27 |     findMin E = assert_total $ idris_crash "empty heap"
 28 |     findMin (T x a m) = x
 29 | 
 30 |     deleteMin E = assert_total $ idris_crash "empty heap"
 31 |     deleteMin (T x a m) = merge a m
 32 |