{-# 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))