{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}

module Test.Credit.Deque.Base (DequeOp(..), Deque(..), BoundedDeque(..), D, BD) where

import Prelude hiding (concat)
import Control.Monad.Credit
import Test.Credit
import Test.QuickCheck

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

instance Arbitrary a => Arbitrary (DequeOp a) where
  arbitrary :: Gen (DequeOp a)
arbitrary = [(Int, Gen (DequeOp a))] -> Gen (DequeOp a)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
7, a -> DequeOp a
forall a. a -> DequeOp a
Cons (a -> DequeOp a) -> Gen a -> Gen (DequeOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
arbitrary)
    , (Int
4, a -> DequeOp a
forall a. a -> DequeOp a
Snoc (a -> DequeOp a) -> Gen a -> Gen (DequeOp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
arbitrary)
    , (Int
2, DequeOp a -> Gen (DequeOp a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DequeOp a
forall a. DequeOp a
Uncons)
    , (Int
6, DequeOp a -> Gen (DequeOp a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DequeOp a
forall a. DequeOp a
Unsnoc)
    , (Int
1, DequeOp a -> Gen (DequeOp a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DequeOp a
forall a. DequeOp a
Concat)
    ]

class Deque q where
  empty :: MonadInherit m => m (q a m)
  cons :: MonadInherit m => a -> q a 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))
  unsnoc :: MonadInherit m => q a m -> m (Maybe (q a m, a))
  concat :: MonadInherit m => q a m -> q a m -> m (q a m)

class Deque q => BoundedDeque q where
  qcost :: Size -> DequeOp a -> Credit

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

instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (D q a m) where
  prettyCell :: D q a m -> m Memory
prettyCell D 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
"" []
  prettyCell (D Size
_ q (PrettyCell a) m
q) = q (PrettyCell a) m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell q (PrettyCell a) m
q

instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (D q a) where
  prettyStructure :: forall (m :: * -> *). MonadMemory m => D q a m -> m Memory
prettyStructure D 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 (D 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, Deque q) => Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
act :: forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
act Size
sz q (PrettyCell a) m
q (Cons a
x) = Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D (Size
sz Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) (q (PrettyCell a) m -> D q a m)
-> m (q (PrettyCell a) m) -> m (D q a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrettyCell a -> q (PrettyCell a) m -> m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadInherit m => a -> q a m -> m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
cons (a -> PrettyCell a
forall a. a -> PrettyCell a
PrettyCell a
x) q (PrettyCell a) m
q
act Size
sz q (PrettyCell a) m
q (Snoc a
x) = Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D (Size
sz Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) (q (PrettyCell a) m -> D q a m)
-> m (q (PrettyCell a) m) -> m (D 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.
(Deque 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 DequeOp 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.
(Deque 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 -> D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure D q a m
forall {k} (q :: * -> k -> *) a (m :: k). D q a m
E
    Just (PrettyCell a
_, q (PrettyCell a) m
q') -> D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D q a m -> m (D q a m)) -> D q a m -> m (D q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D (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'
act Size
sz q (PrettyCell a) m
q DequeOp a
Unsnoc = do
  Maybe (q (PrettyCell a) m, PrettyCell a)
m <- q (PrettyCell a) m -> m (Maybe (q (PrettyCell a) m, PrettyCell a))
forall (m :: * -> *) a.
MonadInherit m =>
q a m -> m (Maybe (q a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
unsnoc q (PrettyCell a) m
q
  case Maybe (q (PrettyCell a) m, PrettyCell a)
m of
    Maybe (q (PrettyCell a) m, PrettyCell a)
Nothing -> D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure D q a m
forall {k} (q :: * -> k -> *) a (m :: k). D q a m
E
    Just (q (PrettyCell a) m
q', PrettyCell a
_) -> D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D q a m -> m (D q a m)) -> D q a m -> m (D q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D (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'
act Size
sz q (PrettyCell a) m
q DequeOp a
Concat = D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D q a m -> m (D q a m)) -> D q a m -> m (D q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D Size
sz q (PrettyCell a) m
q

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

size :: D q a m -> Size
size :: forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
E = Size
0
size (D Size
sz q (PrettyCell a) m
_) = Size
sz

data BD q a m = BD (D q a m) (D q a m)

instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (BD q a m) where
  prettyCell :: BD q a m -> m Memory
prettyCell (BD D q a m
q1 D q a m
q2) = do
    Memory
q1' <- D q a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell D q a m
q1
    Memory
q2' <- D q a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell D q a m
q2
    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
"Concat" [Memory
q1', Memory
q2']

instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (BD q a) where
  prettyStructure :: forall (m :: * -> *). MonadMemory m => BD q a m -> m Memory
prettyStructure (BD D q a m
q1 D q a m
q2) = do
    Memory
q1' <- D q a m -> m Memory
forall (m :: * -> *). MonadMemory m => D q a m -> m Memory
forall (t :: (* -> *) -> *) (m :: * -> *).
(MemoryStructure t, MonadMemory m) =>
t m -> m Memory
prettyStructure D q a m
q1
    Memory
q2' <- D q a m -> m Memory
forall (m :: * -> *). MonadMemory m => D q a m -> m Memory
forall (t :: (* -> *) -> *) (m :: * -> *).
(MemoryStructure t, MonadMemory m) =>
t m -> m Memory
prettyStructure D q a m
q2
    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
"Concat" [Memory
q1', Memory
q2']

act1 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)
act1 :: forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
DequeOp a -> BD q a m -> m (BD q a m)
act1 DequeOp a
op (BD D q a m
q1 D q a m
q2) = do
  q (PrettyCell a) m
q1' <- case D q a m
q1 of
    D q a m
E -> m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadInherit m => m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
empty
    D Size
_ q (PrettyCell a) m
q -> q (PrettyCell a) m -> m (q (PrettyCell a) m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure q (PrettyCell a) m
q
  D q a m
q1'' <- Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
act (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q1) q (PrettyCell a) m
q1' DequeOp a
op 
  BD q a m -> m (BD q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BD q a m -> m (BD q a m)) -> BD q a m -> m (BD q a m)
forall a b. (a -> b) -> a -> b
$ D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
q1'' D q a m
q2

act2 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)
act2 :: forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
DequeOp a -> BD q a m -> m (BD q a m)
act2 DequeOp a
op (BD D q a m
q1 D q a m
q2) = do
  let sz :: Size
sz = D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q2
  q (PrettyCell a) m
q2' <- case D q a m
q2 of
    D q a m
E -> m (q (PrettyCell a) m)
forall (m :: * -> *) a. MonadInherit m => m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
empty
    D Size
_ q (PrettyCell a) m
q -> q (PrettyCell a) m -> m (q (PrettyCell a) m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure q (PrettyCell a) m
q
  D q a m
q2'' <- Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
act (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q2) q (PrettyCell a) m
q2' DequeOp a
op 
  BD q a m -> m (BD q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BD q a m -> m (BD q a m)) -> BD q a m -> m (BD q a m)
forall a b. (a -> b) -> a -> b
$ D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
q1 D q a m
q2''

concatenate :: (MonadInherit m, Deque q) => D q a m -> D q a m -> m (D q a m)
concatenate :: forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
D q a m -> D q a m -> m (D q a m)
concatenate D q a m
E D q a m
E = D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure D q a m
forall {k} (q :: * -> k -> *) a (m :: k). D q a m
E
concatenate (D Size
sz1 q (PrettyCell a) m
q1) D q a m
E = D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D q a m -> m (D q a m)) -> D q a m -> m (D q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D Size
sz1 q (PrettyCell a) m
q1
concatenate D q a m
E (D Size
sz2 q (PrettyCell a) m
q2) = D q a m -> m (D q a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D q a m -> m (D q a m)) -> D q a m -> m (D q a m)
forall a b. (a -> b) -> a -> b
$ Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D Size
sz2 q (PrettyCell a) m
q2
concatenate (D Size
sz1 q (PrettyCell a) m
q1) (D Size
sz2 q (PrettyCell a) m
q2) = Size -> q (PrettyCell a) m -> D q a m
forall {k} (q :: * -> k -> *) a (m :: k).
Size -> q (PrettyCell a) m -> D q a m
D (Size
sz1 Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
sz2) (q (PrettyCell a) m -> D q a m)
-> m (q (PrettyCell a) m) -> m (D q a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> q (PrettyCell a) m -> q (PrettyCell a) m -> m (q (PrettyCell a) m)
forall (m :: * -> *) a.
MonadInherit m =>
q a m -> q a m -> m (q a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> q a m -> m (q a m)
concat q (PrettyCell a) m
q1 q (PrettyCell a) m
q2

instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (BD q a) (DequeOp a) where
  create :: forall (m :: * -> *). MonadInherit m => BD q a m
create = D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
forall {k} (q :: * -> k -> *) a (m :: k). D q a m
E D q a m
forall {k} (q :: * -> k -> *) a (m :: k). D q a m
E
  action :: forall (m :: * -> *).
MonadInherit m =>
BD q a m -> DequeOp a -> (Credit, m (BD q a m))
action (BD D q a m
q1 D q a m
q2) (Cons a
x) = (forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @q (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q1) (a -> DequeOp a
forall a. a -> DequeOp a
Cons a
x), DequeOp a -> BD q a m -> m (BD q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
DequeOp a -> BD q a m -> m (BD q a m)
act1 (a -> DequeOp a
forall a. a -> DequeOp a
Cons a
x) (D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
q1 D q a m
q2))
  action (BD D q a m
q1 D q a m
q2) (Snoc a
x) = (forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @q (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q2) (a -> DequeOp a
forall a. a -> DequeOp a
Snoc a
x), DequeOp a -> BD q a m -> m (BD q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
DequeOp a -> BD q a m -> m (BD q a m)
act2 (a -> DequeOp a
forall a. a -> DequeOp a
Snoc a
x) (D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
q1 D q a m
q2))
  action (BD D q a m
q1 D q a m
q2) DequeOp a
Uncons = (forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @q (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q1) DequeOp Any
forall a. DequeOp a
Uncons, DequeOp a -> BD q a m -> m (BD q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
DequeOp a -> BD q a m -> m (BD q a m)
act1 DequeOp a
forall a. DequeOp a
Uncons (D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
q1 D q a m
q2))
  action (BD D q a m
q1 D q a m
q2) DequeOp a
Unsnoc = (forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @q (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q2) DequeOp Any
forall a. DequeOp a
Unsnoc, DequeOp a -> BD q a m -> m (BD q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
DequeOp a -> BD q a m -> m (BD q a m)
act2 DequeOp a
forall a. DequeOp a
Unsnoc (D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
q1 D q a m
q2))
  action (BD D q a m
q1 D q a m
q2) DequeOp a
Concat = (forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @q (D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q1 Size -> Size -> Size
forall a. Num a => a -> a -> a
+ D q a m -> Size
forall {k} (q :: * -> k -> *) a (m :: k). D q a m -> Size
size D q a m
q2) DequeOp Any
forall a. DequeOp a
Concat, D q a m -> D q a m -> BD q a m
forall {k} (q :: * -> k -> *) a (m :: k).
D q a m -> D q a m -> BD q a m
BD D q a m
forall {k} (q :: * -> k -> *) a (m :: k). D q a m
E (D q a m -> BD q a m) -> m (D q a m) -> m (BD q a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D q a m -> D q a m -> m (D q a m)
forall (m :: * -> *) (q :: * -> (* -> *) -> *) a.
(MonadInherit m, Deque q) =>
D q a m -> D q a m -> m (D q a m)
concatenate D q a m
q1 D q a m
q2)