{-# LANGUAGE GADTs #-}

module Test.Credit.Queue.Bootstrapped where

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

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 BLazyCon m a where
  Rev :: [a] -> BLazyCon m [a]

instance MonadCredit m => HasStep (BLazyCon m) m where
  step :: forall a. BLazyCon m a -> m a
step (Rev [a]
xs) = [a] -> [a] -> m [a]
forall (m :: * -> *) a. MonadCredit m => [a] -> [a] -> m [a]
rev [a]
xs []

type BThunk m = Thunk m (BLazyCon m)

data NEQueue a m = NEQueue
  { forall a (m :: * -> *). NEQueue a m -> Int
lenfm :: !Int
  , forall a (m :: * -> *). NEQueue a m -> [a]
f :: [a]
  , forall a (m :: * -> *).
NEQueue a m -> Bootstrapped (BThunk m [a]) m
m :: Bootstrapped (BThunk m [a]) m
  , forall a (m :: * -> *). NEQueue a m -> BThunk m [a]
ghost :: BThunk m [a]
  , forall a (m :: * -> *). NEQueue a m -> Int
lenr :: !Int
  , forall a (m :: * -> *). NEQueue a m -> [a]
r :: [a]
  }

data Bootstrapped a m = Empty | BQueue (NEQueue a m)

checkQ :: MonadCredit m => NEQueue a m -> m (Bootstrapped a m)
checkQ :: forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (Bootstrapped a m)
checkQ q :: NEQueue a m
q@(NEQueue Int
lenfm [a]
f Bootstrapped (BThunk m [a]) m
m BThunk m [a]
_ Int
lenr [a]
r)
  | Int
lenr Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lenfm = NEQueue a m -> m (Bootstrapped a m)
forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (Bootstrapped a m)
checkF NEQueue a m
q
  | Bool
otherwise = do
    BThunk m [a]
r' <- BLazyCon m [a] -> m (BThunk 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 (BLazyCon m [a] -> m (BThunk m [a]))
-> BLazyCon m [a] -> m (BThunk m [a])
forall a b. (a -> b) -> a -> b
$ [a] -> BLazyCon m [a]
forall {k} a (m :: k). [a] -> BLazyCon m [a]
Rev [a]
r
    BThunk 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 BThunk m [a]
r' Credit
2
    Bootstrapped (BThunk m [a]) m
m' <- Bootstrapped (BThunk m [a]) m
-> BThunk m [a] -> m (Bootstrapped (BThunk m [a]) m)
forall (m :: * -> *) a.
MonadCredit m =>
Bootstrapped a m -> a -> m (Bootstrapped a m)
snoc' Bootstrapped (BThunk m [a]) m
m BThunk m [a]
r'
    NEQueue a m -> m (Bootstrapped a m)
forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (Bootstrapped a m)
checkF (Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
forall a (m :: * -> *).
Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
NEQueue (Int
lenfm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lenr) [a]
f Bootstrapped (BThunk m [a]) m
m' BThunk m [a]
r' Int
0 [])

checkF :: MonadCredit m => NEQueue a m -> m (Bootstrapped a m)
checkF :: forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (Bootstrapped a m)
checkF (NEQueue Int
lenfm [] Bootstrapped (BThunk m [a]) m
Empty BThunk m [a]
_ Int
lenr [a]
r) = Bootstrapped a m -> m (Bootstrapped a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bootstrapped a m
forall a (m :: * -> *). Bootstrapped a m
Empty
checkF (NEQueue Int
lenfm [] (BQueue NEQueue (BThunk m [a]) m
m) BThunk m [a]
ghost Int
lenr [a]
r) = do
  (BThunk m [a]
f, Bootstrapped (BThunk m [a]) m
m') <- NEQueue (BThunk m [a]) m
-> m (BThunk m [a], Bootstrapped (BThunk m [a]) m)
forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (a, Bootstrapped a m)
uncons'' NEQueue (BThunk m [a]) m
m
  [a]
f' <- BThunk 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 BThunk m [a]
f
  Bootstrapped a m -> m (Bootstrapped a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bootstrapped a m -> m (Bootstrapped a m))
-> Bootstrapped a m -> m (Bootstrapped a m)
forall a b. (a -> b) -> a -> b
$ NEQueue a m -> Bootstrapped a m
forall a (m :: * -> *). NEQueue a m -> Bootstrapped a m
BQueue (Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
forall a (m :: * -> *).
Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
NEQueue Int
lenfm [a]
f' Bootstrapped (BThunk m [a]) m
m' BThunk m [a]
ghost Int
lenr [a]
r)
checkF NEQueue a m
q = Bootstrapped a m -> m (Bootstrapped a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bootstrapped a m -> m (Bootstrapped a m))
-> Bootstrapped a m -> m (Bootstrapped a m)
forall a b. (a -> b) -> a -> b
$ NEQueue a m -> Bootstrapped a m
forall a (m :: * -> *). NEQueue a m -> Bootstrapped a m
BQueue NEQueue a m
q

snoc' :: MonadCredit m => Bootstrapped a m -> a -> m (Bootstrapped a m)  
snoc' :: forall (m :: * -> *) a.
MonadCredit m =>
Bootstrapped a m -> a -> m (Bootstrapped a m)
snoc' Bootstrapped a m
Empty a
x = do
  Thunk m (BLazyCon m) [a]
ghost <- BLazyCon m [a] -> m (Thunk m (BLazyCon 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 (BLazyCon m [a] -> m (Thunk m (BLazyCon m) [a]))
-> BLazyCon m [a] -> m (Thunk m (BLazyCon m) [a])
forall a b. (a -> b) -> a -> b
$ [a] -> BLazyCon m [a]
forall {k} a (m :: k). [a] -> BLazyCon m [a]
Rev [a]
forall a. HasCallStack => a
undefined -- never forced
  Bootstrapped a m -> m (Bootstrapped a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bootstrapped a m -> m (Bootstrapped a m))
-> Bootstrapped a m -> m (Bootstrapped a m)
forall a b. (a -> b) -> a -> b
$ NEQueue a m -> Bootstrapped a m
forall a (m :: * -> *). NEQueue a m -> Bootstrapped a m
BQueue (Int
-> [a]
-> Bootstrapped (Thunk m (BLazyCon m) [a]) m
-> Thunk m (BLazyCon m) [a]
-> Int
-> [a]
-> NEQueue a m
forall a (m :: * -> *).
Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
NEQueue Int
1 [a
x] Bootstrapped (Thunk m (BLazyCon m) [a]) m
forall a (m :: * -> *). Bootstrapped a m
Empty Thunk m (BLazyCon m) [a]
ghost Int
0 [])
snoc' (BQueue (NEQueue Int
lenfm [a]
f Bootstrapped (Thunk m (BLazyCon m) [a]) m
m Thunk m (BLazyCon m) [a]
g Int
lenr [a]
r)) a
x = do
  Thunk m (BLazyCon 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 Thunk m (BLazyCon m) [a]
g Credit
1
  NEQueue a m -> m (Bootstrapped a m)
forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (Bootstrapped a m)
checkQ (Int
-> [a]
-> Bootstrapped (Thunk m (BLazyCon m) [a]) m
-> Thunk m (BLazyCon m) [a]
-> Int
-> [a]
-> NEQueue a m
forall a (m :: * -> *).
Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
NEQueue Int
lenfm [a]
f Bootstrapped (Thunk m (BLazyCon m) [a]) m
m Thunk m (BLazyCon m) [a]
g (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]
r))

uncons'' :: MonadCredit m => NEQueue a m -> m (a, Bootstrapped a m)
uncons'' :: forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (a, Bootstrapped a m)
uncons'' (NEQueue Int
lenfm (a
x : [a]
f') Bootstrapped (BThunk m [a]) m
m BThunk m [a]
g Int
lenr [a]
r) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m () -> m (a, Bootstrapped a m) -> m (a, Bootstrapped a m)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
  BThunk 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 BThunk m [a]
g Credit
1
  Bootstrapped a m
q <- NEQueue a m -> m (Bootstrapped a m)
forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (Bootstrapped a m)
checkQ (Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
forall a (m :: * -> *).
Int
-> [a]
-> Bootstrapped (BThunk m [a]) m
-> BThunk m [a]
-> Int
-> [a]
-> NEQueue a m
NEQueue (Int
lenfm Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [a]
f' Bootstrapped (BThunk m [a]) m
m BThunk m [a]
g Int
lenr [a]
r)
  (a, Bootstrapped a m) -> m (a, Bootstrapped a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, Bootstrapped a m
q)

uncons' :: MonadCredit m => Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))
uncons' :: forall (m :: * -> *) a.
MonadCredit m =>
Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))
uncons' Bootstrapped a m
Empty = Maybe (a, Bootstrapped a m) -> m (Maybe (a, Bootstrapped a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, Bootstrapped a m)
forall a. Maybe a
Nothing
uncons' (BQueue NEQueue a m
ne) = (a, Bootstrapped a m) -> Maybe (a, Bootstrapped a m)
forall a. a -> Maybe a
Just ((a, Bootstrapped a m) -> Maybe (a, Bootstrapped a m))
-> m (a, Bootstrapped a m) -> m (Maybe (a, Bootstrapped a m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NEQueue a m -> m (a, Bootstrapped a m)
forall (m :: * -> *) a.
MonadCredit m =>
NEQueue a m -> m (a, Bootstrapped a m)
uncons'' NEQueue a m
ne

instance Queue Bootstrapped where
  empty :: forall (m :: * -> *) a. MonadInherit m => m (Bootstrapped a m)
empty = Bootstrapped a m -> m (Bootstrapped a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bootstrapped a m
forall a (m :: * -> *). Bootstrapped a m
Empty
  snoc :: forall (m :: * -> *) a.
MonadInherit m =>
Bootstrapped a m -> a -> m (Bootstrapped a m)
snoc Bootstrapped a m
q a
x = Bootstrapped a m -> a -> m (Bootstrapped a m)
forall (m :: * -> *) a.
MonadCredit m =>
Bootstrapped a m -> a -> m (Bootstrapped a m)
snoc' Bootstrapped a m
q a
x
  uncons :: forall (m :: * -> *) a.
MonadInherit m =>
Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))
uncons Bootstrapped a m
q = Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))
forall (m :: * -> *) a.
MonadCredit m =>
Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))
uncons' Bootstrapped a m
q

instance BoundedQueue Bootstrapped where
  qcost :: forall a. Size -> QueueOp a -> Credit
qcost Size
n (Snoc a
_) = Credit
3 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (Credit -> Credit -> Credit
forall a. Ord a => a -> a -> a
max Credit
1 (Size -> Credit
logstar Size
n))
  qcost Size
n QueueOp a
Uncons = Credit
6 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (Credit -> Credit -> Credit
forall a. Ord a => a -> a -> a
max Credit
1 (Size -> Credit
logstar Size
n))

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BLazyCon m a) where
  prettyCell :: BLazyCon m a -> m Memory
prettyCell (Rev [a]
xs) = do
    Memory
xs' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [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
"Rev" [Memory
xs']

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Bootstrapped a m) where
  prettyCell :: Bootstrapped a m -> m Memory
prettyCell Bootstrapped a m
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 (BQueue (NEQueue Int
lenfm [a]
f Bootstrapped (BThunk m [a]) m
m BThunk m [a]
_ Int
lenr [a]
r)) = do
    Memory
lenfm' <- Int -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Int
lenfm
    Memory
f' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [a]
f
    Memory
m' <- Bootstrapped (BThunk m [a]) m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Bootstrapped (BThunk m [a]) m
m
    Memory
lenr' <- Int -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Int
lenr
    Memory
r' <- [a] -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell [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
$ String -> [Memory] -> Memory
mkMCell String
"Queue" [Memory
lenfm', Memory
f', Memory
m', Memory
lenr', Memory
r']

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