-{-# LANGUAGE
- EmptyDataDecls,
- TypeFamilies,
- TypeOperators,
- UndecidableInstances
- #-}
-module Data.HList.Heap
- ( Heap
-
- , Empty
- , Unit
- , Insert
- , Merge
- , MergeAll
- , IsEmpty
- , FindMin
- , DeleteMin
- , SplitMin
- )
- where
-
-import Data.HList
-import Types.Data.Bool
-import Types.Data.Ord
-
-
-data Empty
-data Node key value heaps
-
-class Heap h
-instance Heap Empty
-instance Heap hs => Heap (Node k v hs)
-
-type Unit k v = Node k v Nil
-
-type family IsEmpty h
-type instance IsEmpty Empty = True
-type instance IsEmpty (Node k v hs) = False
-
-type Insert k v h = Merge (Unit k v) h
-
-type family Merge h1 h2
-type instance Merge h1 Empty = h1
-type instance Merge Empty h2 = h2
-type instance Merge (Node k1 v1 hs1) (Node k2 v2 hs2)
- = If (k1 :<: k2)
- (Node k1 v1 (Cons (Node k2 v2 hs2) hs1))
- (Node k2 v2 (Cons (Node k1 v1 hs1) hs2))
-
-type family MergeAll hs
-type instance MergeAll Nil = Empty
-type instance MergeAll (Cons h Nil) = h
-type instance MergeAll (Cons h (Cons h' hs))
- = Merge (Merge h h') (MergeAll hs)
-
-type family FindMin h
-type instance FindMin (Node k v hs) = Cons k v
-
-type family DeleteMin h
-type instance DeleteMin Empty = Empty
-type instance DeleteMin (Node k v hs) = MergeAll hs
-
-type family SplitMin h
-type instance SplitMin (Node k v hs) = Cons k (Cons v (MergeAll hs))