module Test.Credit.Queue.Batched where import Prettyprinter (Pretty) import Control.Monad.Credit import Test.Credit import Test.Credit.Queue.Base data Batched a m = Batched [a] [a] rev :: MonadCount m => [a] -> [a] -> m [a] rev :: forall (m :: * -> *) a. MonadCount m => [a] -> [a] -> m [a] rev [] [a] acc = [a] -> m [a] forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure [a] acc rev (a x : [a] xs) [a] acc = m () forall (m :: * -> *). MonadCount m => m () tick m () -> m [a] -> m [a] forall a b. m a -> m b -> m b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> [a] -> [a] -> m [a] forall (m :: * -> *) a. MonadCount m => [a] -> [a] -> m [a] rev [a] xs (a x a -> [a] -> [a] forall a. a -> [a] -> [a] : [a] acc) bqueue :: MonadCount m => Batched a m -> m (Batched a m) bqueue :: forall (m :: * -> *) a. MonadCount m => Batched a m -> m (Batched a m) bqueue (Batched [] [a] rear) = [a] -> [a] -> m [a] forall (m :: * -> *) a. MonadCount m => [a] -> [a] -> m [a] rev [a] rear [] m [a] -> ([a] -> m (Batched a m)) -> m (Batched 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 >>= \[a] f -> Batched a m -> m (Batched a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (Batched a m -> m (Batched a m)) -> Batched a m -> m (Batched a m) forall a b. (a -> b) -> a -> b $ [a] -> [a] -> Batched a m forall {k} a (m :: k). [a] -> [a] -> Batched a m Batched [a] f [] bqueue (Batched [a] front [a] rear) = Batched a m -> m (Batched a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (Batched a m -> m (Batched a m)) -> Batched a m -> m (Batched a m) forall a b. (a -> b) -> a -> b $ [a] -> [a] -> Batched a m forall {k} a (m :: k). [a] -> [a] -> Batched a m Batched [a] front [a] rear instance Queue Batched where empty :: forall (m :: * -> *) a. MonadInherit m => m (Batched a m) empty = Batched a m -> m (Batched a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (Batched a m -> m (Batched a m)) -> Batched a m -> m (Batched a m) forall a b. (a -> b) -> a -> b $ [a] -> [a] -> Batched a m forall {k} a (m :: k). [a] -> [a] -> Batched a m Batched [] [] snoc :: forall (m :: * -> *) a. MonadInherit m => Batched a m -> a -> m (Batched a m) snoc (Batched [a] front [a] rear) a x = Batched a m -> m (Batched a m) forall (m :: * -> *) a. MonadCount m => Batched a m -> m (Batched a m) bqueue ([a] -> [a] -> Batched a m forall {k} a (m :: k). [a] -> [a] -> Batched a m Batched [a] front (a x a -> [a] -> [a] forall a. a -> [a] -> [a] : [a] rear)) uncons :: forall (m :: * -> *) a. MonadInherit m => Batched a m -> m (Maybe (a, Batched a m)) uncons (Batched [] [a] rear) = Maybe (a, Batched a m) -> m (Maybe (a, Batched a m)) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe (a, Batched a m) forall a. Maybe a Nothing uncons (Batched (a x:[a] front) [a] rear) = (a, Batched a m) -> Maybe (a, Batched a m) forall a. a -> Maybe a Just ((a, Batched a m) -> Maybe (a, Batched a m)) -> (Batched a m -> (a, Batched a m)) -> Batched a m -> Maybe (a, Batched a m) forall b c a. (b -> c) -> (a -> b) -> a -> c . (a x,) (Batched a m -> Maybe (a, Batched a m)) -> m (Batched a m) -> m (Maybe (a, Batched a m)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Batched a m -> m (Batched a m) forall (m :: * -> *) a. MonadCount m => Batched a m -> m (Batched a m) bqueue ([a] -> [a] -> Batched a m forall {k} a (m :: k). [a] -> [a] -> Batched a m Batched [a] front [a] rear) instance BoundedQueue Batched where qcost :: forall a. Size -> QueueOp a -> Credit qcost Size n (Snoc a _) = Credit 1 qcost Size n QueueOp a Uncons = Size -> Credit linear Size n instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Batched a m) where prettyCell :: Batched a m -> m Memory prettyCell (Batched [a] f [a] r) = do Memory f' <- [a] -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell [a] f Memory r' <- [a] -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell [a] 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 "Queue" [Memory f', Memory r'] instance Pretty a => MemoryStructure (Batched (PrettyCell a)) where prettyStructure :: forall (m :: * -> *). MonadMemory m => Batched (PrettyCell a) m -> m Memory prettyStructure = Batched (PrettyCell a) m -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell