{-# LANGUAGE TypeFamilies #-}

module Test.Credit.Queue.Physicists where

import Prettyprinter (Pretty)
import Control.Monad.Credit
import Test.Credit
import Test.Credit.Queue.Base

app :: MonadCredit m => [a] -> [a] -> m [a]
app :: forall (m :: * -> *) a. MonadCredit m => [a] -> [a] -> m [a]
app [] [a]
ys = [a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
ys
app (a
x : [a]
xs) [a]
ys = 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. MonadCredit m => [a] -> [a] -> m [a]
app [a]
xs (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys)

rev :: MonadCredit m => [a] -> [a] -> m [a]
rev :: forall (m :: * -> *) a. MonadCredit 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. MonadCredit m => [a] -> [a] -> m [a]
rev [a]
xs (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc)

data PLazyCon m a where
  Empty :: PLazyCon m [a]
  AppRev :: [a] -> [a] -> PLazyCon m [a]
  Tail :: Thunk m (PLazyCon m) [a] -> PLazyCon m [a]

instance MonadCredit m => HasStep (PLazyCon m) m where
  step :: forall a. PLazyCon m a -> m a
step PLazyCon m a
Empty = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  step (AppRev [a]
xs [a]
ys) = [a] -> [a] -> m [a]
forall (m :: * -> *) a. MonadCredit m => [a] -> [a] -> m [a]
app [a]
xs ([a] -> m a) -> m [a] -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [a] -> [a] -> m [a]
forall (m :: * -> *) a. MonadCredit m => [a] -> [a] -> m [a]
rev [a]
ys []
  step (Tail Thunk m (PLazyCon m) [a]
xs) = 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
>> Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
1 ([a] -> a) -> m [a] -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Thunk m (PLazyCon m) [a] -> 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 Thunk m (PLazyCon m) [a]
xs

type PThunk m = Thunk m (PLazyCon m)

data Physicists a m = Queue [a] Int (PThunk m [a]) (PThunk m [a]) Int [a]

checkw :: MonadCredit m => Physicists a m -> m (Physicists a m)
checkw :: forall (m :: * -> *) a.
MonadCredit m =>
Physicists a m -> m (Physicists a m)
checkw (Queue [a]
working Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear) = case [a]
working of
  [] -> do
    [a]
front' <- PThunk m [a] -> 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 PThunk m [a]
front
    Physicists a m -> m (Physicists a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Physicists a m -> m (Physicists a m))
-> Physicists a m -> m (Physicists a m)
forall a b. (a -> b) -> a -> b
$ [a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
forall a (m :: * -> *).
[a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
Queue [a]
front' Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear
  [a]
_ -> Physicists a m -> m (Physicists a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Physicists a m -> m (Physicists a m))
-> Physicists a m -> m (Physicists a m)
forall a b. (a -> b) -> a -> b
$ [a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
forall a (m :: * -> *).
[a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
Queue [a]
working Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear

check :: MonadCredit m => Physicists a m -> m (Physicists a m)
check :: forall (m :: * -> *) a.
MonadCredit m =>
Physicists a m -> m (Physicists a m)
check q :: Physicists a m
q@(Queue [a]
_ Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear) =
  if Int
lenr Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lenf
    then do
      PThunk 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 PThunk m [a]
ghost Credit
1
      Physicists a m -> m (Physicists a m)
forall (m :: * -> *) a.
MonadCredit m =>
Physicists a m -> m (Physicists a m)
checkw Physicists a m
q
    else do
      [a]
working <- PThunk m [a] -> 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 PThunk m [a]
front
      PThunk m [a]
front' <- PLazyCon m [a] -> m (PThunk 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 (PLazyCon m [a] -> m (PThunk m [a]))
-> PLazyCon m [a] -> m (PThunk m [a])
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> PLazyCon m [a]
forall a (m :: * -> *). [a] -> [a] -> PLazyCon m [a]
AppRev [a]
working [a]
rear
      PThunk 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 PThunk m [a]
front' Credit
1
      Physicists a m -> m (Physicists a m)
forall (m :: * -> *) a.
MonadCredit m =>
Physicists a m -> m (Physicists a m)
checkw (Physicists a m -> m (Physicists a m))
-> Physicists a m -> m (Physicists a m)
forall a b. (a -> b) -> a -> b
$ [a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
forall a (m :: * -> *).
[a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
Queue [a]
working (Int
lenf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lenr) PThunk m [a]
front' PThunk m [a]
front' Int
0 []

instance Queue Physicists where
  empty :: forall (m :: * -> *) a. MonadInherit m => m (Physicists a m)
empty = do
    Thunk m (PLazyCon m) [a]
front <- PLazyCon m [a] -> m (Thunk m (PLazyCon 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 PLazyCon m [a]
forall (m :: * -> *) a. PLazyCon m [a]
Empty
    Physicists a m -> m (Physicists a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Physicists a m -> m (Physicists a m))
-> Physicists a m -> m (Physicists a m)
forall a b. (a -> b) -> a -> b
$ [a]
-> Int
-> Thunk m (PLazyCon m) [a]
-> Thunk m (PLazyCon m) [a]
-> Int
-> [a]
-> Physicists a m
forall a (m :: * -> *).
[a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
Queue [] Int
0 Thunk m (PLazyCon m) [a]
front Thunk m (PLazyCon m) [a]
front Int
0 []
  snoc :: forall (m :: * -> *) a.
MonadInherit m =>
Physicists a m -> a -> m (Physicists a m)
snoc (Queue [a]
working Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear) a
x = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m () -> m (Physicists a m) -> m (Physicists a m)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
    PThunk 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 PThunk m [a]
ghost Credit
1
    Physicists a m -> m (Physicists a m)
forall (m :: * -> *) a.
MonadCredit m =>
Physicists a m -> m (Physicists a m)
check ([a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
forall a (m :: * -> *).
[a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
Queue [a]
working Int
lenf PThunk m [a]
front PThunk m [a]
ghost (Int
lenr Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rear))
  uncons :: forall (m :: * -> *) a.
MonadInherit m =>
Physicists a m -> m (Maybe (a, Physicists a m))
uncons (Queue [] Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m ()
-> m (Maybe (a, Physicists a m)) -> m (Maybe (a, Physicists a m))
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (a, Physicists a m) -> m (Maybe (a, Physicists a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, Physicists a m)
forall a. Maybe a
Nothing
  uncons (Queue (a
x : [a]
working) Int
lenf PThunk m [a]
front PThunk m [a]
ghost Int
lenr [a]
rear) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m ()
-> m (Maybe (a, Physicists a m)) -> m (Maybe (a, Physicists a m))
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
    PThunk m [a]
front' <- PLazyCon m [a] -> m (PThunk 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 (PLazyCon m [a] -> m (PThunk m [a]))
-> PLazyCon m [a] -> m (PThunk m [a])
forall a b. (a -> b) -> a -> b
$ PThunk m [a] -> PLazyCon m [a]
forall (m :: * -> *) a. Thunk m (PLazyCon m) [a] -> PLazyCon m [a]
Tail PThunk m [a]
front
    PThunk 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 PThunk m [a]
front' Credit
1
    PThunk 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 PThunk m [a]
ghost Credit
1
    Physicists a m
q' <- Physicists a m -> m (Physicists a m)
forall (m :: * -> *) a.
MonadCredit m =>
Physicists a m -> m (Physicists a m)
check (Physicists a m -> m (Physicists a m))
-> Physicists a m -> m (Physicists a m)
forall a b. (a -> b) -> a -> b
$ [a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
forall a (m :: * -> *).
[a]
-> Int
-> PThunk m [a]
-> PThunk m [a]
-> Int
-> [a]
-> Physicists a m
Queue [a]
working (Int
lenf Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) PThunk m [a]
front' PThunk m [a]
ghost Int
lenr [a]
rear
    Maybe (a, Physicists a m) -> m (Maybe (a, Physicists a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (a, Physicists a m) -> m (Maybe (a, Physicists a m)))
-> Maybe (a, Physicists a m) -> m (Maybe (a, Physicists a m))
forall a b. (a -> b) -> a -> b
$ (a, Physicists a m) -> Maybe (a, Physicists a m)
forall a. a -> Maybe a
Just (a
x, Physicists a m
q')

instance BoundedQueue Physicists where
  qcost :: forall a. Size -> QueueOp a -> Credit
qcost Size
_ (Snoc a
_) = Credit
3
  qcost Size
_ QueueOp a
Uncons = Credit
4

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PLazyCon m a) where
  prettyCell :: PLazyCon m a -> m Memory
prettyCell PLazyCon m a
Empty = 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
"Empty" []
  prettyCell (AppRev [a]
xs [a]
ys) = do
    Memory
xs' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [a]
xs
    Memory
ys' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [a]
ys
    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
"AppRev" [Memory
xs', Memory
ys']
  prettyCell (Tail Thunk m (PLazyCon m) [a]
xs) = do
    Memory
xs' <- Thunk m (PLazyCon m) [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Thunk m (PLazyCon m) [a]
xs
    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
"Tail" [Memory
xs']

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Physicists a m) where
  prettyCell :: Physicists a m -> m Memory
prettyCell (Queue [a]
working Int
lenf PThunk m [a]
front PThunk m [a]
_ Int
lenr [a]
rear) = do
    Memory
working' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [a]
working
    Memory
lenf' <- Int -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Int
lenf
    Memory
front' <- PThunk m [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell PThunk m [a]
front
    Memory
lenr' <- Int -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Int
lenr
    Memory
rear' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [a]
rear
    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
working', Memory
lenf', Memory
front', Memory
lenr', Memory
rear']

instance Pretty a => MemoryStructure (Physicists (PrettyCell a)) where
  prettyStructure :: forall (m :: * -> *).
MonadMemory m =>
Physicists (PrettyCell a) m -> m Memory
prettyStructure = Physicists (PrettyCell a) m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell