module Data.Queue.Indexed.Leftist
(Leftist(..))
where
import Data.Queue.Indexed.Class
import Data.Type.Equality
import Prelude
import TypeLevel.Bool
import TypeLevel.Singletons
import Control.DeepSeq (NFData(rnf))
data Leftist n a where
Leaf :: Leftist 0 a
Node :: !(The Nat (n + m + 1))
-> a
-> Leftist n a
-> Leftist m a
-> !(m <= n)
-> Leftist (n + m + 1) a
rank :: Leftist n s -> The Nat n
rank Leaf = sing
rank (Node r _ _ _ _) = r
instance Ord a => IndexedQueue Leftist a where
minView (Node _ x l r _) = (x, merge l r)
singleton x = Node sing x Leaf Leaf Refl
empty = Leaf
insert = merge . singleton
minViewMay Leaf b _ = b
minViewMay (Node _ x l r _) _ f = f x (merge l r)
instance Ord a =>
MeldableIndexedQueue Leftist a where
merge Leaf h2 = h2
merge h1 Leaf = h1
merge h1@(Node w1 p1 l1 r1 _) h2@(Node w2 p2 l2 r2 _)
| p1 < p2 =
if ll <=. lr
then Node (w1 +. w2) p1 l1 (merge r1 h2)
else Node (w1 +. w2) p1 (merge r1 h2) l1 . totalOrder ll lr
| otherwise =
if rl <=. rr
then Node (w1 +. w2) p2 l2 (merge r2 h1)
else Node (w1 +. w2) p2 (merge r2 h1) l2 . totalOrder rl rr
where
ll = rank r1 +. w2
lr = rank l1
rl = rank r2 +. w1
rr = rank l2
instance NFData a =>
NFData (Leftist n a) where
rnf Leaf = ()
rnf (Node n x l r Refl) = n `seq` rnf x `seq` rnf l `seq` rnf r