{-# LANGUAGE LambdaCase, GADTs #-}

module Test.Credit.Queue.Bankers where

import Control.Monad.Credit
import Data.Maybe (fromMaybe)
import Prettyprinter (Pretty)
import Test.Credit
import Test.Credit.Queue.Base
import Test.Credit.Queue.Streams

data BQueue a m = BQueue
  { forall a (m :: * -> *). BQueue a m -> Int
flen :: !Int
  , forall a (m :: * -> *). BQueue a m -> Int
rlen :: !Int
  , forall a (m :: * -> *). BQueue a m -> Stream m a
front :: Stream m a
  , forall a (m :: * -> *). BQueue a m -> Stream m a
rear  :: Stream m a
  }

allEvaluated :: MonadInherit m => StreamCell m a -> m ()
allEvaluated :: forall (m :: * -> *) a. MonadInherit m => StreamCell m a -> m ()
allEvaluated StreamCell m a
SNil = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
allEvaluated (SCons a
_ Stream m a
xs) = Stream m a -> m ()
forall (m :: * -> *) a. MonadInherit m => Stream m a -> m ()
isEvaluated Stream m a
xs

isEvaluated :: MonadInherit m => Stream m a -> m ()
isEvaluated :: forall (m :: * -> *) a. MonadInherit m => Stream m a -> m ()
isEvaluated Stream m a
s = Stream m a
-> (StreamCell m a -> m ())
-> (SLazyCon m (StreamCell m a) -> m ())
-> m ()
forall (m :: * -> *) (t :: * -> *) a b.
MonadLazy m =>
Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
forall (t :: * -> *) a b.
Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
lazymatch Stream m a
s StreamCell m a -> m ()
forall (m :: * -> *) a. MonadInherit m => StreamCell m a -> m ()
allEvaluated ([Char] -> SLazyCon m (StreamCell m a) -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Stream should be pure")

allInvariant :: MonadInherit m => Maybe Int -> StreamCell m a -> m ()
allInvariant :: forall (m :: * -> *) a.
MonadInherit m =>
Maybe Int -> StreamCell m a -> m ()
allInvariant Maybe Int
_ StreamCell m a
SNil = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
allInvariant Maybe Int
rlen (SCons a
x Stream m a
xs) = Stream m a -> Maybe Int -> m ()
forall (m :: * -> *) a.
MonadInherit m =>
Stream m a -> Maybe Int -> m ()
invariant Stream m a
xs ((Int -> Int) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
2) Maybe Int
rlen)

invariant :: MonadInherit m => Stream m a -> Maybe Int -> m ()
invariant :: forall (m :: * -> *) a.
MonadInherit m =>
Stream m a -> Maybe Int -> m ()
invariant Stream m a
front Maybe Int
rlen = 
  Stream m a
-> (StreamCell m a -> m ())
-> (SLazyCon m (StreamCell m a) -> m ())
-> m ()
forall (m :: * -> *) (t :: * -> *) a b.
MonadLazy m =>
Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
forall (t :: * -> *) a b.
Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
lazymatch Stream m a
front (Maybe Int -> StreamCell m a -> m ()
forall (m :: * -> *) a.
MonadInherit m =>
Maybe Int -> StreamCell m a -> m ()
allInvariant Maybe Int
rlen) ((SLazyCon m (StreamCell m a) -> m ()) -> m ())
-> (SLazyCon m (StreamCell m a) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \case
    SAppend Stream m a1
xs Stream m a1
ys -> do
      Int
lxs <- Stream m a1 -> m Int
forall (m :: * -> *) a. MonadLazy m => Stream m a -> m Int
slength Stream m a1
xs
      Int
lys <- Stream m a1 -> m Int
forall (m :: * -> *) a. MonadLazy m => Stream m a -> m Int
slength Stream m a1
ys
      Stream m a
front 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 -> Credit) -> Int -> Credit
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
lxs) Maybe Int
rlen)
      Stream m a1 -> Maybe Int -> m ()
forall (m :: * -> *) a.
MonadInherit m =>
Stream m a -> Maybe Int -> m ()
invariant Stream m a1
xs Maybe Int
forall a. Maybe a
Nothing
      Stream m a1
ys Stream m a1 -> 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 -> Credit) -> Int -> Credit
forall a b. (a -> b) -> a -> b
$ Int
lys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lxs)
    SReverse Stream m a1
xs Stream m a1
ys -> do
      Int
lxs <- Stream m a1 -> m Int
forall (m :: * -> *) a. MonadLazy m => Stream m a -> m Int
slength Stream m a1
xs
      Stream m a
front 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
lxs)
      Stream m a1 -> m ()
forall (m :: * -> *) a. MonadInherit m => Stream m a -> m ()
isEvaluated Stream m a1
xs
      Stream m a1 -> m ()
forall (m :: * -> *) a. MonadInherit m => Stream m a -> m ()
isEvaluated Stream m a1
ys

bqueue :: MonadInherit m => Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
bqueue :: forall (m :: * -> *) a.
MonadInherit m =>
Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
bqueue Int
fl Int
rl Stream m a
f Stream m a
r = do
  Stream m a -> m ()
forall (m :: * -> *) a. MonadInherit m => Stream m a -> m ()
isEvaluated Stream m a
r
  Stream m a -> Maybe Int -> m ()
forall (m :: * -> *) a.
MonadInherit m =>
Stream m a -> Maybe Int -> m ()
invariant Stream m a
f (Int -> Maybe Int
forall a. a -> Maybe a
Just 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
$ Int -> Int -> Stream m a -> Stream m a -> BQueue a m
forall a (m :: * -> *).
Int -> Int -> Stream m a -> Stream m a -> BQueue a m
BQueue Int
fl Int
rl Stream m a
f Stream m a
r
    else do
      Stream m a
r' <- SLazyCon m (StreamCell m a) -> 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 (SLazyCon m (StreamCell m a) -> m (Stream m a))
-> (Stream m a -> SLazyCon m (StreamCell m a))
-> Stream m a
-> m (Stream m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stream m a -> Stream m a -> SLazyCon m (StreamCell m a)
forall (m :: * -> *) a1.
Stream m a1 -> Stream m a1 -> SLazyCon m (StreamCell m a1)
SReverse Stream m a
r (Stream m a -> m (Stream m a)) -> m (Stream m a) -> m (Stream m a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (Stream m a)
forall (m :: * -> *) a. MonadLazy m => m (Stream m a)
nil
      Stream m a
r' 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
      Int -> Int -> Stream m a -> Stream m a -> BQueue a m
forall a (m :: * -> *).
Int -> Int -> Stream m a -> Stream m a -> BQueue a m
BQueue (Int
fl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
rl) Int
0 (Stream m a -> Stream m a -> BQueue a m)
-> m (Stream m a) -> m (Stream m a -> BQueue a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SLazyCon m (StreamCell m a) -> 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 (SLazyCon m (StreamCell m a) -> m (Stream m a))
-> SLazyCon m (StreamCell m a) -> m (Stream m a)
forall a b. (a -> b) -> a -> b
$ Stream m a -> Stream m a -> SLazyCon m (StreamCell m a)
forall (m :: * -> *) a1.
Stream m a1 -> Stream m a1 -> SLazyCon m (StreamCell m a1)
SAppend Stream m a
f Stream m a
r') m (Stream m a -> BQueue a m) -> m (Stream m a) -> m (BQueue a m)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Stream m a)
forall (m :: * -> *) a. MonadLazy m => m (Stream m a)
nil

instance Queue BQueue where
  empty :: forall (m :: * -> *) a. MonadLazy m => m (BQueue a m)
empty = Int -> Int -> Stream m a -> Stream m a -> BQueue a m
forall a (m :: * -> *).
Int -> Int -> Stream m a -> Stream m a -> BQueue a m
BQueue Int
0 Int
0 (Stream m a -> Stream m a -> BQueue a m)
-> m (Stream m a) -> m (Stream m a -> BQueue a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Stream m a)
forall (m :: * -> *) a. MonadLazy m => m (Stream m a)
nil m (Stream m a -> BQueue a m) -> m (Stream m a) -> m (BQueue a m)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Stream m a)
forall (m :: * -> *) a. MonadLazy m => m (Stream m a)
nil
  snoc :: forall (m :: * -> *) a.
MonadInherit m =>
BQueue a m -> a -> m (BQueue a m)
snoc (BQueue Int
fl Int
rl Stream m a
f Stream m a
r) a
x = do
    Stream m a
f 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
    Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
forall (m :: * -> *) a.
MonadInherit m =>
Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
bqueue Int
fl (Int
rl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Stream m a
f (Stream m a -> m (BQueue a m)) -> m (Stream m a) -> m (BQueue a m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> Stream m a -> m (Stream m a)
forall (m :: * -> *) a.
MonadLazy m =>
a -> Stream m a -> m (Stream m a)
cons a
x Stream m a
r
  uncons :: forall (m :: * -> *) a.
MonadInherit m =>
BQueue a m -> m (Maybe (a, BQueue a m))
uncons (BQueue Int
fl Int
rl Stream m a
f Stream m a
r) = do
    Stream m a
f 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
2
    Stream m a -> m (StreamCell m a)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Stream m a
f m (StreamCell m a)
-> (StreamCell m a -> m (Maybe (a, BQueue a m)))
-> m (Maybe (a, BQueue 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
>>= \case
      SCons a
x Stream m a
f' -> do
        BQueue a m
q <- Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
forall (m :: * -> *) a.
MonadInherit m =>
Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
bqueue (Int
fl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
rl Stream m a
f' Stream m a
r
        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)
      StreamCell m a
SNil -> 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 Int
flen Int
rlen Stream m a
_ Stream m a
_) = 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 Int
fl Int
rl Stream m a
f Stream m a
r) = 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 Int
fl Int
rl Stream m a
f Stream m a
r) = do
    Memory
fl' <- Int -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Int
fl
    Memory
rl' <- Int -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Int
rl
    Memory
f' <- Stream m a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Stream m a
f
    Memory
r' <- Stream m a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Stream m 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
$ [Char] -> [Memory] -> Memory
mkMCell [Char]
"Queue" [Memory
fl', Memory
rl', Memory
f', Memory
r']

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