{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

-- | Classes for common functions between the heaps.
module Data.Queue.Indexed.Class where

import           GHC.TypeLits

-- | A classed for indexed priority queues. Equivalent to 'Data.Heap.Queue'
-- except the queues are indexed by their sizes.
class IndexedQueue h a where

    {-# MINIMAL insert, empty, minViewMay, minView #-}

    -- | The empty queue
    empty
        :: h 0 a

    -- | Return the minimal element, and the rest of the queue.
    minView
        :: h (1 + n) a -> (a, h n a)

    -- | A queue with one element.
    singleton
        :: a -> h 1 a
    singleton = flip insert empty

    -- | Add an element to the queue.
    insert
        :: a -> h n a -> h (1 + n) a

    -- | Pattern match on the queue, and provide a proof that it
    -- is/isn't empty to the caller.
    minViewMay
       :: h n a
       -> (n ~ 0 => b)
       -> (forall m. (1 + m) ~ n => a -> h m a -> b)
       -> b

-- | Queues which can be merged. Conforming members should
-- form a monoid under 'merge' and 'empty'.
class IndexedQueue h a =>
      MeldableIndexedQueue h a where
    -- | Merge two heaps. This operation is associative, and has the
    -- identity of 'empty'.
    --
    -- @'merge' x ('merge' y z) = 'merge' ('merge' x y) z@
    --
    -- @'merge' x 'empty' = 'merge' 'empty' x = x@
    merge
        :: h n a -> h m a -> h (n + m) a