
  0 | module BootstrapHeap
  1 | 
  2 | import Heap
  3 | 
  4 | %default total
  5 | 
  6 | export
  7 | partial
  8 | data BootstrapHeap : (Type -> Type) -> Type -> Type where
  9 |   E : BootstrapHeap h a
 10 |   H : a -> h (BootstrapHeap h a) -> BootstrapHeap h a
 11 | 
 12 | partial
 13 | Eq a => Eq (BootstrapHeap h a) where
 14 |   x == y = case x of
 15 |     (H x' _) => case y of
 16 |       (H y' _) => x' == y'
 17 | 
 18 | partial
 19 | Ord a => Ord (BootstrapHeap h a) where
 20 |   compare x y = case x of
 21 |     (H x' _) => case y of
 22 |       (H y' _) => compare x' y'
 23 | 
 24 | export
 25 | partial
 26 | {h : Type -> Type} -> Heap h => Heap (BootstrapHeap h) where
 27 |   empty = E
 28 |   isEmpty E = True
 29 |   isEmpty _ = False
 30 | 
 31 |   insert x h = merge (H x empty) h
 32 | 
 33 |   merge E h2 = h2
 34 |   merge h1 E = h1
 35 |   merge h1@(H x p1) h2@(H y p2) =
 36 |     if x <= y then H x (insert h2 p1) else H y (insert h1 p2)
 37 | 
 38 |   findMin h = case h of
 39 |     E       => idris_crash "empty heap"
 40 |     (H x p) => x
 41 | 
 42 |   deleteMin E = idris_crash "empty heap"
 43 |   deleteMin (H x p) =
 44 |       if isEmpty p then E
 45 |       else let (H y p1) = findMin p
 46 |                p2 = deleteMin p
 47 |            in (H y (merge p1 p2))
 48 |