0 | module Structures.PriorityQueue.BinomialQueue
  1 |
  2 | import Data.Nat
  3 | import Data.Fin
  4 | import Data.Vect
  5 | import Decidable.Equality
  6 |
  7 | import Structures.PriorityQueue
  8 |
  9 | %default total
 10 |
 11 | ||| Binomial Tree per Optimal purely functional priority queues
 12 | ||| (Brodal, G. S., & Okasaki, C. (1996).)
 13 | |||
 14 | ||| Holds rank^2 elements
 15 | data BinomialTree : (e : Type) -> (rank : Nat) -> Type where
 16 |   Singleton : (element : e)
 17 |     -> BinomialTree e 0
 18 |   Link : (root : BinomialTree e n) -> (leftmost_child : BinomialTree e n)
 19 |     -> BinomialTree e (S n)
 20 | %name BinomialTree bt, ct, dt
 21 |
 22 | BinomialPair : Type -> Type
 23 | BinomialPair e = (rank : Nat ** BinomialTree e rank)
 24 |
 25 | ||| Get the root of a binomial tree
 26 | root : (tree : BinomialTree e n) -> e
 27 | root (Singleton element) = element
 28 | root (Link x leftmost_child) = root x
 29 |
 30 | ||| Link two BiomialTrees together, preserving heap ordering
 31 | |||
 32 | ||| Makes the tree with the larger root the child of the other
 33 | link : Ord e => (x, y : BinomialTree e n) -> BinomialTree e (S n)
 34 | link x y =
 35 |   let (x_val, y_val) = (root x, root y)
 36 |   in if x_val < y_val
 37 |     then Link x y
 38 |     else Link y x
 39 |
 40 | ||| Get the rank of a BinomialTree
 41 | rank : (tree : BinomialTree e n) -> Nat
 42 | rank (Singleton _) = 0
 43 | rank (Link root _) = S (rank root)
 44 |
 45 | rankEq : (tree : BinomialTree e n) -> n = rank tree
 46 | rankEq (Singleton _) = Refl
 47 | rankEq (Link root leftmost_child) =
 48 |   let rest = rankEq root
 49 |   in eqSucc _ _ rest
 50 |
 51 | toPair : (tree : BinomialTree e n) -> BinomialPair e
 52 | toPair tree =
 53 |   (rank tree **
 54 |     rewrite sym $ rankEq tree in tree)
 55 |
 56 | ||| Break the links of a tree to extract the root
 57 | extractRoot : (tree : BinomialTree e n) -> (e, List (BinomialPair e))
 58 | extractRoot (Singleton element) = (element, [])
 59 | extractRoot (Link root leftmost_child) =
 60 |   let (element, rest) = extractRoot root
 61 |   in (element, toPair leftmost_child :: rest)
 62 |
 63 | ||| A binomial queue per Optimal purely functional priority queues
 64 | ||| (Brodal, G. S., & Okasaki, C. (1996).)
 65 | export
 66 | record BinomialQueue (e : Type) where
 67 |   constructor MkBQ
 68 |   o : Ord e
 69 |   forest_size : Nat
 70 |   forest : Vect forest_size (BinomialPair e)
 71 | %name BinomialQueue bq, cq, dq
 72 |
 73 | ||| Insert a tree into its proper location in a list of binomial pairs
 74 | insertTree :
 75 |   Ord e => {n : Nat} ->
 76 |   (x : BinomialPair e) ->
 77 |   (xs : Vect n (BinomialPair e))
 78 |   -> (m : Nat ** Vect m (BinomialPair e))
 79 | insertTree x [] = (1 ** [x])
 80 | insertTree (x_n ** x) ((y_n ** y) :: xs) =
 81 |   case decEq x_n y_n of
 82 |     Yes Refl => insertTree (S x_n ** link x y) xs
 83 |     No _ =>
 84 |       if x_n < y_n
 85 |         then (_ ** (x_n ** x) :: (y_n ** y) :: xs)
 86 |         else
 87 |           let (rest_len ** rest) = insertTree (x_n **x) xs
 88 |           in (_ ** (y_n ** y) :: rest)
 89 |
 90 | ||| meld, phrased in terms of the inner list
 91 | meld' :
 92 |   Ord e => {n, m : Nat} ->
 93 |   (xs : Vect n (BinomialPair e)) ->
 94 |   (ys : Vect m (BinomialPair e))
 95 |   -> (o : Nat ** Vect o (BinomialPair e))
 96 | meld' xs [] = (length xs ** rewrite lengthCorrect xs in xs)
 97 | meld' xs (y :: ys) =
 98 |   let (_ ** res) = insertTree y xs
 99 |   in meld' res ys
100 |
101 | export
102 | PriorityQueue BinomialQueue where
103 |   empty = MkBQ o 0 []
104 |
105 |   singleton element = MkBQ o 1 [(0 ** Singleton element)]
106 |
107 |   isNull bq = null bq.forest
108 |
109 |   length (MkBQ _ forest_size forest) =
110 |     let lens = map (\(x ** _) => 2 `power` x) forest
111 |     in sum lens
112 |
113 |   findMin (MkBQ _ forest_size forest) =
114 |     case forest of
115 |       [] => Nothing
116 |       ((_ ** x) :: xs) =>
117 |         let x = root x
118 |             xs = map (\(_ ** y) => root y) xs
119 |         in Just $ foldl min x xs
120 |
121 |   meld x y =
122 |     let (xs, ys) = (x.forest, y.forest)
123 |         (new_size ** new_forest) = meld' @{x.o} xs ys
124 |     in MkBQ x.o new_size new_forest
125 |
126 |   insert element queue =
127 |     meld (singleton {o = queue.o} element) queue
128 |
129 |   deleteMin (MkBQ o forest_size forest) with (forest)
130 |     deleteMin (MkBQ o 0 forest) | [] = MkBQ o 0 []
131 |     deleteMin (MkBQ o (S 0) forest) | ((rank ** tree) :: []) =
132 |       let rest = reverse . snd . extractRoot $ tree
133 |       in MkBQ o (length rest) (fromList rest)
134 |     deleteMin (MkBQ o (S (S len)) forest) | (x :: y :: xs) =
135 |       let (idx, (min_n ** min_tree)) = findMin (y :: xs) (0, x) 1
136 |           without_min = deleteAt idx forest
137 |           (rest_len ** rest) = listToVect . reverse . snd . extractRoot $ min_tree
138 |           (new_size ** new_forest) = meld' without_min rest
139 |       in MkBQ o new_size new_forest
140 |     where
141 |       listToVect : List a -> (n : Nat ** Vect n a)
142 |       listToVect xs = (length xs ** fromList xs)
143 |       findMin :
144 |         {m : Nat} ->
145 |         (xs : Vect n (BinomialPair e)) ->
146 |         (acc : (Fin m, BinomialPair e)) ->
147 |         (idx : Fin m)
148 |         -> (Fin m, BinomialPair e)
149 |       findMin [] acc idx = acc
150 |       findMin ((x_rank ** x) :: xs) orig_acc@(acc_idx, (acc_rank ** acc)) idx =
151 |         if (<) @{o} (root x) (root acc)
152 |           then findMin xs (idx, (x_rank ** x)) (finS idx)
153 |           else findMin xs orig_acc (finS idx)
154 |