{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, UndecidableInstances #-}

module Test.Credit.Queue.Base where

import Control.Monad.Credit
import Prettyprinter
import Test.Credit
import Test.QuickCheck

data QueueOp a = Snoc a | Uncons
  deriving (QueueOp a -> QueueOp a -> Bool
(QueueOp a -> QueueOp a -> Bool)
-> (QueueOp a -> QueueOp a -> Bool) -> Eq (QueueOp a)
forall a. Eq a => QueueOp a -> QueueOp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => QueueOp a -> QueueOp a -> Bool
== :: QueueOp a -> QueueOp a -> Bool
$c/= :: forall a. Eq a => QueueOp a -> QueueOp a -> Bool
/= :: QueueOp a -> QueueOp a -> Bool
Eq, Eq (QueueOp a)
Eq (QueueOp a) =>
(QueueOp a -> QueueOp a -> Ordering)
-> (QueueOp a -> QueueOp a -> Bool)
-> (QueueOp a -> QueueOp a -> Bool)
-> (QueueOp a -> QueueOp a -> Bool)
-> (QueueOp a -> QueueOp a -> Bool)
-> (QueueOp a -> QueueOp a -> QueueOp a)
-> (QueueOp a -> QueueOp a -> QueueOp a)
-> Ord (QueueOp a)
QueueOp a -> QueueOp a -> Bool
QueueOp a -> QueueOp a -> Ordering
QueueOp a -> QueueOp a -> QueueOp 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 (QueueOp a)
forall a. Ord a => QueueOp a -> QueueOp a -> Bool
forall a. Ord a => QueueOp a -> QueueOp a -> Ordering
forall a. Ord a => QueueOp a -> QueueOp a -> QueueOp a
$ccompare :: forall a. Ord a => QueueOp a -> QueueOp a -> Ordering
compare :: QueueOp a -> QueueOp a -> Ordering
$c< :: forall a. Ord a => QueueOp a -> QueueOp a -> Bool
< :: QueueOp a -> QueueOp a -> Bool
$c<= :: forall a. Ord a => QueueOp a -> QueueOp a -> Bool
<= :: QueueOp a -> QueueOp a -> Bool
$c> :: forall a. Ord a => QueueOp a -> QueueOp a -> Bool
> :: QueueOp a -> QueueOp a -> Bool
$c>= :: forall a. Ord a => QueueOp a -> QueueOp a -> Bool
>= :: QueueOp a -> QueueOp a -> Bool
$cmax :: forall a. Ord a => QueueOp a -> QueueOp a -> QueueOp a
max :: QueueOp a -> QueueOp a -> QueueOp a
$cmin :: forall a. Ord a => QueueOp a -> QueueOp a -> QueueOp a
min :: QueueOp a -> QueueOp a -> QueueOp a
Ord, Int -> QueueOp a -> ShowS
[QueueOp a] -> ShowS
QueueOp a -> String
(Int -> QueueOp a -> ShowS)
-> (QueueOp a -> String)
-> ([QueueOp a] -> ShowS)
-> Show (QueueOp a)
forall a. Show a => Int -> QueueOp a -> ShowS
forall a. Show a => [QueueOp a] -> ShowS
forall a. Show a => QueueOp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> QueueOp a -> ShowS
showsPrec :: Int -> QueueOp a -> ShowS
$cshow :: forall a. Show a => QueueOp a -> String
show :: QueueOp a -> String
$cshowList :: forall a. Show a => [QueueOp a] -> ShowS
showList :: [QueueOp a] -> ShowS
Show)

instance Arbitrary a => Arbitrary (QueueOp a) where
  arbitrary :: Gen (QueueOp a)
arbitrary = [(Int, Gen (QueueOp a))] -> Gen (QueueOp a)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
7, a -> QueueOp a
forall a. a -> QueueOp a
Snoc (a -> QueueOp a) -> Gen a -> Gen (QueueOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
arbitrary)
    , (Int
3, QueueOp a -> Gen (QueueOp a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QueueOp a
forall a. QueueOp a
Uncons)
    ]

class Queue q where
  empty :: MonadInherit m => m (q a m)
  snoc :: MonadInherit m => q a m -> a -> m (q a m)
  uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))

class Queue q => BoundedQueue q where
  qcost :: Size -> QueueOp a -> Credit

data Q q a m = E | Q Size (q (PrettyCell a) m)

instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (Q q a) where
  prettyStructure :: forall (m :: * -> *). MonadMemory m => Q q a m -> m Memory
prettyStructure Q q 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 (Q Size
_ q (PrettyCell a) m
q) = q (PrettyCell a) m -> m Memory
forall (m :: * -> *).
MonadMemory m =>
q (PrettyCell a) m -> m Memory
forall (t :: (* -> *) -> *) (m :: * -> *).
(MemoryStructure t, MonadMemory m) =>
t m -> m Memory
prettyStructure q (PrettyCell a) m
q

act :: (MonadInherit m, Queue q) => Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
act :: forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Queue q) =>
Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
act Size
sz q (PrettyCell a) m
q (Snoc a
x) = Size -> q (PrettyCell a) m -> Q q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> Q q a m
Q (Size
sz Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) (q (PrettyCell a) m -> Q q a m)
-> m (q (PrettyCell a) m) -> m (Q q a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> q (PrettyCell a) m -> PrettyCell a -> m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadInherit m => q a m -> a -> m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Queue q, MonadInherit m) =>
q a m -> a -> m (q a m)
snoc q (PrettyCell a) m
q (a -> PrettyCell a
forall a. a -> PrettyCell a
PrettyCell a
x)
act Size
sz q (PrettyCell a) m
q QueueOp a
Uncons = do
  Maybe (PrettyCell a, q (PrettyCell a) m)
m <- q (PrettyCell a) m -> m (Maybe (PrettyCell a, q (PrettyCell a) m))
forall (m :: * -> *) a.
MonadInherit m =>
q a m -> m (Maybe (a, q a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Queue q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
uncons q (PrettyCell a) m
q
  case Maybe (PrettyCell a, q (PrettyCell a) m)
m of
    Maybe (PrettyCell a, q (PrettyCell a) m)
Nothing -> Q q a m -> m (Q q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Q q a m
forall {k} (q :: * -> k -> *) a (m :: k). Q q a m
E
    Just (PrettyCell a
_, q (PrettyCell a) m
q') -> Q q a m -> m (Q q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Q q a m -> m (Q q a m)) -> Q q a m -> m (Q q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> Q q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> Q q a m
Q (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)) q (PrettyCell a) m
q'

instance (Arbitrary a, BoundedQueue q, Show a) => DataStructure (Q q a) (QueueOp a) where
  create :: forall (m :: * -> *). MonadInherit m => Q q a m
create = Q q a m
forall {k} (q :: * -> k -> *) a (m :: k). Q q a m
E
  action :: forall (m :: * -> *).
MonadInherit m =>
Q q a m -> QueueOp a -> (Credit, m (Q q a m))
action Q q a m
E QueueOp a
op = (forall (q :: * -> (* -> *) -> *) a.
BoundedQueue q =>
Size -> QueueOp a -> Credit
qcost @q Size
0 QueueOp a
op, m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadInherit m => m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Queue q, MonadInherit m) =>
m (q a m)
empty m (q (PrettyCell a) m)
-> (q (PrettyCell a) m -> m (Q q a m)) -> m (Q q 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
>>= (q (PrettyCell a) m -> QueueOp a -> m (Q q a m))
-> QueueOp a -> q (PrettyCell a) m -> m (Q q a m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Queue q) =>
Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
act Size
0) QueueOp a
op)
  action (Q Size
sz q (PrettyCell a) m
q) QueueOp a
op = (forall (q :: * -> (* -> *) -> *) a.
BoundedQueue q =>
Size -> QueueOp a -> Credit
qcost @q Size
sz QueueOp a
op, Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Queue q) =>
Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
act Size
sz q (PrettyCell a) m
q QueueOp a
op)