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