module Test.Credit.Heap.Pairing where

import Prettyprinter (Pretty)

import Control.Monad.Credit
import Test.Credit
import Test.Credit.Heap.Base

-- Binary pairing heaps as in Exercise 5.8 of Okasaki's book.

data PairingHeap a m
  = Nil
  | Heap a (PairingHeap a m) (PairingHeap a m)

-- | At the root, the right child is Empty.
data Pairing a m = Empty | Root a (PairingHeap a m)

link :: Ord a => Pairing a m -> Pairing a m -> Pairing a m
link :: forall {k} a (m :: k).
Ord a =>
Pairing a m -> Pairing a m -> Pairing a m
link Pairing a m
Empty Pairing a m
b = Pairing a m
b
link Pairing a m
a Pairing a m
Empty = Pairing a m
a
link (Root a
x PairingHeap a m
a) (Root a
y PairingHeap a m
b)
  | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y    = a -> PairingHeap a m -> Pairing a m
forall {k} a (m :: k). a -> PairingHeap a m -> Pairing a m
Root a
x (a -> PairingHeap a m -> PairingHeap a m -> PairingHeap a m
forall {k} a (m :: k).
a -> PairingHeap a m -> PairingHeap a m -> PairingHeap a m
Heap a
y PairingHeap a m
b PairingHeap a m
a)
  | Bool
otherwise = a -> PairingHeap a m -> Pairing a m
forall {k} a (m :: k). a -> PairingHeap a m -> Pairing a m
Root a
y (a -> PairingHeap a m -> PairingHeap a m -> PairingHeap a m
forall {k} a (m :: k).
a -> PairingHeap a m -> PairingHeap a m -> PairingHeap a m
Heap a
x PairingHeap a m
a PairingHeap a m
b)

mergePairs :: (MonadCredit m, Ord a) => PairingHeap a m -> m (Pairing a m)
mergePairs :: forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
PairingHeap a m -> m (Pairing a m)
mergePairs PairingHeap a m
Nil = Pairing a m -> m (Pairing a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pairing a m -> m (Pairing a m)) -> Pairing a m -> m (Pairing a m)
forall a b. (a -> b) -> a -> b
$ Pairing a m
forall {k} a (m :: k). Pairing a m
Empty
mergePairs (Heap a
x PairingHeap a m
a1 PairingHeap a m
Nil) = Pairing a m -> m (Pairing a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pairing a m -> m (Pairing a m)) -> Pairing a m -> m (Pairing a m)
forall a b. (a -> b) -> a -> b
$ a -> PairingHeap a m -> Pairing a m
forall {k} a (m :: k). a -> PairingHeap a m -> Pairing a m
Root a
x PairingHeap a m
a1
mergePairs (Heap a
x PairingHeap a m
a1 (Heap a
y PairingHeap a m
a2 PairingHeap a m
a3)) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m () -> m (Pairing a m) -> m (Pairing a m)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Pairing a m -> Pairing a m -> Pairing a m
forall {k} a (m :: k).
Ord a =>
Pairing a m -> Pairing a m -> Pairing a m
link ((Pairing a m -> Pairing a m -> Pairing a m
forall {k} a (m :: k).
Ord a =>
Pairing a m -> Pairing a m -> Pairing a m
link (a -> PairingHeap a m -> Pairing a m
forall {k} a (m :: k). a -> PairingHeap a m -> Pairing a m
Root a
x PairingHeap a m
a1) (a -> PairingHeap a m -> Pairing a m
forall {k} a (m :: k). a -> PairingHeap a m -> Pairing a m
Root a
y PairingHeap a m
a2))) (Pairing a m -> Pairing a m) -> m (Pairing a m) -> m (Pairing a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PairingHeap a m -> m (Pairing a m)
forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
PairingHeap a m -> m (Pairing a m)
mergePairs PairingHeap a m
a3

instance Heap Pairing where
  empty :: forall (m :: * -> *) a. MonadCredit m => m (Pairing a m)
empty = Pairing a m -> m (Pairing a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pairing a m
forall {k} a (m :: k). Pairing a m
Empty
  insert :: forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
a -> Pairing a m -> m (Pairing a m)
insert a
x Pairing a m
h = Pairing a m -> Pairing a m -> m (Pairing a m)
forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
Pairing a m -> Pairing a m -> m (Pairing a m)
forall (h :: * -> (* -> *) -> *) (m :: * -> *) a.
(Heap h, MonadCredit m, Ord a) =>
h a m -> h a m -> m (h a m)
merge (a -> PairingHeap a m -> Pairing a m
forall {k} a (m :: k). a -> PairingHeap a m -> Pairing a m
Root a
x PairingHeap a m
forall {k} a (m :: k). PairingHeap a m
Nil) Pairing a m
h
  merge :: forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
Pairing a m -> Pairing a m -> m (Pairing a m)
merge Pairing a m
a Pairing a m
b = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m () -> m (Pairing a m) -> m (Pairing a m)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Pairing a m -> m (Pairing a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pairing a m -> Pairing a m -> Pairing a m
forall {k} a (m :: k).
Ord a =>
Pairing a m -> Pairing a m -> Pairing a m
link Pairing a m
a Pairing a m
b)
  splitMin :: forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
Pairing a m -> m (Maybe (a, Pairing a m))
splitMin Pairing a m
Empty = Maybe (a, Pairing a m) -> m (Maybe (a, Pairing a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, Pairing a m)
forall a. Maybe a
Nothing
  splitMin (Root a
x PairingHeap a m
h) = (a, Pairing a m) -> Maybe (a, Pairing a m)
forall a. a -> Maybe a
Just ((a, Pairing a m) -> Maybe (a, Pairing a m))
-> (Pairing a m -> (a, Pairing a m))
-> Pairing a m
-> Maybe (a, Pairing a m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,) (Pairing a m -> Maybe (a, Pairing a m))
-> m (Pairing a m) -> m (Maybe (a, Pairing a m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PairingHeap a m -> m (Pairing a m)
forall (m :: * -> *) a.
(MonadCredit m, Ord a) =>
PairingHeap a m -> m (Pairing a m)
mergePairs PairingHeap a m
h

-- We can only prove a log(n) bound for insert, but this seems to work (as conjectured by Okasaki and others).
instance BoundedHeap Pairing where
  hcost :: forall a. Size -> HeapOp a -> Credit
hcost Size
n (Insert a
_) = Credit
1
  hcost Size
n HeapOp a
Merge = Credit
1
  hcost Size
n HeapOp a
SplitMin = Credit
5 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Size -> Credit
log2 (Size
n Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1)

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PairingHeap a m) where
  prettyCell :: PairingHeap a m -> m Memory
prettyCell PairingHeap a m
Nil = Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Nil" []
  prettyCell (Heap a
a PairingHeap a m
l PairingHeap a m
r) = do
    Memory
a' <- a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
a
    Memory
l' <- PairingHeap a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell PairingHeap a m
l
    Memory
r' <- PairingHeap a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell PairingHeap a m
r
    Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Heap" [Memory
a', Memory
l', Memory
r']

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Pairing a m) where
  prettyCell :: Pairing a m -> m Memory
prettyCell Pairing a m
Empty = Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Empty" []
  prettyCell (Root a
a PairingHeap a m
l) = do
    Memory
a' <- a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
a
    Memory
l' <- PairingHeap a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell PairingHeap a m
l
    Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Root" [Memory
a', Memory
l']

instance Pretty a => MemoryStructure (Pairing (PrettyCell a)) where
  prettyStructure :: forall (m :: * -> *).
MonadMemory m =>
Pairing (PrettyCell a) m -> m Memory
prettyStructure = Pairing (PrettyCell a) m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell