{-# LANGUAGE GADTs, LambdaCase #-}

module Test.Credit.Queue.Implicit where

import Prelude hiding (head, tail)
import Control.Monad (when, unless)
import Control.Monad.Credit
import Prettyprinter (Pretty)
import Test.Credit.Queue.Base

-- Main idea:
--  - snoc and tail both cost two credits
--  - the first credit is used to tick
--  - We maintain the invariant: In each queue Deep(f, m, r), m has 2 - (|f| - |r|) credits.
--  - The m thunk represents either a snoc or a tail, and thus requires two credits to force.
--  - snoc and tail spend their second credit on either the old m to be able to force it,
--    or on the new m to maintain the invariant.

data Digit a = Zero | One a | Two a a
  deriving (Digit a -> Digit a -> Bool
(Digit a -> Digit a -> Bool)
-> (Digit a -> Digit a -> Bool) -> Eq (Digit a)
forall a. Eq a => Digit a -> Digit a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Digit a -> Digit a -> Bool
== :: Digit a -> Digit a -> Bool
$c/= :: forall a. Eq a => Digit a -> Digit a -> Bool
/= :: Digit a -> Digit a -> Bool
Eq, Eq (Digit a)
Eq (Digit a) =>
(Digit a -> Digit a -> Ordering)
-> (Digit a -> Digit a -> Bool)
-> (Digit a -> Digit a -> Bool)
-> (Digit a -> Digit a -> Bool)
-> (Digit a -> Digit a -> Bool)
-> (Digit a -> Digit a -> Digit a)
-> (Digit a -> Digit a -> Digit a)
-> Ord (Digit a)
Digit a -> Digit a -> Bool
Digit a -> Digit a -> Ordering
Digit a -> Digit a -> Digit 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 (Digit a)
forall a. Ord a => Digit a -> Digit a -> Bool
forall a. Ord a => Digit a -> Digit a -> Ordering
forall a. Ord a => Digit a -> Digit a -> Digit a
$ccompare :: forall a. Ord a => Digit a -> Digit a -> Ordering
compare :: Digit a -> Digit a -> Ordering
$c< :: forall a. Ord a => Digit a -> Digit a -> Bool
< :: Digit a -> Digit a -> Bool
$c<= :: forall a. Ord a => Digit a -> Digit a -> Bool
<= :: Digit a -> Digit a -> Bool
$c> :: forall a. Ord a => Digit a -> Digit a -> Bool
> :: Digit a -> Digit a -> Bool
$c>= :: forall a. Ord a => Digit a -> Digit a -> Bool
>= :: Digit a -> Digit a -> Bool
$cmax :: forall a. Ord a => Digit a -> Digit a -> Digit a
max :: Digit a -> Digit a -> Digit a
$cmin :: forall a. Ord a => Digit a -> Digit a -> Digit a
min :: Digit a -> Digit a -> Digit a
Ord)

data Implicit a m
  = Shallow (Digit a)
  | Deep (Digit a) (Thunk m (ILazyCon m) (Implicit (a, a) m)) (Digit a)

data ILazyCon m a where
  IPure :: a -> ILazyCon m a
  ISnoc :: Thunk m (ILazyCon m) (Implicit a m) -> a -> ILazyCon m (Implicit a m)
  ITail :: Implicit a m -> ILazyCon m (Implicit a m)

instance MonadCredit m => HasStep (ILazyCon m) m where
  step :: forall a. ILazyCon m a -> m a
step (IPure a
x) = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  step (ISnoc Thunk m (ILazyCon m) (Implicit a m)
t a
p) = do
    Implicit a m
q <- Thunk m (ILazyCon m) (Implicit a m) -> m (Implicit a m)
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 (ILazyCon m) (Implicit a m)
t
    Implicit a m -> a -> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Implicit a m -> a -> m (Implicit a m)
snoc' Implicit a m
q a
p
  step (ITail Implicit a m
q) = Implicit a m -> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Implicit a m -> m (Implicit a m)
tail Implicit a m
q

isEmpty :: Implicit a m -> Bool
isEmpty :: forall a (m :: * -> *). Implicit a m -> Bool
isEmpty (Shallow Digit a
Zero) = Bool
True
isEmpty Implicit a m
_ = Bool
False

head :: MonadCredit m => Implicit a m -> m a
head :: forall (m :: * -> *) a. MonadCredit m => Implicit a m -> m a
head Implicit a m
q = case Implicit a m
q of
  Shallow (One a
x) -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  Deep (Two a
x a
_) Thunk m (ILazyCon m) (Implicit (a, a) m)
_ Digit a
_ -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  Deep (One a
x) Thunk m (ILazyCon m) (Implicit (a, a) m)
_ Digit a
_ -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  Implicit a m
_ -> String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"head: empty queue"

size :: Digit a -> Credit
size :: forall a. Digit a -> Credit
size = \case { Digit a
Zero -> Credit
0; One a
_ -> Credit
1; Two a
_ a
_ -> Credit
2 }

deep :: MonadCredit m => Digit a -> Thunk m (ILazyCon m) (Implicit (a, a) m) -> Digit a -> m (Implicit a m)
deep :: forall (m :: * -> *) a.
MonadCredit m =>
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
deep Digit a
f Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
r = do
  Thunk m (ILazyCon m) (Implicit (a, a) m)
m Thunk m (ILazyCon m) (Implicit (a, a) m) -> Credit -> m ()
forall (m :: * -> *) (t :: * -> *) a.
MonadCredit m =>
Thunk m t a -> Credit -> m ()
forall (t :: * -> *) a. Thunk m t a -> Credit -> m ()
`hasAtLeast` (Credit
2 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- Digit a -> Credit
forall a. Digit a -> Credit
size Digit a
f Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ Digit a -> Credit
forall a. Digit a -> Credit
size Digit a
r)
  Implicit a m -> m (Implicit a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Implicit a m -> m (Implicit a m))
-> Implicit a m -> m (Implicit a m)
forall a b. (a -> b) -> a -> b
$ Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> Implicit a m
forall a (m :: * -> *).
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> Implicit a m
Deep Digit a
f Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
r

snoc' :: MonadCredit m => Implicit a m -> a -> m (Implicit a m)
snoc' :: forall (m :: * -> *) a.
MonadCredit m =>
Implicit a m -> a -> m (Implicit a m)
snoc' Implicit a m
q a
y = do
  m ()
forall (m :: * -> *). MonadCount m => m ()
tick
  case Implicit a m
q of
    Shallow Digit a
Zero -> Implicit a m -> m (Implicit a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Implicit a m -> m (Implicit a m))
-> Implicit a m -> m (Implicit a m)
forall a b. (a -> b) -> a -> b
$ Digit a -> Implicit a m
forall a (m :: * -> *). Digit a -> Implicit a m
Shallow (a -> Digit a
forall a. a -> Digit a
One a
y)
    Shallow (One a
x) -> do
      Thunk m (ILazyCon m) (Implicit (a, a) m)
middle <- ILazyCon m (Implicit (a, a) m)
-> m (Thunk m (ILazyCon m) (Implicit (a, a) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (Implicit (a, a) m)
 -> m (Thunk m (ILazyCon m) (Implicit (a, a) m)))
-> ILazyCon m (Implicit (a, a) m)
-> m (Thunk m (ILazyCon m) (Implicit (a, a) m))
forall a b. (a -> b) -> a -> b
$ Implicit (a, a) m -> ILazyCon m (Implicit (a, a) m)
forall a (m :: * -> *). a -> ILazyCon m a
IPure (Implicit (a, a) m -> ILazyCon m (Implicit (a, a) m))
-> Implicit (a, a) m -> ILazyCon m (Implicit (a, a) m)
forall a b. (a -> b) -> a -> b
$ Digit (a, a) -> Implicit (a, a) m
forall a (m :: * -> *). Digit a -> Implicit a m
Shallow Digit (a, a)
forall a. Digit a
Zero
      Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
deep (a -> a -> Digit a
forall a. a -> a -> Digit a
Two a
x a
y) Thunk m (ILazyCon m) (Implicit (a, a) m)
middle Digit a
forall a. Digit a
Zero
    Deep Digit a
front Thunk m (ILazyCon m) (Implicit (a, a) m)
middle Digit a
Zero -> do
      Thunk m (ILazyCon m) (Implicit (a, a) m)
middle Thunk m (ILazyCon m) (Implicit (a, a) m) -> 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
      Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
deep Digit a
front Thunk m (ILazyCon m) (Implicit (a, a) m)
middle (a -> Digit a
forall a. a -> Digit a
One a
y)
    Deep Digit a
front Thunk m (ILazyCon m) (Implicit (a, a) m)
middle (One a
x) -> do
      Thunk m (ILazyCon m) (Implicit (a, a) m)
middle Thunk m (ILazyCon m) (Implicit (a, a) m) -> Credit -> m ()
forall (m :: * -> *) (t :: * -> *) a.
MonadCredit m =>
Thunk m t a -> Credit -> m ()
forall (t :: * -> *) a. Thunk m t a -> Credit -> m ()
`hasAtLeast` (Credit
2 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- Digit a -> Credit
forall a. Digit a -> Credit
size Digit a
front Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ Credit
1)
      Thunk m (ILazyCon m) (Implicit (a, a) m)
t <- ILazyCon m (Implicit (a, a) m)
-> m (Thunk m (ILazyCon m) (Implicit (a, a) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (Implicit (a, a) m)
 -> m (Thunk m (ILazyCon m) (Implicit (a, a) m)))
-> ILazyCon m (Implicit (a, a) m)
-> m (Thunk m (ILazyCon m) (Implicit (a, a) m))
forall a b. (a -> b) -> a -> b
$ Thunk m (ILazyCon m) (Implicit (a, a) m)
-> (a, a) -> ILazyCon m (Implicit (a, a) m)
forall (m :: * -> *) a.
Thunk m (ILazyCon m) (Implicit a m)
-> a -> ILazyCon m (Implicit a m)
ISnoc Thunk m (ILazyCon m) (Implicit (a, a) m)
middle (a
x, a
y)
      if Digit a -> Credit
forall a. Digit a -> Credit
size Digit a
front Credit -> Credit -> Bool
forall a. Eq a => a -> a -> Bool
== Credit
1
        then Thunk m (ILazyCon m) (Implicit (a, a) m)
t      Thunk m (ILazyCon m) (Implicit (a, a) m) -> 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
        else Thunk m (ILazyCon m) (Implicit (a, a) m)
middle Thunk m (ILazyCon m) (Implicit (a, a) m) -> 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
      Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
deep Digit a
front Thunk m (ILazyCon m) (Implicit (a, a) m)
t Digit a
forall a. Digit a
Zero
    Implicit a m
_ -> String -> m (Implicit a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"snoc: malformed queue"

tail :: MonadCredit m => Implicit a m -> m (Implicit a m)
tail :: forall (m :: * -> *) a.
MonadCredit m =>
Implicit a m -> m (Implicit a m)
tail Implicit a m
q = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m () -> m (Implicit a m) -> m (Implicit a m)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> case Implicit a m
q of
  Shallow (One a
_) -> Implicit a m -> m (Implicit a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Implicit a m -> m (Implicit a m))
-> Implicit a m -> m (Implicit a m)
forall a b. (a -> b) -> a -> b
$ Digit a -> Implicit a m
forall a (m :: * -> *). Digit a -> Implicit a m
Shallow Digit a
forall a. Digit a
Zero
  Deep (Two a
_ a
y) Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
rear -> do
    Thunk m (ILazyCon m) (Implicit (a, a) m) -> 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 (ILazyCon m) (Implicit (a, a) m)
m Credit
1
    Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
deep (a -> Digit a
forall a. a -> Digit a
One a
y) Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
rear
  Deep (One a
_) Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
rear -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Digit a -> Credit
forall a. Digit a -> Credit
size Digit a
rear Credit -> Credit -> Bool
forall a. Eq a => a -> a -> Bool
== Credit
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Thunk m (ILazyCon m) (Implicit (a, a) m) -> 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 (ILazyCon m) (Implicit (a, a) m)
m Credit
1
    Implicit (a, a) m
m' <- Thunk m (ILazyCon m) (Implicit (a, a) m) -> m (Implicit (a, a) m)
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 (ILazyCon m) (Implicit (a, a) m)
m
    if Implicit (a, a) m -> Bool
forall a (m :: * -> *). Implicit a m -> Bool
isEmpty Implicit (a, a) m
m'
      then Implicit a m -> m (Implicit a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Implicit a m -> m (Implicit a m))
-> Implicit a m -> m (Implicit a m)
forall a b. (a -> b) -> a -> b
$ Digit a -> Implicit a m
forall a (m :: * -> *). Digit a -> Implicit a m
Shallow Digit a
rear
      else do
        (a
y, a
z) <- Implicit (a, a) m -> m (a, a)
forall (m :: * -> *) a. MonadCredit m => Implicit a m -> m a
head Implicit (a, a) m
m'
        Thunk m (ILazyCon m) (Implicit (a, a) m)
t <- ILazyCon m (Implicit (a, a) m)
-> m (Thunk m (ILazyCon m) (Implicit (a, a) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (Implicit (a, a) m)
 -> m (Thunk m (ILazyCon m) (Implicit (a, a) m)))
-> ILazyCon m (Implicit (a, a) m)
-> m (Thunk m (ILazyCon m) (Implicit (a, a) m))
forall a b. (a -> b) -> a -> b
$ Implicit (a, a) m -> ILazyCon m (Implicit (a, a) m)
forall a (m :: * -> *). Implicit a m -> ILazyCon m (Implicit a m)
ITail Implicit (a, a) m
m'
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Digit a -> Credit
forall a. Digit a -> Credit
size Digit a
rear Credit -> Credit -> Bool
forall a. Eq a => a -> a -> Bool
== Credit
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Thunk m (ILazyCon m) (Implicit (a, a) m) -> 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 (ILazyCon m) (Implicit (a, a) m)
t Credit
1
        Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Digit a
-> Thunk m (ILazyCon m) (Implicit (a, a) m)
-> Digit a
-> m (Implicit a m)
deep (a -> a -> Digit a
forall a. a -> a -> Digit a
Two a
y a
z) Thunk m (ILazyCon m) (Implicit (a, a) m)
t Digit a
rear
  Implicit a m
_ -> String -> m (Implicit a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"tail: empty queue"

instance Show a => Show (Digit a) where
  show :: Digit a -> String
show Digit a
Zero = String
"Zero"
  show (One a
a) = String
"(One " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Two a
a a
b) = String
"(Two " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

showThunk :: (MonadLazy m, Show a)
          => Thunk m (ILazyCon m) (Implicit a m) -> m String
showThunk :: forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Thunk m (ILazyCon m) (Implicit a m) -> m String
showThunk Thunk m (ILazyCon m) (Implicit a m)
t = Thunk m (ILazyCon m) (Implicit a m)
-> (Implicit a m -> m String)
-> (ILazyCon m (Implicit a m) -> m String)
-> m String
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 Thunk m (ILazyCon m) (Implicit a m)
t Implicit a m -> m String
forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Implicit a m -> m String
showImplicit ((ILazyCon m (Implicit a m) -> m String) -> m String)
-> (ILazyCon m (Implicit a m) -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \case
    IPure Implicit a m
a -> Implicit a m -> m String
forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Implicit a m -> m String
showImplicit Implicit a m
a
    ISnoc Thunk m (ILazyCon m) (Implicit a m)
middle a
xy -> do
      String
m <- Thunk m (ILazyCon m) (Implicit a m) -> m String
forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Thunk m (ILazyCon m) (Implicit a m) -> m String
showThunk Thunk m (ILazyCon m) (Implicit a m)
middle
      String -> m String
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
"(snoc " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
xy String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    ITail Implicit a m
q -> do
      String
m <- Implicit a m -> m String
forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Implicit a m -> m String
showImplicit Implicit a m
q
      String -> m String
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
"(tail " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

showImplicit :: (MonadLazy m, Show a)
             => Implicit a m -> m String
showImplicit :: forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Implicit a m -> m String
showImplicit (Shallow Digit a
d) = do
  String -> m String
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
"(Shallow " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Digit a -> String
forall a. Show a => a -> String
show Digit a
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
showImplicit (Deep Digit a
f Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
r) = do
  String
m' <- Thunk m (ILazyCon m) (Implicit (a, a) m) -> m String
forall (m :: * -> *) a.
(MonadLazy m, Show a) =>
Thunk m (ILazyCon m) (Implicit a m) -> m String
showThunk Thunk m (ILazyCon m) (Implicit (a, a) m)
m
  String -> m String
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
"(Deep " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Digit a -> String
forall a. Show a => a -> String
show Digit a
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
m' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Digit a -> String
forall a. Show a => a -> String
show Digit a
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance Queue Implicit where
  empty :: forall (m :: * -> *) a. MonadInherit m => m (Implicit a m)
empty = Implicit a m -> m (Implicit a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Implicit a m -> m (Implicit a m))
-> Implicit a m -> m (Implicit a m)
forall a b. (a -> b) -> a -> b
$ Digit a -> Implicit a m
forall a (m :: * -> *). Digit a -> Implicit a m
Shallow Digit a
forall a. Digit a
Zero
  snoc :: forall (m :: * -> *) a.
MonadInherit m =>
Implicit a m -> a -> m (Implicit a m)
snoc Implicit a m
q a
y = Implicit a m -> a -> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Implicit a m -> a -> m (Implicit a m)
snoc' Implicit a m
q a
y
  uncons :: forall (m :: * -> *) a.
MonadInherit m =>
Implicit a m -> m (Maybe (a, Implicit a m))
uncons Implicit a m
q =
    if Implicit a m -> Bool
forall a (m :: * -> *). Implicit a m -> Bool
isEmpty Implicit a m
q
      then Maybe (a, Implicit a m) -> m (Maybe (a, Implicit a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, Implicit a m)
forall a. Maybe a
Nothing
      else do
        a
h <- Implicit a m -> m a
forall (m :: * -> *) a. MonadCredit m => Implicit a m -> m a
head Implicit a m
q
        Implicit a m
t <- Implicit a m -> m (Implicit a m)
forall (m :: * -> *) a.
MonadCredit m =>
Implicit a m -> m (Implicit a m)
tail Implicit a m
q
        Maybe (a, Implicit a m) -> m (Maybe (a, Implicit a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (a, Implicit a m) -> m (Maybe (a, Implicit a m)))
-> Maybe (a, Implicit a m) -> m (Maybe (a, Implicit a m))
forall a b. (a -> b) -> a -> b
$ (a, Implicit a m) -> Maybe (a, Implicit a m)
forall a. a -> Maybe a
Just (a
h, Implicit a m
t)

instance BoundedQueue Implicit where
  qcost :: forall a. Size -> QueueOp a -> Credit
qcost Size
_ (Snoc a
_) = Credit
2
  qcost Size
_ QueueOp a
Uncons = Credit
2

instance MemoryCell m a => MemoryCell m (Digit a) where
  prettyCell :: Digit a -> m Memory
prettyCell Digit a
Zero = 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
"Zero" []
  prettyCell (One a
a) = do
    Memory
a' <- a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
a
    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
"One" [Memory
a']
  prettyCell (Two a
a a
b) = do
    Memory
a' <- a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
a
    Memory
b' <- a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
b
    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
"Two" [Memory
a', Memory
b']

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where
  prettyCell :: ILazyCon m a -> m Memory
prettyCell (IPure a
x) = do
    Memory
x' <- a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
x
    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
"IPure" [Memory
x']
  prettyCell (ISnoc Thunk m (ILazyCon m) (Implicit a m)
t a
_) = do
    Memory
t' <- Thunk m (ILazyCon m) (Implicit a m) -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Thunk m (ILazyCon m) (Implicit a m)
t
    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
"ISnoc" [Memory
t']
  prettyCell (ITail Implicit a m
q) = do
    Memory
q' <- Implicit a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Implicit a m
q
    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
"ITail" [Memory
q']

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Implicit a m) where
  prettyCell :: Implicit a m -> m Memory
prettyCell (Shallow Digit a
d) = do
    Memory
d' <- Digit a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Digit a
d
    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
"Shallow" [Memory
d']
  prettyCell (Deep Digit a
f Thunk m (ILazyCon m) (Implicit (a, a) m)
m Digit a
r) = do
    Memory
f' <- Digit a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Digit a
f
    Memory
m' <- Thunk m (ILazyCon m) (Implicit (a, a) m) -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Thunk m (ILazyCon m) (Implicit (a, a) m)
m
    Memory
r' <- Digit a -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Digit 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
"Deep" [Memory
f', Memory
m', Memory
r']

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