module Test.Credit.Queue.Bankers where import Prettyprinter (Pretty) import Control.Monad.Credit import Test.Credit import Test.Credit.Queue.Base import Test.Credit.Queue.Streams data BQueue a m = BQueue { forall a (m :: * -> *). BQueue a m -> Stream m a front :: Stream m a , forall a (m :: * -> *). BQueue a m -> Int flen :: !Int , forall a (m :: * -> *). BQueue a m -> Stream m a rear :: Stream m a , forall a (m :: * -> *). BQueue a m -> Int rlen :: !Int } bqueue :: MonadInherit m => BQueue a m -> m (BQueue a m) bqueue :: forall (m :: * -> *) a. MonadInherit m => BQueue a m -> m (BQueue a m) bqueue (BQueue Stream m a f Int fl Stream m a r Int rl) = do Stream m a -> (SThunk m (Stream m a) -> m ()) -> m () forall (m :: * -> *) a. Monad m => Stream m a -> (SThunk m (Stream m a) -> m ()) -> m () ifIndirect Stream m a f (SThunk m (Stream m a) -> Credit -> m () forall (m :: * -> *) (t :: * -> *) a. MonadCredit m => Thunk m t a -> Credit -> m () forall (t :: * -> *) a. Thunk m t a -> Credit -> m () `hasAtLeast` Int -> Credit forall a b. (Integral a, Num b) => a -> b fromIntegral Int rl) if Int fl Int -> Int -> Bool forall a. Ord a => a -> a -> Bool >= Int rl then BQueue a m -> m (BQueue a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (BQueue a m -> m (BQueue a m)) -> BQueue a m -> m (BQueue a m) forall a b. (a -> b) -> a -> b $ Stream m a -> Int -> Stream m a -> Int -> BQueue a m forall a (m :: * -> *). Stream m a -> Int -> Stream m a -> Int -> BQueue a m BQueue Stream m a f Int fl Stream m a r Int rl else do SThunk m (Stream m a) r' <- SLazyCon m (Stream m a) -> m (SThunk m (Stream m a)) forall (m :: * -> *) (t :: * -> *) a. MonadLazy m => t a -> m (Thunk m t a) forall (t :: * -> *) a. t a -> m (Thunk m t a) delay (Stream m a -> Stream m a -> SLazyCon m (Stream m a) forall (m :: * -> *) a1. Stream m a1 -> Stream m a1 -> SLazyCon m (Stream m a1) SReverse Stream m a r Stream m a forall (m :: * -> *) a. Stream m a SNil) SThunk m (Stream m a) r' SThunk m (Stream m a) -> Credit -> m () forall (m :: * -> *) (t :: * -> *) a. MonadCredit m => Thunk m t a -> Credit -> m () forall (t :: * -> *) a. Thunk m t a -> Credit -> m () `creditWith` Credit 1 SThunk m (Stream m a) f' <- SLazyCon m (Stream m a) -> m (SThunk m (Stream m a)) forall (m :: * -> *) (t :: * -> *) a. MonadLazy m => t a -> m (Thunk m t a) forall (t :: * -> *) a. t a -> m (Thunk m t a) delay (Stream m a -> Stream m a -> SLazyCon m (Stream m a) forall (m :: * -> *) a1. Stream m a1 -> Stream m a1 -> SLazyCon m (Stream m a1) SAppend Stream m a f (SThunk m (Stream m a) -> Stream m a forall (m :: * -> *) a. SThunk m (Stream m a) -> Stream m a SIndirect SThunk m (Stream m a) r')) BQueue a m -> m (BQueue a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (BQueue a m -> m (BQueue a m)) -> BQueue a m -> m (BQueue a m) forall a b. (a -> b) -> a -> b $ Stream m a -> Int -> Stream m a -> Int -> BQueue a m forall a (m :: * -> *). Stream m a -> Int -> Stream m a -> Int -> BQueue a m BQueue (SThunk m (Stream m a) -> Stream m a forall (m :: * -> *) a. SThunk m (Stream m a) -> Stream m a SIndirect SThunk m (Stream m a) f') (Int fl Int -> Int -> Int forall a. Num a => a -> a -> a + Int rl) Stream m a forall (m :: * -> *) a. Stream m a SNil Int 0 instance Queue BQueue where empty :: forall (m :: * -> *) a. MonadInherit m => m (BQueue a m) empty = BQueue a m -> m (BQueue a m) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (BQueue a m -> m (BQueue a m)) -> BQueue a m -> m (BQueue a m) forall a b. (a -> b) -> a -> b $ Stream m a -> Int -> Stream m a -> Int -> BQueue a m forall a (m :: * -> *). Stream m a -> Int -> Stream m a -> Int -> BQueue a m BQueue Stream m a forall (m :: * -> *) a. Stream m a SNil Int 0 Stream m a forall (m :: * -> *) a. Stream m a SNil Int 0 snoc :: forall (m :: * -> *) a. MonadInherit m => BQueue a m -> a -> m (BQueue a m) snoc (BQueue Stream m a f Int fl Stream m a r Int rl) a x = do Stream m a -> m () forall (m :: * -> *) a. MonadInherit m => Stream m a -> m () credit Stream m a f BQueue a m -> m (BQueue a m) forall (m :: * -> *) a. MonadInherit m => BQueue a m -> m (BQueue a m) bqueue (Stream m a -> Int -> Stream m a -> Int -> BQueue a m forall a (m :: * -> *). Stream m a -> Int -> Stream m a -> Int -> BQueue a m BQueue Stream m a f Int fl (a -> Stream m a -> Stream m a forall (m :: * -> *) a. a -> Stream m a -> Stream m a SCons a x Stream m a r) (Int rl Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1)) uncons :: forall (m :: * -> *) a. MonadInherit m => BQueue a m -> m (Maybe (a, BQueue a m)) uncons (BQueue Stream m a f Int fl Stream m a r Int rl) = do Stream m a -> m () forall (m :: * -> *) a. MonadInherit m => Stream m a -> m () credit Stream m a f m () -> m () -> m () forall a b. m a -> m b -> m b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> Stream m a -> m () forall (m :: * -> *) a. MonadInherit m => Stream m a -> m () credit Stream m a f Stream m a -> (a -> Stream m a -> m (Maybe (a, BQueue a m))) -> m (Maybe (a, BQueue a m)) -> m (Maybe (a, BQueue a m)) forall (m :: * -> *) a b. MonadInherit m => Stream m a -> (a -> Stream m a -> m b) -> m b -> m b smatch Stream m a f (\a x Stream m a f -> do BQueue a m q <- BQueue a m -> m (BQueue a m) forall (m :: * -> *) a. MonadInherit m => BQueue a m -> m (BQueue a m) bqueue (Stream m a -> Int -> Stream m a -> Int -> BQueue a m forall a (m :: * -> *). Stream m a -> Int -> Stream m a -> Int -> BQueue a m BQueue Stream m a f (Int fl Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) Stream m a r Int rl) Maybe (a, BQueue a m) -> m (Maybe (a, BQueue a m)) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure (Maybe (a, BQueue a m) -> m (Maybe (a, BQueue a m))) -> Maybe (a, BQueue a m) -> m (Maybe (a, BQueue a m)) forall a b. (a -> b) -> a -> b $ (a, BQueue a m) -> Maybe (a, BQueue a m) forall a. a -> Maybe a Just (a x, BQueue a m q)) (Maybe (a, BQueue a m) -> m (Maybe (a, BQueue a m)) forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe (a, BQueue a m) forall a. Maybe a Nothing) isEmpty :: BQueue a m -> Bool isEmpty :: forall a (m :: * -> *). BQueue a m -> Bool isEmpty (BQueue Stream m a _ Int flen Stream m a _ Int rlen) = Int flen Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int 0 Bool -> Bool -> Bool && Int rlen Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int 0 lazyqueue :: MonadInherit m => BQueue a m -> m [a] lazyqueue :: forall (m :: * -> *) a. MonadInherit m => BQueue a m -> m [a] lazyqueue (BQueue Stream m a f Int fl Stream m a r Int rl) = do [a] f' <- Stream m a -> m [a] forall (m :: * -> *) a. MonadLazy m => Stream m a -> m [a] toList Stream m a f [a] r' <- Stream m a -> m [a] forall (m :: * -> *) a. MonadLazy m => Stream m a -> m [a] toList Stream m a r [a] -> m [a] forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure ([a] -> m [a]) -> [a] -> m [a] forall a b. (a -> b) -> a -> b $ [a] f' [a] -> [a] -> [a] forall a. [a] -> [a] -> [a] ++ [a] -> [a] forall a. [a] -> [a] reverse [a] r' instance BoundedQueue BQueue where qcost :: forall a. Size -> QueueOp a -> Credit qcost Size _ (Snoc a _) = Credit 2 qcost Size _ QueueOp a Uncons = Credit 4 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BQueue a m) where prettyCell :: BQueue a m -> m Memory prettyCell (BQueue Stream m a f Int fl Stream m a r Int rl) = do Memory f' <- Stream m a -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell Stream m a f Memory fl' <- Int -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell Int fl Memory r' <- Stream m a -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell Stream m a r Memory rl' <- Int -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell Int rl 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 fl', Memory r', Memory rl'] instance Pretty a => MemoryStructure (BQueue (PrettyCell a)) where prettyStructure :: forall (m :: * -> *). MonadMemory m => BQueue (PrettyCell a) m -> m Memory prettyStructure = BQueue (PrettyCell a) m -> m Memory forall (m :: * -> *) a. MemoryCell m a => a -> m Memory prettyCell