{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-} module Test.Credit.Heap.Base (HeapOp(..), Heap(..), BoundedHeap(..), H, BH) where import Control.Monad.Credit import Test.Credit import Test.QuickCheck data HeapOp a = Insert a | Merge | SplitMin deriving (HeapOp a -> HeapOp a -> Bool (HeapOp a -> HeapOp a -> Bool) -> (HeapOp a -> HeapOp a -> Bool) -> Eq (HeapOp a) forall a. Eq a => HeapOp a -> HeapOp a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: forall a. Eq a => HeapOp a -> HeapOp a -> Bool == :: HeapOp a -> HeapOp a -> Bool $c/= :: forall a. Eq a => HeapOp a -> HeapOp a -> Bool /= :: HeapOp a -> HeapOp a -> Bool Eq, Eq (HeapOp a) Eq (HeapOp a) => (HeapOp a -> HeapOp a -> Ordering) -> (HeapOp a -> HeapOp a -> Bool) -> (HeapOp a -> HeapOp a -> Bool) -> (HeapOp a -> HeapOp a -> Bool) -> (HeapOp a -> HeapOp a -> Bool) -> (HeapOp a -> HeapOp a -> HeapOp a) -> (HeapOp a -> HeapOp a -> HeapOp a) -> Ord (HeapOp a) HeapOp a -> HeapOp a -> Bool HeapOp a -> HeapOp a -> Ordering HeapOp a -> HeapOp a -> HeapOp a forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall a. Ord a => Eq (HeapOp a) forall a. Ord a => HeapOp a -> HeapOp a -> Bool forall a. Ord a => HeapOp a -> HeapOp a -> Ordering forall a. Ord a => HeapOp a -> HeapOp a -> HeapOp a $ccompare :: forall a. Ord a => HeapOp a -> HeapOp a -> Ordering compare :: HeapOp a -> HeapOp a -> Ordering $c< :: forall a. Ord a => HeapOp a -> HeapOp a -> Bool < :: HeapOp a -> HeapOp a -> Bool $c<= :: forall a. Ord a => HeapOp a -> HeapOp a -> Bool <= :: HeapOp a -> HeapOp a -> Bool $c> :: forall a. Ord a => HeapOp a -> HeapOp a -> Bool > :: HeapOp a -> HeapOp a -> Bool $c>= :: forall a. Ord a => HeapOp a -> HeapOp a -> Bool >= :: HeapOp a -> HeapOp a -> Bool $cmax :: forall a. Ord a => HeapOp a -> HeapOp a -> HeapOp a max :: HeapOp a -> HeapOp a -> HeapOp a $cmin :: forall a. Ord a => HeapOp a -> HeapOp a -> HeapOp a min :: HeapOp a -> HeapOp a -> HeapOp a Ord, Int -> HeapOp a -> ShowS [HeapOp a] -> ShowS HeapOp a -> String (Int -> HeapOp a -> ShowS) -> (HeapOp a -> String) -> ([HeapOp a] -> ShowS) -> Show (HeapOp a) forall a. Show a => Int -> HeapOp a -> ShowS forall a. Show a => [HeapOp a] -> ShowS forall a. Show a => HeapOp a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: forall a. Show a => Int -> HeapOp a -> ShowS showsPrec :: Int -> HeapOp a -> ShowS $cshow :: forall a. Show a => HeapOp a -> String show :: HeapOp a -> String $cshowList :: forall a. Show a => [HeapOp a] -> ShowS showList :: [HeapOp a] -> ShowS Show) instance Arbitrary a => Arbitrary (HeapOp a) where arbitrary :: Gen (HeapOp a) arbitrary = [(Int, Gen (HeapOp a))] -> Gen (HeapOp a) forall a. HasCallStack => [(Int, Gen a)] -> Gen a frequency [ (Int 6, a -> HeapOp a forall a. a -> HeapOp a Insert (a -> HeapOp a) -> Gen a -> Gen (HeapOp a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Gen a forall a. Arbitrary a => Gen a arbitrary) , (Int 3, HeapOp a -> Gen (HeapOp a) forall a. a -> Gen a forall (f :: * -> *) a. Applicative f => a -> f a pure HeapOp a forall a. HeapOp a SplitMin) , (Int 1, HeapOp a -> Gen (HeapOp a) forall a. a -> Gen a forall (f :: * -> *) a. Applicative f => a -> f a pure HeapOp a forall a. HeapOp a Merge) ] class Heap h where empty :: MonadCredit m => m (h a m) insert :: MonadCredit m => Ord a => a -> h a m -> m (h a m) merge :: MonadCredit m => Ord a => h a m -> h a m -> m (h a m) splitMin :: MonadCredit m => Ord a => h a m -> m (Maybe (a, h a m)) class Heap h => BoundedHeap h where hcost :: Size -> HeapOp a -> Credit data H h a m = E | H Size (h (PrettyCell a) m) instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (H h a m) where prettyCell :: H h a m -> m Memory prettyCell H h a m E = 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 "" [] prettyCell (H Size _ h (PrettyCell a) m h) = h (PrettyCell a) m -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell h (PrettyCell a) m h instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (H h a) where prettyStructure :: forall (m :: * -> *). MonadMemory m => H h a m -> m Memory prettyStructure H h a m E = 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 "" [] prettyStructure (H Size _ h (PrettyCell a) m h) = h (PrettyCell a) m -> m Memory forall (m :: * -> *). MonadMemory m => h (PrettyCell a) m -> m Memory forall (t :: (* -> *) -> *) (m :: * -> *). (MemoryStructure t, MonadMemory m) => t m -> m Memory prettyStructure h (PrettyCell a) m h act :: (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) act :: forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) act Size sz h (PrettyCell a) m h (Insert a x) = Size -> h (PrettyCell a) m -> H h a m forall {k} (h :: * -> k -> *) a (m :: k). Size -> h (PrettyCell a) m -> H h a m H (Size sz Size -> Size -> Size forall a. Num a => a -> a -> a + Size 1) (h (PrettyCell a) m -> H h a m) -> m (h (PrettyCell a) m) -> m (H h a m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> PrettyCell a -> h (PrettyCell a) m -> m (h (PrettyCell a) m) forall (m :: * -> *) a. (MonadCredit m, Ord a) => a -> h a m -> m (h a m) forall (h :: * -> (* -> *) -> *) (m :: * -> *) a. (Heap h, MonadCredit m, Ord a) => a -> h a m -> m (h a m) insert (a -> PrettyCell a forall a. a -> PrettyCell a PrettyCell a x) h (PrettyCell a) m h act Size sz h (PrettyCell a) m h HeapOp a Merge = H h a m -> m (H h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (H h a m -> m (H h a m)) -> H h a m -> m (H h a m) forall a b. (a -> b) -> a -> b $ Size -> h (PrettyCell a) m -> H h a m forall {k} (h :: * -> k -> *) a (m :: k). Size -> h (PrettyCell a) m -> H h a m H Size sz h (PrettyCell a) m h act Size sz h (PrettyCell a) m h HeapOp a SplitMin = do Maybe (PrettyCell a, h (PrettyCell a) m) m <- h (PrettyCell a) m -> m (Maybe (PrettyCell a, h (PrettyCell a) m)) forall (m :: * -> *) a. (MonadCredit m, Ord a) => h a m -> m (Maybe (a, h a m)) forall (h :: * -> (* -> *) -> *) (m :: * -> *) a. (Heap h, MonadCredit m, Ord a) => h a m -> m (Maybe (a, h a m)) splitMin h (PrettyCell a) m h case Maybe (PrettyCell a, h (PrettyCell a) m) m of Maybe (PrettyCell a, h (PrettyCell a) m) Nothing -> H h a m -> m (H h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure H h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m E Just (PrettyCell a _, h (PrettyCell a) m h') -> H h a m -> m (H h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (H h a m -> m (H h a m)) -> H h a m -> m (H h a m) forall a b. (a -> b) -> a -> b $ Size -> h (PrettyCell a) m -> H h a m forall {k} (h :: * -> k -> *) a (m :: k). Size -> h (PrettyCell a) m -> H h a m H (Size -> Size -> Size forall a. Ord a => a -> a -> a max Size 0 (Size sz Size -> Size -> Size forall a. Num a => a -> a -> a - Size 1)) h (PrettyCell a) m h' instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (H h a) (HeapOp a) where create :: forall (m :: * -> *). MonadInherit m => H h a m create = H h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m E action :: forall (m :: * -> *). MonadInherit m => H h a m -> HeapOp a -> (Credit, m (H h a m)) action H h a m E HeapOp a op = (forall (h :: * -> (* -> *) -> *) a. BoundedHeap h => Size -> HeapOp a -> Credit hcost @h Size 0 HeapOp a op, m (h (PrettyCell a) m) forall (m :: * -> *) a. MonadCredit m => m (h a m) forall (h :: * -> (* -> *) -> *) (m :: * -> *) a. (Heap h, MonadCredit m) => m (h a m) empty m (h (PrettyCell a) m) -> (h (PrettyCell a) m -> m (H h a m)) -> m (H h a m) forall a b. m a -> (a -> m b) -> m b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= (h (PrettyCell a) m -> HeapOp a -> m (H h a m)) -> HeapOp a -> h (PrettyCell a) m -> m (H h a m) forall a b c. (a -> b -> c) -> b -> a -> c flip (Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) act Size 0) HeapOp a op) action (H Size sz h (PrettyCell a) m h) HeapOp a op = (forall (h :: * -> (* -> *) -> *) a. BoundedHeap h => Size -> HeapOp a -> Credit hcost @h Size sz HeapOp a op, Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) act Size sz h (PrettyCell a) m h HeapOp a op) size :: H h a m -> Size size :: forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m E = Size 0 size (H Size sz h (PrettyCell a) m _) = Size sz data BH h a m = BH (H h a m) (H h a m) instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (BH h a m) where prettyCell :: BH h a m -> m Memory prettyCell (BH H h a m h1 H h a m h2) = do Memory h1' <- H h a m -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell H h a m h1 Memory h2' <- H h a m -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell H h a m h2 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 "Merge" [Memory h1', Memory h2'] instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (BH h a) where prettyStructure :: forall (m :: * -> *). MonadMemory m => BH h a m -> m Memory prettyStructure (BH H h a m h1 H h a m h2) = do Memory h1' <- H h a m -> m Memory forall (m :: * -> *). MonadMemory m => H h a m -> m Memory forall (t :: (* -> *) -> *) (m :: * -> *). (MemoryStructure t, MonadMemory m) => t m -> m Memory prettyStructure H h a m h1 Memory h2' <- H h a m -> m Memory forall (m :: * -> *). MonadMemory m => H h a m -> m Memory forall (t :: (* -> *) -> *) (m :: * -> *). (MemoryStructure t, MonadMemory m) => t m -> m Memory prettyStructure H h a m h2 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 "Merge" [Memory h1', Memory h2'] act1 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m) act1 :: forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m) act1 HeapOp a op (BH H h a m h1 H h a m h2) = do h (PrettyCell a) m h1' <- case H h a m h1 of H h a m E -> m (h (PrettyCell a) m) forall (m :: * -> *) a. MonadCredit m => m (h a m) forall (h :: * -> (* -> *) -> *) (m :: * -> *) a. (Heap h, MonadCredit m) => m (h a m) empty H Size _ h (PrettyCell a) m h -> h (PrettyCell a) m -> m (h (PrettyCell a) m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure h (PrettyCell a) m h H h a m h1'' <- Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) act (H h a m -> Size forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m h1) h (PrettyCell a) m h1' HeapOp a op BH h a m -> m (BH h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (BH h a m -> m (BH h a m)) -> BH h a m -> m (BH h a m) forall a b. (a -> b) -> a -> b $ H h a m -> H h a m -> BH h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> H h a m -> BH h a m BH H h a m h1'' H h a m h2 act2 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m) act2 :: forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m) act2 HeapOp a op (BH H h a m h1 H h a m h2) = do h (PrettyCell a) m h2' <- case H h a m h2 of H h a m E -> m (h (PrettyCell a) m) forall (m :: * -> *) a. MonadCredit m => m (h a m) forall (h :: * -> (* -> *) -> *) (m :: * -> *) a. (Heap h, MonadCredit m) => m (h a m) empty H Size _ h (PrettyCell a) m h -> h (PrettyCell a) m -> m (h (PrettyCell a) m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure h (PrettyCell a) m h H h a m h2'' <- Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m) act (H h a m -> Size forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m h2) h (PrettyCell a) m h2' HeapOp a op BH h a m -> m (BH h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (BH h a m -> m (BH h a m)) -> BH h a m -> m (BH h a m) forall a b. (a -> b) -> a -> b $ H h a m -> H h a m -> BH h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> H h a m -> BH h a m BH H h a m h1 H h a m h2'' mergeH :: (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m) mergeH :: forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m) mergeH H h a m E H h a m E = H h a m -> m (H h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure H h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m E mergeH (H Size sz1 h (PrettyCell a) m h1) H h a m E = H h a m -> m (H h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (H h a m -> m (H h a m)) -> H h a m -> m (H h a m) forall a b. (a -> b) -> a -> b $ Size -> h (PrettyCell a) m -> H h a m forall {k} (h :: * -> k -> *) a (m :: k). Size -> h (PrettyCell a) m -> H h a m H Size sz1 h (PrettyCell a) m h1 mergeH H h a m E (H Size sz2 h (PrettyCell a) m h2) = H h a m -> m (H h a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (H h a m -> m (H h a m)) -> H h a m -> m (H h a m) forall a b. (a -> b) -> a -> b $ Size -> h (PrettyCell a) m -> H h a m forall {k} (h :: * -> k -> *) a (m :: k). Size -> h (PrettyCell a) m -> H h a m H Size sz2 h (PrettyCell a) m h2 mergeH (H Size sz1 h (PrettyCell a) m h1) (H Size sz2 h (PrettyCell a) m h2) = Size -> h (PrettyCell a) m -> H h a m forall {k} (h :: * -> k -> *) a (m :: k). Size -> h (PrettyCell a) m -> H h a m H (Size sz1 Size -> Size -> Size forall a. Num a => a -> a -> a + Size sz2) (h (PrettyCell a) m -> H h a m) -> m (h (PrettyCell a) m) -> m (H h a m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> h (PrettyCell a) m -> h (PrettyCell a) m -> m (h (PrettyCell a) m) forall (m :: * -> *) a. (MonadCredit m, Ord a) => h a m -> h a m -> m (h a m) forall (h :: * -> (* -> *) -> *) (m :: * -> *) a. (Heap h, MonadCredit m, Ord a) => h a m -> h a m -> m (h a m) merge h (PrettyCell a) m h1 h (PrettyCell a) m h2 instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (BH h a) (HeapOp a) where create :: forall (m :: * -> *). MonadInherit m => BH h a m create = H h a m -> H h a m -> BH h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> H h a m -> BH h a m BH H h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m E H h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m E action :: forall (m :: * -> *). MonadInherit m => BH h a m -> HeapOp a -> (Credit, m (BH h a m)) action (BH H h a m h1 H h a m h2) (Insert a a) = (forall (h :: * -> (* -> *) -> *) a. BoundedHeap h => Size -> HeapOp a -> Credit hcost @h (H h a m -> Size forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m h1) (a -> HeapOp a forall a. a -> HeapOp a Insert a a), HeapOp a -> BH h a m -> m (BH h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m) act1 (a -> HeapOp a forall a. a -> HeapOp a Insert a a) (H h a m -> H h a m -> BH h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> H h a m -> BH h a m BH H h a m h1 H h a m h2)) action (BH H h a m h1 H h a m h2) HeapOp a SplitMin = (forall (h :: * -> (* -> *) -> *) a. BoundedHeap h => Size -> HeapOp a -> Credit hcost @h (H h a m -> Size forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m h2) HeapOp Any forall a. HeapOp a SplitMin, HeapOp a -> BH h a m -> m (BH h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m) act2 HeapOp a forall a. HeapOp a SplitMin (H h a m -> H h a m -> BH h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> H h a m -> BH h a m BH H h a m h1 H h a m h2)) action (BH H h a m h1 H h a m h2) HeapOp a Merge = (forall (h :: * -> (* -> *) -> *) a. BoundedHeap h => Size -> HeapOp a -> Credit hcost @h (H h a m -> Size forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m h1 Size -> Size -> Size forall a. Num a => a -> a -> a + H h a m -> Size forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> Size size H h a m h2) HeapOp Any forall a. HeapOp a Merge, H h a m -> H h a m -> BH h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m -> H h a m -> BH h a m BH H h a m forall {k} (h :: * -> k -> *) a (m :: k). H h a m E (H h a m -> BH h a m) -> m (H h a m) -> m (BH h a m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> H h a m -> H h a m -> m (H h a m) forall (m :: * -> *) (h :: * -> (* -> *) -> *) a. (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m) mergeH H h a m h1 H h a m h2)