
  0 | module BinomialHeap
  1 | 
  2 | import Data.List
  3 | 
  4 | import Heap
  5 | 
  6 | %default total
  7 | 
  8 | data Tree a = Node Int a (List (Tree a))
  9 | 
 10 | export
 11 | data BinomialHeap a = BH (List (Tree a))
 12 | 
 13 | rank : Tree a -> Int
 14 | rank (Node r x c) = r
 15 | 
 16 | root : Tree a -> a
 17 | root (Node r x c) = x
 18 | 
 19 | link : Ord a => Tree a -> Tree a -> Tree a
 20 | link t1@(Node r x1 c1) t2@(Node _ x2 c2) =
 21 |   if x1 <= x2 then Node (r + 1) x1 (t2 :: c1) else Node (r + 1) x2 (t1 :: c2)
 22 | 
 23 | insTree : Ord a => Tree a -> List (Tree a) -> List (Tree a)
 24 | insTree t []             = [t]
 25 | insTree t ts@(t' :: ts') =
 26 |   if rank t < rank t' then t :: ts else assert_total $ insTree (link t t') ts'
 27 | 
 28 | mrg : Ord a => List (Tree a) -> List (Tree a) -> List (Tree a)
 29 | mrg ts1                  []           = ts1
 30 | mrg     []           ts2              = ts2
 31 | mrg ts1@(t1 :: ts1') ts2@(t2 :: ts2') = case compare (rank t1) (rank t2) of
 32 |   LT => t1 :: assert_total (mrg ts1' ts2)
 33 |   GT => t2 :: assert_total (mrg ts1 ts2')
 34 |   EQ => insTree (link t1 t2) (assert_total $ mrg ts1' ts2')
 35 | 
 36 | removeMinTree : Ord a => List (Tree a) -> (Tree a, List (Tree a))
 37 | removeMinTree [] = assert_total $ idris_crash "empty heap"
 38 | removeMinTree [t] = (t, [])
 39 | removeMinTree (t :: ts) = let (t', ts') = removeMinTree ts in
 40 |   if root t < root t' then (t, ts) else (t', t :: ts')
 41 | 
 42 | export
 43 | Heap BinomialHeap where
 44 |   empty = BH []
 45 |   isEmpty (BH ts) = isNil ts
 46 | 
 47 |   insert x (BH ts) = BH (insTree (Node 0 x []) ts)
 48 | 
 49 |   merge (BH ts1) (BH ts2) = BH (mrg ts1 ts2)
 50 | 
 51 |   findMin (BH ts) = root (fst (removeMinTree ts))
 52 | 
 53 |   deleteMin (BH ts) = let (Node _ x ts1, ts2) = removeMinTree ts
 54 |     in BH (mrg (reverse ts1) ts2)
 55 |